CVC3
theory_arith_old.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith_old.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh.
6  *
7  * Created: Fri Jan 17 18:39:18 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "theory_arith_old.h"
23 #include "arith_proof_rules.h"
24 //#include "arith_expr.h"
25 #include "arith_exception.h"
26 #include "typecheck_exception.h"
27 #include "eval_exception.h"
28 #include "parser_exception.h"
29 #include "smtlib_exception.h"
30 #include "theory_core.h"
31 #include "command_line_flags.h"
32 //TODO: remove this dependency
33 #include "../theory_core/core_proof_rules.h"
34 
35 
36 using namespace std;
37 using namespace CVC3;
38 
39 
40 ///////////////////////////////////////////////////////////////////////////////
41 // TheoryArithOld::FreeConst Methods //
42 ///////////////////////////////////////////////////////////////////////////////
43 
44 namespace CVC3 {
45 
46 ostream& operator<<(ostream& os, const TheoryArithOld::FreeConst& fc) {
47  os << "FreeConst(r=" << fc.getConst() << ", "
48  << (fc.strict()? "strict" : "non-strict") << ")";
49  return os;
50 }
51 
52 ///////////////////////////////////////////////////////////////////////////////
53 // TheoryArithOld::Ineq Methods //
54 ///////////////////////////////////////////////////////////////////////////////
55 
56 ostream& operator<<(ostream& os, const TheoryArithOld::Ineq& ineq) {
57  os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
58  << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
59  << ineq.getConst() << ")";
60  return os;
61 }
62 } // End of namespace CVC3
63 
64 
65 ///////////////////////////////////////////////////////////////////////////////
66 // TheoryArithOld Private Methods //
67 ///////////////////////////////////////////////////////////////////////////////
68 
69 
70 Theorem TheoryArithOld::isIntegerThm(const Expr& e) {
71  // Quick checks
72  Type t = e.getType();
73  if (isReal(t)) return Theorem();
74  if (isInt(t)) return typePred(e);
75 
76  // Try harder
77  return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
78 }
79 
80 
81 Theorem TheoryArithOld::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
82  const Expr& e = thm.getExpr();
83  // We found it!
84  if(e == isIntE) return thm;
85 
86  Theorem res;
87  // If the theorem is an AND, look inside each child
88  if(e.isAnd()) {
89  int i, iend=e.arity();
90  for(i=0; i<iend; ++i) {
91  res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
92  if(!res.isNull()) return res;
93  }
94  }
95  return res;
96 }
97 
98 const Rational& TheoryArithOld::freeConstIneq(const Expr& ineq, bool varOnRHS) {
99  DebugAssert(isIneq(ineq), "TheoryArithOld::freeConstIneq("+ineq.toString()+")");
100  const Expr& e = varOnRHS? ineq[0] : ineq[1];
101 
102  switch(e.getKind()) {
103  case PLUS:
104  return e[0].getRational();
105  case RATIONAL_EXPR:
106  return e.getRational();
107  default: { // MULT, DIV, or Variable
108  static Rational zero(0);
109  return zero;
110  }
111  }
112 }
113 
114 
116 TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
117  bool& subsumed) {
118  TRACE("arith ineq", "TheoryArithOld::updateSubsumptionDB(", ineq,
119  ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
120  DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArithOld::updateSubsumptionDB("
121  +ineq.toString()+")");
122  // Indexing expression: same as ineq only without the free const
123  Expr index;
124  const Expr& t = varOnRHS? ineq[0] : ineq[1];
125  bool strict(isLT(ineq));
126  Rational c(0);
127  if(isPlus(t)) {
128  DebugAssert(t.arity() >= 2, "TheoryArithOld::updateSubsumptionDB("
129  +ineq.toString()+")");
130  c = t[0].getRational(); // Extract the free const in ineq
131  Expr newT;
132  if(t.arity() == 2) {
133  newT = t[1];
134  } else {
135  vector<Expr> kids;
136  Expr::iterator i=t.begin(), iend=t.end();
137  kids.push_back(rat(0));
138  for(++i; i!=iend; ++i) kids.push_back(*i);
139  DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
140  +", ineq = "+ineq.toString());
141  newT = plusExpr(kids);
142  }
143  if(varOnRHS)
144  index = leExpr(rat(0), canonSimplify(ineq[1] - newT).getRHS());
145  else
146  index = leExpr(canonSimplify(ineq[0]-newT).getRHS(), rat(0));
147  } else if(isRational(t)) {
148  c = t.getRational();
149  if(varOnRHS)
150  index = leExpr(rat(0), ineq[1]);
151  else
152  index = leExpr(ineq[0], rat(0));
153  } else if(isLT(ineq))
154  index = leExpr(ineq[0], ineq[1]);
155  else
156  index = ineq;
157  // Now update the database, check for subsumption, and extract the constant
158  CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index),
159  iend=d_freeConstDB.end();
160  if(i == iend) {
161  subsumed = false;
162  // Create a new entry
163  CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
164  obj = FreeConst(c,strict);
165  TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
166  return obj.get();
167  } else {
168  CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
169  const FreeConst& fc = obj.get();
170  if(varOnRHS) {
171  subsumed = (c < fc.getConst() ||
172  (c == fc.getConst() && (!strict || fc.strict())));
173  } else {
174  subsumed = (c > fc.getConst() ||
175  (c == fc.getConst() && (strict || !fc.strict())));
176  }
177  if(!subsumed) {
178  obj = FreeConst(c,strict);
179  TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
180  }
181  return obj.get();
182  }
183 }
184 
185 
186 bool TheoryArithOld::kidsCanonical(const Expr& e) {
187  if(isLeaf(e)) return true;
188  bool res(true);
189  for(int i=0; res && i<e.arity(); ++i) {
190  Expr simp(canon(e[i]).getRHS());
191  res = (e[i] == simp);
192  IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
193  << "\nsimplified = " << simp << endl;)
194  }
195  return res;
196 }
197 
198 
199 ///////////////////////////////////////////////////////////////////////////////
200 // //
201 // Function: TheoryArithOld::canon //
202 // Author: Clark Barrett, Vijay Ganesh. //
203 // Created: Sat Feb 8 14:46:32 2003 //
204 // Description: Compute a canonical form for expression e and return a //
205 // theorem that e is equal to its canonical form. //
206 // Note that canonical form for arith expressions is one of the following: //
207 // 1. rational constant //
208 // 2. arithmetic leaf //
209 // (i.e. variable or term from some other theory) //
210 // 3. (MULT rat leaf) //
211 // where rat is a non-zero rational constant, leaf is an arithmetic leaf //
212 // 4. (PLUS const term_0 term_1 ... term_n) //
213 // where each term_i is either a leaf or (MULT rat leaf) //
214 // and each leaf in term_i must be strictly greater than the leaf in //
215 // term_{i+1}. //
216 // //
217 ///////////////////////////////////////////////////////////////////////////////
218 Theorem TheoryArithOld::canon(const Expr& e)
219 {
220  TRACE("arith canon","canon(",e,") {");
221  DebugAssert(kidsCanonical(e), "TheoryArithOld::canon("+e.toString()+")");
222  Theorem result;
223  switch (e.getKind()) {
224  case UMINUS: {
225  Theorem thm = d_rules->uMinusToMult(e[0]);
226  Expr e2 = thm.getRHS();
227  result = transitivityRule(thm, canon(e2));
228  }
229  break;
230  case PLUS: /* {
231  Theorem plusThm, plusThm1;
232  plusThm = d_rules->canonFlattenSum(e);
233  plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS());
234  result = transitivityRule(plusThm,plusThm1);
235  }
236  */
237  result = d_rules->canonPlus(e);
238  break;
239  case MINUS: {
240  DebugAssert(e.arity() == 2,"");
241  Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
242  // this produces e0 + (-1)*e1; we have to canonize it in 2 steps
243  Expr sum(minus_eq_sum.getRHS());
244  Theorem thm(canon(sum[1]));
245  if(thm.getLHS() == thm.getRHS())
246  result = canonThm(minus_eq_sum);
247  // The sum changed; do the work
248  else {
249  vector<unsigned> changed;
250  vector<Theorem> thms;
251  changed.push_back(1);
252  thms.push_back(thm);
253  Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
254  result = transitivityRule(minus_eq_sum, sum_eq_canon);
255  }
256  break;
257  }
258 
259  case MULT:
260  result = d_rules->canonMult(e);
261  break;
262  /*
263  case MULT: {
264  Theorem thmMult, thmMult1;
265  Expr exprMult;
266  Expr e0 = e[0];
267  Expr e1 = e[1];
268  if(e0.isRational()) {
269  if(rat(0) == e0)
270  result = d_rules->canonMultZero(e1);
271  else if (rat(1) == e0)
272  result = d_rules->canonMultOne(e1);
273  else
274  switch(e1.getKind()) {
275  case RATIONAL_EXPR :
276  result = d_rules->canonMultConstConst(e0,e1);
277  break;
278  case MULT:
279  DebugAssert(e1[0].isRational(),
280  "theory_arith::canon:\n "
281  "canon:MULT:MULT child is not canonical: "
282  + e1[0].toString());
283 
284  thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]);
285  result = transitivityRule(thmMult,canon(thmMult.getRHS()));
286  break;
287  case PLUS:{
288  Theorem thmPlus, thmPlus1;
289  Expr ePlus;
290  std::vector<Theorem> thmPlusVector;
291  thmPlus = d_rules->canonMultConstSum(e0,e1);
292  ePlus = thmPlus.getRHS();
293  Expr::iterator i = ePlus.begin();
294  for(;i != ePlus.end();++i)
295  thmPlusVector.push_back(canon(*i));
296  thmPlus1 = substitutivityRule(PLUS, thmPlusVector);
297  result = transitivityRule(thmPlus, thmPlus1);
298  break;
299  }
300  default:
301  result = reflexivityRule(e);
302  break;
303  }
304  }
305  else {
306  if(e1.isRational()){
307 
308  // canonMultTermConst just reverses the order of the const and the
309  // term. Then canon is called again.
310  Theorem t1 = d_rules->canonMultTermConst(e1,e0);
311  result = transitivityRule(t1,canon(t1.getRHS()));
312  }
313  else
314 
315  // This is where the assertion for non-linear multiplication is
316  // produced.
317  result = d_rules->canonMultTerm1Term2(e0,e1);
318  }
319  break;
320  }
321 
322  */
323  case DIVIDE:{
324  /*
325  case DIVIDE:{
326  if (e[1].isRational()) {
327  if (e[1].getRational() == 0)
328  throw ArithException("Divide by 0 error in "+e.toString());
329  Theorem thm = d_rules->canonDivideVar(e[0], e[1]);
330  Expr e2 = thm.getRHS();
331  result = transitivityRule(thm, canon(e2));
332  }
333  else
334  {
335  // TODO: to be handled
336  throw ArithException("Divide by a non-const not handled in "+e.toString());
337  }
338  break;
339  }
340  */
341 
342  // Division by 0 is OK (total extension, protected by TCCs)
343  // if (e[1].isRational() && e[1].getRational() == 0)
344  // throw ArithException("Divide by 0 error in "+e.toString());
345  if (e[1].getKind() == PLUS)
346  throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
347  result = d_rules->canonDivide(e);
348  break;
349  }
350  case POW:
351  if(e[1].isRational())
352  result = d_rules->canonPowConst(e);
353  else {
354  // x ^ 1 --> x
355  if (e[0].isRational() && e[0].getRational() == 1) {
356  result = d_rules->powerOfOne(e);
357  } else
358  result = reflexivityRule(e);
359  }
360  break;
361  default:
362  result = reflexivityRule(e);
363  break;
364  }
365  TRACE("arith canon","canon => ",result," }");
366  return result;
367 }
368 
369 
370 Theorem
371 TheoryArithOld::canonSimplify(const Expr& e) {
372  TRACE("arith simplify", "canonSimplify(", e, ") {");
373  DebugAssert(kidsCanonical(e),
374  "TheoryArithOld::canonSimplify("+e.toString()+")");
375  DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
376  Expr tmp(e);
377  Theorem thm = canon(e);
378  if(thm.getRHS().hasFind())
379  thm = transitivityRule(thm, find(thm.getRHS()));
380  // We shouldn't rely on simplification in this function anymore
381  DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
382  "canonSimplify("+e.toString()+")\n"
383  +"canon(e) = "+thm.getRHS().toString()
384  +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
385 // if(tmp != thm.getRHS())
386 // thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
387 // while(tmp != thm.getRHS()) {
388 // tmp = thm.getRHS();
389 // thm = canon(thm);
390 // if(tmp != thm.getRHS())
391 // thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
392 // }
393  TRACE("arith", "canonSimplify =>", thm, " }");
394  return thm;
395 }
396 
397 /*! accepts a theorem, canonizes it, applies iffMP and substituvity to
398  * derive the canonized thm
399  */
400 Theorem
401 TheoryArithOld::canonPred(const Theorem& thm) {
402  vector<Theorem> thms;
403  DebugAssert(thm.getExpr().arity() == 2,
404  "TheoryArithOld::canonPred: bad theorem: "+thm.toString());
405  Expr e(thm.getExpr());
406  thms.push_back(canonSimplify(e[0]));
407  thms.push_back(canonSimplify(e[1]));
408  Theorem result = iffMP(thm, substitutivityRule(e.getOp(), thms));
409 
410  return result;
411 }
412 
413 /*! accepts an equivalence theorem, canonizes it, applies iffMP and
414  * substituvity to derive the canonized thm
415  */
416 Theorem
417 TheoryArithOld::canonPredEquiv(const Theorem& thm) {
418  vector<Theorem> thms;
419  DebugAssert(thm.getRHS().arity() == 2,
420  "TheoryArithOld::canonPredEquiv: bad theorem: "+thm.toString());
421  Expr e(thm.getRHS());
422  thms.push_back(canonSimplify(e[0]));
423  thms.push_back(canonSimplify(e[1]));
424  Theorem result = transitivityRule(thm, substitutivityRule(e.getOp(), thms));
425 
426  return result;
427 }
428 
429 /*! accepts an equivalence theorem whose RHS is a conjunction,
430  * canonizes it, applies iffMP and substituvity to derive the
431  * canonized thm
432  */
433 Theorem
434 TheoryArithOld::canonConjunctionEquiv(const Theorem& thm) {
435  vector<Theorem> thms;
436  return thm;
437 }
438 
439 /*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
440  * -# translate e to the form e' = 0
441  * -# if (e'.isRational()) then {if e' != 0 return false else true}
442  * -# a for loop checks if all the variables are integers.
443  * - if not isolate a suitable real variable and call processRealEq().
444  * - if all variables are integers then isolate suitable variable
445  * and call processIntEq().
446  */
447 Theorem TheoryArithOld::doSolve(const Theorem& thm)
448 {
449  const Expr& e = thm.getExpr();
450  if (e.isTrue() || e.isFalse()) return thm;
451  TRACE("arith eq","doSolve(",e,") {");
452  DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
453  Theorem eqnThm;
454  vector<Theorem> thms;
455  // Move LHS to the RHS, if necessary
456  if(e[0].isRational() && e[0].getRational() == 0)
457  eqnThm = thm;
458  else {
459  eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
460  eqnThm = canonPred(eqnThm);
461  }
462  // eqnThm is of the form 0 = e'
463  // 'right' is of the form e'
464  Expr right = eqnThm.getRHS();
465  // Check for trivial equation
466  if (right.isRational()) {
467  Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
468  TRACE("arith eq","doSolve => ",result," }");
469  return result;
470  }
471 
472  //normalize
473  eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
474  TRACE("arith eq","doSolve => ",eqnThm.getExpr()," }");
475  right = eqnThm.getRHS();
476 
477  //eqn is of the form 0 = e' and is normalized where 'right' denotes e'
478  //FIXME: change processRealEq to accept equations as well instead of theorems
479 
480  try {
481  if (isMult(right)) {
482  DebugAssert(right.arity() > 1, "Expected arity > 1");
483  if (right[0].isRational()) {
484  Rational r = right[0].getRational();
485  if (r == 0) return getCommonRules()->trueTheorem();
486  else if (r == 1) {
487  enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
488  return getCommonRules()->trueTheorem();
489  }
490  Theorem res = iffMP(eqnThm,
491  d_rules->multEqn(eqnThm.getLHS(),
492  right, rat(1/r)));
493  res = canonPred(res);
494  return doSolve(res);
495  }
496  else {
497  enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
498  return getCommonRules()->trueTheorem();
499  }
500  }
501  else if (isPow(right)) {
502  DebugAssert(right.arity() == 2, "Expected arity 2");
503  if (right[0].isRational()) {
504  return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
505  }
506  throw ArithException("Can't solve exponential eqn: "+eqnThm.toString());
507  }
508  else {
509  if(!isInteger(right)) {
510  return processRealEq(eqnThm);
511  }
512  else {
513  return processIntEq(eqnThm);
514  }
515  }
516  } catch(ArithException& e) {
517  FatalAssert(false, "We should never get here!!! : " + e.toString());
518 
519 // // Nonlinear bail out
520 // Theorem res;
521 // if (isPlus(right)) {
522 // // Solve for something
523 // // Try to simulate groebner basis by picking the highest term
524 // Expr isolated = right[1];
525 // int isolated_degree = termDegree(isolated);
526 // for (int i = 2; i < right.arity(); i ++) {
527 // int degree = termDegree(right[i]);
528 // if (degree > isolated_degree) {
529 // isolated = right[i];
530 // isolated_degree = degree;
531 // }
532 // }
533 // Rational coeff;
534 // if (isMult(isolated) && isolated[0].isRational()) {
535 // coeff = isolated[0].getRational();
536 // DebugAssert(coeff != 0, "Expected nonzero coeff");
537 // isolated = canon(isolated / rat(coeff)).getRHS();
538 // } else coeff = 1;
539 // res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff)));
540 // res = canonPred(res);
541 // res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(), isolated, EQ));
542 // res = canonPred(res);
543 // TRACE("arith nonlinear", "solved for: ", res.getExpr(), "");
544 // } else
545 // res = symmetryRule(eqnThm); // Flip to e' = 0
546 // TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
547 // IF_DEBUG(debugger.counter("FAILED to solve equalities")++;)
548 // setIncomplete("Non-linear arithmetic equalities");
549 //
550 // // Since we are forgetting about this equation, setup for updates
551 // TRACE("arith nonlinear", "adding setup to ", eqnThm.getExpr(), "");
552 // setupRec(eqnThm.getExpr());
553 // return getCommonRules()->trueTheorem();
554  }
555  FatalAssert(false, "");
556  return Theorem();
557 }
558 
559 /*! pick a monomial for the input equation. This function is used only
560  * if the equation is an integer equation. Choose the monomial with
561  * the smallest absolute value of coefficient.
562  */
563 bool TheoryArithOld::pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin)
564 {
565  DebugAssert(isPlus(right) && right.arity() > 1,
566  "TheoryArithOld::pickIntEqMonomial right is wrong :-): " +
567  right.toString());
568  DebugAssert(right[0].isRational(),
569  "TheoryArithOld::pickIntEqMonomial. right[0] must be const" +
570  right.toString());
571 // DebugAssert(isInteger(right),
572 // "TheoryArithOld::pickIntEqMonomial: right is of type int: " +
573 // right.toString());
574  //right is of the form "C + a1x1 + ... + anxn". min is initialized
575  //to a1
576  Expr::iterator istart = right.begin(), iend = right.end();
577  istart++;
578  Expr::iterator i = istart, j;
579  bool found = false;
580  nonlin = false;
581  Rational min, coeff;
582  Expr leaf;
583  for(; i != iend; ++i) {
584  if (isLeaf(*i)) {
585  leaf = *i;
586  coeff = 1;
587  }
588  else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
589  leaf = (*i)[1];
590  coeff = abs((*i)[0].getRational());
591  }
592  else {
593  nonlin = true;
594  continue;
595  }
596  for (j = istart; j != iend; ++j) {
597  if (j != i && isLeafIn(leaf, *j)) break;
598  }
599  if (j == iend) {
600  if (!found || min > coeff) {
601  min = coeff;
602  isolated = *i;
603  found = true;
604  }
605  }
606  }
607  return found;
608 }
609 
610 /*! input is 0=e' Theorem and some of the vars in e' are of
611  * type REAL. isolate one of them and send back to framework. output
612  * is "var = e''" Theorem.
613  */
614 Theorem
615 TheoryArithOld::processRealEq(const Theorem& eqn)
616 {
617  DebugAssert(eqn.getLHS().isRational() &&
618  eqn.getLHS().getRational() == 0,
619  "processRealEq invariant violated");
620  Expr right = eqn.getRHS();
621  // Find variable to isolate and store it in left. Pick the largest
622  // (according to the total ordering) variable. FIXME: change from
623  // total ordering to the ordering we devised for inequalities.
624 
625  // TODO: I have to pick a variable that appears as a variable in the
626  // term but does not appear as a variable anywhere else. The variable
627  // must appear as a single leaf and not in a MULT expression with some
628  // other variables and nor in a POW expression.
629 
630  bool found = false;
631  Expr left;
632 
633  if (isPlus(right)) {
634  DebugAssert(right[0].isRational(), "Expected first term to be rational");
635  for(int i = 1, iend = right.arity(); i < iend; ++i) {
636  Expr c = right[i];
637  DebugAssert(!isRational(c), "Expected non-rational");
638  if(!isInteger(c)) {
639  if (isLeaf(c) ||
640  ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
641  Expr leaf = isLeaf(c) ? c : c[1];
642  int j;
643  for (j = 1; j < iend; ++j) {
644  if (j!= i
645  && isLeafIn(leaf, right[j])
646  ) {
647  break;
648  }
649  }
650  if (j == iend) {
651  left = c;
652  found = true;
653  break;
654  }
655  }
656  }
657  }
658  }
659  else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
660  isLeaf(right)) {
661  left = right;
662  found = true;
663  }
664 
665  if (!found) {
666  // The only way we can not get an isolated in the reals is if all of them
667  // are non-linear. In this case we might have some integers to solve for
668  // so we try that. The integer solver shouldn't be able to solve for the
669  // reals, as they are not solvable and we should be safe. One of such
670  // examples is if some constant ITE got skolemized and we have an equation
671  // like SKOLEM = x^2 (bug79), in which case we should solve for the SKOLEM
672  // where skolem is an INT variable.
673  if (isNonlinearEq(eqn.getExpr()))
674  return processIntEq(eqn);
675  else throw
676  ArithException("Can't find a leaf for solve in "+eqn.toString());
677  }
678 
679  Rational r = -1;
680  if (isMult(left)) {
681  DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
682  DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
683  r = -1/left[0].getRational();
684  left = left[1];
685  }
686 
687  DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
688  "TheoryArithOld::ProcessRealEq: left is integer:\n left = "
689  +left.toString());
690  // Normalize equation so that coefficient of the monomial
691  // corresponding to "left" in eqn[1] is -1
692  Theorem result(iffMP(eqn,
693  d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
694  result = canonPred(result);
695 
696  // Isolate left
697  result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
698  result.getRHS(), left, EQ));
699  result = canonPred(result);
700  TRACE("arith","processRealEq => ",result," }");
701  return result;
702 }
703 
704 
705 void TheoryArithOld::getFactors(const Expr& e, set<Expr>& factors)
706 {
707  switch (e.getKind()) {
708  case RATIONAL_EXPR: break;
709  case MULT: {
710  Expr::iterator i = e.begin(), iend = e.end();
711  for (; i != iend; ++i) {
712  getFactors(*i, factors);
713  }
714  break;
715  }
716  case POW: {
717  DebugAssert(e.arity() == 2, "invariant violated");
718  if (!isIntegerConst(e[0]) || e[0].getRational() <= 0) {
719  throw ArithException("not positive integer exponent in "+e.toString());
720  }
721  if (isLeaf(e[1])) factors.insert(e[1]);
722  break;
723  }
724  default: {
725  DebugAssert(isLeaf(e), "expected leaf");
726  DebugAssert(factors.find(e) == factors.end(), "expected new entry");
727  factors.insert(e);
728  break;
729  }
730  }
731 }
732 
733 
734 /*!
735  * \param eqn is a single equation 0 = e
736  * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
737  */
738 Theorem
739 TheoryArithOld::processSimpleIntEq(const Theorem& eqn)
740 {
741  TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
742  DebugAssert(eqn.isRewrite(),
743  "TheoryArithOld::processSimpleIntEq: eqn must be equality" +
744  eqn.getExpr().toString());
745 
746  Expr right = eqn.getRHS();
747 
748  DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
749  "TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" +
750  eqn.getExpr().toString());
751 
752  DebugAssert(!isMult(right) && !isPow(right), "should have been handled above");
753  if (isPlus(right)) {
754  if (2 == right.arity() &&
755  (isLeaf(right[1]) ||
756  (isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
757  //we take care of special cases like 0 = c + a.x, 0 = c + x,
758  Expr c,x;
759  separateMonomial(right[1], c, x);
760  Theorem isIntx(isIntegerThm(x));
761  DebugAssert(!isIntx.isNull(), "right = "+right.toString()
762  +"\n x = "+x.toString());
763  Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
764  TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
765  return res;
766  }
767  // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
768  Expr isolated;
769  bool nonlin;
770  if (pickIntEqMonomial(right, isolated, nonlin)) {
771  TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
772 
773  // First, we compute the 'sign factor' with which to multiply the
774  // eqn. if the coeff of isolated is positive (i.e. 'isolated' is
775  // of the form x or a.x where a>0 ) then r must be -1 and if coeff
776  // of 'isolated' is negative, r=1.
777  Rational r = isMult(isolated) ?
778  ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
779  Theorem result;
780  if (-1 == r) {
781  // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
782  // positive. modify eqn (0=e') to the equation (0=canon(-1*e'))
783  result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
784  result = canonPred(result);
785  Expr e = result.getRHS();
786 
787  // Isolate the 'isolated'
788  result = iffMP(result,
789  d_rules->plusPredicate(result.getLHS(),result.getRHS(),
790  isolated, EQ));
791  } else {
792  //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
793  const Rational& minusa = isolated[0].getRational();
794  Rational a = -1*minusa;
795  isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
796 
797  // Isolate the 'isolated'
798  result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
799  right,isolated,EQ));
800  }
801  // Canonize the result
802  result = canonPred(result);
803 
804  //if isolated is 'x' or 1*x, then return result else continue processing.
805  if(!isMult(isolated) || isolated[0].getRational() == 1) {
806  TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
807  return result;
808  } else if (!nonlin) {
809  DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
810  "TheoryArithOld::processSimpleIntEq: isolated must be mult "
811  "with coeff >= 2.\n isolated = " + isolated.toString());
812 
813  // Compute IS_INTEGER() for lhs and rhs
814  Expr lhs = result.getLHS();
815  Expr rhs = result.getRHS();
816  Expr a, x;
817  separateMonomial(lhs, a, x);
818  Theorem isIntLHS = isIntegerThm(x);
819  vector<Theorem> isIntRHS;
820  if(!isPlus(rhs)) { // rhs is a MULT
821  Expr c, v;
822  separateMonomial(rhs, c, v);
823  isIntRHS.push_back(isIntegerThm(v));
824  DebugAssert(!isIntRHS.back().isNull(), "");
825  } else { // rhs is a PLUS
826  DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
827  DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
828  Expr::iterator i=rhs.begin(), iend=rhs.end();
829  ++i; // Skip the free constant
830  for(; i!=iend; ++i) {
831  Expr c, v;
832  separateMonomial(*i, c, v);
833  isIntRHS.push_back(isIntegerThm(v));
834  DebugAssert(!isIntRHS.back().isNull(), "");
835  }
836  }
837  // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
838  result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
839  // Skolemize the quantifier
840  result = getCommonRules()->skolemize(result);
841  // Canonize t2 and t3 generated by this rule
842  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
843  "processSimpleIntEq: result = "+result.getExpr().toString());
844  Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
845  Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
846  Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
847  if(newRes.getExpr() != result.getExpr()) result = newRes;
848 
849  TRACE("arith eq", "processSimpleIntEq => ", result, " }");
850  return result;
851  }
852  }
853  throw
854  ArithException("Can't find a leaf for solve in "+eqn.toString());
855  } else {
856  // eqn is 0 = x. Flip it and return
857  Theorem result = symmetryRule(eqn);
858  TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
859  return result;
860  }
861 }
862 
863 /*! input is 0=e' Theorem and all of the vars in e' are of
864  * type INT. isolate one of them and send back to framework. output
865  * is "var = e''" Theorem and some associated equations in
866  * solved form.
867  */
868 Theorem
869 TheoryArithOld::processIntEq(const Theorem& eqn)
870 {
871  TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
872  // Equations in the solved form.
873  std::vector<Theorem> solvedAndNewEqs;
874  Theorem newEq(eqn), result;
875  bool done(false);
876  do {
877  result = processSimpleIntEq(newEq);
878  // 'result' is of the from (x1=t1) AND 0=t'
879  if(result.isRewrite()) {
880  solvedAndNewEqs.push_back(result);
881  done = true;
882  }
883  else if (result.getExpr().isBoolConst()) {
884  done = true;
885  }
886  else {
887  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
888  "TheoryArithOld::processIntEq("+eqn.getExpr().toString()
889  +")\n result = "+result.getExpr().toString());
890  solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
891  newEq = getCommonRules()->andElim(result, 1);
892  }
893  } while(!done);
894  Theorem res;
895  if (result.getExpr().isFalse()) res = result;
896  else if (solvedAndNewEqs.size() > 0)
897  res = solvedForm(solvedAndNewEqs);
898  else res = result;
899  TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
900  return res;
901 }
902 
903 /*!
904  * Takes a vector of equations and for every equation x_i=t_i
905  * substitutes t_j for x_j in t_i for all j>i. This turns the system
906  * of equations into a solved form.
907  *
908  * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
909  * i<j, but not for i>=j.
910  */
911 Theorem
912 TheoryArithOld::solvedForm(const vector<Theorem>& solvedEqs)
913 {
914  DebugAssert(solvedEqs.size() > 0, "TheoryArithOld::solvedForm()");
915 
916  // Trace code
917  TRACE_MSG("arith eq", "TheoryArithOld::solvedForm:solvedEqs(\n [");
918  IF_DEBUG(if(debugger.trace("arith eq")) {
919  for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
920  jend=solvedEqs.end(); j!=jend;++j)
921  TRACE("arith eq", "", j->getExpr(), ",\n ");
922  })
923  TRACE_MSG("arith eq", " ]) {");
924  // End of Trace code
925 
926  vector<Theorem>::const_reverse_iterator
927  i = solvedEqs.rbegin(),
928  iend = solvedEqs.rend();
929  // Substitution map: a variable 'x' is mapped to a Theorem x=t.
930  // This map accumulates the resulting solved form.
931  ExprMap<Theorem> subst;
932  for(; i!=iend; ++i) {
933  if(i->isRewrite()) {
934  Theorem thm = substAndCanonize(*i, subst);
935  TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
936  thm.getExpr(), "");
937  subst[i->getLHS()] = thm;
938  }
939  else {
940  // This is the FALSE case: just return the contradiction
941  DebugAssert(i->getExpr().isFalse(),
942  "TheoryArithOld::solvedForm: an element of solvedEqs must "
943  "be either EQ or FALSE: "+i->toString());
944  return *i;
945  }
946  }
947  // Now we've collected the solved form in 'subst'. Wrap it up into
948  // a conjunction and return.
949  vector<Theorem> thms;
950  for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
951  i!=iend; ++i)
952  thms.push_back(i->second);
953 
954  if (thms.size() > 1) return getCommonRules()->andIntro(thms);
955  else return thms.back();
956 }
957 
958 
959 /*!
960  * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
961  * element of subst is a fully canonized equation of the form x=e,
962  * indexed by the LHS variable.
963  */
964 
965 Theorem
966 TheoryArithOld::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
967 {
968  TRACE("arith eq", "substAndCanonize(", t, ") {");
969  // Quick and dirty check: return immediately if subst is empty
970  if(subst.empty()) {
971  Theorem res(reflexivityRule(t));
972  TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
973  return res;
974  }
975  // Check if we can substitute 't' directly
976  ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
977  if(i!=iend) {
978  TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
979  return i->second;
980  }
981  // The base case: t is an i-leaf
982  if(isLeaf(t)) {
983  Theorem res(reflexivityRule(t));
984  TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
985  return res;
986  }
987  // 't' is an arithmetic term; recurse into the children
988  vector<Theorem> thms;
989  vector<unsigned> changed;
990  for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
991  Theorem thm = substAndCanonize(t[j], subst);
992  if(thm.getRHS() != t[j]) {
993  thm = canonThm(thm);
994  thms.push_back(thm);
995  changed.push_back(j);
996  }
997  }
998  // Do the actual substitution and canonize the result
999  Theorem res;
1000  if(thms.size() > 0) {
1001  res = substitutivityRule(t, changed, thms);
1002  res = canonThm(res);
1003  }
1004  else
1005  res = reflexivityRule(t);
1006  TRACE("arith eq", "substAndCanonize => ", res, " }");
1007  return res;
1008 }
1009 
1010 
1011 /*!
1012  * ASSUMPTION: 't' is a fully canonized equation of the form x = t,
1013  * and so is every element of subst, indexed by the LHS variable.
1014  */
1015 
1016 Theorem
1017 TheoryArithOld::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
1018 {
1019  // Quick and dirty check: return immediately if subst is empty
1020  if(subst.empty()) return eq;
1021 
1022  DebugAssert(eq.isRewrite(), "TheoryArithOld::substAndCanonize: t = "
1023  +eq.getExpr().toString());
1024  const Expr& t = eq.getRHS();
1025  // Do the actual substitution in the term t
1026  Theorem thm = substAndCanonize(t, subst);
1027  // Substitution had no result: return the original equation
1028  if(thm.getRHS() == t) return eq;
1029  // Otherwise substitute the result into the equation
1030  vector<Theorem> thms;
1031  vector<unsigned> changed;
1032  thms.push_back(thm);
1033  changed.push_back(1);
1034  return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
1035 }
1036 
1037 void TheoryArithOld::processBuffer()
1038 {
1039  // Process the inequalities in the buffer
1040  bool varOnRHS;
1041 
1042  // If we are in difference logic only, just return
1043  if (diffLogicOnly) return;
1044 
1045  while (!inconsistent() && (d_bufferIdx_0 < d_buffer_0.size() || d_bufferIdx_1 < d_buffer_1.size() || d_bufferIdx_2 < d_buffer_2.size() || d_bufferIdx_3 < d_buffer_3.size())) {
1046 
1047  // Get the unprojected inequality
1048  Theorem ineqThm;
1049  if (d_bufferIdx_0 < d_buffer_0.size()) {
1050  ineqThm = d_buffer_0[d_bufferIdx_0];
1051  d_bufferIdx_0 = d_bufferIdx_0 + 1;
1052  } else if (d_bufferIdx_1 < d_buffer_1.size()) {
1053  ineqThm = d_buffer_1[d_bufferIdx_1];
1054  d_bufferIdx_1 = d_bufferIdx_1 + 1;
1055  } else if (d_bufferIdx_2 < d_buffer_2.size()) {
1056  ineqThm = d_buffer_2[d_bufferIdx_2];
1057  d_bufferIdx_2 = d_bufferIdx_2 + 1;
1058  } else {
1059  ineqThm = d_buffer_3[d_bufferIdx_3];
1060  d_bufferIdx_3 = d_bufferIdx_3 + 1;
1061  }
1062 
1063 // // Skip this inequality if it is stale
1064 // if(isStale(ineqThm.getExpr())) {
1065 // TRACE("arith buffer", "processBuffer(", ineqThm.getExpr(), ")... skipping stale");
1066 // continue;
1067 // }
1068  // Dejan: project the finds, not the originals (if not projected already)
1069  const Expr& inequality = ineqThm.getExpr();
1070  Theorem inequalityFindThm = inequalityToFind(ineqThm, true);
1071  Expr inequalityFind = inequalityFindThm.getExpr();
1072 // if (inequality != inequalityFind)
1073 // enqueueFact(inequalityFindThm);
1074 
1075  TRACE("arith buffer", "processing: ", inequality, "");
1076  TRACE("arith buffer", "with find : ", inequalityFind, "");
1077 
1078  if (!isIneq(inequalityFind)) {
1079  TRACE("arith buffer", "find not an inequality... ", "", "skipping");
1080  continue;
1081  }
1082 
1083  if (alreadyProjected.find(inequalityFind) != alreadyProjected.end()) {
1084  TRACE("arith buffer", "already projected ... ", "", "skipping");
1085  continue;
1086  }
1087 
1088 
1089  // We put the dummy for now, isolate variable will set it properly (or the find's one)
1090  // This one is just if the find is different. If the find is different
1091  // We will not check it again in update, so we're fine
1092  Expr dummy;
1093  alreadyProjected[inequality] = dummy;
1094  if (inequality != inequalityFind) {
1095 
1096  alreadyProjected[inequalityFind] = dummy;
1097 
1098  Expr rhs = inequalityFind[1];
1099 
1100  // Collect the statistics about variables
1101  if(isPlus(rhs)) {
1102  for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) {
1103  Expr monomial = *i;
1104  updateStats(monomial);
1105  }
1106  } else // It's a monomial
1107  updateStats(rhs);
1108  }
1109 
1110  // See if this one is subsumed by a stronger inequality
1111  // c1 <= t1, t2 <= c2
1112  Rational c1, c2;
1113  Expr t1, t2;
1114  // Every term in the buffer has to have a lower bound set!!!
1115  // Except for the ones that changed the find
1116  extractTermsFromInequality(inequalityFind, c1, t1, c2, t2);
1117  if (termLowerBound.find(t1) != termLowerBound.end() && c1 != termLowerBound[t1]) {
1118  TRACE("arith ineq", "skipping because stronger bounds asserted ", inequalityFind.toString(), ":" + t1.toString());
1119  DebugAssert(termLowerBoundThm.find(t1) != termLowerBoundThm.end(), "No lower bound on asserted atom!!! " + t1.toString());
1120  Theorem strongerBound = termLowerBoundThm[t1];
1121  //enqueueFact(d_rules->implyWeakerInequality(strongerBound.getExpr(), inequalityFindThm.getExpr()));
1122  continue;
1123  }
1124 
1125  Theorem thm1 = isolateVariable(inequalityFindThm, varOnRHS);
1126  const Expr& ineq = thm1.getExpr();
1127  if (ineq.isFalse())
1128  setInconsistent(thm1);
1129  else
1130  if(!ineq.isTrue()) {
1131 
1132  // Check that the variable is indeed isolated correctly
1133  DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]), "TheoryArithOld::processBuffer(): bad result from isolateVariable:\nineq = "+ineq.toString());
1134  // Update the constained maps
1135  updateConstrained(inequalityFindThm.getExpr());
1136  // and project the inequality
1137  projectInequalities(thm1, varOnRHS);
1138  }
1139  }
1140 }
1141 
1142 
1143 void TheoryArithOld::updateStats(const Rational& c, const Expr& v)
1144 {
1145  TRACE("arith stats", "updateStats("+c.toString()+", ", v, ")");
1146 
1147  // we can get numbers as checking for variables is not possible (nonlinear stuff)
1148  if (v.isRational()) return;
1149 
1150  if (v.getType() != d_realType) {
1151  // Dejan: update the max coefficient of the variable
1152  if (c < 0) {
1153  // Goes to the left side
1154  ExprMap<Rational>::iterator maxFind = maxCoefficientLeft.find(v);
1155  if (maxFind == maxCoefficientLeft.end()) {
1156  maxCoefficientLeft[v] = - c;
1157  TRACE("arith stats", "max left", "", "");
1158  }
1159  else
1160  if ((*maxFind).second < -c) {
1161  TRACE("arith stats", "max left", "", "");
1162  maxCoefficientLeft[v] = -c;
1163  }
1164  } else {
1165  // Stays on the right side
1166  ExprMap<Rational>::iterator maxFind = maxCoefficientRight.find(v);
1167  if (maxFind == maxCoefficientRight.end()) {
1168  maxCoefficientRight[v] = c;
1169  TRACE("arith stats", "max right", "", "");
1170  }
1171  else
1172  if((*maxFind).second < c) {
1173  TRACE("arith stats", "max right", "", "");
1174  maxCoefficientRight[v] = c;
1175  }
1176  }
1177  }
1178 
1179  if(c > 0) {
1180  if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
1181  else d_countRight[v] = 1;
1182  }
1183  else
1184  if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
1185  else d_countLeft[v] = 1;
1186 }
1187 
1188 
1189 void TheoryArithOld::updateStats(const Expr& monomial)
1190 {
1191  Expr c, m;
1192  separateMonomial(monomial, c, m);
1193  updateStats(c.getRational(), m);
1194 }
1195 
1196 int TheoryArithOld::extractTermsFromInequality(const Expr& inequality,
1197  Rational& c1, Expr& t1,
1198  Rational& c2, Expr& t2) {
1199 
1200  TRACE("arith extract", "extract(", inequality.toString(), ")");
1201 
1202  DebugAssert(isIneq(inequality), "extractTermsFromInequality: expexting an inequality got: " + inequality.getString() + ")");
1203 
1204  Expr rhs = inequality[1];
1205 
1206  c1 = 0;
1207 
1208  // Extract the non-constant term (both sides)
1209  vector<Expr> positive_children, negative_children;
1210  if (isPlus(rhs)) {
1211  int start_i = 0;
1212  if (rhs[0].isRational()) {
1213  start_i = 1;
1214  c1 = -rhs[0].getRational();
1215  }
1216  int end_i = rhs.arity();
1217  for(int i = start_i; i < end_i; i ++) {
1218  const Expr& term = rhs[i];
1219  positive_children.push_back(term);
1220  negative_children.push_back(canon(multExpr(rat(-1),term)).getRHS());
1221  }
1222  } else {
1223  positive_children.push_back(rhs);
1224  negative_children.push_back(canon(multExpr(rat(-1), rhs)).getRHS());
1225  }
1226 
1227  int num_vars = positive_children.size();
1228 
1229  // c1 <= t1
1230  t1 = (num_vars > 1 ? canon(plusExpr(positive_children)).getRHS() : positive_children[0]);
1231 
1232  // c2 is the upper bound on t2 : t2 <= c2
1233  c2 = -c1;
1234  t2 = (num_vars > 1 ? canon(plusExpr(negative_children)).getRHS() : negative_children[0]);
1235 
1236  TRACE("arith extract", "extract: ", c1.toString() + " <= ", t1.toString());
1237 
1238  return num_vars;
1239 }
1240 
1241 bool TheoryArithOld::addToBuffer(const Theorem& thm, bool priority) {
1242 
1243  TRACE("arith buffer", "addToBuffer(", thm.getExpr().toString(), ")");
1244 
1245  Expr ineq = thm.getExpr();
1246  const Expr& rhs = thm.getExpr()[1];
1247 
1248  bool nonLinear = false;
1249  Rational nonLinearConstant = 0;
1250  Expr compactNonLinear;
1251  Theorem compactNonLinearThm;
1252 
1253  // Collect the statistics about variables and check for non-linearity
1254  if(isPlus(rhs)) {
1255  for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) {
1256  Expr monomial = *i;
1257  updateStats(monomial);
1258  // check for non-linear
1259  if (isMult(monomial)) {
1260  if ((monomial[0].isRational() && monomial.arity() >= 3) ||
1261  (!monomial[0].isRational() && monomial.arity() >= 2) ||
1262  (monomial.arity() == 2 && isPow(monomial[1])))
1263  nonLinear = true;
1264  }
1265  }
1266  if (nonLinear) {
1267  compactNonLinearThm = d_rules->compactNonLinearTerm(rhs);
1268  compactNonLinear = compactNonLinearThm.getRHS();
1269  }
1270  }
1271  else // It's a monomial
1272  {
1273  updateStats(rhs);
1274  if (isMult(rhs))
1275  if ((rhs[0].isRational() && rhs.arity() >= 3)
1276  || (!rhs[0].isRational() && rhs.arity() >= 2)
1277  || (rhs.arity() == 2 && isPow(rhs[1]))) {
1278  nonLinear = true;
1279  compactNonLinear = rhs;
1280  compactNonLinearThm = reflexivityRule(compactNonLinear);
1281  }
1282  }
1283 
1284  if (bufferedInequalities.find(ineq) != bufferedInequalities.end()) {
1285  TRACE("arith buffer", "addToBuffer()", "", "... already in db");
1286  if (formulaAtoms.find(ineq) != formulaAtoms.end()) {
1287  TRACE("arith buffer", "it's a formula atom, enqueuing.", "", "");
1288  enqueueFact(thm);
1289  }
1290  return false;
1291  }
1292 
1293  if (nonLinear && (isMult(rhs) || compactNonLinear != rhs)) {
1294  TRACE("arith nonlinear", "compact version of ", rhs, " is " + compactNonLinear.toString());
1295  // Replace the rhs with the compacted nonlinear term
1296  Theorem thm1 = (compactNonLinear != rhs ?
1297  iffMP(thm, substitutivityRule(ineq, 1, compactNonLinearThm)) : thm);
1298  // Now, try to deduce the signednes of multipliers
1299  Rational c = (isMult(rhs) ? 0 : compactNonLinear[0].getRational());
1300  // We can deduct the signs if the constant is not bigger than 0
1301  if (c <= 0) {
1302  thm1 = d_rules->nonLinearIneqSignSplit(thm1);
1303  TRACE("arith nonlinear", "spliting on signs : ", thm1.getExpr(), "");
1304  enqueueFact(thm1);
1305  }
1306  }
1307 
1308  // Get c1, c2, t1, t2 such that c1 <= t1 and t2 <= c2
1309  Expr t1, t2;
1310  Rational c1, c2;
1311  int num_vars = extractTermsFromInequality(ineq, c1, t1, c2, t2);
1312 
1313  // If 2 variable, do add to difference logic (allways, just in case)
1314  bool factIsDiffLogic = false;
1315  if (num_vars <= 2) {
1316 
1317  TRACE("arith diff", t2, " < ", c2);
1318  // c1 <= t1, check if difference logic
1319  // t1 of the form 0 + ax + by
1320  Expr ax = (num_vars == 2 ? t2[1] : t2);
1321  Expr a_expr, x;
1322  separateMonomial(ax, a_expr, x);
1323  Rational a = a_expr.getRational();
1324  Expr by = (num_vars == 2 ? t2[2] : (a < 0 ? zero : rat(-1)*zero));
1325  Expr b_expr, y;
1326  separateMonomial(by, b_expr, y);
1327  Rational b = b_expr.getRational();
1328 
1329  // Check for non-linear
1330  if (!isLeaf(x) || !isLeaf(y))
1331  setIncomplete("Non-linear arithmetic inequalities");
1332 
1333  if (a == 1 && b == -1) {
1334  diffLogicGraph.addEdge(x, y, c2, thm);
1335  factIsDiffLogic = true;
1336  }
1337  else if (a == -1 && b == 1) {
1338  diffLogicGraph.addEdge(y, x, c2, thm);
1339  factIsDiffLogic = true;
1340  }
1341  // Not difference logic, put it in the 3 or more vars buffer
1342  else {
1343  diffLogicOnly = false;
1344  TRACE("arith diff", "not diff logic", thm.getExpr().toString(), "");
1345  }
1346 
1347  if (diffLogicGraph.isUnsat()) {
1348  TRACE("diff unsat", "UNSAT", " : ", diffLogicGraph.getUnsatTheorem());
1349  setInconsistent(diffLogicGraph.getUnsatTheorem());
1350  return false;
1351  }
1352  } else {
1353  diffLogicOnly = false;
1354  TRACE("arith diff", "not diff logic", thm.getExpr().toString(), "");
1355  }
1356 
1357  // For now we treat all the bound as LE, weaker
1358  CDMap<Expr, Rational>::iterator find_lower = termLowerBound.find(t1);
1359  if (find_lower != termLowerBound.end()) {
1360  // found bound c <= t1
1361  Rational found_c = (*find_lower).second;
1362  // If found c is bigger than the new one, we are done
1363  if (c1 <= found_c && !(found_c == c1 && ineq.getKind() == LT)) {
1364  TRACE("arith buffer", "addToBuffer()", "", "... lower_bound subsumed");
1365  // Removed assert. Can happen that an atom is not asserted yet, and get's implied as
1366  // a formula atom and then asserted here. it's fine
1367  //DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + "");
1368  return false;
1369  } else {
1370  Theorem oldLowerBound = termLowerBoundThm[t1];
1371  Expr oldIneq = oldLowerBound.getExpr();
1372  if (formulaAtoms.find(oldIneq) != formulaAtoms.end())
1373  enqueueFact(getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, oldIneq)));
1374  termLowerBound[t1] = c1;
1375  termLowerBoundThm[t1] = thm;
1376  }
1377  } else {
1378  termLowerBound[t1] = c1;
1379  termLowerBoundThm[t1] = thm;
1380  }
1381 
1382  CDMap<Expr, Rational>::iterator find_upper = termUpperBound.find(t2);
1383  if (find_upper != termUpperBound.end()) {
1384  // found bound t2 <= c
1385  Rational found_c = (*find_upper).second;
1386  // If found c is smaller than the new one, we are done
1387  if (found_c <= c2 && !(found_c == c2 && ineq.getKind() == LT)) {
1388  TRACE("arith buffer", "addToBuffer()", "", "... upper_bound subsumed");
1389  //DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + "");
1390  return false;
1391  } else {
1392  termUpperBound[t2] = c2;
1393  termUpperBoundThm[t2] = thm;
1394  }
1395  } else {
1396  termUpperBound[t2] = c2;
1397  termUpperBoundThm[t2] = thm;
1398  }
1399 
1400  // See if the bounds on the term can infer conflict or equality
1401  if (termUpperBound.find(t1) != termUpperBound.end() &&
1402  termLowerBound.find(t1) != termLowerBound.end() &&
1403  termUpperBound[t1] <= termLowerBound[t1]) {
1404  Theorem thm1 = termUpperBoundThm[t1];
1405  Theorem thm2 = termLowerBoundThm[t1];
1406  TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString());
1407  enqueueFact(d_rules->addInequalities(thm1, thm2));
1408  } else
1409  if (termUpperBound.find(t2) != termUpperBound.end() &&
1410  termLowerBound.find(t2) != termLowerBound.end() &&
1411  termUpperBound[t2] <= termLowerBound[t2]) {
1412  Theorem thm1 = termUpperBoundThm[t2];
1413  Theorem thm2 = termLowerBoundThm[t2];
1414  TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString());
1415  enqueueFact(d_rules->addInequalities(thm1, thm2));
1416  }
1417 
1418  if (true) {
1419  // See if we can propagate anything to the formula atoms
1420  // c1 <= t1 ===> c <= t1 for c < c1
1421  AtomsMap::iterator find = formulaAtomLowerBound.find(t1);
1422  AtomsMap::iterator find_end = formulaAtomLowerBound.end();
1423  if (find != find_end) {
1424  set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
1425  set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
1426  while (bounds != bounds_end) {
1427  TRACE("arith atoms", "trying propagation", ineq, (*bounds).second);
1428  const Expr& implied = (*bounds).second;
1429  // Try to do some theory propagation
1430  if ((*bounds).first < c1 || (!(ineq.getKind() == LE && implied.getKind() == LT) && (*bounds).first == c1)) {
1431  // c1 <= t1 => c <= t1 (for c <= c1)
1432  // c1 < t1 => c <= t1 (for c <= c1)
1433  // c1 <= t1 => c < t1 (for c < c1)
1434  Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, implied));
1435  enqueueFact(impliedThm);
1436  }
1437  bounds ++;
1438  }
1439  }
1440 
1441  //
1442  // c1 <= t1 ==> !(t1 <= c) for c < c1
1443  // ==> !(-c <= t2)
1444  // i.e. all coefficient in in the implied are opposite of t1
1445  find = formulaAtomUpperBound.find(t1);
1446  find_end = formulaAtomUpperBound.end();
1447  if (find != find_end) {
1448  set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
1449  set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
1450  while (bounds != bounds_end) {
1451  TRACE("arith atoms", "trying propagation", ineq, (*bounds).second);
1452  const Expr& implied = (*bounds).second;
1453  // Try to do some theory propagation
1454  if ((*bounds).first < c1) {
1455  Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyNegatedInequality(ineq, implied));
1456  enqueueFact(impliedThm);
1457  }
1458  bounds ++;
1459  }
1460  }
1461  }
1462 
1463  // Register this as a resource
1464  theoryCore()->getResource();
1465 
1466  // If out of resources, bail out
1467  if (theoryCore()->outOfResources()) return false;
1468 
1469  // Checking because we could have projected it as a find of some other
1470  // equation
1471  if (alreadyProjected.find(ineq) == alreadyProjected.end()) {
1472  // We buffer it if it's not marked for not buffering
1473  if (dontBuffer.find(ineq) == dontBuffer.end()) {
1474  // We give priority to the one that can produce a conflict
1475  if (priority)
1476  d_buffer_0.push_back(thm);
1477  else {
1478  // Push it into the buffer (one var)
1479  if (num_vars == 1) d_buffer_1.push_back(thm);
1480  else if (num_vars == 2) d_buffer_2.push_back(thm);
1481  else d_buffer_3.push_back(thm);
1482  }
1483 
1484  if (factIsDiffLogic) diff_logic_size = diff_logic_size + 1;
1485  }
1486  }
1487 
1488  // Remember that it's in the buffer
1489  bufferedInequalities[ineq] = thm;
1490 
1491  // Since we care about this atom, lets set it up
1492  if (!ineq.hasFind())
1493  theoryCore()->setupTerm(ineq, this, thm);
1494 
1495  return true;
1496 }
1497 
1498 
1499 Theorem TheoryArithOld::isolateVariable(const Theorem& inputThm,
1500  bool& isolatedVarOnRHS)
1501 {
1502  Theorem result(inputThm);
1503  const Expr& e = inputThm.getExpr();
1504  TRACE("arith","isolateVariable(",e,") {");
1505  TRACE("arith ineq", "isolateVariable(", e, ") {");
1506  //we assume all the children of e are canonized
1507  DebugAssert(isLT(e)||isLE(e),
1508  "TheoryArithOld::isolateVariable: " + e.toString() +
1509  " wrong kind");
1510  int kind = e.getKind();
1511  DebugAssert(e[0].isRational() && e[0].getRational() == 0,
1512  "TheoryArithOld::isolateVariable: theorem must be of "
1513  "the form 0 < rhs: " + inputThm.toString());
1514 
1515  const Expr& zero = e[0];
1516  Expr right = e[1];
1517  // Check for trivial in-equation.
1518  if (right.isRational()) {
1519  result = iffMP(result, d_rules->constPredicate(e));
1520  TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
1521  TRACE("arith","isolateVariable => ",result," }");
1522  return result;
1523  }
1524 
1525  // Normalization of inequality to make coefficients integer and
1526  // relatively prime.
1527 
1528  Expr factor(computeNormalFactor(right, false));
1529  TRACE("arith", "isolateVariable: factor = ", factor, "");
1530  DebugAssert(factor.getRational() > 0,
1531  "isolateVariable: factor="+factor.toString());
1532  // Now multiply the inequality by the factor, unless it is 1
1533  if(factor.getRational() != 1) {
1534  result = iffMP(result, d_rules->multIneqn(e, factor));
1535  // And canonize the result
1536  result = canonPred(result);
1537  result = rafineInequalityToInteger(result);
1538  right = result.getExpr()[1];
1539  }
1540 
1541  // Find monomial to isolate and store it in isolatedMonomial
1542  Expr isolatedMonomial = right;
1543 
1544  if (isPlus(right))
1545  isolatedMonomial = pickMonomial(right);
1546 
1547  TRACE("arith ineq", "isolatedMonomial => ",isolatedMonomial,"");
1548 
1549  // Set the correct isolated monomial
1550  // Now, if something gets updated, but this monomial is not changed, we don't
1551  // Have to rebuffer it as the projection will still be accurate when updated
1552  alreadyProjected[e] = isolatedMonomial;
1553 
1554  Rational r = -1;
1555  isolatedVarOnRHS = true;
1556  if (isMult(isolatedMonomial)) {
1557  r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
1558  isolatedVarOnRHS =
1559  ((isolatedMonomial[0].getRational()) >= 0)? true : false;
1560  }
1561  isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
1562  TRACE("arith ineq", "-(isolatedMonomial) => ",isolatedMonomial,"");
1563  // Isolate isolatedMonomial on to the LHS
1564  result = iffMP(result, d_rules->plusPredicate(zero, right,
1565  isolatedMonomial, kind));
1566  // Canonize the resulting inequality
1567  TRACE("arith ineq", "resutl => ",result,"");
1568  result = canonPred(result);
1569  if(1 != r) {
1570  result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
1571  result = canonPred(result);
1572  }
1573  TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
1574  TRACE("arith","isolateVariable => ",result," }");
1575  return result;
1576 }
1577 
1578 Expr
1579 TheoryArithOld::computeNormalFactor(const Expr& right, bool normalizeConstants) {
1580  // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
1581  // of the form c1/d1*x1 + ... + cn/dn*xn
1582  Rational factor;
1583  if(isPlus(right)) {
1584  vector<Rational> nums, denoms;
1585  for(int i=0, iend=right.arity(); i<iend; ++i) {
1586  switch(right[i].getKind()) {
1587  case RATIONAL_EXPR:
1588  if (normalizeConstants) {
1589  Rational c(abs(right[i].getRational()));
1590  nums.push_back(c.getNumerator());
1591  denoms.push_back(c.getDenominator());
1592  break;
1593  }
1594  break;
1595  case MULT: {
1596  Rational c(abs(right[i][0].getRational()));
1597  nums.push_back(c.getNumerator());
1598  denoms.push_back(c.getDenominator());
1599  break;
1600  }
1601  default: // it's a variable
1602  nums.push_back(1);
1603  denoms.push_back(1);
1604  break;
1605  }
1606  }
1607  Rational gcd_nums = gcd(nums);
1608  // x/0 == 0 in our model, as a total extension of arithmetic. The
1609  // particular value of x/0 is irrelevant, since the DP is guarded
1610  // by the top-level TCCs, and it is safe to return any value in
1611  // cases when terms are undefined.
1612  factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
1613  } else if(isMult(right)) {
1614  const Rational& r = right[0].getRational();
1615  factor = (r==0)? 0 : (1/abs(r));
1616  }
1617  else
1618  factor = 1;
1619  return rat(factor);
1620 }
1621 
1622 
1623 bool TheoryArithOld::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
1624 {
1625  DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
1626  "TheoryArithOld::findMaxVar: isolatedMonomial cannot be rational" +
1627  isolatedMonomial.toString());
1628  Expr c, var0, var1;
1629  separateMonomial(isolatedMonomial, c, var0);
1630  separateMonomial(var2, c, var1);
1631  return var0 < var1;
1632 }
1633 
1634 /*! "Stale" means it contains non-simplified subexpressions. For
1635  * terms, it checks the expression's find pointer; for formulas it
1636  * checks the children recursively (no caching!). So, apply it with
1637  * caution, and only to simple atomic formulas (like inequality).
1638  */
1639 bool TheoryArithOld::isStale(const Expr& e) {
1640  if(e.isTerm())
1641  return e != find(e).getRHS();
1642  // It's better be a simple predicate (like inequality); we check the
1643  // kids recursively
1644  bool stale=false;
1645  for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
1646  stale = isStale(*i);
1647  return stale;
1648 }
1649 
1650 
1651 bool TheoryArithOld::isStale(const TheoryArithOld::Ineq& ineq) {
1652  TRACE("arith stale", "isStale(", ineq, ") {");
1653  const Expr& ineqExpr = ineq.ineq().getExpr();
1654  const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
1655  bool strict(isLT(ineqExpr));
1656  const FreeConst& fc = ineq.getConst();
1657 
1658  bool subsumed;
1659 
1660  if (ineqExpr.hasFind() && find(ineqExpr[1]).getRHS() != ineqExpr[1])
1661  return true;
1662 
1663  if(ineq.varOnRHS()) {
1664  subsumed = (c < fc.getConst() ||
1665  (c == fc.getConst() && !strict && fc.strict()));
1666  } else {
1667  subsumed = (c > fc.getConst() ||
1668  (c == fc.getConst() && strict && !fc.strict()));
1669  }
1670 
1671  bool res;
1672  if(subsumed) {
1673  res = true;
1674  TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
1675  }
1676  else {
1677  res = isStale(ineqExpr);
1678  TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
1679  }
1680  return res;
1681 }
1682 
1683 
1684 void TheoryArithOld::separateMonomial(const Expr& e, Expr& c, Expr& var) {
1685  TRACE("separateMonomial", "separateMonomial(", e, ")");
1686  DebugAssert(!isPlus(e),
1687  "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
1688  if(isMult(e)) {
1689  DebugAssert(e.arity() >= 2,
1690  "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
1691  c = e[0];
1692  if(e.arity() == 2) var = e[1];
1693  else {
1694  vector<Expr> kids = e.getKids();
1695  kids[0] = rat(1);
1696  var = multExpr(kids);
1697  }
1698  } else {
1699  c = rat(1);
1700  var = e;
1701  }
1702  DebugAssert(c.isRational(), "TheoryArithOld::separateMonomial(e = "
1703  +e.toString()+", c = "+c.toString()+")");
1704  DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
1705  "TheoryArithOld::separateMonomial(e = "
1706  +e.toString()+", var = "+var.toString()+")");
1707 }
1708 
1709 
1710 void TheoryArithOld::projectInequalities(const Theorem& theInequality,
1711  bool isolatedVarOnRHS)
1712 {
1713 
1714  TRACE("arith project", "projectInequalities(", theInequality.getExpr(),
1715  ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
1716  +") {");
1717  DebugAssert(isLE(theInequality.getExpr()) ||
1718  isLT(theInequality.getExpr()),
1719  "TheoryArithOld::projectIsolatedVar: "\
1720  "theInequality is of the wrong form: " +
1721  theInequality.toString());
1722 
1723  //TODO: DebugAssert to check if the isolatedMonomial is of the right
1724  //form and the whether we are indeed getting inequalities.
1725  Theorem theIneqThm(theInequality);
1726  Expr theIneq = theIneqThm.getExpr();
1727 
1728  // If the inequality is strict and integer, change it to non-strict
1729  if(isLT(theIneq)) {
1730  Theorem isIntLHS(isIntegerThm(theIneq[0]));
1731  Theorem isIntRHS(isIntegerThm(theIneq[1]));
1732  if ((!isIntLHS.isNull() && !isIntRHS.isNull())) {
1733  Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, !isolatedVarOnRHS);
1734  theIneqThm = canonPred(iffMP(theIneqThm, thm));
1735  theIneq = theIneqThm.getExpr();
1736  }
1737  }
1738 
1739  Expr isolatedMonomial = isolatedVarOnRHS ? theIneq[1] : theIneq[0];
1740 
1741  Expr monomialVar, a;
1742  separateMonomial(isolatedMonomial, a, monomialVar);
1743 
1744  bool subsumed;
1745  const FreeConst& bestConst = updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
1746 
1747  if(subsumed) {
1748  IF_DEBUG(debugger.counter("subsumed inequalities")++;)
1749  TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
1750  } else {
1751  // If the isolated variable is actually a non-linear term, we are
1752  // incomplete
1753  if(isMult(monomialVar) || isPow(monomialVar))
1754  setIncomplete("Non-linear arithmetic inequalities");
1755 
1756  // First, we need to make sure the isolated inequality is
1757  // setup properly.
1758  // setupRec(theIneq[0]);
1759  // setupRec(theIneq[1]);
1760  theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
1761  theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
1762  // Add the inequality into the appropriate DB.
1763  ExprMap<CDList<Ineq> *>& db1 = isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
1764  ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
1765  if(it1 == db1.end()) {
1766  CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
1767  list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1768  db1[monomialVar] = list;
1769  }
1770  else
1771  ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1772 
1773  ExprMap<CDList<Ineq> *>& db2 = isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
1774  ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
1775  if(it == db2.end()) {
1776  TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
1777  return;
1778  }
1779 
1780  CDList<Ineq>& listOfDBIneqs = *((*it).second);
1781  Theorem betaLTt, tLTalpha, thm;
1782  for(int i = listOfDBIneqs.size() - 1; !inconsistent() && i >= 0; --i) {
1783  const Ineq& ineqEntry = listOfDBIneqs[i];
1784  const Theorem& ineqThm = ineqEntry.ineq(); //inequalityToFind(ineqEntry.ineq(), isolatedVarOnRHS);
1785 
1786  // ineqExntry might be stale
1787 
1788  if(!isStale(ineqEntry)) {
1789  betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
1790  tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
1791 
1792  thm = normalizeProjectIneqs(betaLTt, tLTalpha);
1793  if (thm.isNull()) continue;
1794 
1795  IF_DEBUG(debugger.counter("real shadows")++;)
1796 
1797  // Check for TRUE and FALSE theorems
1798  Expr e(thm.getExpr());
1799 
1800  if(e.isFalse()) {
1801  setInconsistent(thm);
1802  TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
1803  return;
1804  }
1805  else {
1806  if(!e.isTrue() && !e.isEq()) {
1807  // setup the term so that it comes out in updates
1808  addToBuffer(thm, false);
1809  }
1810  else if(e.isEq())
1811  enqueueFact(thm);
1812  }
1813  } else {
1814  IF_DEBUG(debugger.counter("stale inequalities")++;)
1815  }
1816  }
1817  }
1818 
1819  TRACE_MSG("arith ineq", "projectInequalities => }");
1820 }
1821 
1822 Theorem TheoryArithOld::normalizeProjectIneqs(const Theorem& ineqThm1,
1823  const Theorem& ineqThm2)
1824 {
1825  //ineq1 is of the form beta < b.x or beta < x [ or with <= ]
1826  //ineq2 is of the form a.x < alpha or x < alpha.
1827  Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
1828  Expr ineq1 = betaLTt.getExpr();
1829  Expr ineq2 = tLTalpha.getExpr();
1830  Expr c,x;
1831  separateMonomial(ineq2[0], c, x);
1832  Theorem isIntx(isIntegerThm(x));
1833  Theorem isIntBeta(isIntegerThm(ineq1[0]));
1834  Theorem isIntAlpha(isIntegerThm(ineq2[1]));
1835  bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
1836 
1837  TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
1838  ", "+ineq2.toString()+") {");
1839  DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
1840  (isLE(ineq2) || isLT(ineq2)),
1841  "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
1842  ineq1.toString() + ineq2.toString());
1843  DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
1844  "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
1845  ineq1.toString() + ineq2.toString());
1846 
1847  //compute the factors to multiply the two inequalities with
1848  //so that they get the form beta < t and t < alpha.
1849  Rational factor1 = 1, factor2 = 1;
1850  Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
1851  Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
1852  if(b != a) {
1853  factor1 = a;
1854  factor2 = b;
1855  }
1856 
1857  //if the ineqs are of type int then apply one of the gray
1858  //dark shadow rules.
1859  // FIXME: intResult should also be checked for immediate
1860  // optimizations, as those below for 'result'. Also, if intResult
1861  // is a single inequality, we may want to handle it similarly to the
1862  // 'result' rather than enqueuing directly.
1863  if(isInt && (a >= 2 || b >= 2)) {
1864  Theorem intResult;
1865  if(a <= b)
1866  intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
1867  isIntAlpha, isIntBeta, isIntx);
1868  else
1869  intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
1870  isIntAlpha, isIntBeta, isIntx);
1871  enqueueFact(intResult);
1872  // Fetch dark and gray shadows
1873  const Expr& DorG = intResult.getExpr();
1874  DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
1875  const Expr& G = DorG[1];
1876  DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
1877  // Set the higher splitter priority for dark shadow
1878 // Expr tmp = simplifyExpr(D);
1879 // if (!tmp.isBoolConst())
1880 // addSplitter(tmp, 5);
1881  // Also set a higher priority to the NEGATION of GRAY_SHADOW
1882  Expr tmp = simplifyExpr(!G);
1883  if (!tmp.isBoolConst())
1884  addSplitter(tmp, 1);
1885  IF_DEBUG(debugger.counter("dark+gray shadows")++;)
1886 
1887  // Dejan: Let's forget about the real shadow, we are doing integers
1888 // /return intResult;
1889  }
1890 
1891  //actually normalize the inequalities
1892  if(1 != factor1) {
1893  Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
1894  betaLTt = canonPred(thm2);
1895  ineq1 = betaLTt.getExpr();
1896  }
1897  if(1 != factor2) {
1898  Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
1899  tLTalpha = canonPred(thm2);
1900  ineq2 = tLTalpha.getExpr();
1901  }
1902 
1903  //IF_DEBUG(debugger.counter("real shadows")++;)
1904 
1905  Expr beta(ineq1[0]);
1906  Expr alpha(ineq2[1]);
1907  // In case of alpha <= t <= alpha, we generate t = alpha
1908  if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
1909  Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
1910  TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1911  return result;
1912  }
1913 
1914  // Check if this inequality is a finite interval
1915 // if(isInt)
1916 // processFiniteInterval(betaLTt, tLTalpha);
1917 
1918 // // Only do the real shadow if a and b = 1
1919 // if (isInt && a > 1 && b > 1)
1920 // return Theorem();
1921 
1922  //project the normalized inequalities.
1923 
1924  Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
1925 
1926  // FIXME: Clark's changes. Is 'rewrite' more or less efficient?
1927 // result = iffMP(result, rewrite(result.getExpr()));
1928 // TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1929 
1930  // Now, transform the result into 0 < rhs and see if rhs is a const
1931  Expr e(result.getExpr());
1932  // int kind = e.getKind();
1933  if(!(e[0].isRational() && e[0].getRational() == 0))
1934  result = iffMP(result, d_rules->rightMinusLeft(e));
1935  result = canonPred(result);
1936 
1937  //result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
1938  Expr right = result.getExpr()[1];
1939  // Check for trivial inequality
1940  if (right.isRational())
1941  result = iffMP(result, d_rules->constPredicate(result.getExpr()));
1942  else
1943  result = normalize(result);
1944  TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1945  return result;
1946 }
1947 
1948 Rational TheoryArithOld::currentMaxCoefficient(Expr var)
1949 {
1950  // We prefer real variables
1951  if (var.getType() == d_realType) return -100;
1952 
1953  // Find the biggest left side coefficient
1954  ExprMap<Rational>::iterator findMaxLeft = maxCoefficientLeft.find(var);
1955  Rational leftMax = -1;
1956  if (findMaxLeft != maxCoefficientLeft.end())
1957  leftMax = (*findMaxLeft).second;
1958 
1959  //
1960  ExprMap<Rational>::iterator findMaxRight = maxCoefficientRight.find(var);
1961  Rational rightMax = -1;
1962  if (findMaxRight != maxCoefficientRight.end())
1963  rightMax = (*findMaxRight).second;
1964 
1965  // What is the max coefficient
1966  // If one is undefined, dont take it. My first thought was to project away unbounded
1967  // ones, but it happens that you get another constraint on it later and the hell breaks
1968  // loose if they have big coefficients.
1969  Rational returnValue;
1970  if (leftMax == -1) returnValue = rightMax;
1971  else if (rightMax == -1) returnValue = leftMax;
1972  else if (leftMax < rightMax) returnValue = rightMax;
1973  else returnValue = leftMax;
1974 
1975  TRACE("arith stats", "max coeff of ", var.toString(), ": " + returnValue.toString() + "(left=" + leftMax.toString() + ",right=" + rightMax.toString());
1976 
1977  return returnValue;
1978 }
1979 
1980 void TheoryArithOld::fixCurrentMaxCoefficient(Expr var, Rational max) {
1981  fixedMaxCoefficient[var] = max;
1982 }
1983 
1984 void TheoryArithOld::selectSmallestByCoefficient(const vector<Expr>& input, vector<Expr>& output) {
1985 
1986  // Clear the output vector
1987  output.clear();
1988 
1989  // Get the first variable, and set it as best
1990  Expr best_variable = input[0];
1991  Rational best_coefficient = currentMaxCoefficient(best_variable);
1992  output.push_back(best_variable);
1993 
1994  for(unsigned int i = 1; i < input.size(); i ++) {
1995 
1996  // Get the current variable
1997  Expr current_variable = input[i];
1998  // Get the current variable's max coefficient
1999  Rational current_coefficient = currentMaxCoefficient(current_variable);
2000 
2001  // If strictly better than the current best, remember it
2002  if ((current_coefficient < best_coefficient)) {
2003  best_variable = current_variable;
2004  best_coefficient = current_coefficient;
2005  output.clear();
2006  }
2007 
2008  // If equal to the current best, push it to the stack (in 10% range)
2009  if (current_coefficient == best_coefficient)
2010  output.push_back(current_variable);
2011  }
2012 
2013  // Fix the selected best coefficient
2014  //fixCurrentMaxCoefficient(best_variable, best_coefficient);
2015 }
2016 
2017 Expr TheoryArithOld::pickMonomial(const Expr& right)
2018 {
2019  DebugAssert(isPlus(right), "TheoryArithOld::pickMonomial: Wrong Kind: " +
2020  right.toString());
2021  if(theoryCore()->getFlags()["var-order"].getBool()) {
2022  Expr::iterator i = right.begin();
2023  Expr isolatedMonomial = right[1];
2024  //PLUS always has at least two elements and the first element is
2025  //always a constant. hence ++i in the initialization of the for
2026  //loop.
2027  for(++i; i != right.end(); ++i)
2028  if(lessThanVar(isolatedMonomial,*i))
2029  isolatedMonomial = *i;
2030  return isolatedMonomial;
2031  }
2032 
2033  ExprMap<Expr> var2monomial;
2034  vector<Expr> vars;
2035  Expr::iterator i = right.begin(), iend = right.end();
2036  for(;i != iend; ++i) {
2037  if(i->isRational())
2038  continue;
2039  Expr c, var;
2040  separateMonomial(*i, c, var);
2041  var2monomial[var] = *i;
2042  vars.push_back(var);
2043  }
2044 
2045  vector<Expr> largest;
2046  d_graph.selectLargest(vars, largest);
2047  DebugAssert(0 < largest.size(),
2048  "TheoryArithOld::pickMonomial: selectLargest: failed!!!!");
2049 
2050  // DEJAN: Rafine the largest by coefficient values
2051  vector<Expr> largest_small_coeff;
2052  selectSmallestByCoefficient(largest, largest_small_coeff);
2053  DebugAssert(0 < largest_small_coeff.size(), "TheoryArithOld::pickMonomial: selectLargestByCOefficient: failed!!!!");
2054 
2055  size_t pickedVar = 0;
2056  // Pick the variable which will generate the fewest number of
2057  // projections
2058 
2059  size_t size = largest_small_coeff.size();
2060  int minProjections = -1;
2061  if (size > 1)
2062  for(size_t k=0; k< size; ++k) {
2063  const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
2064  // Grab the counters for the variable
2065  int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
2066  int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
2067  int n(nRight*nLeft);
2068  TRACE("arith ineq", "pickMonomial: var=", var,
2069  ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
2070  if(minProjections < 0 || minProjections > n) {
2071  minProjections = n;
2072  pickedVar = k;
2073  }
2074  TRACE("arith ineq", "Number of projections for "+var.toString()+" = ", n, "");
2075  }
2076 
2077 
2078  const Expr& largestVar = largest_small_coeff[pickedVar];
2079  // FIXME: TODO: update the counters (subtract counts for the vars
2080  // other than largestVar
2081 
2082  // Update the graph (all edges to the largest in the graph, not just the small coefficients).
2083  for(size_t k = 0; k < vars.size(); ++k) {
2084  if(vars[k] != largestVar)
2085  d_graph.addEdge(largestVar, vars[k]);
2086  }
2087 
2088  TRACE("arith buffer", "picked var : ", var2monomial[largestVar].toString(), "");
2089 
2090  return var2monomial[largestVar];
2091 }
2092 
2093 void TheoryArithOld::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
2094 {
2095  TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
2096  DebugAssert(e1 != e2, "TheoryArithOld::VarOrderGraph::addEdge("
2097  +e1.toString()+", "+e2.toString()+")");
2098  d_edges[e1].push_back(e2);
2099 }
2100 
2101 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
2102 //comparable)
2103 bool TheoryArithOld::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
2104 {
2105  d_cache.clear();
2106  //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
2107  return dfs(e1,e2);
2108 }
2109 
2110 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
2111 bool TheoryArithOld::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
2112 {
2113  if(e1 == e2)
2114  return true;
2115  if(d_cache.count(e2) > 0)
2116  return false;
2117  if(d_edges.count(e2) == 0)
2118  return false;
2119  d_cache[e2] = true;
2120  vector<Expr>& e2Edges = d_edges[e2];
2121  vector<Expr>::iterator i = e2Edges.begin();
2122  vector<Expr>::iterator iend = e2Edges.end();
2123  //if dfs finds e1 then i != iend else i is equal to iend
2124  for(; i != iend && !dfs(e1,*i); ++i);
2125  return (i != iend);
2126 }
2127 
2128 void TheoryArithOld::VarOrderGraph::dfs(const Expr& v, vector<Expr>& output_list)
2129 {
2130  TRACE("arith shared", "dfs(", v.toString(), ")");
2131 
2132  // If visited already we are done
2133  if (d_cache.count(v) > 0) return;
2134 
2135  // Dfs further
2136  if(d_edges.count(v) != 0) {
2137  // We have edges, so lets dfs it further
2138  vector<Expr>& vEdges = d_edges[v];
2139  vector<Expr>::iterator e = vEdges.begin();
2140  vector<Expr>::iterator e_end = vEdges.end();
2141  while (e != e_end) {
2142  dfs(*e, output_list);
2143  e ++;
2144  }
2145  }
2146 
2147  // Mark as visited and add to the output list
2148  d_cache[v] = true;
2149  output_list.push_back(v);
2150 }
2151 
2152 void TheoryArithOld::VarOrderGraph::getVerticesTopological(vector<Expr>& output_list)
2153 {
2154  // Clear the cache
2155  d_cache.clear();
2156  output_list.clear();
2157 
2158  // Go through all the vertices and run a dfs from them
2159  ExprMap< vector<Expr> >::iterator v_it = d_edges.begin();
2160  ExprMap< vector<Expr> >::iterator v_it_end = d_edges.end();
2161  while (v_it != v_it_end)
2162  {
2163  // Run dfs from this vertex
2164  dfs(v_it->first, output_list);
2165  // Go to the next one
2166  v_it ++;
2167  }
2168 }
2169 
2170 void TheoryArithOld::VarOrderGraph::selectSmallest(vector<Expr>& v1,
2171  vector<Expr>& v2)
2172 {
2173  int v1Size = v1.size();
2174  vector<bool> v3(v1Size);
2175  for(int j=0; j < v1Size; ++j)
2176  v3[j] = false;
2177 
2178  for(int j=0; j < v1Size; ++j) {
2179  if(v3[j]) continue;
2180  for(int i =0; i < v1Size; ++i) {
2181  if((i == j) || v3[i])
2182  continue;
2183  if(lessThan(v1[i],v1[j])) {
2184  v3[j] = true;
2185  break;
2186  }
2187  }
2188  }
2189  vector<Expr> new_v1;
2190 
2191  for(int j = 0; j < v1Size; ++j)
2192  if(!v3[j]) v2.push_back(v1[j]);
2193  else new_v1.push_back(v1[j]);
2194  v1 = new_v1;
2195 }
2196 
2197 
2198 void TheoryArithOld::VarOrderGraph::selectLargest(const vector<Expr>& v1,
2199  vector<Expr>& v2)
2200 {
2201  int v1Size = v1.size();
2202  vector<bool> v3(v1Size);
2203  for(int j=0; j < v1Size; ++j)
2204  v3[j] = false;
2205 
2206  for(int j=0; j < v1Size; ++j) {
2207  if(v3[j]) continue;
2208  for(int i =0; i < v1Size; ++i) {
2209  if((i == j) || v3[i])
2210  continue;
2211  if(lessThan(v1[j],v1[i])) {
2212  v3[j] = true;
2213  break;
2214  }
2215  }
2216  }
2217 
2218  for(int j = 0; j < v1Size; ++j)
2219  if(!v3[j]) v2.push_back(v1[j]);
2220 }
2221 
2222 ///////////////////////////////////////////////////////////////////////////////
2223 // TheoryArithOld Public Methods //
2224 ///////////////////////////////////////////////////////////////////////////////
2225 
2226 
2227 TheoryArithOld::TheoryArithOld(TheoryCore* core)
2228  : TheoryArith(core, "ArithmeticOld"),
2229  d_diseq(core->getCM()->getCurrentContext()),
2230  d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
2231  diseqSplitAlready(core->getCM()->getCurrentContext()),
2232  d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
2233  d_freeConstDB(core->getCM()->getCurrentContext()),
2234  d_buffer_0(core->getCM()->getCurrentContext()),
2235  d_buffer_1(core->getCM()->getCurrentContext()),
2236  d_buffer_2(core->getCM()->getCurrentContext()),
2237  d_buffer_3(core->getCM()->getCurrentContext()),
2238  // Initialize index to 0 at scope 0
2239  d_bufferIdx_0(core->getCM()->getCurrentContext(), 0, 0),
2240  d_bufferIdx_1(core->getCM()->getCurrentContext(), 0, 0),
2241  d_bufferIdx_2(core->getCM()->getCurrentContext(), 0, 0),
2242  d_bufferIdx_3(core->getCM()->getCurrentContext(), 0, 0),
2243  diff_logic_size(core->getCM()->getCurrentContext(), 0, 0),
2244  d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
2245  d_splitSign(&(core->getFlags()["nonlinear-sign-split"].getBool())),
2246  d_grayShadowThres(&(core->getFlags()["grayshadow-threshold"].getInt())),
2247  d_countRight(core->getCM()->getCurrentContext()),
2248  d_countLeft(core->getCM()->getCurrentContext()),
2249  d_sharedTerms(core->getCM()->getCurrentContext()),
2250  d_sharedTermsList(core->getCM()->getCurrentContext()),
2251  d_sharedVars(core->getCM()->getCurrentContext()),
2252  bufferedInequalities(core->getCM()->getCurrentContext()),
2253  termLowerBound(core->getCM()->getCurrentContext()),
2254  termLowerBoundThm(core->getCM()->getCurrentContext()),
2255  termUpperBound(core->getCM()->getCurrentContext()),
2256  termUpperBoundThm(core->getCM()->getCurrentContext()),
2257  alreadyProjected(core->getCM()->getCurrentContext()),
2258  dontBuffer(core->getCM()->getCurrentContext()),
2259  diffLogicOnly(core->getCM()->getCurrentContext(), true, 0),
2260  diffLogicGraph(0, core, 0, core->getCM()->getCurrentContext()),
2261  shared_index_1(core->getCM()->getCurrentContext(), 0, 0),
2262  shared_index_2(core->getCM()->getCurrentContext(), 0, 0),
2263  termUpperBounded(core->getCM()->getCurrentContext()),
2264  termLowerBounded(core->getCM()->getCurrentContext()),
2265  d_varConstrainedPlus(core->getCM()->getCurrentContext()),
2266  d_varConstrainedMinus(core->getCM()->getCurrentContext()),
2267  termConstrainedBelow(core->getCM()->getCurrentContext()),
2268  termConstrainedAbove(core->getCM()->getCurrentContext())
2269 {
2270  IF_DEBUG(d_diseq.setName("CDList[TheoryArithOld::d_diseq]");)
2271  IF_DEBUG(d_buffer_0.setName("CDList[TheoryArithOld::d_buffer_0]");)
2272  IF_DEBUG(d_buffer_1.setName("CDList[TheoryArithOld::d_buffer_1]");)
2273  IF_DEBUG(d_buffer_2.setName("CDList[TheoryArithOld::d_buffer_2]");)
2274  IF_DEBUG(d_buffer_3.setName("CDList[TheoryArithOld::d_buffer_3]");)
2275  IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_0]");)
2276  IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_1]");)
2277  IF_DEBUG(d_bufferIdx_2.setName("CDList[TheoryArithOld::d_bufferIdx_2]");)
2278  IF_DEBUG(d_bufferIdx_3.setName("CDList[TheoryArithOld::d_bufferIdx_3]");)
2279 
2280  getEM()->newKind(REAL, "_REAL", true);
2281  getEM()->newKind(INT, "_INT", true);
2282  getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
2283 
2284  getEM()->newKind(UMINUS, "_UMINUS");
2285  getEM()->newKind(PLUS, "_PLUS");
2286  getEM()->newKind(MINUS, "_MINUS");
2287  getEM()->newKind(MULT, "_MULT");
2288  getEM()->newKind(DIVIDE, "_DIVIDE");
2289  getEM()->newKind(POW, "_POW");
2290  getEM()->newKind(INTDIV, "_INTDIV");
2291  getEM()->newKind(MOD, "_MOD");
2292  getEM()->newKind(LT, "_LT");
2293  getEM()->newKind(LE, "_LE");
2294  getEM()->newKind(GT, "_GT");
2295  getEM()->newKind(GE, "_GE");
2296  getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
2297  getEM()->newKind(NEGINF, "_NEGINF");
2298  getEM()->newKind(POSINF, "_POSINF");
2299  getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
2300  getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
2301 
2302  getEM()->newKind(REAL_CONST, "_REAL_CONST");
2303 
2304  d_kinds.push_back(REAL);
2305  d_kinds.push_back(INT);
2306  d_kinds.push_back(SUBRANGE);
2307  d_kinds.push_back(IS_INTEGER);
2308  d_kinds.push_back(UMINUS);
2309  d_kinds.push_back(PLUS);
2310  d_kinds.push_back(MINUS);
2311  d_kinds.push_back(MULT);
2312  d_kinds.push_back(DIVIDE);
2313  d_kinds.push_back(POW);
2314  d_kinds.push_back(INTDIV);
2315  d_kinds.push_back(MOD);
2316  d_kinds.push_back(LT);
2317  d_kinds.push_back(LE);
2318  d_kinds.push_back(GT);
2319  d_kinds.push_back(GE);
2320  d_kinds.push_back(RATIONAL_EXPR);
2321  d_kinds.push_back(NEGINF);
2322  d_kinds.push_back(POSINF);
2323  d_kinds.push_back(DARK_SHADOW);
2324  d_kinds.push_back(GRAY_SHADOW);
2325  d_kinds.push_back(REAL_CONST);
2326 
2327  registerTheory(this, d_kinds, true);
2328 
2331  diffLogicGraph.setArith(this);
2332 
2333  d_realType = Type(getEM()->newLeafExpr(REAL));
2334  d_intType = Type(getEM()->newLeafExpr(INT));
2335 
2336  // Make the zero variable
2337  Theorem thm_exists_zero = getCommonRules()->varIntroSkolem(rat(0));
2338  zero = thm_exists_zero.getExpr()[1];
2339 }
2340 
2341 
2342 // Destructor: delete the proof rules class if it's present
2344  if(d_rules != NULL) delete d_rules;
2345  // Clear the inequality databases
2346  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
2347  iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
2348  delete (i->second);
2349  free(i->second);
2350  }
2351  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
2352  iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
2353  delete (i->second);
2354  free (i->second);
2355  }
2356  unregisterTheory(this, d_kinds, true);
2357 }
2358 
2359 void TheoryArithOld::collectVars(const Expr& e, vector<Expr>& vars,
2360  set<Expr>& cache) {
2361  // Check the cache first
2362  if(cache.count(e) > 0) return;
2363  // Not processed yet. Cache the expression and proceed
2364  cache.insert(e);
2365  if(isLeaf(e)) vars.push_back(e);
2366  else
2367  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
2368  collectVars(*i, vars, cache);
2369 }
2370 
2371 void
2373 (const Theorem& alphaLEax,
2374  const Theorem& bxLEbeta) {
2375  const Expr& ineq1(alphaLEax.getExpr());
2376  const Expr& ineq2(bxLEbeta.getExpr());
2377  DebugAssert(isLE(ineq1), "TheoryArithOld::processFiniteInterval: ineq1 = "
2378  +ineq1.toString());
2379  DebugAssert(isLE(ineq2), "TheoryArithOld::processFiniteInterval: ineq2 = "
2380  +ineq2.toString());
2381  // If the inequalities are not integer, just return (nothing to do)
2382  if(!isInteger(ineq1[0])
2383  || !isInteger(ineq1[1])
2384  || !isInteger(ineq2[0])
2385  || !isInteger(ineq2[1]))
2386  return;
2387 
2388  const Expr& ax = ineq1[1];
2389  const Expr& bx = ineq2[0];
2390  DebugAssert(!isPlus(ax) && !isRational(ax),
2391  "TheoryArithOld::processFiniteInterval:\n ax = "+ax.toString());
2392  DebugAssert(!isPlus(bx) && !isRational(bx),
2393  "TheoryArithOld::processFiniteInterval:\n bx = "+bx.toString());
2394  Expr a = isMult(ax)? ax[0] : rat(1);
2395  Expr b = isMult(bx)? bx[0] : rat(1);
2396 
2397  Theorem thm1(alphaLEax), thm2(bxLEbeta);
2398  // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
2399  if(a != b) {
2400  thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
2401  thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
2402  }
2403  // Check that a*beta - b*alpha == c > 0
2404  const Expr& alphaLEt = thm1.getExpr();
2405  const Expr& alpha = alphaLEt[0];
2406  const Expr& t = alphaLEt[1];
2407  const Expr& beta = thm2.getExpr()[1];
2408  Expr c = canon(beta - alpha).getRHS();
2409 
2410  if(c.isRational() && c.getRational() >= 1) {
2411  // This is a finite interval. First, derive t <= alpha + c:
2412  // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
2413  // Then substitute that in thm2
2414  Theorem bEQac = symmetryRule(canon(alpha + c));
2415  // Substitute beta == alpha+c for the second child of thm2
2416  vector<unsigned> changed;
2417  vector<Theorem> thms;
2418  changed.push_back(1);
2419  thms.push_back(bEQac);
2420  Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
2421  tLEac = iffMP(thm2, tLEac);
2422  // Derive and enqueue the finite interval constraint
2423  Theorem isInta(isIntegerThm(alpha));
2424  Theorem isIntt(isIntegerThm(t));
2425  if (d_sharedTerms.find(thm1.getExpr()[1]) != d_sharedTerms.end())
2426  enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
2427  }
2428 }
2429 
2430 
2431 void
2433  // If x is not integer, do not bother
2434  if(!isInteger(x)) return;
2435  // Process every pair of the opposing inequalities for 'x'
2436  ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
2437  iLeft = d_inequalitiesLeftDB.find(x);
2438  if(iLeft == d_inequalitiesLeftDB.end()) return;
2439  iRight = d_inequalitiesRightDB.find(x);
2440  if(iRight == d_inequalitiesRightDB.end()) return;
2441  // There are some opposing inequalities; get the lists
2442  CDList<Ineq>& ineqsLeft = *(iLeft->second);
2443  CDList<Ineq>& ineqsRight = *(iRight->second);
2444  // Get the sizes of the lists
2445  size_t sizeLeft = ineqsLeft.size();
2446  size_t sizeRight = ineqsRight.size();
2447  // Process all the pairs of the opposing inequalities
2448  for(size_t l=0; l<sizeLeft; ++l)
2449  for(size_t r=0; r<sizeRight; ++r)
2450  processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
2451 }
2452 
2453 /*! This function recursively decends expression tree <strong>without
2454  * caching</strong> until it hits a node that is already setup. Be
2455  * careful on what expressions you are calling it.
2456  */
2457 void
2459  if(e.hasFind()) return;
2460  // First, set up the kids recursively
2461  for (int k = 0; k < e.arity(); ++k) {
2462  setupRec(e[k]);
2463  }
2464  // Create a find pointer for e
2465  e.setFind(reflexivityRule(e));
2466  e.setEqNext(reflexivityRule(e));
2467  // And call our own setup()
2468  setup(e);
2469 }
2470 
2471 
2473  return;
2474  if (d_sharedTerms.find(e) == d_sharedTerms.end()) {
2475  d_sharedTerms[e] = true;
2477  }
2478 }
2479 
2480 
2482 {
2483  TRACE("arith assert", "assertFact(", e.getExpr().toString(), ")");
2484 
2485  // Pick up any multiplicative case splits and enqueue them
2486  for (unsigned i = 0; i < multiplicativeSignSplits.size(); i ++)
2488  multiplicativeSignSplits.clear();
2489 
2490  const Expr& expr = e.getExpr();
2491  if (expr.isNot() && expr[0].isEq()) {
2492  IF_DEBUG(debugger.counter("[arith] received disequalities")++;)
2493  d_diseq.push_back(e);
2494  }
2495  else if (!expr.isEq()){
2496  if (expr.isNot()) {
2497  // If expr[0] is asserted to *not* be an integer, we track it
2498  // so we will detect if it ever becomes equal to an integer.
2499  if (expr[0].getKind() == IS_INTEGER) {
2500  expr[0][0].addToNotify(this, expr[0]);
2501  }
2502  // This can only be negation of dark or gray shadows, or
2503  // disequalities, which we ignore. Negations of inequalities
2504  // are handled in rewrite, we don't even receive them here.
2505  }
2506  else if(isDarkShadow(expr)) {
2508  IF_DEBUG(debugger.counter("received DARK_SHADOW")++;)
2509  }
2510  else if(isGrayShadow(expr)) {
2511  IF_DEBUG(debugger.counter("received GRAY_SHADOW")++;)
2512  const Rational& c1 = expr[2].getRational();
2513  const Rational& c2 = expr[3].getRational();
2514 
2515  // If gray shadow bigger than the treshold, we are done
2516  if (*d_grayShadowThres > -1 && (c2 - c1 > *d_grayShadowThres)) {
2517  setIncomplete("Some gray shadows ignored due to threshold");
2518  return;
2519  }
2520 
2521  const Expr& v = expr[0];
2522  const Expr& ee = expr[1];
2523  if(c1 == c2)
2525  else {
2526  Theorem gThm(e);
2527  // Check if we can reduce the number of cases in G(ax,c,c1,c2)
2528  if(ee.isRational() && isMult(v)
2529  && v[0].isRational() && v[0].getRational() >= 2) {
2530  IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++;)
2531  gThm = d_rules->grayShadowConst(e);
2532  }
2533  // (Possibly) new gray shadow
2534  const Expr& g = gThm.getExpr();
2535  if(g.isFalse())
2536  setInconsistent(gThm);
2537  else if(g[2].getRational() == g[3].getRational())
2539  else if(g[3].getRational() - g[2].getRational() <= 5) {
2540  // Assert c1+e <= v <= c2+e
2542  // Split G into 2 cases x = l_bound and the other
2543  Theorem thm2 = d_rules->splitGrayShadowSmall(gThm);
2544  enqueueFact(thm2);
2545  }
2546  else {
2547  // Assert c1+e <= v <= c2+e
2549  // Split G into 2 cases (binary search b/w c1 and c2)
2550  Theorem thm2 = d_rules->splitGrayShadow(gThm);
2551  enqueueFact(thm2);
2552  }
2553  }
2554  }
2555  else {
2556  DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr),
2557  "expected LE or LT: "+expr.toString());
2558  if(isLE(expr) || isLT(expr)) {
2559  IF_DEBUG(debugger.counter("recevied inequalities")++;)
2560 
2561  // Buffer the inequality
2562  addToBuffer(e);
2563 
2564  unsigned total_buf_size = d_buffer_0.size() + d_buffer_1.size() + d_buffer_2.size() + d_buffer_3.size();
2565  unsigned processed = d_bufferIdx_0 + d_bufferIdx_1 + d_bufferIdx_2 + d_bufferIdx_3;
2566  TRACE("arith ineq", "buffer.size() = ", total_buf_size,
2567  ", index="+int2string(processed)
2568  +", threshold="+int2string(*d_bufferThres));
2569 
2570  if(!diffLogicOnly && *d_bufferThres >= 0 && (total_buf_size > *d_bufferThres + processed) && !d_inModelCreation) {
2571  processBuffer();
2572  }
2573  } else {
2574  IF_DEBUG(debugger.counter("arith IS_INTEGER")++;)
2575  if (!isInteger(expr[0])) {
2577  }
2578  }
2579  }
2580  }
2581  else {
2582  IF_DEBUG(debugger.counter("[arith] received t1=t2")++;)
2583 
2584 // const Expr lhs = e.getExpr()[0];
2585 // const Expr rhs = e.getExpr()[1];
2586 //
2587 // CDMap<Expr, Rational>::iterator l_bound_find = termLowerBound[lhs];
2588 // if (l_bound_find != termLowerBound.end()) {
2589 // Rational lhs_bound = (*l_bound_find).second;
2590 // CDMap<Expr, Rational>::iterator l_bound_find_rhs = termLowerBound[rhs];
2591 // if (l_bound_find_rhs != termLowerBound.end()) {
2592 //
2593 // } else {
2594 // // Add the new bound for the rhs
2595 // termLowerBound[rhs] = lhs_bound;
2596 // termLowerBoundThm =
2597 // }
2598 //
2599 // }
2600 
2601 
2602  }
2603 }
2604 
2605 
2606 void TheoryArithOld::checkSat(bool fullEffort)
2607 {
2608  // vector<Expr>::const_iterator e;
2609  // vector<Expr>::const_iterator eEnd;
2610  // TODO: convert back to use iterators
2611  TRACE("arith checksat", "checksat(fullEffort = ", fullEffort? "true, modelCreation = " : "false, modelCreation = ", (d_inModelCreation ? "true)" : "false)"));
2612  TRACE("arith ineq", "TheoryArithOld::checkSat(fullEffort=",
2613  fullEffort? "true" : "false", ")");
2614  if (fullEffort) {
2615 
2616  // Process the buffer if necessary
2617  if (!inconsistent())
2618  processBuffer();
2619 
2620  if (!inconsistent()) {
2621  // If in model creation we might have to reconsider some of the dis-equalities
2622  if (d_inModelCreation) d_diseqIdx = 0;
2623 
2624  // Now go and try to split
2625  for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
2626 
2627  // Get the disequality theorem and the expression
2628  Theorem diseqThm = d_diseq[d_diseqIdx];
2629  Expr diseq = diseqThm.getExpr();
2630 
2631  // If we split on this one already
2632  if (diseqSplitAlready.find(diseq) != diseqSplitAlready.end()) {
2633  TRACE("arith::unconstrained", "checking disequaliy: ", diseq[0] , " already split");
2634  continue;
2635  }
2636 
2637  // Get the equality
2638  Expr eq = diseq[0];
2639 
2640  // Get the left-hand-side and the right-hands side
2641  Expr lhs = eq[0];
2642  Expr rhs = eq[1];
2643  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , "");
2644  DebugAssert(lhs.hasFind() && rhs.hasFind(), "Part of dis-equality has no find!");
2645  lhs = find(lhs).getRHS();
2646  rhs = find(rhs).getRHS();
2647  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " after find");
2648 
2649  // If the value of the equality is already determined by instantiation, we just skip it
2650  // This can happen a lot as we infer equalities in difference logic
2651  if (lhs.isRational() && rhs.isRational()) {
2652  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " skipping");
2653  continue;
2654  }
2655 
2656  // We can allow ourselfs not to care about specific values if we are
2657  // not in model creation or it's not an integer constraint
2658  if (!d_inModelCreation) {
2659  bool unconstrained = isUnconstrained(lhs) || isUnconstrained(rhs);
2660  if (unconstrained) {
2661  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " unconstrained skipping");
2662  continue;
2663  }
2664  bool intConstraint = !isIntegerThm(lhs).isNull() && !isIntegerThm(rhs).isNull();
2665  if (!intConstraint) {
2666  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " not integer skipping");
2667  continue;
2668  }
2669  }
2670 
2671  TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " splitting");
2672 
2673  // We don't know the value of the disequality, split on it (for now)
2674  Theorem lemma = d_rules->diseqToIneq(diseqThm);
2675 
2676  // Enqueue it
2677  enqueueFact(lemma);
2678 
2679  // Mark it as split already
2680  diseqSplitAlready[diseq] = true;
2681  }
2682  }
2683 
2684  IF_DEBUG(
2685  {
2686  bool dejans_printouts = false;
2687  if (dejans_printouts) {
2688  cerr << "Disequalities after CheckSat" << endl;
2689  for (unsigned i = 0; i < d_diseq.size(); i ++) {
2690  Expr diseq = d_diseq[i].getExpr();
2691  Expr d_find = find(diseq[0]).getRHS();
2692  cerr << diseq.toString() << ":" << d_find.toString() << endl;
2693  }
2694  cerr << "Arith Buffer after CheckSat (0)" << endl;
2695  for (unsigned i = 0; i < d_buffer_0.size(); i ++) {
2696  Expr ineq = d_buffer_0[i].getExpr();
2697  Expr rhs = find(ineq[1]).getRHS();
2698  cerr << ineq.toString() << ":" << rhs.toString() << endl;
2699  }
2700  cerr << "Arith Buffer after CheckSat (1)" << endl;
2701  for (unsigned i = 0; i < d_buffer_1.size(); i ++) {
2702  Expr ineq = d_buffer_1[i].getExpr();
2703  Expr rhs = find(ineq[1]).getRHS();
2704  cerr << ineq.toString() << ":" << rhs.toString() << endl;
2705  }
2706  cerr << "Arith Buffer after CheckSat (2)" << endl;
2707  for (unsigned i = 0; i < d_buffer_2.size(); i ++) {
2708  Expr ineq = d_buffer_2[i].getExpr();
2709  Expr rhs = find(ineq[1]).getRHS();
2710  cerr << ineq.toString() << ":" << rhs.toString() << endl;
2711  }
2712  cerr << "Arith Buffer after CheckSat (3)" << endl;
2713  for (unsigned i = 0; i < d_buffer_3.size(); i ++) {
2714  Expr ineq = d_buffer_3[i].getExpr();
2715  Expr rhs = find(ineq[1]).getRHS();
2716  cerr << ineq.toString() << ":" << rhs.toString() << endl;
2717  }
2718  }
2719  }
2720  )
2721  }
2722 }
2723 
2724 
2725 
2727 {
2728  d_inModelCreation = true;
2729  TRACE("model", "refineCounterExample[TheoryArithOld] ", "", "{");
2731  iend = d_sharedTerms.end();
2732  // Add equalities over all pairs of shared terms as suggested
2733  // splitters. Notice, that we want to split on equality
2734  // (positively) first, to reduce the size of the model.
2735  for(; it!=iend; ++it) {
2736  // Copy by value: the elements in the pair from *it are NOT refs in CDMap
2737  Expr e1 = (*it).first;
2738  for(it2 = it, ++it2; it2!=iend; ++it2) {
2739  Expr e2 = (*it2).first;
2741  "TheoryArithOld::refineCounterExample: e1 = "+e1.toString()
2742  +"\n type(e1) = "+e1.getType().toString());
2743  if(findExpr(e1) != findExpr(e2)) {
2745  "TheoryArithOld::refineCounterExample: e2 = "+e2.toString()
2746  +"\n type(e2) = "+e2.getType().toString());
2747  Expr eq = simplifyExpr(e1.eqExpr(e2));
2748  if (!eq.isBoolConst()) {
2749  addSplitter(eq);
2750  }
2751  }
2752  }
2753  }
2754  TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
2755 }
2756 
2757 
2758 void
2759 TheoryArithOld::findRationalBound(const Expr& varSide, const Expr& ratSide,
2760  const Expr& var,
2761  Rational &r)
2762 {
2763  Expr c, x;
2764  separateMonomial(varSide, c, x);
2765 
2766  if (!findExpr(ratSide).isRational() && isNonlinearEq(ratSide.eqExpr(rat(0))))
2767  throw ArithException("Could not generate the model due to non-linear arithmetic");
2768 
2770  "seperateMonomial failed");
2771  DebugAssert(findExpr(ratSide).isRational(),
2772  "smallest variable in graph, should not have variables"
2773  " in inequalities: ");
2774  DebugAssert(x == var, "separateMonomial found different variable: "
2775  + var.toString());
2776  r = findExpr(ratSide).getRational() / findExpr(c).getRational();
2777 }
2778 
2779 bool
2781 {
2782  bool strictLB=false, strictUB=false;
2783  bool right = (d_inequalitiesRightDB.count(e) > 0
2784  && d_inequalitiesRightDB[e]->size() > 0);
2785  bool left = (d_inequalitiesLeftDB.count(e) > 0
2786  && d_inequalitiesLeftDB[e]->size() > 0);
2787  int numRight = 0, numLeft = 0;
2788  if(right) { //rationals less than e
2789  CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
2790  for(unsigned int i=0; i<ratsLTe->size(); i++) {
2791  DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
2792  Expr ineq = (*ratsLTe)[i].ineq().getExpr();
2793  Expr leftSide = ineq[0], rightSide = ineq[1];
2794  Rational r;
2795  findRationalBound(rightSide, leftSide, e , r);
2796  if(numRight==0 || r>glb){
2797  glb = r;
2798  strictLB = isLT(ineq);
2799  }
2800  numRight++;
2801  }
2802  TRACE("model", " =>Lower bound ", glb.toString(), "");
2803  }
2804  if(left) { //rationals greater than e
2805  CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
2806  for(unsigned int i=0; i<ratsGTe->size(); i++) {
2807  DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
2808  Expr ineq = (*ratsGTe)[i].ineq().getExpr();
2809  Expr leftSide = ineq[0], rightSide = ineq[1];
2810  Rational r;
2811  findRationalBound(leftSide, rightSide, e, r);
2812  if(numLeft==0 || r<lub) {
2813  lub = r;
2814  strictUB = isLT(ineq);
2815  }
2816  numLeft++;
2817  }
2818  TRACE("model", " =>Upper bound ", lub.toString(), "");
2819  }
2820  if(!left && !right) {
2821  lub = 0;
2822  glb = 0;
2823  }
2824  if(!left && right) {lub = glb +2;}
2825  if(!right && left) {glb = lub-2;}
2826  DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
2827  "than least upper bound");
2828  return strictLB;
2829 }
2830 
2831 void TheoryArithOld::assignVariables(std::vector<Expr>&v)
2832 {
2833  int count = 0;
2834 
2835  if (diffLogicOnly)
2836  {
2837  // Compute the model
2839  // Get values for the variables
2840  for (unsigned i = 0; i < v.size(); i ++) {
2841  Expr x = v[i];
2843  }
2844  // Done
2845  return;
2846  }
2847 
2848  while (v.size() > 0)
2849  {
2850  std::vector<Expr> bottom;
2851  d_graph.selectSmallest(v, bottom);
2852  TRACE("model", "Finding variables to assign. Iteration # ", count, "");
2853  for(unsigned int i = 0; i<bottom.size(); i++)
2854  {
2855  Expr e = bottom[i];
2856  TRACE("model", "Found: ", e, "");
2857  // Check if it is already a concrete constant
2858  if(e.isRational()) continue;
2859 
2860  Rational lub, glb;
2861  bool strictLB;
2862  strictLB = findBounds(e, lub, glb);
2863  Rational mid;
2864  if(isInteger(e)) {
2865  if(strictLB && glb.isInteger())
2866  mid = glb + 1;
2867  else
2868  mid = ceil(glb);
2869  }
2870  else
2871  mid = (lub + glb)/2;
2872 
2873  TRACE("model", "Assigning mid = ", mid, " {");
2874  assignValue(e, rat(mid));
2875  TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
2876  if(inconsistent()) return; // Punt immediately if failed
2877  }
2878  count++;
2879  }
2880 }
2881 
2882 void TheoryArithOld::computeModelBasic(const std::vector<Expr>& v)
2883 {
2884  d_inModelCreation = true;
2885  vector<Expr> reps;
2886  TRACE("model", "Arith=>computeModel ", "", "{");
2887  for(unsigned int i=0; i <v.size(); ++i) {
2888  const Expr& e = v[i];
2889  if(findExpr(e) == e) {
2890  TRACE("model", "arith variable:", e , "");
2891  reps.push_back(e);
2892  }
2893  else {
2894  TRACE("model", "arith variable:", e , "");
2895  TRACE("model", " ==> is defined by: ", findExpr(e) , "");
2896  }
2897  }
2898  assignVariables(reps);
2899  TRACE("model", "Arith=>computeModel", "", "}");
2900  d_inModelCreation = false;
2901 }
2902 
2903 // For any arith expression 'e', if the subexpressions are assigned
2904 // concrete values, then find(e) must already be a concrete value.
2905 void TheoryArithOld::computeModel(const Expr& e, vector<Expr>& vars) {
2906  DebugAssert(findExpr(e).isRational(), "TheoryArithOld::computeModel("
2907  +e.toString()+")\n e is not assigned concrete value.\n"
2908  +" find(e) = "+findExpr(e).toString());
2909  assignValue(simplify(e));
2910  vars.push_back(e);
2911 }
2912 
2914 
2915  // Check if this is a rewrite theorem
2916  bool rewrite = thm.isRewrite();
2917 
2918  // If it's an integer theorem, then rafine it to integer domain
2919  Expr eq = (rewrite ? thm.getRHS() : thm.getExpr());
2920 
2921  TRACE("arith rafine", "TheoryArithOld::checkIntegerEquality(", eq, ")");
2922  DebugAssert(eq.getKind() == EQ, "checkIntegerEquality: must be an equality");
2923 
2924  // Trivial equalities, we don't care
2925  if (!isPlus(eq[1]) && !isPlus(eq[0])) return thm;
2926  Expr old_sum = (isPlus(eq[1]) ? eq[1] : eq[0]);
2927 
2928  // Get the sum part
2929  vector<Expr> children;
2930  bool const_is_integer = true; // Assuming only one constant is present (canon called before this)
2931  for (int i = 0; i < old_sum.arity(); i ++)
2932  if (!old_sum[i].isRational())
2933  children.push_back(old_sum[i]);
2934  else
2935  const_is_integer = old_sum[i].getRational().isInteger();
2936 
2937  // If the constants are integers, we don't care
2938  if (const_is_integer) return thm;
2939 
2940  Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]);
2941  // Check for integer of the remainder of the sum
2942  Theorem isIntegerEquality = isIntegerThm(sum);
2943  // If it is an integer, it's unsat
2944  if (!isIntegerEquality.isNull()) {
2945  Theorem false_thm = d_rules->intEqualityRationalConstant(isIntegerEquality, eq);
2946  if (rewrite) return transitivityRule(thm, false_thm);
2947  else return iffMP(thm, false_thm);
2948  }
2949  else return thm;
2950 }
2951 
2952 
2954 
2955  // Check if this is a rewrite theorem
2956  bool rewrite = thm.isRewrite();
2957 
2958  // If it's an integer theorem, then rafine it to integer domain
2959  Expr ineq = (rewrite ? thm.getRHS() : thm.getExpr());
2960 
2961  TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger(", ineq, ")");
2962  DebugAssert(isIneq(ineq), "rafineInequalityToInteger: must be an inequality");
2963 
2964  // Trivial inequalities are rafined
2965  // if (!isPlus(ineq[1])) return thm;
2966 
2967  // Get the sum part
2968  vector<Expr> children;
2969  if (isPlus(ineq[1])) {
2970  for (int i = 0; i < ineq[1].arity(); i ++)
2971  if (!ineq[1][i].isRational())
2972  children.push_back(ineq[1][i]);
2973  } else children.push_back(ineq[1]);
2974 
2975  Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]);
2976  // Check for integer of the remainder of the sum
2977  Theorem isIntegerInequality = isIntegerThm(sum);
2978  // If it is an integer, do rafine it
2979  if (!isIntegerInequality.isNull()) {
2980  Theorem rafine = d_rules->rafineStrictInteger(isIntegerInequality, ineq);
2981  TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger()", "=>", rafine.getRHS());
2982  if (rewrite) return canonPredEquiv(transitivityRule(thm, rafine));
2983  else return canonPred(iffMP(thm, rafine));
2984  }
2985  else return thm;
2986 }
2987 
2988 
2989 
2990 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
2991  * and returns a theorem to that effect. assumes e is non-trivial
2992  * i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
2993  */
2995  //e is an eqn or ineqn. e is not a trivial eqn or ineqn
2996  //trivial means 0 = const or 0 <= const.
2997  TRACE("arith normalize", "normalize(", e, ") {");
2998  DebugAssert(e.isEq() || isIneq(e),
2999  "normalize: input must be Eq or Ineq: " + e.toString());
3000  DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
3001  "normalize: if (e is ineq) then e[0] must be 0" +
3002  e.toString());
3003  if(e.isEq()) {
3004  if(e[0].isRational()) {
3005  DebugAssert(0 == e[0].getRational(),
3006  "normalize: if e is Eq and e[0] is rat then e[0]==0");
3007  }
3008  else {
3009  //if e[0] is not rational then e[1] must be rational.
3010  DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
3011  "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
3012  " e = "+e.toString());
3013  }
3014  }
3015 
3016  Expr factor;
3017  if(e[0].isRational())
3018  factor = computeNormalFactor(e[1], false);
3019  else
3020  factor = computeNormalFactor(e[0], false);
3021 
3022  TRACE("arith normalize", "normalize: factor = ", factor, "");
3023  DebugAssert(factor.getRational() > 0,
3024  "normalize: factor="+ factor.toString());
3025 
3026  Theorem thm(reflexivityRule(e));
3027  // Now multiply the equality by the factor, unless it is 1
3028  if(factor.getRational() != 1) {
3029  int kind = e.getKind();
3030  switch(kind) {
3031  case EQ:
3032  //TODO: DEJAN FIX
3033  thm = d_rules->multEqn(e[0], e[1], factor);
3034  // And canonize the result
3035  thm = canonPredEquiv(thm);
3036 
3037  // If this is an equation of the form 0 = c + sum, c is not integer, but sum is
3038  // then equation has no solutions
3039  thm = checkIntegerEquality(thm);
3040 
3041  break;
3042  case LE:
3043  case LT:
3044  case GE:
3045  case GT: {
3046  thm = d_rules->multIneqn(e, factor);
3047  // And canonize the result
3048  thm = canonPredEquiv(thm);
3049  // Try to rafine to integer domain
3050  thm = rafineInequalityToInteger(thm);
3051  break;
3052  }
3053 
3054  default:
3055  // MS .net doesn't accept "..." + int
3056  ostringstream ss;
3057  ss << "normalize: control should not reach here " << kind;
3058  DebugAssert(false, ss.str());
3059  break;
3060  }
3061  } else
3062  if (e.getKind() == EQ)
3063  thm = checkIntegerEquality(thm);
3064 
3065  TRACE("arith normalize", "normalize => ", thm, " }");
3066  return(thm);
3067 }
3068 
3069 
3071  if (eIffEqn.isRewrite()) return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
3072  else return iffMP(eIffEqn, normalize(eIffEqn.getExpr()));
3073 }
3074 
3075 
3077 {
3078  DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
3079  TRACE("arith", "TheoryArithOld::rewrite(", e, ") {");
3080  Theorem thm;
3081  if (!e.isTerm()) {
3082  if (!e.isAbsLiteral()) {
3083  if (e.isPropAtom() && leavesAreNumConst(e)) {
3084  if (e.getSize() < 200) {
3085  Expr eNew = e;
3086  thm = reflexivityRule(eNew);
3087  while (eNew.containsTermITE()) {
3088  thm = transitivityRule(thm, getCommonRules()->liftOneITE(eNew));
3089  DebugAssert(!thm.isRefl(), "Expected non-reflexive");
3090  thm = transitivityRule(thm, theoryCore()->getCoreRules()->rewriteIteCond(thm.getRHS()));
3091  thm = transitivityRule(thm, simplify(thm.getRHS()));
3092  eNew = thm.getRHS();
3093  }
3094  }
3095  else {
3096  thm = d_rules->rewriteLeavesConst(e);
3097  if (thm.isRefl()) {
3098  e.setRewriteNormal();
3099  }
3100  else {
3101  thm = transitivityRule(thm, simplify(thm.getRHS()));
3102  }
3103  }
3104 // if (!thm.getRHS().isBoolConst()) {
3105 // e.setRewriteNormal();
3106 // thm = reflexivityRule(e);
3107 // }
3108  }
3109  else {
3110  e.setRewriteNormal();
3111  thm = reflexivityRule(e);
3112  }
3113  TRACE("arith", "TheoryArithOld::rewrite[non-literal] => ", thm, " }");
3114  return thm;
3115  }
3116  switch(e.getKind()) {
3117  case EQ:
3118  {
3119  // canonical form for an equality of two leaves
3120  // is just l == r instead of 0 + (-1 * l) + r = 0.
3121  if (isLeaf(e[0]) && isLeaf(e[1]))
3122  thm = reflexivityRule(e);
3123  else { // Otherwise, it is "lhs = 0"
3124  //first convert e to the form 0=e'
3125  if((e[0].isRational() && e[0].getRational() == 0)
3126  || (e[1].isRational() && e[1].getRational() == 0))
3127  //already in 0=e' or e'=0 form
3128  thm = reflexivityRule(e);
3129  else {
3130  thm = d_rules->rightMinusLeft(e);
3131  thm = canonPredEquiv(thm);
3132  }
3133  // Check for trivial equation
3134  if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
3135  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
3136  } else {
3137  //else equation is non-trivial
3138  thm = normalize(thm);
3139  // Normalization may yield non-simplified terms
3140  if (!thm.getRHS().isBoolConst())
3141  thm = canonPredEquiv(thm);
3142  }
3143  }
3144 
3145  // Equations must be oriented such that lhs >= rhs as Exprs;
3146  // this ordering is given by operator<(Expr,Expr).
3147  const Expr& eq = thm.getRHS();
3148  if(eq.isEq() && eq[0] < eq[1])
3150 
3151  // Check if the equation is nonlinear
3152  Expr nonlinearEq = thm.getRHS();
3153  if (nonlinearEq.isEq() && isNonlinearEq(nonlinearEq)) {
3154 
3155  TRACE("arith nonlinear", "nonlinear eq rewrite: ", nonlinearEq, "");
3156 
3157  Expr left = nonlinearEq[0];
3158  Expr right = nonlinearEq[1];
3159 
3160  // Check for multiplicative equations, i.e. x*y = 0
3161  if (isNonlinearSumTerm(left) && right.isRational() && right.getRational() == 0) {
3162  Theorem eq_thm = d_rules->multEqZero(nonlinearEq);
3163  thm = transitivityRule(thm, eq_thm);
3164  thm = transitivityRule(thm, theoryCore()->simplify(thm.getRHS()));
3165  break;
3166  }
3167 
3168  // Heuristics for a sum
3169  if (isPlus(left)) {
3170 
3171  // Search for common factor
3172  if (left[0].getRational() == 0) {
3173  Expr::iterator i = left.begin(), iend = left.end();
3174  ++ i;
3175  set<Expr> factors;
3176  set<Expr>::iterator is, isend;
3177  getFactors(*i, factors);
3178  for (++i; i != iend; ++i) {
3179  set<Expr> factors2;
3180  getFactors(*i, factors2);
3181  for (is = factors.begin(), isend = factors.end(); is != isend;) {
3182  if (factors2.find(*is) == factors2.end()) {
3183  factors.erase(is ++);
3184  } else
3185  ++ is;
3186  }
3187  if (factors.empty()) break;
3188  }
3189  if (!factors.empty()) {
3190  thm = transitivityRule(thm, d_rules->divideEqnNonConst(left, rat(0), *(factors.begin())));
3191  // got (factor != 0) OR (left / factor = right / factor), need to simplify
3192  thm = transitivityRule(thm, simplify(thm.getRHS()));
3193  TRACE("arith nonlinear", "nonlinear eq rewrite (factoring): ", thm.getRHS(), "");
3194  break;
3195  }
3196  }
3197 
3198  // Look for equal powers (eq in the form of c + pow1 - pow2 = 0)
3199  Rational constant;
3200  Expr power1;
3201  Expr power2;
3202  if (isPowersEquality(nonlinearEq, power1, power2)) {
3203  // Eliminate the powers
3204  thm = transitivityRule(thm, d_rules->elimPower(nonlinearEq));
3205  thm = transitivityRule(thm, simplify(thm.getRHS()));
3206  TRACE("arith nonlinear", "nonlinear eq rewrite (equal powers): ", thm.getRHS(), "");
3207  break;
3208  } else
3209  // Look for one power equality (c - pow = 0);
3210  if (isPowerEquality(nonlinearEq, constant, power1)) {
3211  Rational pow1 = power1[0].getRational();
3212  if (pow1 % 2 == 0 && constant < 0) {
3213  thm = transitivityRule(thm, d_rules->evenPowerEqNegConst(nonlinearEq));
3214  TRACE("arith nonlinear", "nonlinear eq rewrite (even power = negative): ", thm.getRHS(), "");
3215  break;
3216  }
3217  DebugAssert(constant != 0, "Expected nonzero const");
3218  Rational root = ratRoot(constant, pow1.getUnsigned());
3219  if (root != 0) {
3220  thm = transitivityRule(thm, d_rules->elimPowerConst(nonlinearEq, root));
3221  thm = transitivityRule(thm, simplify(thm.getRHS()));
3222  TRACE("arith nonlinear", "nonlinear eq rewrite (rational root): ", thm.getRHS(), "");
3223  break;
3224  } else {
3225  Theorem isIntPower(isIntegerThm(left));
3226  if (!isIntPower.isNull()) {
3227  thm = transitivityRule(thm, d_rules->intEqIrrational(nonlinearEq, isIntPower));
3228  TRACE("arith nonlinear", "nonlinear eq rewrite (irational root): ", thm.getRHS(), "");
3229  break;
3230  }
3231  }
3232  }
3233  }
3234 
3235  // Non-solvable nonlinear equations are rewritten as conjunction of inequalities
3236  if ( (nonlinearEq[0].arity() > 1 && !canPickEqMonomial(nonlinearEq[0])) ||
3237  (nonlinearEq[1].arity() > 1 && !canPickEqMonomial(nonlinearEq[1])) ) {
3238  thm = transitivityRule(thm, d_rules->eqToIneq(nonlinearEq));
3239  thm = transitivityRule(thm, simplify(thm.getRHS()));
3240  TRACE("arith nonlinear", "nonlinear eq rewrite (not solvable): ", thm.getRHS(), "");
3241  break;
3242  }
3243  }
3244  }
3245  break;
3246  case GRAY_SHADOW:
3247  case DARK_SHADOW:
3248  thm = reflexivityRule(e);
3249  break;
3250  case IS_INTEGER: {
3251  Theorem res(isIntegerDerive(e, typePred(e[0])));
3252  if(!res.isNull())
3253  thm = getCommonRules()->iffTrue(res);
3254  else
3255  thm = reflexivityRule(e);
3256  break;
3257  }
3258  case NOT:
3259  if (!isIneq(e[0]))
3260  //in this case we have "NOT of DARK or GRAY_SHADOW."
3261  thm = reflexivityRule(e);
3262  else {
3263  //In this case we have the "NOT of ineq". get rid of NOT
3264  //and then treat like an ineq
3265  thm = d_rules->negatedInequality(e);
3266  DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
3267  "Expected GE or GT");
3268  thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
3269  thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
3270  thm = canonPredEquiv(thm);
3271 
3272  // If the inequality is strict and integer, change it to non-strict
3273  Expr theIneq = thm.getRHS();
3274  if(isLT(theIneq)) {
3275  // Check if integer
3276  Theorem isIntLHS(isIntegerThm(theIneq[0]));
3277  Theorem isIntRHS(isIntegerThm(theIneq[1]));
3278  bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
3279  if (isInt) {
3280  thm = canonPredEquiv(
3281  transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true)));
3282  }
3283  }
3284 
3285  // Check for trivial inequation
3286  if ((thm.getRHS())[1].isRational())
3287  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
3288  else {
3289  //else ineq is non-trivial
3290  thm = normalize(thm);
3291  // Normalization may yield non-simplified terms
3292  thm = canonPredEquiv(thm);
3293  }
3294  }
3295  break;
3296  case LT:
3297  case GT:
3298  case LE:
3299  case GE: {
3300 
3301  if (isGE(e) || isGT(e)) {
3302  thm = d_rules->flipInequality(e);
3303  thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
3304  }
3305  else
3306  thm = d_rules->rightMinusLeft(e);
3307 
3308  thm = canonPredEquiv(thm);
3309 
3310  // If the inequality is strict and integer, change it to non-strict
3311  Expr theIneq = thm.getRHS();
3312  if(isLT(theIneq)) {
3313  // Check if integer
3314  Theorem isIntLHS(isIntegerThm(theIneq[0]));
3315  Theorem isIntRHS(isIntegerThm(theIneq[1]));
3316  bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
3317  if (isInt) {
3318  thm = canonPredEquiv(
3319  transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true)));
3320  }
3321  }
3322 
3323  // Check for trivial inequation
3324  if ((thm.getRHS())[1].isRational())
3325  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
3326  else { // ineq is non-trivial
3327  thm = normalize(thm);
3328  thm = canonPredEquiv(thm);
3329  if (thm.getRHS()[1].isRational())
3330  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
3331  }
3332  break;
3333  }
3334  default:
3335  DebugAssert(false,
3336  "Theory_Arith::rewrite: control should not reach here");
3337  break;
3338  }
3339  }
3340  else {
3341  if (e.isAtomic())
3342  thm = canon(e);
3343  else
3344  thm = reflexivityRule(e);
3345  }
3346  // TODO: this needs to be reviewed, esp for non-linear case
3347  // Arith canonization is idempotent
3348  if (theoryOf(thm.getRHS()) == this)
3349  thm.getRHS().setRewriteNormal();
3350  TRACE("arith", "TheoryArithOld::rewrite => ", thm, " }");
3351  return thm;
3352 }
3353 
3354 
3356 {
3357  if (!e.isTerm()) {
3358  if (e.isNot()) return;
3359  // if(e.getKind() == IS_INTEGER) {
3360  // e[0].addToNotify(this, e);
3361  // return;
3362  // }
3363  if (isIneq(e)) {
3364  DebugAssert((isLT(e)||isLE(e)) &&
3365  e[0].isRational() && e[0].getRational() == 0,
3366  "TheoryArithOld::setup: expected 0 < rhs:" + e.toString());
3367  e[1].addToNotify(this, e);
3368  } else {
3369 // if (e.isEq()) {
3370 // // Nonlinear solved equations
3371 // if (isNonlinearEq(e) && e[0].isRational() && e[0].getRational() == 0)
3372 // e[0].addToNotify(this, e);
3373 // }
3374 //
3375 // DebugAssert(isGrayShadow(e), "TheoryArithOld::setup: expected grayshadow" + e.toString());
3376 //
3377 // // Do not add the variable, just the subterm e[0].addToNotify(this, e);
3378 // e[1].addToNotify(this, e);
3379  }
3380  return;
3381  }
3382  int k(0), ar(e.arity());
3383  for ( ; k < ar; ++k) {
3384  e[k].addToNotify(this, e);
3385  TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
3386  }
3387 }
3388 
3389 
3390 void TheoryArithOld::update(const Theorem& e, const Expr& d)
3391 {
3392  TRACE("arith update", "update on " + d.toString() + " with ", e.getRHS().toString(), ".");
3393 
3394  if (inconsistent()) return;
3395 
3396  // We accept atoms without find, but only inequalities (they come from the buffer)
3397  DebugAssert(d.hasFind() || isIneq(d), "update on a non-inequality term/atom");
3398 
3399  IF_DEBUG(debugger.counter("arith update total")++;)
3400 // if (isGrayShadow(d)) {
3401 // TRACE("shadow update", "updating index of " + d.toString() + " with ", e.getRHS().toString(), ".");
3402 //
3403 // // Substitute e[1] for e[0] in d and enqueue new shadow
3404 // DebugAssert(e.getLHS() == d[1], "Mismatch");
3405 // Theorem thm = find(d);
3406 //
3407 // // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
3408 // vector<unsigned> changed;
3409 // vector<Theorem> children;
3410 // changed.push_back(1);
3411 // children.push_back(e);
3412 // Theorem thm2 = substitutivityRule(d, changed, children);
3413 // if (thm.getRHS() == trueExpr()) {
3414 // enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
3415 // }
3416 // else {
3417 // enqueueFact(getCommonRules()->iffFalseElim(
3418 // transitivityRule(symmetryRule(thm2), thm)));
3419 // }
3420 // IF_DEBUG(debugger.counter("arith update ineq")++;)
3421 // }
3422 // else
3423  if (isIneq(d)) {
3424 
3425  // Substitute e[1] for e[0] in d and enqueue new inequality
3426  DebugAssert(e.getLHS() == d[1], "Mismatch");
3427  Theorem thm;
3428  if (d.hasFind()) thm = find(d);
3429 
3430 // bool diff_logic = false;
3431 // Expr new_rhs = e.getRHS();
3432 // if (!isPlus(new_rhs)) {
3433 // if (isLeaf(new_rhs)) diff_logic = true;
3434 // }
3435 // else {
3436 // int arity = new_rhs.arity();
3437 // if (arity == 2) {
3438 // if (new_rhs[0].isRational()) diff_logic = true;
3439 // else {
3440 // Expr ax = new_rhs[0], a, x;
3441 // Expr by = new_rhs[1], b, y;
3442 // separateMonomial(ax, a, x);
3443 // separateMonomial(by, b, y);
3444 // if ((a.getRational() == 1 && b.getRational() == -1) ||
3445 // (a.getRational() == -1 && b.getRational() == 1))
3446 // diff_logic = true;
3447 // }
3448 // } else {
3449 // if (arity == 3 && new_rhs[0].isRational()) {
3450 // Expr ax = new_rhs[1], a, x;
3451 // Expr by = new_rhs[2], b, y;
3452 // separateMonomial(ax, a, x);
3453 // separateMonomial(by, b, y);
3454 // if ((a.getRational() == 1 && b.getRational() == -1) ||
3455 // (a.getRational() == -1 && b.getRational() == 1))
3456 // diff_logic = true;
3457 // }
3458 // }
3459 // }
3460 
3461  // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
3462  vector<unsigned> changed;
3463  vector<Theorem> children;
3464  changed.push_back(1);
3465  children.push_back(e);
3466  Theorem thm2 = substitutivityRule(d, changed, children);
3467  Expr newIneq = thm2.getRHS();
3468 
3469  // If this inequality is bufferred but not yet projected, just wait for it
3470  // but don't add the find to the buffer as it will be projected as a find
3471  // We DO want it to pass through all the buffer stuff but NOT get into the buffer
3472  // NOTE: this means that the difference logic WILL get processed
3473  if ((thm.isNull() || thm.getRHS() != falseExpr()) &&
3476  TRACE("arith update", "simplified but not projected : ", thm2.getRHS(), "");
3477  dontBuffer[thm2.getRHS()] = true;
3478  }
3479 
3480  if (thm.isNull()) {
3481  // This hy is in the buffer, not in the core
3482  // if it has been projected, than it's parent has been projected and will get reprojected
3483  // accuratlz. If it has not been projected, we don't care it's still there
3484  TRACE("arith update", "in udpate, but no find", "", "");
3486  if (thm2.getRHS()[1].isRational()) enqueueFact(iffMP(bufferedInequalities[d], thm2));
3487  else if (alreadyProjected.find(d) != alreadyProjected.end()) {
3488  // the parent will get reprojected
3489  alreadyProjected[d] = d;
3490  }
3491  }
3492  }
3493  else if (thm.getRHS() == trueExpr()) {
3494  if (!newIneq[1].isRational() || newIneq[1].getRational() <= 0)
3495  enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
3496  }
3497  else {
3498  enqueueFact(getCommonRules()->iffFalseElim(
3499  transitivityRule(symmetryRule(thm2), thm)));
3500  }
3501  IF_DEBUG(debugger.counter("arith update ineq")++;)
3502  }
3503  else if (d.isEq()) {
3504  TRACE("arith nonlinear", "TheoryArithOld::update() on equality ", d, "");
3505  // We get equalitites from the non-solve nonlinear equations
3506  // only the right hand sides get updated
3507  vector<unsigned> changed;
3508  vector<Theorem> children;
3509  changed.push_back(0);
3510  children.push_back(e);
3511  Theorem thm = substitutivityRule(d, changed, children);
3512  Expr newEq = thm.getRHS();
3513 
3514  Theorem d_find = find(d);
3515  if (d_find.getRHS() == trueExpr()) enqueueFact(iffMP(getCommonRules()->iffTrueElim(d_find), thm));
3516  else enqueueFact(getCommonRules()->iffFalseElim(transitivityRule(symmetryRule(thm), d_find)));
3517  }
3518  else if (d.getKind() == IS_INTEGER) {
3519  // This should only happen if !d has been asserted
3520  DebugAssert(e.getRHS() == findExpr(d[0]), "Unexpected");
3521  if (isInteger(e.getRHS())) {
3522  Theorem thm = substitutivityRule(d, find(d[0]));
3523  thm = transitivityRule(symmetryRule(find(d)), thm);
3524  thm = iffMP(thm, simplify(thm.getExpr()));
3525  setInconsistent(thm);
3526  }
3527  else {
3528  e.getRHS().addToNotify(this, d);
3529  }
3530  }
3531  else if (find(d).getRHS() == d) {
3532 // Theorem thm = canonSimp(d);
3533 // TRACE("arith", "TheoryArithOld::update(): thm = ", thm, "");
3534 // DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
3535 // +thm.getExpr().toString());
3536 // assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
3537 // IF_DEBUG(debugger.counter("arith update find(d)=d")++;)
3538  Theorem thm = simplify(d);
3539  // If the original is was a shared term, add this one as as a shared term also
3541  DebugAssert(thm.getRHS().isAtomic(), "Expected atomic");
3542  assertEqualities(thm);
3543  }
3544 }
3545 
3546 
3548 {
3549  DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
3550  const Expr& lhs = thm.getLHS();
3551  const Expr& rhs = thm.getRHS();
3552 
3553  // Check for already solved equalities.
3554 
3555  // Have to be careful about the types: integer variable cannot be
3556  // assigned a real term. Also, watch for e[0] being a subexpression
3557  // of e[1]: this would create an unsimplifiable expression.
3558  if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
3559  && (!isInteger(lhs) || isInteger(rhs))
3560  // && !e[0].subExprOf(e[1])
3561  )
3562  return thm;
3563 
3564  // Symmetric version is already solved
3565  if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
3566  && (!isInteger(rhs) || isInteger(lhs))
3567  // && !e[1].subExprOf(e[0])
3568  )
3569  return symmetryRule(thm);
3570 
3571  return doSolve(thm);
3572 }
3573 
3574 
3575 void TheoryArithOld::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
3576  switch(e.getKind()) {
3577  case RATIONAL_EXPR: // Skip the constants
3578  break;
3579  case PLUS:
3580  case MULT:
3581  case DIVIDE:
3582  case POW: // This is not a variable; extract the variables from children
3583  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
3584  // getModelTerm(*i, v);
3585  v.push_back(*i);
3586  break;
3587  default: { // Otherwise it's a variable. Check if it has a find pointer
3588  Expr e2(findExpr(e));
3589  if(e==e2) {
3590  TRACE("model", "TheoryArithOld::computeModelTerm(", e, "): a variable");
3591  // Leave it alone (it has no descendants)
3592  // v.push_back(e);
3593  } else {
3594  TRACE("model", "TheoryArithOld::computeModelTerm("+e.toString()
3595  +"): has find pointer to ", e2, "");
3596  v.push_back(e2);
3597  }
3598  }
3599  }
3600 }
3601 
3602 
3604  Expr tExpr = t.getExpr();
3605  switch(tExpr.getKind()) {
3606  case INT:
3607  return Expr(IS_INTEGER, e);
3608  case SUBRANGE: {
3609  std::vector<Expr> kids;
3610  kids.push_back(Expr(IS_INTEGER, e));
3611  kids.push_back(leExpr(tExpr[0], e));
3612  kids.push_back(leExpr(e, tExpr[1]));
3613  return andExpr(kids);
3614  }
3615  default:
3616  return e.getEM()->trueExpr();
3617  }
3618 }
3619 
3620 
3622 {
3623  if (e.isRewrite()) {
3624  DebugAssert(e.getLHS().isTerm(), "Expected equation");
3625  if (isLeaf(e.getLHS())) {
3626  // should be in solved form
3627  DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
3628  "Not in solved form: lhs appears in rhs");
3629  }
3630  else {
3631  DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
3633  "Expected at least one unsimplified leaf on lhs");
3634  }
3635  DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
3636  "Expected canonSimp(rhs) = canonSimp(rhs)");
3637  }
3638  else {
3639  Expr expr = e.getExpr();
3640  if (expr.isFalse()) return;
3641 
3642  vector<Theorem> eqs;
3643  Theorem thm;
3644  int index, index2;
3645 
3646  for (index = 0; index < expr.arity(); ++index) {
3647  thm = getCommonRules()->andElim(e, index);
3648  eqs.push_back(thm);
3649  if (thm.getExpr().isFalse()) return;
3650  DebugAssert(eqs[index].isRewrite() &&
3651  eqs[index].getLHS().isTerm(), "Expected equation");
3652  }
3653 
3654  // Check for solved form
3655  for (index = 0; index < expr.arity(); ++index) {
3656  DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
3657  DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
3658  "Expected canonSimp(rhs) = canonSimp(rhs)");
3659  DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
3660  "Failed recursive canonSimp check");
3661  for (index2 = 0; index2 < expr.arity(); ++index2) {
3662  DebugAssert(index == index2 ||
3663  eqs[index].getLHS() != eqs[index2].getLHS(),
3664  "Not in solved form: repeated lhs");
3665  DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
3666  "Not in solved form: lhs appears in rhs");
3667  }
3668  }
3669  }
3670 }
3671 
3672 
3674 {
3675  switch (e.getKind()) {
3676  case INT:
3677  case REAL:
3678  if (e.arity() > 0) {
3679  throw Exception("Ill-formed arithmetic type: "+e.toString());
3680  }
3681  break;
3682  case SUBRANGE:
3683  if (e.arity() != 2 ||
3684  !isIntegerConst(e[0]) ||
3685  !isIntegerConst(e[1]) ||
3686  e[0].getRational() > e[1].getRational()) {
3687  throw Exception("bad SUBRANGE type expression"+e.toString());
3688  }
3689  break;
3690  default:
3691  DebugAssert(false, "Unexpected kind in TheoryArithOld::checkType"
3692  +getEM()->getKindName(e.getKind()));
3693  }
3694 }
3695 
3696 
3698  bool enumerate, bool computeSize)
3699 {
3700  Cardinality card = CARD_INFINITE;
3701  switch (e.getKind()) {
3702  case SUBRANGE: {
3703  card = CARD_FINITE;
3704  Expr typeExpr = e;
3705  if (enumerate) {
3706  Rational r = typeExpr[0].getRational() + n;
3707  if (r <= typeExpr[1].getRational()) {
3708  e = rat(r);
3709  }
3710  else e = Expr();
3711  }
3712  if (computeSize) {
3713  Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1;
3714  n = r.getUnsigned();
3715  }
3716  break;
3717  }
3718  default:
3719  break;
3720  }
3721  return card;
3722 }
3723 
3724 
3726 {
3727  switch (e.getKind()) {
3728  case REAL_CONST:
3729  e.setType(d_realType);
3730  break;
3731  case RATIONAL_EXPR:
3732  if(e.getRational().isInteger())
3733  e.setType(d_intType);
3734  else
3735  e.setType(d_realType);
3736  break;
3737  case UMINUS:
3738  case PLUS:
3739  case MINUS:
3740  case MULT:
3741  case POW: {
3742  bool isInt = true;
3743  for(int k = 0; k < e.arity(); ++k) {
3744  if(d_realType != getBaseType(e[k]))
3745  throw TypecheckException("Expecting type REAL with `" +
3746  getEM()->getKindName(e.getKind()) + "',\n"+
3747  "but got a " + getBaseType(e[k]).toString()+
3748  " for:\n" + e.toString());
3749  if(isInt && !isInteger(e[k]))
3750  isInt = false;
3751  }
3752  if(isInt)
3753  e.setType(d_intType);
3754  else
3755  e.setType(d_realType);
3756  break;
3757  }
3758  case DIVIDE: {
3759  Expr numerator = e[0];
3760  Expr denominator = e[1];
3761  if (getBaseType(numerator) != d_realType ||
3762  getBaseType(denominator) != d_realType) {
3763  throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
3764  "but got " + getBaseType(numerator).toString()+
3765  " and " + getBaseType(denominator).toString() +
3766  " for:\n" + e.toString());
3767  }
3768  if(denominator.isRational() && 1 == denominator.getRational())
3769  e.setType(numerator.getType());
3770  else
3771  e.setType(d_realType);
3772  break;
3773  }
3774  case LT:
3775  case LE:
3776  case GT:
3777  case GE:
3778  case GRAY_SHADOW:
3779  // Need to know types for all exprs -Clark
3780  // e.setType(boolType());
3781  // break;
3782  case DARK_SHADOW:
3783  for (int k = 0; k < e.arity(); ++k) {
3784  if (d_realType != getBaseType(e[k]))
3785  throw TypecheckException("Expecting type REAL with `" +
3786  getEM()->getKindName(e.getKind()) + "',\n"+
3787  "but got a " + getBaseType(e[k]).toString()+
3788  " for:\n" + e.toString());
3789  }
3790 
3791  e.setType(boolType());
3792  break;
3793  case IS_INTEGER:
3794  if(d_realType != getBaseType(e[0]))
3795  throw TypecheckException("Expected type REAL, but got "
3796  +getBaseType(e[0]).toString()
3797  +"\n\nExpr = "+e.toString());
3798  e.setType(boolType());
3799  break;
3800  default:
3801  DebugAssert(false,"TheoryArithOld::computeType: unexpected expression:\n "
3802  +e.toString());
3803  break;
3804  }
3805 }
3806 
3807 
3809  IF_DEBUG(int kind = t.getExpr().getKind();)
3810  DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
3811  "TheoryArithOld::computeBaseType("+t.toString()+")");
3812  return realType();
3813 }
3814 
3815 
3816 Expr
3818  Expr tcc(Theory::computeTCC(e));
3819  switch(e.getKind()) {
3820  case DIVIDE:
3821  DebugAssert(e.arity() == 2, "");
3822  return tcc.andExpr(!(e[1].eqExpr(rat(0))));
3823  default:
3824  return tcc;
3825  }
3826 }
3827 
3828 ///////////////////////////////////////////////////////////////////////////////
3829 //parseExprOp:
3830 //translating special Exprs to regular EXPR??
3831 ///////////////////////////////////////////////////////////////////////////////
3832 Expr
3834  //TRACE("parser", "TheoryArithOld::parseExprOp(", e, ")");
3835  //std::cout << "Were here";
3836  // If the expression is not a list, it must have been already
3837  // parsed, so just return it as is.
3838  switch(e.getKind()) {
3839  case ID: {
3840  int kind = getEM()->getKind(e[0].getString());
3841  switch(kind) {
3842  case NULL_KIND: return e; // nothing to do
3843  case REAL:
3844  case INT:
3845  case NEGINF:
3846  case POSINF: return getEM()->newLeafExpr(kind);
3847  default:
3848  DebugAssert(false, "Bad use of bare keyword: "+e.toString());
3849  return e;
3850  }
3851  }
3852  case RAW_LIST: break; // break out of switch, do the hard work
3853  default:
3854  return e;
3855  }
3856 
3857  DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
3858  "TheoryArithOld::parseExprOp:\n e = "+e.toString());
3859 
3860  const Expr& c1 = e[0][0];
3861  int kind = getEM()->getKind(c1.getString());
3862  switch(kind) {
3863  case UMINUS: {
3864  if(e.arity() != 2)
3865  throw ParserException("UMINUS requires exactly one argument: "
3866  +e.toString());
3867  return uminusExpr(parseExpr(e[1]));
3868  }
3869  case PLUS: {
3870  vector<Expr> k;
3871  Expr::iterator i = e.begin(), iend=e.end();
3872  // Skip first element of the vector of kids in 'e'.
3873  // The first element is the operator.
3874  ++i;
3875  // Parse the kids of e and push them into the vector 'k'
3876  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
3877  return plusExpr(k);
3878  }
3879  case MINUS: {
3880  if(e.arity() == 2) {
3881  if (false && (getEM()->getInputLang() == SMTLIB_LANG
3882  || getEM()->getInputLang() == SMTLIB_V2_LANG)) {
3883  throw ParserException("Unary Minus should use '~' instead of '-' in SMT-LIB expr:"
3884  +e.toString());
3885  }
3886  else {
3887  return uminusExpr(parseExpr(e[1]));
3888  }
3889  }
3890  else if(e.arity() == 3)
3891  return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
3892  else
3893  throw ParserException("MINUS requires one or two arguments:"
3894  +e.toString());
3895  }
3896  case MULT: {
3897  vector<Expr> k;
3898  Expr::iterator i = e.begin(), iend=e.end();
3899  // Skip first element of the vector of kids in 'e'.
3900  // The first element is the operator.
3901  ++i;
3902  // Parse the kids of e and push them into the vector 'k'
3903  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
3904  return multExpr(k);
3905  }
3906  case POW: {
3907  return powExpr(parseExpr(e[1]), parseExpr(e[2]));
3908  }
3909  case DIVIDE:
3910  { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
3911  case LT:
3912  { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
3913  case LE:
3914  { return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
3915  case GT:
3916  { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
3917  case GE:
3918  { return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
3919  case INTDIV:
3920  case MOD:
3921  case SUBRANGE: {
3922  vector<Expr> k;
3923  Expr::iterator i = e.begin(), iend=e.end();
3924  // Skip first element of the vector of kids in 'e'.
3925  // The first element is the operator.
3926  ++i;
3927  // Parse the kids of e and push them into the vector 'k'
3928  for(; i!=iend; ++i)
3929  k.push_back(parseExpr(*i));
3930  return Expr(kind, k, e.getEM());
3931  }
3932  case IS_INTEGER: {
3933  if(e.arity() != 2)
3934  throw ParserException("IS_INTEGER requires exactly one argument: "
3935  +e.toString());
3936  return Expr(IS_INTEGER, parseExpr(e[1]));
3937  }
3938  default:
3939  DebugAssert(false,
3940  "TheoryArithOld::parseExprOp: invalid input " + e.toString());
3941  break;
3942  }
3943  return e;
3944 }
3945 
3946 ///////////////////////////////////////////////////////////////////////////////
3947 // Pretty-printing //
3948 ///////////////////////////////////////////////////////////////////////////////
3949 
3950 
3951 ExprStream&
3953  switch(os.lang()) {
3954  case SIMPLIFY_LANG:
3955  switch(e.getKind()) {
3956  case RATIONAL_EXPR:
3957  e.print(os);
3958  break;
3959  case SUBRANGE:
3960  os <<"ERROR:SUBRANGE:not supported in Simplify\n";
3961  break;
3962  case IS_INTEGER:
3963  os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
3964  break;
3965  case PLUS: {
3966  int i=0, iend=e.arity();
3967  os << "(+ ";
3968  if(i!=iend) os << e[i];
3969  ++i;
3970  for(; i!=iend; ++i) os << " " << e[i];
3971  os << ")";
3972  break;
3973  }
3974  case MINUS:
3975  os << "(- " << e[0] << " " << e[1]<< ")";
3976  break;
3977  case UMINUS:
3978  os << "-" << e[0] ;
3979  break;
3980  case MULT: {
3981  int i=0, iend=e.arity();
3982  os << "(* " ;
3983  if(i!=iend) os << e[i];
3984  ++i;
3985  for(; i!=iend; ++i) os << " " << e[i];
3986  os << ")";
3987  break;
3988  }
3989  case POW:
3990  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
3991  break;
3992  case DIVIDE:
3993  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
3994  break;
3995  case LT:
3996  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
3997  }
3998  os << "(< " << e[0] << " " << e[1] <<")";
3999  break;
4000  case LE:
4001  os << "(<= " << e[0] << " " << e[1] << ")";
4002  break;
4003  case GT:
4004  os << "(> " << e[0] << " " << e[1] << ")";
4005  break;
4006  case GE:
4007  os << "(>= " << e[0] << " " << e[1] << ")";
4008  break;
4009  case DARK_SHADOW:
4010  case GRAY_SHADOW:
4011  os <<"ERROR:SHADOW:not supported in Simplify\n";
4012  break;
4013  default:
4014  // Print the top node in the default LISP format, continue with
4015  // pretty-printing for children.
4016  e.print(os);
4017 
4018  break;
4019  }
4020  break; // end of case SIMPLIFY_LANG
4021 
4022  case TPTP_LANG:
4023  switch(e.getKind()) {
4024  case RATIONAL_EXPR:
4025  e.print(os);
4026  break;
4027  case SUBRANGE:
4028  os <<"ERROR:SUBRANGE:not supported in TPTP\n";
4029  break;
4030  case IS_INTEGER:
4031  os <<"ERROR:IS_INTEGER:not supported in TPTP\n";
4032  break;
4033  case PLUS: {
4034  if(!isInteger(e[0])){
4035  os<<"ERRPR:plus only supports inteters now in TPTP\n";
4036  break;
4037  }
4038 
4039  int i=0, iend=e.arity();
4040  if(iend <=1){
4041  os<<"ERROR,plus must have more than two numbers in TPTP\n";
4042  break;
4043  }
4044 
4045  for(i=0; i <= iend-2; ++i){
4046  os << "$plus_int(";
4047  os << e[i] << ",";
4048  }
4049 
4050  os<< e[iend-1];
4051 
4052  for(i=0 ; i <= iend-2; ++i){
4053  os << ")";
4054  }
4055 
4056  break;
4057  }
4058  case MINUS:
4059  if(!isInteger(e[0])){
4060  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4061  break;
4062  }
4063 
4064  os << "$minus_int(" << e[0] << "," << e[1]<< ")";
4065  break;
4066  case UMINUS:
4067  if(!isInteger(e[0])){
4068  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4069  break;
4070  }
4071 
4072  os << "$uminus_int(" << e[0] <<")" ;
4073  break;
4074  case MULT: {
4075  if(!isInteger(e[0])){
4076  os<<"ERRPR:times only supports inteters now in TPTP\n";
4077  break;
4078  }
4079 
4080  int i=0, iend=e.arity();
4081  if(iend <=1){
4082  os<<"ERROR:times must have more than two numbers in TPTP\n";
4083  break;
4084  }
4085 
4086  for(i=0; i <= iend-2; ++i){
4087  os << "$times_int(";
4088  os << e[i] << ",";
4089  }
4090 
4091  os<< e[iend-1];
4092 
4093  for(i=0 ; i <= iend-2; ++i){
4094  os << ")";
4095  }
4096 
4097  break;
4098  }
4099  case POW:
4100 
4101  if(!isInteger(e[0])){
4102  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4103  break;
4104  }
4105 
4106  os << "$power_int(" << push << e[1] << space << "^ " << e[0] << push << ")";
4107  break;
4108 
4109  case DIVIDE:
4110  if(!isInteger(e[0])){
4111  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4112  break;
4113  }
4114 
4115  os << "divide_int(" <<e[0] << "," << e[1] << ")";
4116  break;
4117 
4118  case LT:
4119  if(!isInteger(e[0])){
4120  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4121  break;
4122  }
4123  os << "$less_int(" << e[0] << "," << e[1] <<")";
4124  break;
4125 
4126  case LE:
4127  if(!isInteger(e[0])){
4128  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4129  break;
4130  }
4131 
4132  os << "$lesseq_int(" << e[0] << "," << e[1] << ")";
4133  break;
4134 
4135  case GT:
4136  if(!isInteger(e[0])){
4137  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4138  break;
4139  }
4140 
4141  os << "$greater_int(" << e[0] << "," << e[1] << ")";
4142  break;
4143 
4144  case GE:
4145  if(!isInteger(e[0])){
4146  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4147  break;
4148  }
4149 
4150  os << "$greatereq_int(" << e[0] << "," << e[1] << ")";
4151  break;
4152  case DARK_SHADOW:
4153  case GRAY_SHADOW:
4154  os <<"ERROR:SHADOW:not supported in TPTP\n";
4155  break;
4156 
4157  case INT:
4158  os <<"$int";
4159  break;
4160  case REAL:
4161  os <<"ERROR:REAL not supported in TPTP\n";
4162  default:
4163  // Print the top node in the default LISP format, continue with
4164  // pretty-printing for children.
4165  e.print(os);
4166 
4167  break;
4168  }
4169  break; // end of case TPTP_LANG
4170 
4171  case PRESENTATION_LANG:
4172  switch(e.getKind()) {
4173  case REAL:
4174  os << "REAL";
4175  break;
4176  case INT:
4177  os << "INT";
4178  break;
4179  case RATIONAL_EXPR:
4180  e.print(os);
4181  break;
4182  case NEGINF:
4183  os << "NEGINF";
4184  break;
4185  case POSINF:
4186  os << "POSINF";
4187  break;
4188  case SUBRANGE:
4189  if(e.arity() != 2) e.printAST(os);
4190  else
4191  os << "[" << push << e[0] << ".." << e[1] << push << "]";
4192  break;
4193  case IS_INTEGER:
4194  if(e.arity() == 1)
4195  os << "IS_INTEGER(" << push << e[0] << push << ")";
4196  else
4197  e.printAST(os);
4198  break;
4199  case PLUS: {
4200  int i=0, iend=e.arity();
4201  os << "(" << push;
4202  if(i!=iend) os << e[i];
4203  ++i;
4204  for(; i!=iend; ++i) os << space << "+ " << e[i];
4205  os << push << ")";
4206  break;
4207  }
4208  case MINUS:
4209  os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
4210  break;
4211  case UMINUS:
4212  os << "-(" << push << e[0] << push << ")";
4213  break;
4214  case MULT: {
4215  int i=0, iend=e.arity();
4216  os << "(" << push;
4217  if(i!=iend) os << e[i];
4218  ++i;
4219  for(; i!=iend; ++i) os << space << "* " << e[i];
4220  os << push << ")";
4221  break;
4222  }
4223  case POW:
4224  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
4225  break;
4226  case DIVIDE:
4227  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
4228  break;
4229  case LT:
4230  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
4231  }
4232  os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
4233  break;
4234  case LE:
4235  os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
4236  break;
4237  case GT:
4238  os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
4239  break;
4240  case GE:
4241  os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
4242  break;
4243  case DARK_SHADOW:
4244  os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
4245  break;
4246  case GRAY_SHADOW:
4247  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
4248  << "," << space << e[2] << "," << space << e[3] << push << ")";
4249  break;
4250  default:
4251  // Print the top node in the default LISP format, continue with
4252  // pretty-printing for children.
4253  e.printAST(os);
4254 
4255  break;
4256  }
4257  break; // end of case PRESENTATION_LANG
4258  case SPASS_LANG: {
4259  switch(e.getKind()) {
4260  case REAL_CONST:
4261  printRational(os, e[0].getRational(), true);
4262  break;
4263  case RATIONAL_EXPR:
4264  printRational(os, e.getRational());
4265  break;
4266  case REAL:
4267  throw SmtlibException("TheoryArithOld::print: SPASS: REAL not implemented");
4268  break;
4269  case INT:
4270  throw SmtlibException("TheoryArithOld::print: SPASS: INT not implemented");
4271  break;
4272  case SUBRANGE:
4273  throw SmtlibException("TheoryArithOld::print: SPASS: SUBRANGE not implemented");
4274  break;
4275  case IS_INTEGER:
4276  throw SmtlibException("TheoryArithOld::print: SPASS: IS_INTEGER not implemented");
4277  case PLUS: {
4278  int arity = e.arity();
4279  if(2 == arity) {
4280  os << push << "plus("
4281  << e[0] << "," << space << e[1]
4282  << push << ")";
4283  }
4284  else if(2 < arity) {
4285  for (int i = 0 ; i < arity - 2; i++){
4286  os << push << "plus(";
4287  os << e[i] << "," << space;
4288  }
4289  os << push << "plus("
4290  << e[arity - 2] << "," << space << e[arity - 1]
4291  << push << ")";
4292  for (int i = 0 ; i < arity - 2; i++){
4293  os << push << ")";
4294  }
4295  }
4296  else {
4297  throw SmtlibException("TheoryArithOld::print: SPASS: Less than two arguments for plus");
4298  }
4299  break;
4300  }
4301  case MINUS: {
4302  os << push << "plus(" << e[0]
4303  << "," << space << push << "mult(-1,"
4304  << space << e[1] << push << ")" << push << ")";
4305  break;
4306  }
4307  case UMINUS: {
4308  os << push << "plus(0,"
4309  << space << push << "mult(-1,"
4310  << space << e[0] << push << ")" << push << ")";
4311  break;
4312  }
4313  case MULT: {
4314  int arity = e.arity();
4315  if (2 == arity){
4316  os << push << "mult("
4317  << e[0] << "," << space << e[1]
4318  << push << ")";
4319  }
4320  else if (2 < arity){
4321  for (int i = 0 ; i < arity - 2; i++){
4322  os << push << "mult(";
4323  os << e[i] << "," << space;
4324  }
4325  os << push << "mult("
4326  << e[arity - 2] << "," << space << e[arity - 1]
4327  << push << ")";
4328  for (int i = 0 ; i < arity - 2; i++){
4329  os << push << ")";
4330  }
4331  }
4332  else{
4333  throw SmtlibException("TheoryArithOld::print: SPASS: Less than two arguments for mult");
4334  }
4335  break;
4336  }
4337  case POW:
4338  if (e[0].isRational() && e[0].getRational().isInteger()) {
4339  int i=0, iend=e[0].getRational().getInt();
4340  for(; i!=iend; ++i) {
4341  if (i < iend-2) {
4342  os << push << "mult(";
4343  }
4344  os << e[1] << "," << space;
4345  }
4346  os << push << "mult("
4347  << e[1] << "," << space << e[1];
4348  for (i=0; i < iend-1; ++i) {
4349  os << push << ")";
4350  }
4351  }
4352  else {
4353  throw SmtlibException("TheoryArithOld::print: SPASS: POW not supported: " + e.toString(PRESENTATION_LANG));
4354  }
4355  break;
4356  case DIVIDE: {
4357  os << "ERROR "<< endl;break;
4358  throw SmtlibException("TheoryArithOld::print: SPASS: unexpected use of DIVIDE");
4359  break;
4360  }
4361  case LT: {
4362  Rational r;
4363  os << push << "ls(" << space;
4364  os << e[0] << "," << space << e[1] << push << ")";
4365  break;
4366  }
4367  case LE: {
4368  Rational r;
4369  os << push << "le(" << space;
4370  os << e[0] << "," << space << e[1] << push << ")";
4371  break;
4372  }
4373  case GT: {
4374  Rational r;
4375  os << push << "gs(" << space;
4376  os << e[0] << "," << space << e[1] << push << ")";
4377  break;
4378  }
4379  case GE: {
4380  Rational r;
4381  os << push << "ge(" << space;
4382  os << e[0] << "," << space << e[1] << push << ")";
4383  break;
4384  }
4385 
4386  default:
4387  throw SmtlibException("TheoryArithOld::print: SPASS: default not supported");
4388  }
4389  break; // end of case SPASS_LANG
4390  }
4391  case SMTLIB_LANG:
4392  case SMTLIB_V2_LANG: {
4393  switch(e.getKind()) {
4394  case REAL_CONST:
4395  printRational(os, e[0].getRational(), true);
4396  break;
4397  case RATIONAL_EXPR:
4398  printRational(os, e.getRational());
4399  break;
4400  case REAL:
4401  os << "Real";
4402  break;
4403  case INT:
4404  os << "Int";
4405  break;
4406  case SUBRANGE:
4407  throw SmtlibException("TheoryArithOld::print: SMTLIB: SUBRANGE not implemented");
4408 // if(e.arity() != 2) e.print(os);
4409 // else
4410 // os << "(" << push << "SUBRANGE" << space << e[0]
4411 // << space << e[1] << push << ")";
4412  break;
4413  case IS_INTEGER:
4414  if(e.arity() == 1) {
4415  if (os.lang() == SMTLIB_LANG) {
4416  os << "(" << push << "IsInt" << space << e[0] << push << ")";
4417  }
4418  else {
4419  os << "(" << push << "is_int" << space << e[0] << push << ")";
4420  }
4421  }
4422  else
4423  throw SmtlibException("TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly");
4424  break;
4425  case PLUS: {
4426  if(e.arity() == 1 && os.lang() == SMTLIB_V2_LANG) {
4427  os << e[0];
4428  } else {
4429  os << "(" << push << "+";
4430  Expr::iterator i = e.begin(), iend = e.end();
4431  for(; i!=iend; ++i) {
4432  os << space << (*i);
4433  }
4434  os << push << ")";
4435  }
4436  break;
4437  }
4438  case MINUS: {
4439  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
4440  break;
4441  }
4442  case UMINUS: {
4443  if (os.lang() == SMTLIB_LANG) {
4444  os << "(" << push << "~" << space << e[0] << push << ")";
4445  }
4446  else {
4447  os << "(" << push << "-" << space << e[0] << push << ")";
4448  }
4449  break;
4450  }
4451  case MULT: {
4452  int i=0, iend=e.arity();
4453  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
4454  os << e[0];
4455  } else {
4456  for(; i!=iend; ++i) {
4457  if (i < iend-1) {
4458  os << "(" << push << "*";
4459  }
4460  os << space << e[i];
4461  }
4462  for (i=0; i < iend-1; ++i) os << push << ")";
4463  }
4464  break;
4465  }
4466  case POW:
4467  if (e[0].isRational() && e[0].getRational().isInteger()) {
4468  int i=0, iend=e[0].getRational().getInt();
4469  for(; i!=iend; ++i) {
4470  if (i < iend-1) {
4471  os << "(" << push << "*";
4472  }
4473  os << space << e[1];
4474  }
4475  for (i=0; i < iend-1; ++i) os << push << ")";
4476  }
4477  else
4478  throw SmtlibException("TheoryArithOld::print: SMTLIB: POW not supported: " + e.toString(PRESENTATION_LANG));
4479  // os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
4480  break;
4481  case DIVIDE: {
4482  throw SmtlibException("TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE");
4483  break;
4484  }
4485  case LT: {
4486  Rational r;
4487  os << "(" << push << "<" << space;
4488  os << e[0] << space << e[1] << push << ")";
4489  break;
4490  }
4491  case LE: {
4492  Rational r;
4493  os << "(" << push << "<=" << space;
4494  os << e[0] << space << e[1] << push << ")";
4495  break;
4496  }
4497  case GT: {
4498  Rational r;
4499  os << "(" << push << ">" << space;
4500  os << e[0] << space << e[1] << push << ")";
4501  break;
4502  }
4503  case GE: {
4504  Rational r;
4505  os << "(" << push << ">=" << space;
4506  os << e[0] << space << e[1] << push << ")";
4507  break;
4508  }
4509  case DARK_SHADOW:
4510  throw SmtlibException("TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported");
4511  os << "(" << push << "DARK_SHADOW" << space << e[0]
4512  << space << e[1] << push << ")";
4513  break;
4514  case GRAY_SHADOW:
4515  throw SmtlibException("TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported");
4516  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
4517  << "," << space << e[2] << "," << space << e[3] << push << ")";
4518  break;
4519  default:
4520  throw SmtlibException("TheoryArithOld::print: SMTLIB: default not supported");
4521  // Print the top node in the default LISP format, continue with
4522  // pretty-printing for children.
4523  e.printAST(os);
4524 
4525  break;
4526  }
4527  break; // end of case SMTLIB_LANG
4528  }
4529  case LISP_LANG:
4530  switch(e.getKind()) {
4531  case REAL:
4532  case INT:
4533  case RATIONAL_EXPR:
4534  case NEGINF:
4535  case POSINF:
4536  e.print(os);
4537  break;
4538  case SUBRANGE:
4539  if(e.arity() != 2) e.printAST(os);
4540  else
4541  os << "(" << push << "SUBRANGE" << space << e[0]
4542  << space << e[1] << push << ")";
4543  break;
4544  case IS_INTEGER:
4545  if(e.arity() == 1)
4546  os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
4547  else
4548  e.printAST(os);
4549  break;
4550  case PLUS: {
4551  int i=0, iend=e.arity();
4552  os << "(" << push << "+";
4553  for(; i!=iend; ++i) os << space << e[i];
4554  os << push << ")";
4555  break;
4556  }
4557  case MINUS:
4558  //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
4559  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
4560  break;
4561  case UMINUS:
4562  os << "(" << push << "-" << space << e[0] << push << ")";
4563  break;
4564  case MULT: {
4565  int i=0, iend=e.arity();
4566  os << "(" << push << "*";
4567  for(; i!=iend; ++i) os << space << e[i];
4568  os << push << ")";
4569  break;
4570  }
4571  case POW:
4572  os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
4573  break;
4574  case DIVIDE:
4575  os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
4576  break;
4577  case LT:
4578  os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
4579  break;
4580  case LE:
4581  os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
4582  break;
4583  case GT:
4584  os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
4585  break;
4586  case GE:
4587  os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
4588  break;
4589  case DARK_SHADOW:
4590  os << "(" << push << "DARK_SHADOW" << space << e[0]
4591  << space << e[1] << push << ")";
4592  break;
4593  case GRAY_SHADOW:
4594  os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
4595  << e[1] << space << e[2] << space << e[3] << push << ")";
4596  break;
4597  default:
4598  // Print the top node in the default LISP format, continue with
4599  // pretty-printing for children.
4600  e.printAST(os);
4601 
4602  break;
4603  }
4604  break; // end of case LISP_LANG
4605  default:
4606  // Print the top node in the default LISP format, continue with
4607  // pretty-printing for children.
4608  e.printAST(os);
4609  }
4610  return os;
4611 }
4612 
4613 Theorem TheoryArithOld::inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS) {
4614 
4615  // Which side of the inequality
4616  int index = (normalizeRHS ? 1 : 0);
4617 
4618  TRACE("arith find", "inequalityToFind(", int2string(index) + ", " + inequalityThm.getExpr().toString(), ")");
4619 
4620  // Get the inequality expression
4621  const Expr& inequality = inequalityThm.getExpr();
4622 
4623  // The theorem we will return
4624  Theorem inequalityFindThm;
4625 
4626  // If the inequality side has a find
4627  if (inequality[index].hasFind()) {
4628  // Get the find of the rhs (lhs)
4629  Theorem rhsFindThm = inequality[index].getFind();
4630  // Get the theorem simplifys the find (in case the updates haven't updated all the finds yet
4631  // Fixed with d_theroyCore.inUpdate()
4632  rhsFindThm = transitivityRule(rhsFindThm, simplify(rhsFindThm.getRHS()));
4633  // If not the same as the original
4634  Expr rhsFind = rhsFindThm.getRHS();
4635  if (rhsFind != inequality[index]) {
4636  // Substitute in the inequality
4637  vector<unsigned> changed;
4638  vector<Theorem> children;
4639  changed.push_back(index);
4640  children.push_back(rhsFindThm);
4641  rhsFindThm = iffMP(inequalityThm, substitutivityRule(inequality, changed, children));
4642  // If on the left-hand side, we are done
4643  if (index == 0)
4644  inequalityFindThm = rhsFindThm;
4645  else
4646  // If on the right-hand side and left-hand side is 0, normalize it
4647  if (inequality[0].isRational() && inequality[0].getRational() == 0)
4648  inequalityFindThm = normalize(rhsFindThm);
4649  else
4650  inequalityFindThm = rhsFindThm;
4651  } else
4652  inequalityFindThm = inequalityThm;
4653  } else
4654  inequalityFindThm = inequalityThm;
4655 
4656 
4657  TRACE("arith find", "inequalityToFind ==>", inequalityFindThm.getExpr(), "");
4658 
4659  return inequalityFindThm;
4660 }
4661 
4663  // Trace it
4664  TRACE("arith atoms", "registerAtom(", e.toString(), ")");
4665 
4666  // Mark it
4667  formulaAtoms[e] = true;
4668 
4669  // If it is a atomic formula, add it to the map
4670  if (e.isAbsAtomicFormula() && isIneq(e)) {
4671  Expr rightSide = e[1];
4672  Rational leftSide = e[0].getRational();
4673 
4674  //Get the terms for : c1 op t1 and t2 -op c2
4675  Expr t1, t2;
4676  Rational c1, c2;
4677  extractTermsFromInequality(e, c1, t1, c2, t2);
4678 
4679  if (true) {
4680  TRACE("arith atoms", "registering lower bound for ", t1.toString(), " = " + c1.toString() + ")");
4681  formulaAtomLowerBound[t1].insert(pair<Rational, Expr>(c1, e));
4682 
4683  // See if the bounds on the registered term can infered from already asserted facts
4685  if (lowerBoundFind != termLowerBound.end()) {
4686  Rational boundValue = (*lowerBoundFind).second;
4687  Theorem boundThm = termLowerBoundThm[t1];
4688  Expr boundIneq = boundThm.getExpr();
4689  if (boundValue > c1 || (boundValue == c1 && !(boundIneq.getKind() == LE && e.getKind() == LT))) {
4690  enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyWeakerInequality(boundIneq, e)));
4691  }
4692  }
4693 
4694  // See if the bounds on the registered term can falsified from already asserted facts
4696  if (upperBoundFind != termUpperBound.end()) {
4697  Rational boundValue = (*upperBoundFind).second;
4698  Theorem boundThm = termUpperBoundThm[t1];
4699  Expr boundIneq = boundThm.getExpr();
4700  if (boundValue < c1 || (boundValue == c1 && boundIneq.getKind() == LT && e.getKind() == LT)) {
4701  enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyNegatedInequality(boundIneq, e)));
4702  }
4703  }
4704 
4705  TRACE("arith atoms", "registering upper bound for ", t2.toString(), " = " + c2.toString() + ")");
4706  formulaAtomUpperBound[t2].insert(pair<Rational, Expr>(c2, e));
4707  }
4708  }
4709 }
4710 
4712  : d_pathLenghtThres(&(core->getFlags()["pathlength-threshold"].getInt())),
4713  arith(arith),
4714  core(core),
4715  rules(rules),
4716  unsat_theorem(context),
4717  biggestEpsilon(context, 0, 0),
4718  smallestPathDifference(context, 1, 0),
4719  leGraph(context),
4720  varInCycle(context)
4721 {
4722 }
4723 
4725  return unsat_theorem;
4726 }
4727 
4729  return !getUnsatTheorem().isNull();
4730 }
4731 
4733  Expr index = x - y;
4734 
4735  Graph::iterator find_le = leGraph.find(index);
4736  if (find_le != leGraph.end()) {
4737  EdgeInfo edge_info = (*find_le).second;
4738  if (edge_info.isDefined()) return true;
4739  }
4740 
4741  return false;
4742 }
4743 
4745  return (varInCycle.find(x) != varInCycle.end());
4746 }
4747 
4749  Expr index = x - y;
4750  Graph::ElementReference edge_info = leGraph[index];
4751 
4752  // If a new edge and x != y, then add vertices to the apropriate lists
4753  if (x != y && !edge_info.get().isDefined()) {
4754 
4755  // Adding a new edge, take a resource
4756  core->getResource();
4757 
4758  EdgesList::iterator y_it = incomingEdges.find(y);
4759  if (y_it == incomingEdges.end() || (*y_it).second == 0) {
4760  CDList<Expr>* list = new(true) CDList<Expr>(core->getCM()->getCurrentContext());
4761  list->push_back(x);
4762  incomingEdges[y] = list;
4763  } else
4764  ((*y_it).second)->push_back(x);
4765 
4766  EdgesList::iterator x_it = outgoingEdges.find(x);
4767  if (x_it == outgoingEdges.end() || (*x_it).second == 0) {
4768  CDList<Expr>* list = new(true) CDList<Expr>(core->getCM()->getCurrentContext());
4769  list->push_back(y);
4770  outgoingEdges[x] = list;
4771  } else
4772  ((*x_it).second)->push_back(y);
4773  }
4774 
4775  return edge_info;
4776 }
4777 
4779  if (!existsEdge(x, y))
4780  return EpsRational::PlusInfinity;
4781  else {
4782  EdgeInfo edgeInfo = getEdge(x, y).get();
4783  return edgeInfo.length;
4784  }
4785 }
4786 
4787 
4788 void TheoryArithOld::DifferenceLogicGraph::addEdge(const Expr& x, const Expr& y, const Rational& bound, const Theorem& edge_thm) {
4789 
4790  TRACE("arith diff", x, " --> ", y);
4791  DebugAssert(x != y, "addEdge, given two equal expressions!");
4792 
4793  if (isUnsat()) return;
4794 
4795  // If out of resources, bail out
4796  if (core->outOfResources()) return;
4797 
4798  // Get the kind of the inequality (NOTE isNull -- for model computation we add a vertex with no theorem)
4799  // FIXME: Later, add a debug assert for the theorem that checks that this variable is cvc3diffLogicSource
4800  int kind = (edge_thm.isNull() ? LE : edge_thm.getExpr().getKind());
4801  DebugAssert(kind == LT || kind == LE, "addEdge, not an <= or <!");
4802 
4803  // Get the EpsRational bound
4804  Rational k = (kind == LE ? 0 : -1);
4805  EpsRational c(bound, k);
4806 
4807  // Get the current (or a fresh new edge info)
4808  Graph::ElementReference edgeInfoRef = getEdge(x, y);
4809  // If uninitialized, or smaller length (we prefer shorter paths, so one edge is better)
4810  EdgeInfo edgeInfo = edgeInfoRef.get();
4811  // If the edge changed to the better, do the work
4812  if (!edgeInfo.isDefined() || c <= edgeInfo.length) {
4813 
4814  // Update model generation data
4815  if (edgeInfo.isDefined()) {
4816  EpsRational difference = edgeInfo.length - c;
4817  Rational rationalDifference = difference.getRational();
4818  if (rationalDifference > 0 && rationalDifference < smallestPathDifference) {
4819  smallestPathDifference = rationalDifference;
4820  TRACE("diff model", "smallest path difference : ", smallestPathDifference, "");
4821  }
4822  }
4823  Rational newEpsilon = - c.getEpsilon();
4824  if (newEpsilon > biggestEpsilon) {
4825  biggestEpsilon = newEpsilon;
4826  TRACE("diff model", "biggest epsilon : ", biggestEpsilon, "");
4827  }
4828 
4829  // Set the edge info
4830  edgeInfo.length = c;
4831  edgeInfo.explanation = edge_thm;
4832  edgeInfo.path_length_in_edges = 1;
4833  edgeInfoRef = edgeInfo;
4834 
4835 
4836  // Try simple cycle x --> y --> x, to keep invariants (no cycles or one negative)
4837  if (existsEdge(y, x)) {
4838  varInCycle[x] = true;
4839  varInCycle[y] = true;
4840  tryUpdate(x, y, x);
4841  if (isUnsat())
4842  return;
4843  }
4844 
4845  // For all edges coming into x, z ---> x, update z ---> y and add updated ones to the updated_in_y vector
4846  CDList<Expr>* in_x = incomingEdges[x];
4847  vector<Expr> updated_in_y;
4848  updated_in_y.push_back(x);
4849 
4850  // If there
4851  if (in_x) {
4852  IF_DEBUG(int total = 0; int updated = 0;);
4853  for (unsigned it = 0; it < in_x->size() && !isUnsat(); it ++) {
4854  const Expr& z = (*in_x)[it];
4855  if (z != arith->zero && z.hasFind() && core->find(z).getRHS() != z) continue;
4856  if (z != y && z != x && x != y) {
4857  IF_DEBUG(total ++;);
4858  TRACE("diff update", "trying with ", z.toString() + " --> ", x.toString());
4859  if (tryUpdate(z, x, y)) {
4860  updated_in_y.push_back(z);
4861  IF_DEBUG(updated++;);
4862  }
4863  }
4864  }
4865  TRACE("diff updates", "Updates : ", int2string(updated), " of " + int2string(total));
4866  }
4867 
4868  // For all edges coming into y, z_1 ---> y, and all edges going out of y, y ---> z_2, update z1 --> z_2
4869  CDList<Expr>* out_y = outgoingEdges[y];
4870  if (out_y)
4871  for (unsigned it_z1 = 0; it_z1 < updated_in_y.size() && !isUnsat(); it_z1 ++) {
4872  for (unsigned it_z2 = 0; it_z2 < out_y->size() && !isUnsat(); it_z2 ++) {
4873  const Expr& z1 = updated_in_y[it_z1];
4874  const Expr& z2 = (*out_y)[it_z2];
4875  if (z2 != arith->zero && z2.hasFind() && core->find(z2).getRHS() != z2) continue;
4876  if (z1 != z2 && z1 != y && z2 != y)
4877  tryUpdate(z1, y, z2);
4878  }
4879  }
4880 
4881  } else {
4882  TRACE("arith propagate", "could have propagated ", edge_thm.getExpr(), edge_thm.isAssump() ? " ASSUMPTION " : "not assumption");
4883 
4884  }
4885 
4886 }
4887 
4888 void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(const Expr& x, const Expr& z, const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems) {
4889  TRACE("arith diff", "Getting theorems from ", x, " to " + z.toString() + " length = " + edgeInfo.length.toString() + ", edge_length = " + int2string(edgeInfo.path_length_in_edges));
4890 
4891  if (edgeInfo.path_length_in_edges == 1) {
4892  DebugAssert(x == sourceVertex || z == sourceVertex || !edgeInfo.explanation.isNull(), "Edge from " + x.toString() + " to " + z.toString() + " has no theorem!");
4893  if (x != sourceVertex && z != sourceVertex)
4894  outputTheorems.push_back(edgeInfo.explanation);
4895  }
4896  else {
4897  const Expr& y = edgeInfo.in_path_vertex;
4898  EdgeInfo x_y = getEdge(x, y);
4899  DebugAssert(x_y.isDefined(), "getEdgeTheorems: the cycle edge is not defined!");
4900  EdgeInfo y_z = getEdge(y, z);
4901  DebugAssert(y_z.isDefined(), "getEdgeTheorems: the cycle edge is not defined!");
4902  getEdgeTheorems(x, y, x_y, outputTheorems);
4903  getEdgeTheorems(y, z, y_z, outputTheorems);
4904  }
4905 }
4906 
4908 
4909  // Get the cycle info
4910  Graph::ElementReference x_x_cycle_ref = getEdge(x, x);
4911  EdgeInfo x_x_cycle = x_x_cycle_ref.get();
4912 
4913  DebugAssert(x_x_cycle.isDefined(), "analyseConflict: the cycle edge is not defined!");
4914 
4915  // Vector to keep the theorems in
4916  vector<Theorem> inequalities;
4917 
4918  // Get the theorems::analyse
4919  getEdgeTheorems(x, x, x_x_cycle, inequalities);
4920 
4921  // Set the unsat theorem
4922  unsat_theorem = rules->cycleConflict(inequalities);
4923 
4924  TRACE("diff unsat", "negative cycle : ", int2string(inequalities.size()), " vertices.");
4925 }
4926 
4928 
4929  // x -> y -> z, if z -> x they are all in a cycle
4930  if (existsEdge(z, x)) {
4931  varInCycle[x] = true;
4932  varInCycle[y] = true;
4933  varInCycle[z] = true;
4934  }
4935 
4936  //Get all the edges
4937  Graph::ElementReference x_y_le_ref = getEdge(x, y);
4938  EdgeInfo x_y_le = x_y_le_ref;
4939  if (*d_pathLenghtThres >= 0 && x_y_le.path_length_in_edges > *d_pathLenghtThres) return false;
4940 
4941  Graph::ElementReference y_z_le_ref = getEdge(y, z);
4942  EdgeInfo y_z_le = y_z_le_ref;
4943  if (*d_pathLenghtThres >= 0 && y_z_le.path_length_in_edges > *d_pathLenghtThres) return false;
4944 
4945  Graph::ElementReference x_z_le_ref = getEdge(x, z);
4946  EdgeInfo x_z_le = x_z_le_ref;
4947 
4948  bool cycle = (x == z);
4949  bool updated = false;
4950 
4951  // Try <= + <= --> <=
4952  if (!isUnsat() && x_y_le.isDefined() && y_z_le.isDefined()) {
4953  EpsRational combined_length = x_y_le.length + y_z_le.length;
4954  int combined_edge_length = x_y_le.path_length_in_edges + y_z_le.path_length_in_edges;
4955 
4956  if (!x_z_le.isDefined() || combined_length < x_z_le.length ||
4957  (combined_length == x_z_le.length && (combined_edge_length < x_z_le.path_length_in_edges))) {
4958 
4959  if (!cycle || combined_length <= EpsRational::Zero) {
4960 
4961  if (!cycle || combined_length < EpsRational::Zero) {
4962 
4963  // Remember the path differences
4964  if (!cycle) {
4965  EpsRational difference = x_z_le.length - combined_length;
4966  Rational rationalDifference = difference.getRational();
4967  Rational newEpsilon = - x_z_le.length.getEpsilon();
4968  if (rationalDifference > 0 && rationalDifference < smallestPathDifference) {
4969  smallestPathDifference = rationalDifference;
4970  TRACE("diff model", "smallest path difference : ", smallestPathDifference, "");
4971  }
4972  if (newEpsilon > biggestEpsilon) {
4973  biggestEpsilon = newEpsilon;
4974  TRACE("diff model", "biggest epsilon : ", biggestEpsilon, "");
4975  }
4976  }
4977 
4978  // If we have a constraint among two integers variables strenghten it
4979  bool addAndEnqueue = false;
4980  if (core->okToEnqueue() && !combined_length.isInteger())
4981  if (x.getType() == arith->intType() && z.getType() == arith->intType())
4982  addAndEnqueue = true;
4983 
4984  x_z_le.length = combined_length;
4985  x_z_le.path_length_in_edges = combined_edge_length;
4986  x_z_le.in_path_vertex = y;
4987  x_z_le_ref = x_z_le;
4988 
4989  if (addAndEnqueue) {
4990  vector<Theorem> pathTheorems;
4991  getEdgeTheorems(x, z, x_z_le, pathTheorems);
4992  core->enqueueFact(rules->addInequalities(pathTheorems));
4993  }
4994 
4995  TRACE("arith diff", x.toString() + " -- > " + z.toString(), " : ", combined_length.toString());
4996  updated = true;
4997  } else
4998  if (core->okToEnqueue()) {
4999  // 0 length cycle
5000  vector<Theorem> antecedentThms;
5001  getEdgeTheorems(x, y, x_y_le, antecedentThms);
5002  getEdgeTheorems(y, z, y_z_le, antecedentThms);
5003  core->enqueueFact(rules->implyEqualities(antecedentThms));
5004  }
5005 
5006  // Try to propagate somthing in the original formula
5007  if (updated && !cycle && x != sourceVertex && z != sourceVertex && core->okToEnqueue())
5008  arith->tryPropagate(x, z, x_z_le, LE);
5009 
5010  }
5011 
5012  if (cycle && combined_length < EpsRational::Zero)
5013  analyseConflict(x, LE);
5014  }
5015  }
5016 
5017  return updated;
5018 }
5019 
5021 
5022 }
5023 
5025  for (EdgesList::iterator it = incomingEdges.begin(), it_end = incomingEdges.end(); it != it_end; it ++) {
5026  if ((*it).second) {
5027  delete (*it).second;
5028  free ((*it).second);
5029  }
5030  }
5031  for (EdgesList::iterator it = outgoingEdges.begin(), it_end = outgoingEdges.end(); it != it_end; it ++) {
5032  if ((*it).second) {
5033  delete (*it).second;
5034  free ((*it).second);
5035  }
5036  }
5037 }
5038 
5039 void TheoryArithOld::tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind) {
5040 
5041  TRACE("diff atoms", "trying propagation", " x = " + x.toString(), " y = " + y.toString());
5042 
5043  // bail on non representative terms (we don't pass non-representative terms)
5044 // if (x.hasFind() && find(x).getRHS() != x) return;
5045 // if (y.hasFind() && find(y).getRHS() != y) return;
5046 
5047  // given edge x - z (kind) lenth
5048 
5049  // Make the index (c1 <= y - x)
5050  vector<Expr> t1_summands;
5051  t1_summands.push_back(rat(0));
5052  if (y != zero) t1_summands.push_back(y);
5053  // We have to canonize in case it is nonlinear
5054  // nonlinear terms are canonized with a constants --> 1*x*y, hence (-1)*1*x*y will not be canonical
5055  if (x != zero) t1_summands.push_back(canon(rat(-1)*x).getRHS());
5056  Expr t1 = canon(plusExpr(t1_summands)).getRHS();
5057 
5058  TRACE("diff atoms", "trying propagation", " t1 = " + t1.toString(), "");
5059 
5060  // The constant c1 <= y - x
5061  Rational c1 = - x_y_edge.length.getRational();
5062 
5063  // See if we can propagate anything to the formula atoms
5064  // c1 <= t1 ===> c <= t1 for c < c1
5065  AtomsMap::iterator find = formulaAtomLowerBound.find(t1);
5066  AtomsMap::iterator find_end = formulaAtomLowerBound.end();
5067  if (find != find_end) {
5068  set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
5069  set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
5070  while (bounds != bounds_end) {
5071  const Expr& implied = (*bounds).second;
5072  // Try to do some theory propagation
5073  if ((*bounds).first < c1 || (implied.getKind() == LE && (*bounds).first == c1)) {
5074  TRACE("diff atoms", "found propagation", "", "");
5075  // c1 <= t1 => c <= t1 (for c <= c1)
5076  // c1 < t1 => c <= t1 (for c <= c1)
5077  // c1 <= t1 => c < t1 (for c < c1)
5078  vector<Theorem> antecedentThms;
5079  diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms);
5080  Theorem impliedThm = d_rules->implyWeakerInequalityDiffLogic(antecedentThms, implied);
5081  enqueueFact(impliedThm);
5082  }
5083  bounds ++;
5084  }
5085  }
5086 
5087  //
5088  // c1 <= t1 ==> !(t1 <= c) for c < c1
5089  // ==> !(-c <= t2)
5090  // i.e. all coefficient in in the implied are opposite of t1
5091  find = formulaAtomUpperBound.find(t1);
5092  find_end = formulaAtomUpperBound.end();
5093  if (find != find_end) {
5094  set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
5095  set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
5096  while (bounds != bounds_end) {
5097  const Expr& implied = (*bounds).second;
5098  // Try to do some theory propagation
5099  if ((*bounds).first < c1) {
5100  TRACE("diff atoms", "found negated propagation", "", "");
5101  vector<Theorem> antecedentThms;
5102  diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms);
5103  Theorem impliedThm = d_rules->implyNegatedInequalityDiffLogic(antecedentThms, implied);
5104  enqueueFact(impliedThm);
5105  }
5106  bounds ++;
5107  }
5108  }
5109 }
5110 
5112 
5113  // If source vertex is null, create it
5114  if (sourceVertex.isNull()) {
5115  Theorem thm_exists_zero = arith->getCommonRules()->varIntroSkolem(arith->zero);
5116  sourceVertex = thm_exists_zero.getExpr()[1];
5117  }
5118 
5119  // The empty theorem to pass around
5120  Theorem thm;
5121 
5122  // Add an edge to all the vertices
5123  EdgesList::iterator vertexIt = incomingEdges.begin();
5124  EdgesList::iterator vertexItEnd = incomingEdges.end();
5125  for (; vertexIt != vertexItEnd; vertexIt ++) {
5126  Expr vertex = (*vertexIt).first;
5127  if (core->find(vertex).getRHS() != vertex) continue;
5128  if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
5129  addEdge(sourceVertex, vertex, 0, thm);
5130  }
5131  vertexIt = outgoingEdges.begin();
5132  vertexItEnd = outgoingEdges.end();
5133  for (; vertexIt != vertexItEnd; vertexIt ++) {
5134  Expr vertex = (*vertexIt).first;
5135  if (core->find(vertex).getRHS() != vertex) continue;
5136  if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
5137  addEdge(sourceVertex, vertex, 0, thm);
5138  }
5139 
5140  // Also add an edge to cvcZero
5141  if (!existsEdge(sourceVertex, arith->zero))
5142  addEdge(sourceVertex, arith->zero, 0, thm);
5143 
5144  // For the < edges we will have a small enough epsilon to add
5145  // So, we will upper-bound the number of vertices and then divide
5146  // the smallest edge with that number so as to not be able to bypass
5147 
5148 }
5149 
5151 
5152  // For numbers, return it's value
5153  if (x.isRational()) return x.getRational();
5154 
5155  // For the source vertex, we don't care
5156  if (x == sourceVertex) return 0;
5157 
5158  // The path from source to targer vertex
5159  Graph::ElementReference x_le_c_ref = getEdge(sourceVertex, x);
5160  EdgeInfo x_le_c = x_le_c_ref;
5161 
5162  // The path from source to zero (adjusment)
5163  Graph::ElementReference zero_le_c_ref = getEdge(sourceVertex, arith->zero);
5164  EdgeInfo zero_le_c = zero_le_c_ref;
5165 
5166  TRACE("diff model", "zero adjustment: ", zero_le_c.length.getRational(), "");
5167  TRACE("diff model", "zero adjustment (eps): ", zero_le_c.length.getEpsilon(), "");
5168 
5169  // Value adjusted with the epsilon
5170  Rational epsAdjustment = (biggestEpsilon > 0 ? (x_le_c.length.getEpsilon() - zero_le_c.length.getEpsilon()) * smallestPathDifference / (2 * (biggestEpsilon + 1)) : 0);
5171  Rational value = x_le_c.length.getRational() + epsAdjustment;
5172 
5173  TRACE("diff model" , "biggest epsilon: ", biggestEpsilon, "");
5174  TRACE("diff model" , "smallestPathDifference: ", smallestPathDifference, "");
5175  TRACE("diff model" , "x_le_c.getEpsilon: ", x_le_c.length.getEpsilon(), "");
5176  TRACE("diff model" , "x_le_c.length: ", x_le_c.length.getRational(), "");
5177 
5178  // Value adjusted with the shift for zero
5179  value = zero_le_c.length.getRational() - value;
5180 
5181  TRACE("diff model", "Value of ", x, " : " + value.toString());
5182 
5183  // Return it
5184  return value;
5185 }
5186 
5187 // The infinity constant
5189 // The negative infinity constant
5191 // The negative infinity constant
5193 
5195  multiplicativeSignSplits.push_back(case_split_thm);
5196 }
5197 
5198 bool TheoryArithOld::addPairToArithOrder(const Expr& smaller, const Expr& bigger) {
5199  TRACE("arith var order", "addPairToArithOrder(" + smaller.toString(), ", ", bigger.toString() + ")");
5200  // We only accept arithmetic terms
5201  if (!isReal(smaller.getType()) && !isInt(smaller.getType())) return false;
5202  if (!isReal(bigger.getType()) && !isInt(bigger.getType())) return false;
5203  // We don't want to introduce loops
5204  FatalAssert(!d_graph.lessThan(smaller, bigger), "The pair (" + bigger.toString() + "," + smaller.toString() + ") is already in the order");
5205  // Update the graph
5206  d_graph.addEdge(smaller, bigger);
5207  return true;
5208 }
5209 
5211  if (isPow(term)) return true;
5212  if (!isMult(term)) return false;
5213  int vars = 0;
5214  for (int j = 0; j < term.arity(); j ++)
5215  if (isPow(term[j])) return true;
5216  else if (isLeaf(term[j])) {
5217  vars ++;
5218  if (vars > 1) return true;
5219  }
5220  return false;
5221 }
5222 
5224 
5225  DebugAssert(e.isEq(), "TheoryArithOld::isNonlinear: expecting an equation" + e.toString());
5226 
5227  const Expr& lhs = e[0];
5228  const Expr& rhs = e[1];
5229 
5230  if (isNonlinearSumTerm(lhs) || isNonlinearSumTerm(rhs)) return true;
5231 
5232  // Check the right-hand side
5233  for (int i = 0; i < lhs.arity(); i ++)
5234  if (isNonlinearSumTerm(lhs[i])) return true;
5235 
5236  // Check the left hand side
5237  for (int i = 0; i < rhs.arity(); i ++)
5238  if (isNonlinearSumTerm(rhs[i])) return true;
5239 
5240  return false;
5241 }
5242 
5243 
5244 bool TheoryArithOld::isPowersEquality(const Expr& eq, Expr& power1, Expr& power2) {
5245  // equality should be in the form 0 + x1^n - x2^n = 0
5246  DebugAssert(eq.isEq(), "TheoryArithOld::isPowersEquality, expecting an equality got " + eq.toString());
5247 
5248  if (!isPlus(eq[0])) return false;
5249  if (eq[0].arity() != 3) return false;
5250  if (!(eq[0][0].isRational()) || !(eq[0][0].getRational() == 0)) return false;
5251 
5252  // Process the first term
5253  Expr term1 = eq[0][1];
5254  Rational term1_c;
5255  if (isPow(term1)) {
5256  term1_c = 1;
5257  power1 = term1;
5258  } else
5259  if (isMult(term1) && term1.arity() == 2) {
5260  if (term1[0].isRational()) {
5261  term1_c = term1[0].getRational();
5262  if (isPow(term1[1])) {
5263  if (term1_c == 1) power1 = term1[1];
5264  else if (term1_c == -1) power2 = term1[1];
5265  else return false;
5266  } else return false;
5267  } else return false;
5268  } else return false;
5269 
5270  // Process the second term
5271  Expr term2 = eq[0][2];
5272  Rational term2_c;
5273  if (isPow(term2)) {
5274  term2_c = 1;
5275  power1 = term2;
5276  } else
5277  if (isMult(term2) && term2.arity() == 2) {
5278  if (term2[0].isRational()) {
5279  term2_c = term2[0].getRational();
5280  if (isPow(term2[1])) {
5281  if (term2_c == 1) power1 = term2[1];
5282  else if (term2_c == -1) power2 = term2[1];
5283  else return false;
5284  } else return false;
5285  } else return false;
5286  } else return false;
5287 
5288  // Check that they are of opposite signs
5289  if (term1_c == term2_c) return false;
5290 
5291  // Check that the powers are equal numbers
5292  if (!power1[0].isRational()) return false;
5293  if (!power2[0].isRational()) return false;
5294  if (power1[0].getRational() != power2[0].getRational()) return false;
5295 
5296  // Everything is fine
5297  return true;
5298 }
5299 
5300 bool TheoryArithOld::isPowerEquality(const Expr& eq, Rational& constant, Expr& power1) {
5301  DebugAssert(eq.isEq(), "TheoryArithOld::isPowerEquality, expecting an equality got " + eq.toString());
5302 
5303  if (!isPlus(eq[0])) return false;
5304  if (eq[0].arity() != 2) return false;
5305  if (!eq[0][0].isRational()) return false;
5306 
5307  constant = eq[0][0].getRational();
5308 
5309  Expr term = eq[0][1];
5310  if (isPow(term)) {
5311  power1 = term;
5312  constant = -constant;
5313  } else
5314  if (isMult(term) && term.arity() == 2) {
5315  if (term[0].isRational() && isPow(term[1])) {
5316  Rational term2_c = term[0].getRational();
5317  if (term2_c == 1) {
5318  power1 = term[1];
5319  constant = -constant;
5320  } else if (term2_c == -1) {
5321  power1 = term[1];
5322  return true;
5323  } else return false;
5324  } else return false;
5325  } else return false;
5326 
5327  // Check that the power is an integer
5328  if (!power1[0].isRational()) return false;
5329  if (!power1[0].getRational().isInteger()) return false;
5330 
5331  return true;
5332 }
5333 
5335  if (isLeaf(e)) return 1;
5336  if (isPow(e)) return termDegree(e[1]) * e[0].getRational().getInt();
5337  if (isMult(e)) {
5338  int degree = 0;
5339  for (int i = 0; i < e.arity(); i ++) degree += termDegree(e[i]);
5340  return degree;
5341  }
5342  return 0;
5343 }
5344 
5346 {
5347  DebugAssert(right.arity() > 1, "TheoryArithOld::canPickEqMonomial, expecting > 1 child, got " + right.arity());
5348 
5349  Expr::iterator istart = right.begin();
5350  Expr::iterator iend = right.end();
5351 
5352  // Skip the first one
5353  istart++;
5354  for(Expr::iterator i = istart; i != iend; ++i) {
5355 
5356  Expr leaf;
5357  Rational coeff;
5358 
5359  // Check if linear term
5360  if (isLeaf(*i)) {
5361  leaf = *i;
5362  coeff = 1;
5363  } else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
5364  leaf = (*i)[1];
5365  coeff = abs((*i)[0].getRational());
5366  } else
5367  continue;
5368 
5369  // If integer, must be coeff 1/-1
5370  if (!isIntegerThm(leaf).isNull())
5371  if (coeff != 1 && coeff != -1)
5372  continue;
5373 
5374  // Check if a leaf in other ones
5375  Expr::iterator j;
5376  for (j = istart; j != iend; ++j)
5377  if (j != i && isLeafIn(leaf, *j))
5378  break;
5379  if (j == iend)
5380  return true;
5381  }
5382 
5383  return false;
5384 }
5385 
5387  TRACE("arith shared", "isBounded(", t.toString(), ")");
5388  return hasUpperBound(t, queryType) && hasLowerBound(t, queryType);
5389 }
5390 
5392 {
5393  TRACE("arith shared", "getUpperBound(", t.toString(), ")");
5394 
5395  // If t is a constant it's bounded
5396  if (t.isRational()) {
5397  TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + t.getRational().toString());
5398  return t.getRational();
5399  }
5400 
5401  // If buffered, just return it
5403  if (find_t != termUpperBounded.end()) {
5404  TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + (*find_t).second.toString());
5405  return (*find_t).second;
5406  } else if (queryType == QueryWithCacheAll) {
5407  // Asked for cache query, so no bound is found
5408  TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> +inf");
5410  }
5411 
5412  // Assume it's not bounded
5414 
5415  // We always buffer the leaves, so all that's left are the terms
5416  if (!isLeaf(t)) {
5417  if (isMult(t)) {
5418  // We only handle linear terms
5419  if (!isNonlinearSumTerm(t)) {
5420  // Separate the multiplication
5421  Expr c, v;
5422  separateMonomial(t, c, v);
5423  // Get the upper-bound for the variable
5424  if (c.getRational() > 0) upperBound = getUpperBound(v);
5425  else upperBound = getLowerBound(v);
5426  if (upperBound.isFinite()) upperBound = upperBound * c.getRational();
5428  }
5429  } else if (isPlus(t)) {
5430  // If one of them is unconstrained then the term itself is unconstrained
5432  for (int i = 0; i < t.arity(); i ++) {
5433  Expr t_i = t[i];
5434  DifferenceLogicGraph::EpsRational t_i_upperBound = getUpperBound(t_i, queryType);
5435  if (t_i_upperBound.isFinite()) upperBound = upperBound + t_i_upperBound;
5436  else {
5438  // Not-bounded, check for constrained
5440  for(; i < t.arity() && isConstrainedAbove(t[i], QueryWithCacheLeaves); i ++);
5441  if (i == t.arity()) {
5442  TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> constrained");
5443  termConstrainedAbove[t] = true;
5444  }
5445  break;
5446  } else break;
5447  }
5448  }
5449  }
5450  }
5451 
5452  // Buffer it
5453  if (upperBound.isFinite()) {
5454  termUpperBounded[t] = upperBound;
5455  termConstrainedAbove[t] = true;
5456  }
5457 
5458  // Return if bounded or not
5459  TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + upperBound.toString());
5460  return upperBound;
5461 }
5462 
5464 {
5465  TRACE("arith shared", "getLowerBound(", t.toString(), ")");
5466 
5467  // If t is a constant it's bounded
5468  if (t.isRational()) {
5469  TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + t.getRational().toString());
5470  return t.getRational();
5471  }
5472 
5473  // If buffered, just return it
5475  if (t_find != termLowerBounded.end()) {
5476  TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + (*t_find).second.toString());
5477  return (*t_find).second;
5478  } else if (queryType == QueryWithCacheAll) {
5479  // Asked for cache query, so no bound is found
5480  TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> -inf");
5482  }
5483 
5484  // Assume it's not bounded
5486 
5487  // Leaves are always buffered
5488  if (!isLeaf(t)) {
5489  if (isMult(t)) {
5490  // We only handle linear terms
5491  if (!isNonlinearSumTerm(t)) {
5492  // Separate the multiplication
5493  Expr c, v;
5494  separateMonomial(t, c, v);
5495  // Get the upper-bound for the variable
5496  if (c.getRational() > 0) lowerBound = getLowerBound(v);
5497  else lowerBound = getUpperBound(v);
5498  if (lowerBound.isFinite()) lowerBound = lowerBound * c.getRational();
5500  }
5501  } else if (isPlus(t)) {
5502  // If one of them is unconstrained then the term itself is unconstrained
5504  for (int i = 0; i < t.arity(); i ++) {
5505  Expr t_i = t[i];
5506  DifferenceLogicGraph::EpsRational t_i_lowerBound = getLowerBound(t_i, queryType);
5507  if (t_i_lowerBound.isFinite()) lowerBound = lowerBound + t_i_lowerBound;
5508  else {
5510  // Not-bounded, check for constrained
5512  for(; i < t.arity() && isConstrainedBelow(t[i], QueryWithCacheLeaves); i ++);
5513  if (i == t.arity()) {
5514  TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> constrained");
5515  termConstrainedBelow[t] = true;
5516  }
5517  break;
5518  } else break;
5519  }
5520  }
5521  }
5522  }
5523 
5524  // Buffer it
5525  if (lowerBound.isFinite()) {
5526  termLowerBounded[t] = lowerBound;
5527  termConstrainedBelow[t] = true;
5528  }
5529 
5530  // Return if bounded or not
5531  TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + lowerBound.toString());
5532  return lowerBound;
5533 }
5534 
5536 {
5537  int computeTermBoundsConstrainedCount = 0;
5538 
5539  vector<Expr> sorted_vars;
5540  // Get the variables in the topological order
5541  if (!diffLogicOnly) d_graph.getVerticesTopological(sorted_vars);
5542  // Or if difference logic only, just get them
5543  else {
5544  diffLogicGraph.getVariables(sorted_vars);
5545  IF_DEBUG(
5546  diffLogicGraph.writeGraph(cerr);
5547  )
5548  }
5549 
5550  // Go in the reverse topological order and try to see if the vats are constrained/bounded
5551  for (int i = sorted_vars.size() - 1; i >= 0; i --)
5552  {
5553  // Get the variable
5554  Expr v = sorted_vars[i];
5555 
5556  // If the find is not identity, skip it
5557  if (v.hasFind() && find(v).getRHS() != v) continue;
5558 
5559  TRACE("arith shared", "processing: ", v.toString(), "");
5560 
5561  // If the variable is not an integer, it's unconstrained, unless we are in model generation
5562  if (isIntegerThm(v).isNull() && !d_inModelCreation) continue;
5563 
5564  // We only do the computation if the variable is not already constrained
5565  if (!isConstrained(v, QueryWithCacheAll)) {
5566 
5567  // Recall if we already computed the constraint
5568  bool constrainedAbove = isConstrained(v, QueryWithCacheAll);
5569 
5570  // See if it's bounded from above in the difference graph
5572  if (!constrainedAbove) constrainedAbove = upperBound.isFinite();
5573 
5574  // Try to refine the bound by checking projected inequalities
5575  if (!diffLogicOnly) {
5576  ExprMap<CDList<Ineq> *>::iterator v_left_find = d_inequalitiesLeftDB.find(v);
5577  // If not constraint from one side, it's unconstrained
5578  if (v_left_find != d_inequalitiesLeftDB.end()) {
5579  // Check right hand side for an unconstrained variable
5580  CDList<Ineq>*& left_list = (*v_left_find).second;
5581  if (left_list && left_list->size() > 0) {
5582  for (unsigned ineq_i = 0; ineq_i < left_list->size(); ineq_i ++) {
5583  // Get the inequality
5584  Ineq ineq = (*left_list)[ineq_i];
5585  // Get the right-hand side (v <= rhs)
5586  Expr rhs = ineq.ineq().getExpr()[1];
5587  // If rhs changed, skip it
5588  if (rhs.hasFind() && find(rhs).getRHS() != rhs) continue;
5589  // Compute the upper bound while
5591  if (currentUpperBound.isFinite() && (!upperBound.isFinite() || currentUpperBound < upperBound)) {
5592  upperBound = currentUpperBound;
5593  constrainedAbove = true;
5594  }
5595  // If not constrained, check if right-hand-side is constrained
5596  if (!constrainedAbove) constrainedAbove = isConstrainedAbove(rhs, QueryWithCacheAll);
5597  }
5598  }
5599  }
5600  }
5601  // Difference logic case (no projections)
5602  else if (!constrainedAbove) {
5603  // If there is no incoming edges, then the variable is not constrained
5604  if (!diffLogicGraph.hasIncoming(v)) constrainedAbove = false;
5605  // If there is a cycle from t to t, all the variables
5606  // in the graph are constrained by each-other (we could
5607  // choose one, but it's too complicated)
5608  else if (diffLogicGraph.inCycle(v)) constrainedAbove = true;
5609  // Otherwise, since there is no bounds, and the cycles
5610  // can be shifted (since one of them can be taken as
5611  // unconstrained), we can assume that the variables is
5612  // not constrained. Conundrum here is that when in model-generation
5613  // we actually should take it as constrained so that it's
5614  // split on and we are on the safe side
5615  else constrainedAbove = d_inModelCreation;
5616  }
5617 
5618  // Cache the upper bound and upper constrained computation
5619  if (constrainedAbove) termConstrainedAbove[v] = true;
5620  if (upperBound.isFinite()) termUpperBounded[v] = upperBound;
5621 
5622  // Recall the below computation if it's there
5623  bool constrainedBelow = isConstrainedBelow(v, QueryWithCacheAll);
5624 
5625  // See if it's bounded from below in the difference graph
5627  if (lowerBound.isFinite()) lowerBound = -lowerBound;
5629  if (!constrainedBelow) constrainedBelow = lowerBound.isFinite();
5630 
5631  // Try to refine the bound by checking projected inequalities
5632  if (!diffLogicOnly) {
5633  ExprMap<CDList<Ineq> *>::iterator v_right_find = d_inequalitiesRightDB.find(v);
5634  // If not constraint from one side, it's unconstrained
5635  if (v_right_find != d_inequalitiesRightDB.end()) {
5636  // Check right hand side for an unconstrained variable
5637  CDList<Ineq>*& right_list = (*v_right_find).second;
5638  if (right_list && right_list->size() > 0) {
5639  for (unsigned ineq_i = 0; ineq_i < right_list->size(); ineq_i ++) {
5640  // Get the inequality
5641  Ineq ineq = (*right_list)[ineq_i];
5642  // Get the right-hand side (lhs <= 0)
5643  Expr lhs = ineq.ineq().getExpr()[0];
5644  // If lhs has changed, skip it
5645  if (lhs.hasFind() && find(lhs).getRHS() != lhs) continue;
5646  // Compute the lower bound
5648  if (currentLowerBound.isFinite() && (!lowerBound.isFinite() || currentLowerBound > lowerBound)) {
5649  lowerBound = currentLowerBound;
5650  constrainedBelow = true;
5651  }
5652  // If not constrained, check if right-hand-side is constrained
5653  if (!constrainedBelow) constrainedBelow = isConstrainedBelow(lhs, QueryWithCacheAll);
5654  }
5655  }
5656  }
5657  }
5658  // Difference logic case (no projections)
5659  else if (!constrainedBelow) {
5660  // If there is no incoming edges, then the variable is not constrained
5661  if (!diffLogicGraph.hasOutgoing(v)) constrainedBelow = false;
5662  // If there is a cycle from t to t, all the variables
5663  // in the graph are constrained by each-other (we could
5664  // choose one, but it's too complicated)
5665  else if (diffLogicGraph.inCycle(v)) constrainedBelow = true;
5666  // Otherwise, since there is no bounds, and the cycles
5667  // can be shifted (since one of them can be taken as
5668  // unconstrained), we can assume that the variables is
5669  // not constrained. Conundrum here is that when in model-generation
5670  // we actually should take it as constrained so that it's
5671  // split on and we are on the safe side
5672  else constrainedBelow = d_inModelCreation;
5673  }
5674 
5675  // Cache the lower bound and lower constrained computation
5676  if (constrainedBelow) termConstrainedBelow[v] = true;
5677  if (lowerBound.isFinite()) termLowerBounded[v] = lowerBound;
5678 
5679  // Is this variable constrained
5680  if (constrainedAbove && constrainedBelow) computeTermBoundsConstrainedCount ++;
5681 
5682  TRACE("arith shared", (constrainedAbove && constrainedBelow ? "constrained " : "unconstrained "), "", "");
5683  } else
5684  computeTermBoundsConstrainedCount ++;
5685  }
5686 
5687  TRACE("arith shared", "number of constrained variables : ", int2string(computeTermBoundsConstrainedCount), " of " + int2string(sorted_vars.size()));
5688 
5689  return computeTermBoundsConstrainedCount;
5690 }
5691 
5693 {
5694  TRACE("arith shared", "isConstrainedAbove(", t.toString(), ")");
5695 
5696  // Rational numbers are constrained
5697  if (t.isRational()) {
5698  TRACE("arith shared", "isConstrainedAbove() ==> true", "", "");
5699  return true;
5700  }
5701 
5702  // Look it up in the cache
5704  if (t_find != termConstrainedAbove.end()) {
5705  TRACE("arith shared", "isConstrainedAbove() ==> true", "", "");
5706  return true;
5707  }
5708  else if (queryType == QueryWithCacheAll) {
5709  TRACE("arith shared", "isConstrainedAbove() ==> false", "", "");
5710  return false;
5711  }
5712 
5713  bool constrainedAbove = true;
5714 
5715  if (isLeaf(t)) {
5716  // Leaves are always cached
5717  constrainedAbove = false;
5718  } else {
5719  if (isMult(t)) {
5720  // Non-linear terms are constrained by default
5721  // we only deal with the linear stuff
5722  if (!isNonlinearSumTerm(t)) {
5723  // Separate the multiplication
5724  Expr c, v;
5725  separateMonomial(t, c, v);
5726  // Check if the variable is constrained
5727  if (c.getRational() > 0) constrainedAbove = isConstrainedAbove(v, queryType);
5728  else constrainedAbove = isConstrainedBelow(v, queryType);
5729  }
5730  } else if (isPlus(t)) {
5731  // If one of them is unconstrained then the term itself is unconstrained
5732  for (int i = 0; i < t.arity() && constrainedAbove; i ++)
5733  if (!isConstrainedAbove(t[i])) constrainedAbove = false;
5734  }
5735  }
5736 
5737  // Remember it
5738  if (constrainedAbove) termConstrainedAbove[t] = true;
5739 
5740  TRACE("arith shared", "isConstrainedAbove() ==> ", constrainedAbove ? "true" : "false", "");
5741 
5742  // Return in
5743  return constrainedAbove;
5744 }
5745 
5747 {
5748  TRACE("arith shared", "isConstrainedBelow(", t.toString(), ")");
5749 
5750  // Rational numbers are constrained
5751  if (t.isRational()) return true;
5752 
5753  // Look it up in the cache
5755  if (t_find != termConstrainedBelow.end()) {
5756  TRACE("arith shared", "isConstrainedBelow() ==> true", "", "");
5757  return true;
5758  }
5759  else if (queryType == QueryWithCacheAll) {
5760  TRACE("arith shared", "isConstrainedBelow() ==> false", "", "");
5761  return false;
5762  }
5763 
5764  bool constrainedBelow = true;
5765 
5766  if (isLeaf(t)) {
5767  // Leaves are always cached
5768  constrainedBelow = false;
5769  } else {
5770  if (isMult(t)) {
5771  // Non-linear terms are constrained by default
5772  // we only deal with the linear stuff
5773  if (!isNonlinearSumTerm(t)) {
5774  // Separate the multiplication
5775  Expr c, v;
5776  separateMonomial(t, c, v);
5777  // Check if the variable is constrained
5778  if (c.getRational() > 0) constrainedBelow = isConstrainedBelow(v, queryType);
5779  else constrainedBelow = isConstrainedAbove(v, queryType);
5780  }
5781  } else if (isPlus(t)) {
5782  // If one of them is unconstrained then the term itself is unconstrained
5783  constrainedBelow = true;
5784  for (int i = 0; i < t.arity() && constrainedBelow; i ++)
5785  if (!isConstrainedBelow(t[i]))
5786  constrainedBelow = false;
5787  }
5788  }
5789 
5790  // Cache it
5791  if (constrainedBelow) termConstrainedBelow[t] = true;
5792 
5793  TRACE("arith shared", "isConstrainedBelow() ==> ", constrainedBelow ? "true" : "false", "");
5794 
5795  // Return it
5796  return constrainedBelow;
5797 }
5798 
5799 bool TheoryArithOld::isConstrained(const Expr& t, bool intOnly, BoundsQueryType queryType)
5800 {
5801  TRACE("arith shared", "isConstrained(", t.toString(), ")");
5802  // For the reals we consider them unconstrained if not asked for full check
5803  if (intOnly && isIntegerThm(t).isNull()) return false;
5804  bool result = (isConstrainedAbove(t, queryType) && isConstrainedBelow(t, queryType));
5805  TRACE("arith shared", "isConstrained(", t.toString(), (result ? ") ==> true " : ") ==> false ") );
5806  return result;
5807 }
5808 
5810 {
5811  EdgesList::iterator find_x = incomingEdges.find(x);
5812 
5813  // No edges at all meaning no incoming
5814  if (find_x == incomingEdges.end()) return false;
5815 
5816  // The pointer being null, also no incoming
5817  CDList<Expr>*& list = (*find_x).second;
5818  if (!list) return false;
5819 
5820  // If in model creation, source vertex goes to all vertices
5821  if (sourceVertex.isNull())
5822  return list->size() > 0;
5823  else
5824  return list->size() > 1;
5825 }
5826 
5828 {
5829  EdgesList::iterator find_x = outgoingEdges.find(x);
5830 
5831  // No edges at all meaning no incoming
5832  if (find_x == outgoingEdges.end()) return false;
5833 
5834  // The pointer being null, also no incoming
5835  CDList<Expr>*& list = (*find_x).second;
5836  if (!list) return false;
5837 
5838  // If the list is not empty we have outgoing edges
5839  return list->size() > 0;
5840 }
5841 
5843 {
5844  set<Expr> vars_set;
5845 
5846  EdgesList::iterator incoming_it = incomingEdges.begin();
5847  EdgesList::iterator incoming_it_end = incomingEdges.end();
5848  while (incoming_it != incoming_it_end) {
5849  Expr var = (*incoming_it).first;
5850  if (var != sourceVertex)
5851  vars_set.insert(var);
5852  incoming_it ++;
5853  }
5854 
5855  EdgesList::iterator outgoing_it = outgoingEdges.begin();
5856  EdgesList::iterator outgoing_it_end = outgoingEdges.end();
5857  while (outgoing_it != outgoing_it_end) {
5858  Expr var = (*outgoing_it).first;
5859  if (var != sourceVertex)
5860  vars_set.insert(var);
5861  outgoing_it ++;
5862  }
5863 
5864  set<Expr>::iterator set_it = vars_set.begin();
5865  set<Expr>::iterator set_it_end = vars_set.end();
5866  while (set_it != set_it_end) {
5867  variables.push_back(*set_it);
5868  set_it ++;
5869  }
5870 }
5871 
5873  return;
5874  out << "digraph G {" << endl;
5875 
5876  EdgesList::iterator incoming_it = incomingEdges.begin();
5877  EdgesList::iterator incoming_it_end = incomingEdges.end();
5878  while (incoming_it != incoming_it_end) {
5879 
5880  Expr var_u = (*incoming_it).first;
5881 
5882  CDList<Expr>* edges = (*incoming_it).second;
5883  if (edges)
5884  for (unsigned edge_i = 0; edge_i < edges->size(); edge_i ++) {
5885  Expr var_v = (*edges)[edge_i];
5886  out << var_u.toString() << " -> " << var_v.toString() << endl;
5887  }
5888 
5889  incoming_it ++;
5890  }
5891 
5892  out << "}" << endl;
5893 }
5894 
5896  if (isPlus(t)) {
5897  for (int i = 0; i < t.arity(); ++ i) {
5898  if (isUnconstrained(t[i])) {
5899  TRACE("arith::unconstrained", "isUnconstrained(", t, ") => true (subterm)");
5900  return true;
5901  }
5902  }
5903  } else {
5904  Expr c, var;
5905  separateMonomial(t, c, var);
5906  if (var.isRational()) {
5907  TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false (rational)");
5908  return false;
5909  }
5910  if (isMult(var)) {
5911  TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false (multiplication)");
5912  return false;
5913  }
5914  if (diffLogicOnly) {
5916  return true;
5917  }
5919  return true;
5920  }
5921  }
5922  TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false");
5923  return false;
5924 }
5925 
5927  TRACE("arith::unconstrained", "updateConstrained(", t, ")");
5928  if (isIneq(t)) {
5929  updateConstrained(t[1]);
5930  } else if (isPlus(t)) {
5931  for (int i = 0; i < t.arity(); ++ i) {
5932  updateConstrained(t[i]);
5933  }
5934  } else {
5935  Expr c, var;
5936  separateMonomial(t, c, var);
5937  if (var.isRational() || isMult(var)) {
5938  return;
5939  }
5940  if (c.getRational() < 0) {
5941  d_varConstrainedMinus[var] = true;
5942  } else {
5943  d_varConstrainedPlus[var] = true;
5944  }
5945  }
5946 }