CVC3  2.4.1
theory_arith3.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith3.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_arith3.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 
33 
34 using namespace std;
35 using namespace CVC3;
36 
37 
38 ///////////////////////////////////////////////////////////////////////////////
39 // TheoryArith3::FreeConst Methods //
40 ///////////////////////////////////////////////////////////////////////////////
41 
42 namespace CVC3 {
43 
44 ostream& operator<<(ostream& os, const TheoryArith3::FreeConst& fc) {
45  os << "FreeConst(r=" << fc.getConst() << ", "
46  << (fc.strict()? "strict" : "non-strict") << ")";
47  return os;
48 }
49 
50 ///////////////////////////////////////////////////////////////////////////////
51 // TheoryArith3::Ineq Methods //
52 ///////////////////////////////////////////////////////////////////////////////
53 
54 ostream& operator<<(ostream& os, const TheoryArith3::Ineq& ineq) {
55  os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
56  << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
57  << ineq.getConst() << ")";
58  return os;
59 }
60 } // End of namespace CVC3
61 
62 
63 ///////////////////////////////////////////////////////////////////////////////
64 // TheoryArith3 Private Methods //
65 ///////////////////////////////////////////////////////////////////////////////
66 
67 
68 Theorem TheoryArith3::isIntegerThm(const Expr& e) {
69  // Quick check
70  if(isReal(e.getType())) return Theorem();
71  // Try harder
72  return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
73 }
74 
75 
76 Theorem TheoryArith3::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
77  const Expr& e = thm.getExpr();
78  // We found it!
79  if(e == isIntE) return thm;
80 
81  Theorem res;
82  // If the theorem is an AND, look inside each child
83  if(e.isAnd()) {
84  int i, iend=e.arity();
85  for(i=0; i<iend; ++i) {
86  res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
87  if(!res.isNull()) return res;
88  }
89  }
90  return res;
91 }
92 
93 const Rational& TheoryArith3::freeConstIneq(const Expr& ineq, bool varOnRHS) {
94  DebugAssert(isIneq(ineq), "TheoryArith3::freeConstIneq("+ineq.toString()+")");
95  const Expr& e = varOnRHS? ineq[0] : ineq[1];
96 
97  switch(e.getKind()) {
98  case PLUS:
99  return e[0].getRational();
100  case RATIONAL_EXPR:
101  return e.getRational();
102  default: { // MULT, DIV, or Variable
103  static Rational zero(0);
104  return zero;
105  }
106  }
107 }
108 
109 
111 TheoryArith3::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
112  bool& subsumed) {
113  TRACE("arith ineq", "TheoryArith3::updateSubsumptionDB(", ineq,
114  ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
115  DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArith3::updateSubsumptionDB("
116  +ineq.toString()+")");
117  // Indexing expression: same as ineq only without the free const
118  Expr index;
119  const Expr& t = varOnRHS? ineq[0] : ineq[1];
120  bool strict(isLT(ineq));
121  Rational c(0);
122  if(isPlus(t)) {
123  DebugAssert(t.arity() >= 2, "TheoryArith3::updateSubsumptionDB("
124  +ineq.toString()+")");
125  c = t[0].getRational(); // Extract the free const in ineq
126  Expr newT;
127  if(t.arity() == 2) {
128  newT = t[1];
129  } else {
130  vector<Expr> kids;
131  Expr::iterator i=t.begin(), iend=t.end();
132  for(++i; i!=iend; ++i) kids.push_back(*i);
133  DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
134  +", ineq = "+ineq.toString());
135  newT = plusExpr(kids);
136  }
137  if(varOnRHS)
138  index = leExpr(newT, ineq[1]);
139  else
140  index = leExpr(ineq[0], newT);
141  } else if(isRational(t)) {
142  c = t.getRational();
143  if(varOnRHS)
144  index = leExpr(rat(0), ineq[1]);
145  else
146  index = leExpr(ineq[0], rat(0));
147  } else if(isLT(ineq))
148  index = leExpr(ineq[0], ineq[1]);
149  else
150  index = ineq;
151  // Now update the database, check for subsumption, and extract the constant
152  CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index),
153  iend=d_freeConstDB.end();
154  if(i == iend) {
155  subsumed = false;
156  // Create a new entry
157  CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
158  obj = FreeConst(c,strict);
159  TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
160  return obj.get();
161  } else {
162  CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
163  const FreeConst& fc = obj.get();
164  if(varOnRHS) {
165  subsumed = (c < fc.getConst() ||
166  (c == fc.getConst() && (!strict || fc.strict())));
167  } else {
168  subsumed = (c > fc.getConst() ||
169  (c == fc.getConst() && (strict || !fc.strict())));
170  }
171  if(!subsumed) {
172  obj = FreeConst(c,strict);
173  TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
174  }
175  return obj.get();
176  }
177 }
178 
179 
180 bool TheoryArith3::kidsCanonical(const Expr& e) {
181  if(isLeaf(e)) return true;
182  bool res(true);
183  for(int i=0; res && i<e.arity(); ++i) {
184  Expr simp(canon(e[i]).getRHS());
185  res = (e[i] == simp);
186  IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
187  << "\nsimplified = " << simp << endl;)
188  }
189  return res;
190 }
191 
192 
193 ///////////////////////////////////////////////////////////////////////////////
194 // //
195 // Function: TheoryArith3::canon //
196 // Author: Clark Barrett, Vijay Ganesh. //
197 // Created: Sat Feb 8 14:46:32 2003 //
198 // Description: Compute a canonical form for expression e and return a //
199 // theorem that e is equal to its canonical form. //
200 // Note that canonical form for arith expressions is one of the following: //
201 // 1. rational constant //
202 // 2. arithmetic leaf //
203 // (i.e. variable or term from some other theory) //
204 // 3. (MULT rat leaf) //
205 // where rat is a non-zero rational constant, leaf is an arithmetic leaf //
206 // 4. (PLUS const term_0 term_1 ... term_n) //
207 // where each term_i is either a leaf or (MULT rat leaf) //
208 // and each leaf in term_i must be strictly greater than the leaf in //
209 // term_{i+1}. //
210 // //
211 ///////////////////////////////////////////////////////////////////////////////
212 Theorem TheoryArith3::canon(const Expr& e)
213 {
214  TRACE("arith canon","canon(",e,") {");
215  DebugAssert(kidsCanonical(e), "TheoryArith3::canon("+e.toString()+")");
216  Theorem result;
217  switch (e.getKind()) {
218  case UMINUS: {
219  Theorem thm = d_rules->uMinusToMult(e[0]);
220  Expr e2 = thm.getRHS();
221  result = transitivityRule(thm, canon(e2));
222  }
223  break;
224  case PLUS: /* {
225  Theorem plusThm, plusThm1;
226  plusThm = d_rules->canonFlattenSum(e);
227  plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS());
228  result = transitivityRule(plusThm,plusThm1);
229  }
230  */
231  result = d_rules->canonPlus(e);
232  break;
233  case MINUS: {
234  DebugAssert(e.arity() == 2,"");
235  Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
236  // this produces e0 + (-1)*e1; we have to canonize it in 2 steps
237  Expr sum(minus_eq_sum.getRHS());
238  Theorem thm(canon(sum[1]));
239  if(thm.getLHS() == thm.getRHS())
240  result = canonThm(minus_eq_sum);
241  // The sum changed; do the work
242  else {
243  vector<unsigned> changed;
244  vector<Theorem> thms;
245  changed.push_back(1);
246  thms.push_back(thm);
247  Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
248  result = transitivityRule(minus_eq_sum, sum_eq_canon);
249  }
250  break;
251  }
252 
253  case MULT:
254  result = d_rules->canonMult(e);
255  break;
256  /*
257  case MULT: {
258  Theorem thmMult, thmMult1;
259  Expr exprMult;
260  Expr e0 = e[0];
261  Expr e1 = e[1];
262  if(e0.isRational()) {
263  if(rat(0) == e0)
264  result = d_rules->canonMultZero(e1);
265  else if (rat(1) == e0)
266  result = d_rules->canonMultOne(e1);
267  else
268  switch(e1.getKind()) {
269  case RATIONAL_EXPR :
270  result = d_rules->canonMultConstConst(e0,e1);
271  break;
272  case MULT:
273  DebugAssert(e1[0].isRational(),
274  "theory_arith::canon:\n "
275  "canon:MULT:MULT child is not canonical: "
276  + e1[0].toString());
277 
278  thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]);
279  result = transitivityRule(thmMult,canon(thmMult.getRHS()));
280  break;
281  case PLUS:{
282  Theorem thmPlus, thmPlus1;
283  Expr ePlus;
284  std::vector<Theorem> thmPlusVector;
285  thmPlus = d_rules->canonMultConstSum(e0,e1);
286  ePlus = thmPlus.getRHS();
287  Expr::iterator i = ePlus.begin();
288  for(;i != ePlus.end();++i)
289  thmPlusVector.push_back(canon(*i));
290  thmPlus1 = substitutivityRule(PLUS, thmPlusVector);
291  result = transitivityRule(thmPlus, thmPlus1);
292  break;
293  }
294  default:
295  result = reflexivityRule(e);
296  break;
297  }
298  }
299  else {
300  if(e1.isRational()){
301 
302  // canonMultTermConst just reverses the order of the const and the
303  // term. Then canon is called again.
304  Theorem t1 = d_rules->canonMultTermConst(e1,e0);
305  result = transitivityRule(t1,canon(t1.getRHS()));
306  }
307  else
308 
309  // This is where the assertion for non-linear multiplication is
310  // produced.
311  result = d_rules->canonMultTerm1Term2(e0,e1);
312  }
313  break;
314  }
315 
316  */
317  case DIVIDE:{
318  /*
319  case DIVIDE:{
320  if (e[1].isRational()) {
321  if (e[1].getRational() == 0)
322  throw ArithException("Divide by 0 error in "+e.toString());
323  Theorem thm = d_rules->canonDivideVar(e[0], e[1]);
324  Expr e2 = thm.getRHS();
325  result = transitivityRule(thm, canon(e2));
326  }
327  else
328  {
329  // TODO: to be handled
330  throw ArithException("Divide by a non-const not handled in "+e.toString());
331  }
332  break;
333  }
334  */
335 
336  // Division by 0 is OK (total extension, protected by TCCs)
337 // if (e[1].isRational() && e[1].getRational() == 0)
338 // throw ArithException("Divide by 0 error in "+e.toString());
339  if (e[1].getKind() == PLUS)
340  throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
341  result = d_rules->canonDivide(e);
342  break;
343  }
344  case POW:
345  if(e[1].isRational())
346  result = d_rules->canonPowConst(e);
347  else
348  result = reflexivityRule(e);
349  break;
350  default:
351  result = reflexivityRule(e);
352  break;
353  }
354  TRACE("arith canon","canon => ",result," }");
355  return result;
356 }
357 
358 
359 Theorem
360 TheoryArith3::canonSimplify(const Expr& e) {
361  TRACE("arith", "canonSimplify(", e, ") {");
362  DebugAssert(kidsCanonical(e),
363  "TheoryArith3::canonSimplify("+e.toString()+")");
364  DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
365  Expr tmp(e);
366  Theorem thm = canon(e);
367  if(thm.getRHS().hasFind())
368  thm = transitivityRule(thm, find(thm.getRHS()));
369  // We shouldn't rely on simplification in this function anymore
370  DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
371  "canonSimplify("+e.toString()+")\n"
372  +"canon(e) = "+thm.getRHS().toString()
373  +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
374 // if(tmp != thm.getRHS())
375 // thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
376 // while(tmp != thm.getRHS()) {
377 // tmp = thm.getRHS();
378 // thm = canon(thm);
379 // if(tmp != thm.getRHS())
380 // thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
381 // }
382  TRACE("arith", "canonSimplify =>", thm, " }");
383  return thm;
384 }
385 
386 /*! accepts a theorem, canonizes it, applies iffMP and substituvity to
387  * derive the canonized thm
388  */
389 Theorem
390 TheoryArith3::canonPred(const Theorem& thm) {
391  vector<Theorem> thms;
392  DebugAssert(thm.getExpr().arity() == 2,
393  "TheoryArith3::canonPred: bad theorem: "+thm.toString());
394  Expr e(thm.getExpr());
395  thms.push_back(canonSimplify(e[0]));
396  thms.push_back(canonSimplify(e[1]));
397  return iffMP(thm, substitutivityRule(e.getOp(), thms));
398 }
399 
400 /*! accepts an equivalence theorem, canonizes it, applies iffMP and
401  * substituvity to derive the canonized thm
402  */
403 Theorem
404 TheoryArith3::canonPredEquiv(const Theorem& thm) {
405  vector<Theorem> thms;
406  DebugAssert(thm.getRHS().arity() == 2,
407  "TheoryArith3::canonPredEquiv: bad theorem: "+thm.toString());
408  Expr e(thm.getRHS());
409  thms.push_back(canonSimplify(e[0]));
410  thms.push_back(canonSimplify(e[1]));
411  return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
412 }
413 
414 /*! accepts an equivalence theorem whose RHS is a conjunction,
415  * canonizes it, applies iffMP and substituvity to derive the
416  * canonized thm
417  */
418 Theorem
419 TheoryArith3::canonConjunctionEquiv(const Theorem& thm) {
420  vector<Theorem> thms;
421  return thm;
422 }
423 
424 /*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
425  * -# translate e to the form e' = 0
426  * -# if (e'.isRational()) then {if e' != 0 return false else true}
427  * -# a for loop checks if all the variables are integers.
428  * - if not isolate a suitable real variable and call processRealEq().
429  * - if all variables are integers then isolate suitable variable
430  * and call processIntEq().
431  */
432 Theorem TheoryArith3::doSolve(const Theorem& thm)
433 {
434  const Expr& e = thm.getExpr();
435  TRACE("arith eq","doSolve(",e,") {");
436  DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
437  Theorem eqnThm;
438  vector<Theorem> thms;
439  // Move LHS to the RHS, if necessary
440  if(e[0].isRational() && e[0].getRational() == 0)
441  eqnThm = thm;
442  else {
443  eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
444  eqnThm = canonPred(eqnThm);
445  }
446  // eqnThm is of the form 0 = e'
447  // 'right' is of the form e'
448  Expr right = eqnThm.getRHS();
449  // Check for trivial equation
450  if (right.isRational()) {
451  Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
452  TRACE("arith eq","doSolve => ",result," }");
453  return result;
454  }
455 
456  //normalize
457  eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
458  right = eqnThm.getRHS();
459 
460  //eqn is of the form 0 = e' and is normalized where 'right' denotes e'
461  //FIXME: change processRealEq to accept equations as well instead of theorems
462 
463  try {
464  if (isMult(right)) {
465  DebugAssert(right.arity() > 1, "Expected arity > 1");
466  if (right[0].isRational()) {
467  Rational r = right[0].getRational();
468  if (r == 0) return getCommonRules()->trueTheorem();
469  else if (r == 1) {
470  enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
471  return getCommonRules()->trueTheorem();
472  }
473  Theorem res = iffMP(eqnThm,
474  d_rules->multEqn(eqnThm.getLHS(),
475  right, rat(1/r)));
476  res = canonPred(res);
477  return doSolve(res);
478  }
479  else {
480  enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
481  return getCommonRules()->trueTheorem();
482  }
483  }
484  else if (isPow(right)) {
485  DebugAssert(right.arity() == 2, "Expected arity 2");
486  if (right[0].isRational()) {
487  return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
488  }
489  throw ArithException("Can't solve exponential eqn: "+eqnThm.toString());
490  }
491  else {
492  if(!isInteger(right)) {
493  return processRealEq(eqnThm);
494  }
495  else {
496  return processIntEq(eqnThm);
497  }
498  }
499  } catch(ArithException& e) {
500 
501  // Nonlinear heuristics
502  Theorem res;
503  if (isPlus(right)) {
504 
505  // Search for common factor
506  if (right[0].getRational() == 0) {
507  Expr::iterator i = right.begin(), iend = right.end();
508  ++i;
509  set<Expr> factors;
510  set<Expr>::iterator is, isend;
511  getFactors(*i, factors);
512  for (++i; i != iend; ++i) {
513  set<Expr> factors2;
514  getFactors(*i, factors2);
515  for (is = factors.begin(), isend = factors.end(); is != isend; ++is) {
516  if (factors2.find(*is) == factors2.end()) {
517  factors.erase(is);
518  }
519  }
520  if (factors.empty()) break;
521  }
522  if (!factors.empty()) {
523  enqueueFact(iffMP(eqnThm, d_rules->divideEqnNonConst(rat(0), right, *(factors.begin()))));
524  return getCommonRules()->trueTheorem();
525  }
526  }
527 
528  // Solve for something
529  Expr isolated = right[1];
530  Rational coeff;
531  if (isMult(isolated) && isolated[0].isRational()) {
532  coeff = isolated[0].getRational();
533  DebugAssert(coeff != 0, "Expected nonzero coeff");
534  isolated = canon(isolated / rat(coeff)).getRHS();
535  } else coeff = 1;
536  res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff)));
537  res = canonPred(res);
538  res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(),
539  isolated, EQ));
540  res = canonPred(res);
541 
542  // Look for equal powers
543  if (isPow(res.getLHS())) {
544  Expr left = res.getLHS();
545  if (isInteger(left[0])) {
546  Rational pow = left[0].getRational();
547  if (pow > 1) {
548  right = res.getRHS();
549  if (isPow(right) && right[0] == left[0]) {
550  enqueueFact(iffMP(res, d_rules->elimPower(res.getExpr())));
551  return getCommonRules()->trueTheorem();
552  }
553  else if (right.isRational()) {
554  Rational r = right.getRational();
555  if (pow % 2 == 0 && r < 0) {
556  return iffMP(res, d_rules->evenPowerEqNegConst(res.getExpr()));
557  }
558  DebugAssert(r != 0, "Expected nonzero const");
559  Rational root = ratRoot(r, pow.getUnsigned());
560  if (root != 0) {
561  enqueueFact(iffMP(res, d_rules->elimPowerConst(res.getExpr(), root)));
562  return getCommonRules()->trueTheorem();
563  }
564  else if (isInt(left[1].getType())) {
565  Theorem isIntx(isIntegerThm(left[1]));
566  DebugAssert(!isIntx.isNull(), "left = "+left.toString());
567  return iffMP(res, d_rules->intEqIrrational(res.getExpr(), isIntx));
568  }
569  }
570  }
571  }
572  }
573  }
574  else {
575  res = symmetryRule(eqnThm); // Flip to e' = 0
576  }
577  TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
578  IF_DEBUG(debugger.counter("FAILED to solve equalities")++;)
579  setIncomplete("Non-linear arithmetic equalities");
580  return res;
581  }
582  FatalAssert(false, "");
583  return Theorem();
584 }
585 
586 /*! pick a monomial for the input equation. This function is used only
587  * if the equation is an integer equation. Choose the monomial with
588  * the smallest absolute value of coefficient.
589  */
590 bool TheoryArith3::pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin)
591 {
592  DebugAssert(isPlus(right) && right.arity() > 1,
593  "TheoryArith3::pickIntEqMonomial right is wrong :-): " +
594  right.toString());
595  DebugAssert(right[0].isRational(),
596  "TheoryArith3::pickIntEqMonomial. right[0] must be const" +
597  right.toString());
598  DebugAssert(isInteger(right),
599  "TheoryArith3::pickIntEqMonomial: right is of type int: " +
600  right.toString());
601  //right is of the form "C + a1x1 + ... + anxn". min is initialized
602  //to a1
603  Expr::iterator istart = right.begin(), iend = right.end();
604  istart++;
605  Expr::iterator i = istart, j;
606  bool found = false;
607  nonlin = false;
608  Rational min, coeff;
609  Expr leaf;
610  for(; i != iend; ++i) {
611  if (isLeaf(*i)) {
612  leaf = *i;
613  coeff = 1;
614  }
615  else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
616  leaf = (*i)[1];
617  coeff = abs((*i)[0].getRational());
618  }
619  else {
620  nonlin = true;
621  continue;
622  }
623  for (j = istart; j != iend; ++j) {
624  if (j != i && isLeafIn(leaf, *j)) break;
625  }
626  if (j == iend) {
627  if (!found || min > coeff) {
628  min = coeff;
629  isolated = *i;
630  found = true;
631  }
632  }
633  }
634  return found;
635 }
636 
637 /*! input is 0=e' Theorem and some of the vars in e' are of
638  * type REAL. isolate one of them and send back to framework. output
639  * is "var = e''" Theorem.
640  */
641 Theorem
642 TheoryArith3::processRealEq(const Theorem& eqn)
643 {
644  DebugAssert(eqn.getLHS().isRational() &&
645  eqn.getLHS().getRational() == 0,
646  "processRealEq invariant violated");
647  Expr right = eqn.getRHS();
648  // Find variable to isolate and store it in left. Pick the largest
649  // (according to the total ordering) variable. FIXME: change from
650  // total ordering to the ordering we devised for inequalities.
651 
652  // TODO: I have to pick a variable that appears as a variable in the
653  // term but does not appear as a variable anywhere else. The variable
654  // must appear as a single leaf and not in a MULT expression with some
655  // other variables and nor in a POW expression.
656 
657  bool found = false;
658 
659  Expr left;
660 
661  if (isPlus(right)) {
662  for(int i = right.arity()-1; i>=0; --i) {
663  Expr c = right[i];
664  if(isRational(c))
665  continue;
666  if(!isInteger(c)) {
667  if (isLeaf(c) ||
668  ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
669  int numoccurs = 0;
670  Expr leaf = isLeaf(c) ? c : c[1];
671  for (int j = 0; j < right.arity(); ++j) {
672  if (j!= i
673  && isLeafIn(leaf, right[j])
674  ) {
675  numoccurs++;
676  break;
677  }
678  }
679  if (!numoccurs) {
680  left = c;
681  found = true;
682  break;
683  }
684  }
685  }
686  }
687  }
688  else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
689  isLeaf(right)) {
690  left = right;
691  found = true;
692  }
693 
694  if (!found) {
695  throw
696  ArithException("Can't find a leaf for solve in "+eqn.toString());
697  }
698 
699  Rational r = -1;
700  if (isMult(left)) {
701  DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
702  DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
703  r = -1/left[0].getRational();
704  left = left[1];
705  }
706 
707  DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
708  "TheoryArith3::ProcessRealEq: left is integer:\n left = "
709  +left.toString());
710  // Normalize equation so that coefficient of the monomial
711  // corresponding to "left" in eqn[1] is -1
712  Theorem result(iffMP(eqn,
713  d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
714  result = canonPred(result);
715 
716  // Isolate left
717  result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
718  result.getRHS(), left, EQ));
719  result = canonPred(result);
720  TRACE("arith","processRealEq => ",result," }");
721  return result;
722 }
723 
724 
725 void TheoryArith3::getFactors(const Expr& e, set<Expr>& factors)
726 {
727  switch (e.getKind()) {
728  case RATIONAL_EXPR: break;
729  case MULT: {
730  Expr::iterator i = e.begin(), iend = e.end();
731  for (; i != iend; ++i) {
732  getFactors(*i, factors);
733  }
734  break;
735  }
736  case POW: {
737  DebugAssert(e.arity() == 2, "invariant violated");
738  if (!isIntegerConst(e[0]) || e[0].getRational() <= 0) {
739  throw ArithException("not positive integer exponent in "+e.toString());
740  }
741  if (isLeaf(e[1])) factors.insert(e[1]);
742  break;
743  }
744  default: {
745  DebugAssert(isLeaf(e), "expected leaf");
746  DebugAssert(factors.find(e) == factors.end(), "expected new entry");
747  factors.insert(e);
748  break;
749  }
750  }
751 }
752 
753 
754 /*!
755  * \param eqn is a single equation 0 = e
756  * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
757  */
758 Theorem
759 TheoryArith3::processSimpleIntEq(const Theorem& eqn)
760 {
761  TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
762  DebugAssert(eqn.isRewrite(),
763  "TheoryArith3::processSimpleIntEq: eqn must be equality" +
764  eqn.getExpr().toString());
765 
766  Expr right = eqn.getRHS();
767 
768  DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
769  "TheoryArith3::processSimpleIntEq: LHS must be 0:\n" +
770  eqn.getExpr().toString());
771 
772  DebugAssert(!isMult(right) && !isPow(right), "should have been handled above");
773  if (isPlus(right)) {
774  if (2 == right.arity() &&
775  (isLeaf(right[1]) ||
776  (isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
777  //we take care of special cases like 0 = c + a.x, 0 = c + x,
778  Expr c,x;
779  separateMonomial(right[1], c, x);
780  Theorem isIntx(isIntegerThm(x));
781  DebugAssert(!isIntx.isNull(), "right = "+right.toString()
782  +"\n x = "+x.toString());
783  Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
784  TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
785  return res;
786  }
787  // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
788  Expr isolated;
789  bool nonlin;
790  if (pickIntEqMonomial(right, isolated, nonlin)) {
791  TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
792 
793  // First, we compute the 'sign factor' with which to multiply the
794  // eqn. if the coeff of isolated is positive (i.e. 'isolated' is
795  // of the form x or a.x where a>0 ) then r must be -1 and if coeff
796  // of 'isolated' is negative, r=1.
797  Rational r = isMult(isolated) ?
798  ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
799  Theorem result;
800  if (-1 == r) {
801  // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
802  // positive. modify eqn (0=e') to the equation (0=canon(-1*e'))
803  result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
804  result = canonPred(result);
805  Expr e = result.getRHS();
806 
807  // Isolate the 'isolated'
808  result = iffMP(result,
809  d_rules->plusPredicate(result.getLHS(),result.getRHS(),
810  isolated, EQ));
811  } else {
812  //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
813  const Rational& minusa = isolated[0].getRational();
814  Rational a = -1*minusa;
815  isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
816 
817  // Isolate the 'isolated'
818  result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
819  right,isolated,EQ));
820  }
821  // Canonize the result
822  result = canonPred(result);
823 
824  //if isolated is 'x' or 1*x, then return result else continue processing.
825  if(!isMult(isolated) || isolated[0].getRational() == 1) {
826  TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
827  return result;
828  } else if (!nonlin) {
829  DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
830  "TheoryArith3::processSimpleIntEq: isolated must be mult "
831  "with coeff >= 2.\n isolated = " + isolated.toString());
832 
833  // Compute IS_INTEGER() for lhs and rhs
834  Expr lhs = result.getLHS();
835  Expr rhs = result.getRHS();
836  Expr a, x;
837  separateMonomial(lhs, a, x);
838  Theorem isIntLHS = isIntegerThm(x);
839  vector<Theorem> isIntRHS;
840  if(!isPlus(rhs)) { // rhs is a MULT
841  Expr c, v;
842  separateMonomial(rhs, c, v);
843  isIntRHS.push_back(isIntegerThm(v));
844  DebugAssert(!isIntRHS.back().isNull(), "");
845  } else { // rhs is a PLUS
846  DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
847  DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
848  Expr::iterator i=rhs.begin(), iend=rhs.end();
849  ++i; // Skip the free constant
850  for(; i!=iend; ++i) {
851  Expr c, v;
852  separateMonomial(*i, c, v);
853  isIntRHS.push_back(isIntegerThm(v));
854  DebugAssert(!isIntRHS.back().isNull(), "");
855  }
856  }
857  // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
858  result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
859  // Skolemize the quantifier
860  result = getCommonRules()->skolemize(result);
861  // Canonize t2 and t3 generated by this rule
862  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
863  "processSimpleIntEq: result = "+result.getExpr().toString());
864  Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
865  Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
866  Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
867  if(newRes.getExpr() != result.getExpr()) result = newRes;
868 
869  TRACE("arith eq", "processSimpleIntEq => ", result, " }");
870  return result;
871  }
872  }
873  throw
874  ArithException("Can't find a leaf for solve in "+eqn.toString());
875  } else {
876  // eqn is 0 = x. Flip it and return
877  Theorem result = symmetryRule(eqn);
878  TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
879  return result;
880  }
881 }
882 
883 /*! input is 0=e' Theorem and all of the vars in e' are of
884  * type INT. isolate one of them and send back to framework. output
885  * is "var = e''" Theorem and some associated equations in
886  * solved form.
887  */
888 Theorem
889 TheoryArith3::processIntEq(const Theorem& eqn)
890 {
891  TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
892  // Equations in the solved form.
893  std::vector<Theorem> solvedAndNewEqs;
894  Theorem newEq(eqn), result;
895  bool done(false);
896  do {
897  result = processSimpleIntEq(newEq);
898  // 'result' is of the from (x1=t1) AND 0=t'
899  if(result.isRewrite()) {
900  solvedAndNewEqs.push_back(result);
901  done = true;
902  }
903  else if (result.getExpr().isBoolConst()) {
904  done = true;
905  }
906  else {
907  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
908  "TheoryArith3::processIntEq("+eqn.getExpr().toString()
909  +")\n result = "+result.getExpr().toString());
910  solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
911  newEq = getCommonRules()->andElim(result, 1);
912  }
913  } while(!done);
914  Theorem res;
915  if (result.getExpr().isFalse()) res = result;
916  else if (solvedAndNewEqs.size() > 0)
917  res = solvedForm(solvedAndNewEqs);
918  else res = result;
919  TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
920  return res;
921 }
922 
923 /*!
924  * Takes a vector of equations and for every equation x_i=t_i
925  * substitutes t_j for x_j in t_i for all j>i. This turns the system
926  * of equations into a solved form.
927  *
928  * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
929  * i<j, but not for i>=j.
930  */
931 Theorem
932 TheoryArith3::solvedForm(const vector<Theorem>& solvedEqs)
933 {
934  DebugAssert(solvedEqs.size() > 0, "TheoryArith3::solvedForm()");
935 
936  // Trace code
937  TRACE_MSG("arith eq", "TheoryArith3::solvedForm:solvedEqs(\n [");
938  IF_DEBUG(if(debugger.trace("arith eq")) {
939  for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
940  jend=solvedEqs.end(); j!=jend;++j)
941  TRACE("arith eq", "", j->getExpr(), ",\n ");
942  })
943  TRACE_MSG("arith eq", " ]) {");
944  // End of Trace code
945 
946  vector<Theorem>::const_reverse_iterator
947  i = solvedEqs.rbegin(),
948  iend = solvedEqs.rend();
949  // Substitution map: a variable 'x' is mapped to a Theorem x=t.
950  // This map accumulates the resulting solved form.
951  ExprMap<Theorem> subst;
952  for(; i!=iend; ++i) {
953  if(i->isRewrite()) {
954  Theorem thm = substAndCanonize(*i, subst);
955  TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
956  thm.getExpr(), "");
957  subst[i->getLHS()] = thm;
958  }
959  else {
960  // This is the FALSE case: just return the contradiction
961  DebugAssert(i->getExpr().isFalse(),
962  "TheoryArith3::solvedForm: an element of solvedEqs must "
963  "be either EQ or FALSE: "+i->toString());
964  return *i;
965  }
966  }
967  // Now we've collected the solved form in 'subst'. Wrap it up into
968  // a conjunction and return.
969  vector<Theorem> thms;
970  for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
971  i!=iend; ++i)
972  thms.push_back(i->second);
973  if (thms.size() > 1)
974  return getCommonRules()->andIntro(thms);
975  else
976  return thms.back();
977 }
978 
979 
980 /*!
981  * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
982  * element of subst is a fully canonized equation of the form x=e,
983  * indexed by the LHS variable.
984  */
985 
986 Theorem
987 TheoryArith3::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
988 {
989  TRACE("arith eq", "substAndCanonize(", t, ") {");
990  // Quick and dirty check: return immediately if subst is empty
991  if(subst.empty()) {
992  Theorem res(reflexivityRule(t));
993  TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
994  return res;
995  }
996  // Check if we can substitute 't' directly
997  ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
998  if(i!=iend) {
999  TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
1000  return i->second;
1001  }
1002  // The base case: t is an i-leaf
1003  if(isLeaf(t)) {
1004  Theorem res(reflexivityRule(t));
1005  TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
1006  return res;
1007  }
1008  // 't' is an arithmetic term; recurse into the children
1009  vector<Theorem> thms;
1010  vector<unsigned> changed;
1011  for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
1012  Theorem thm = substAndCanonize(t[j], subst);
1013  if(thm.getRHS() != t[j]) {
1014  thm = canonThm(thm);
1015  thms.push_back(thm);
1016  changed.push_back(j);
1017  }
1018  }
1019  // Do the actual substitution and canonize the result
1020  Theorem res;
1021  if(thms.size() > 0) {
1022  res = substitutivityRule(t, changed, thms);
1023  res = canonThm(res);
1024  }
1025  else
1026  res = reflexivityRule(t);
1027  TRACE("arith eq", "substAndCanonize => ", res, " }");
1028  return res;
1029 }
1030 
1031 
1032 /*!
1033  * ASSUMPTION: 't' is a fully canonized equation of the form x = t,
1034  * and so is every element of subst, indexed by the LHS variable.
1035  */
1036 
1037 Theorem
1038 TheoryArith3::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
1039 {
1040  // Quick and dirty check: return immediately if subst is empty
1041  if(subst.empty()) return eq;
1042 
1043  DebugAssert(eq.isRewrite(), "TheoryArith3::substAndCanonize: t = "
1044  +eq.getExpr().toString());
1045  const Expr& t = eq.getRHS();
1046  // Do the actual substitution in the term t
1047  Theorem thm = substAndCanonize(t, subst);
1048  // Substitution had no result: return the original equation
1049  if(thm.getRHS() == t) return eq;
1050  // Otherwise substitute the result into the equation
1051  vector<Theorem> thms;
1052  vector<unsigned> changed;
1053  thms.push_back(thm);
1054  changed.push_back(1);
1055  return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
1056 }
1057 
1058 
1059 void TheoryArith3::processBuffer()
1060 {
1061  // Process the inequalities in the buffer
1062  bool varOnRHS;
1063 
1064  for(; !inconsistent() && d_bufferIdx < d_buffer.size();
1065  d_bufferIdx = d_bufferIdx+1) {
1066  const Theorem& ineqThm = d_buffer[d_bufferIdx];
1067  // Skip this inequality if it is stale
1068  if(isStale(ineqThm.getExpr())) continue;
1069  Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
1070  const Expr& ineq = thm1.getExpr();
1071  if((ineq).isFalse())
1072  setInconsistent(thm1);
1073  else if(!ineq.isTrue()) {
1074  // Check that the variable is indeed isolated correctly
1075  DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]),
1076  "TheoryArith3::processBuffer(): bad result from "
1077  "isolateVariable:\nineq = "+ineq.toString());
1078  // and project the inequality
1079  projectInequalities(thm1, varOnRHS);
1080  }
1081  }
1082 }
1083 
1084 
1085 void TheoryArith3::updateStats(const Rational& c, const Expr& v)
1086 {
1087  TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
1088 
1089  // Dejan: update the max coefficient of the variable
1090  if (c < 0) {
1091  // Goes to the left side
1092  CDMap<Expr, Rational>::iterator maxFind = maxCoefficientLeft.find(v);
1093  if (maxFind == maxCoefficientLeft.end())
1094  maxCoefficientLeft[v] = - c;
1095  else
1096  if ((*maxFind).second < -c)
1097  (*maxFind).second = -c;
1098  } else {
1099  // Stays on the right side
1100  CDMap<Expr, Rational>::iterator maxFind = maxCoefficientRight.find(v);
1101  if (maxFind == maxCoefficientRight.end())
1102  maxCoefficientRight[v] = c;
1103  else
1104  if((*maxFind).second < c)
1105  (*maxFind).second = c;
1106  }
1107 
1108  if(c > 0) {
1109  if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
1110  else d_countRight[v] = 1;
1111  }
1112  else
1113  if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
1114  else d_countLeft[v] = 1;
1115 }
1116 
1117 
1118 void TheoryArith3::updateStats(const Expr& monomial)
1119 {
1120  Expr c, m;
1121  separateMonomial(monomial, c, m);
1122  updateStats(c.getRational(), m);
1123 }
1124 
1125 
1126 void TheoryArith3::addToBuffer(const Theorem& thm) {
1127  // First, turn the inequality into 0 < rhs
1128  // FIXME: check if this can be optimized away
1129  Theorem result(thm);
1130  const Expr& e = thm.getExpr();
1131  // int kind = e.getKind();
1132  if(!(e[0].isRational() && e[0].getRational() == 0)) {
1133  result = iffMP(result, d_rules->rightMinusLeft(e));
1134  result = canonPred(result);
1135  }
1136  TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
1137  // Push it into the buffer
1138  d_buffer.push_back(thm);
1139 
1140  // Collect the statistics about variables
1141  const Expr& rhs = thm.getExpr()[1];
1142  if(isPlus(rhs))
1143  for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
1144  updateStats(*i);
1145  else // It's a monomial
1146  updateStats(rhs);
1147 }
1148 
1149 
1150 Theorem TheoryArith3::isolateVariable(const Theorem& inputThm,
1151  bool& isolatedVarOnRHS)
1152 {
1153  Theorem result(inputThm);
1154  const Expr& e = inputThm.getExpr();
1155  TRACE("arith","isolateVariable(",e,") {");
1156  TRACE("arith ineq", "isolateVariable(", e, ") {");
1157  //we assume all the children of e are canonized
1158  DebugAssert(isLT(e)||isLE(e),
1159  "TheoryArith3::isolateVariable: " + e.toString() +
1160  " wrong kind");
1161  int kind = e.getKind();
1162  DebugAssert(e[0].isRational() && e[0].getRational() == 0,
1163  "TheoryArith3::isolateVariable: theorem must be of "
1164  "the form 0 < rhs: " + inputThm.toString());
1165 
1166  const Expr& zero = e[0];
1167  Expr right = e[1];
1168  // Check for trivial in-equation.
1169  if (right.isRational()) {
1170  result = iffMP(result, d_rules->constPredicate(e));
1171  TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
1172  TRACE("arith","isolateVariable => ",result," }");
1173  return result;
1174  }
1175 
1176  // Normalization of inequality to make coefficients integer and
1177  // relatively prime.
1178 
1179  Expr factor(computeNormalFactor(right));
1180  TRACE("arith", "isolateVariable: factor = ", factor, "");
1181  DebugAssert(factor.getRational() > 0,
1182  "isolateVariable: factor="+factor.toString());
1183  // Now multiply the inequality by the factor, unless it is 1
1184  if(factor.getRational() != 1) {
1185  result = iffMP(result, d_rules->multIneqn(e, factor));
1186  // And canonize the result
1187  result = canonPred(result);
1188  right = result.getExpr()[1];
1189  }
1190 
1191  // Find monomial to isolate and store it in isolatedMonomial
1192  Expr isolatedMonomial = right;
1193 
1194  if (isPlus(right))
1195  isolatedMonomial = pickMonomial(right);
1196 
1197  Rational r = -1;
1198  isolatedVarOnRHS = true;
1199  if (isMult(isolatedMonomial)) {
1200  r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
1201  isolatedVarOnRHS =
1202  ((isolatedMonomial[0].getRational()) >= 0)? true : false;
1203  }
1204  isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
1205  // Isolate isolatedMonomial on to the LHS
1206  result = iffMP(result, d_rules->plusPredicate(zero, right,
1207  isolatedMonomial, kind));
1208  // Canonize the resulting inequality
1209  result = canonPred(result);
1210  if(1 != r) {
1211  result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
1212  result = canonPred(result);
1213  }
1214  TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
1215  TRACE("arith","isolateVariable => ",result," }");
1216  return result;
1217 }
1218 
1219 Expr
1220 TheoryArith3::computeNormalFactor(const Expr& right) {
1221  // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
1222  // of the form c1/d1*x1 + ... + cn/dn*xn
1223  Rational factor;
1224  if(isPlus(right)) {
1225  vector<Rational> nums, denoms;
1226  for(int i=0, iend=right.arity(); i<iend; ++i) {
1227  switch(right[i].getKind()) {
1228  case RATIONAL_EXPR: {
1229  Rational c(abs(right[i].getRational()));
1230  nums.push_back(c.getNumerator());
1231  denoms.push_back(c.getDenominator());
1232  break;
1233  }
1234  case MULT: {
1235  Rational c(abs(right[i][0].getRational()));
1236  nums.push_back(c.getNumerator());
1237  denoms.push_back(c.getDenominator());
1238  break;
1239  }
1240  default: // it's a variable
1241  nums.push_back(1);
1242  denoms.push_back(1);
1243  break;
1244  }
1245  }
1246  Rational gcd_nums = gcd(nums);
1247  // x/0 == 0 in our model, as a total extension of arithmetic. The
1248  // particular value of x/0 is irrelevant, since the DP is guarded
1249  // by the top-level TCCs, and it is safe to return any value in
1250  // cases when terms are undefined.
1251  factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
1252  } else if(isMult(right)) {
1253  const Rational& r = right[0].getRational();
1254  factor = (r==0)? 0 : (1/abs(r));
1255  }
1256  else
1257  factor = 1;
1258  return rat(factor);
1259 }
1260 
1261 
1262 bool TheoryArith3::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
1263 {
1264  DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
1265  "TheoryArith3::findMaxVar: isolatedMonomial cannot be rational" +
1266  isolatedMonomial.toString());
1267  Expr c, var0, var1;
1268  separateMonomial(isolatedMonomial, c, var0);
1269  separateMonomial(var2, c, var1);
1270  return var0 < var1;
1271 }
1272 
1273 /*! "Stale" means it contains non-simplified subexpressions. For
1274  * terms, it checks the expression's find pointer; for formulas it
1275  * checks the children recursively (no caching!). So, apply it with
1276  * caution, and only to simple atomic formulas (like inequality).
1277  */
1278 bool TheoryArith3::isStale(const Expr& e) {
1279  if(e.isTerm())
1280  return e != find(e).getRHS();
1281  // It's better be a simple predicate (like inequality); we check the
1282  // kids recursively
1283  bool stale=false;
1284  for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
1285  stale = isStale(*i);
1286  return stale;
1287 }
1288 
1289 
1290 bool TheoryArith3::isStale(const TheoryArith3::Ineq& ineq) {
1291  TRACE("arith ineq", "isStale(", ineq, ") {");
1292  const Expr& ineqExpr = ineq.ineq().getExpr();
1293  const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
1294  bool strict(isLT(ineqExpr));
1295  const FreeConst& fc = ineq.getConst();
1296 
1297  bool subsumed;
1298 
1299  if(ineq.varOnRHS()) {
1300  subsumed = (c < fc.getConst() ||
1301  (c == fc.getConst() && !strict && fc.strict()));
1302  } else {
1303  subsumed = (c > fc.getConst() ||
1304  (c == fc.getConst() && strict && !fc.strict()));
1305  }
1306 
1307  bool res;
1308  if(subsumed) {
1309  res = true;
1310  TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
1311  }
1312  else {
1313  res = isStale(ineqExpr);
1314  TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
1315  }
1316  return res;
1317 }
1318 
1319 
1320 void TheoryArith3::separateMonomial(const Expr& e, Expr& c, Expr& var) {
1321  TRACE("separateMonomial", "separateMonomial(", e, ")");
1322  DebugAssert(!isPlus(e),
1323  "TheoryArith3::separateMonomial(e = "+e.toString()+")");
1324  if(isMult(e)) {
1325  DebugAssert(e.arity() >= 2,
1326  "TheoryArith3::separateMonomial(e = "+e.toString()+")");
1327  c = e[0];
1328  if(e.arity() == 2) var = e[1];
1329  else {
1330  vector<Expr> kids = e.getKids();
1331  kids[0] = rat(1);
1332  var = multExpr(kids);
1333  }
1334  } else {
1335  c = rat(1);
1336  var = e;
1337  }
1338  DebugAssert(c.isRational(), "TheoryArith3::separateMonomial(e = "
1339  +e.toString()+", c = "+c.toString()+")");
1340  DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
1341  "TheoryArith3::separateMonomial(e = "
1342  +e.toString()+", var = "+var.toString()+")");
1343 }
1344 
1345 
1346 void TheoryArith3::projectInequalities(const Theorem& theInequality,
1347  bool isolatedVarOnRHS)
1348 {
1349  TRACE("arith ineq", "projectInequalities(", theInequality.getExpr(),
1350  ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
1351  +") {");
1352  DebugAssert(isLE(theInequality.getExpr()) ||
1353  isLT(theInequality.getExpr()),
1354  "TheoryArith3::projectIsolatedVar: "\
1355  "theInequality is of the wrong form: " +
1356  theInequality.toString());
1357  //TODO: DebugAssert to check if the isolatedMonomial is of the right
1358  //form and the whether we are indeed getting inequalities.
1359  Theorem theIneqThm(theInequality);
1360  Expr theIneq = theIneqThm.getExpr();
1361 
1362  Theorem isIntLHS(isIntegerThm(theIneq[0]));
1363  Theorem isIntRHS(isIntegerThm(theIneq[1]));
1364  bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
1365  // If the inequality is strict and integer, change it to non-strict
1366  if(isLT(theIneq) && isInt) {
1367  Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
1368  !isolatedVarOnRHS);
1369  theIneqThm = canonPred(iffMP(theIneqThm, thm));
1370  theIneq = theIneqThm.getExpr();
1371  }
1372  Expr isolatedMonomial =
1373  isolatedVarOnRHS ? theIneq[1] : theIneq[0];
1374 
1375  Expr monomialVar, a;
1376  separateMonomial(isolatedMonomial, a, monomialVar);
1377 
1378  bool subsumed;
1379  const FreeConst& bestConst =
1380  updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
1381 
1382  if(subsumed) {
1383  IF_DEBUG(debugger.counter("subsumed inequalities")++;)
1384  TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
1385  } else {
1386  // If the isolated variable is actually a non-linear term, we are
1387  // incomplete
1388  if(isMult(monomialVar) || isPow(monomialVar))
1389  setIncomplete("Non-linear arithmetic inequalities");
1390 
1391  // First, we need to make sure the isolated inequality is
1392  // setup properly.
1393  // setupRec(theIneq[0]);
1394  // setupRec(theIneq[1]);
1395  theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
1396  theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
1397  // Add the inequality into the appropriate DB.
1398  ExprMap<CDList<Ineq> *>& db1 =
1399  isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
1400  ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
1401  if(it1 == db1.end()) {
1402  CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
1403  list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1404  db1[monomialVar] = list;
1405  }
1406  else
1407  ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1408 
1409  ExprMap<CDList<Ineq> *>& db2 =
1410  isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
1411  ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
1412  if(it == db2.end()) {
1413  TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
1414  return;
1415  }
1416 
1417  CDList<Ineq>& listOfDBIneqs = *((*it).second);
1418  Theorem betaLTt, tLTalpha, thm;
1419  for(size_t i = 0, iend=listOfDBIneqs.size(); i!=iend; ++i) {
1420  const Ineq& ineqEntry = listOfDBIneqs[i];
1421  const Theorem& ineqThm = ineqEntry.ineq();
1422  if(!isStale(ineqEntry)) {
1423  betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
1424  tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
1425  thm = normalizeProjectIneqs(betaLTt, tLTalpha);
1426 
1427  IF_DEBUG(debugger.counter("real shadows")++;)
1428 
1429  // Check for TRUE and FALSE theorems
1430  Expr e(thm.getExpr()); if(e.isFalse()) {
1431  setInconsistent(thm);
1432  TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
1433  return;
1434  }
1435  else {
1436  if(!e.isTrue() && !e.isEq())
1437  addToBuffer(thm);
1438  else if(e.isEq())
1439  enqueueFact(thm);
1440  }
1441  } else {
1442  IF_DEBUG(debugger.counter("stale inequalities")++;)
1443  }
1444  }
1445  }
1446  TRACE_MSG("arith ineq", "projectInequalities => }");
1447 }
1448 
1449 Theorem TheoryArith3::normalizeProjectIneqs(const Theorem& ineqThm1,
1450  const Theorem& ineqThm2)
1451 {
1452  //ineq1 is of the form beta < b.x or beta < x [ or with <= ]
1453  //ineq2 is of the form a.x < alpha or x < alpha.
1454  Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
1455  Expr ineq1 = betaLTt.getExpr();
1456  Expr ineq2 = tLTalpha.getExpr();
1457  Expr c,x;
1458  separateMonomial(ineq2[0], c, x);
1459  Theorem isIntx(isIntegerThm(x));
1460  Theorem isIntBeta(isIntegerThm(ineq1[0]));
1461  Theorem isIntAlpha(isIntegerThm(ineq2[1]));
1462  bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
1463 
1464  TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
1465  ", "+ineq2.toString()+") {");
1466  DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
1467  (isLE(ineq2) || isLT(ineq2)),
1468  "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
1469  ineq1.toString() + ineq2.toString());
1470  DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
1471  "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
1472  ineq1.toString() + ineq2.toString());
1473 
1474  //compute the factors to multiply the two inequalities with
1475  //so that they get the form beta < t and t < alpha.
1476  Rational factor1 = 1, factor2 = 1;
1477  Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
1478  Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
1479  if(b != a) {
1480  factor1 = a;
1481  factor2 = b;
1482  }
1483 
1484  //if the ineqs are of type int then apply one of the gray
1485  //dark shadow rules.
1486  // FIXME: intResult should also be checked for immediate
1487  // optimizations, as those below for 'result'. Also, if intResult
1488  // is a single inequality, we may want to handle it similarly to the
1489  // 'result' rather than enqueuing directly.
1490  if(isInt && (a >= 2 || b >= 2)) {
1491  Theorem intResult;
1492  if(a <= b)
1493  intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
1494  isIntAlpha, isIntBeta, isIntx);
1495  else
1496  intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
1497  isIntAlpha, isIntBeta, isIntx);
1498  enqueueFact(intResult);
1499  // Fetch dark and gray shadows
1500  const Expr& DorG = intResult.getExpr();
1501  DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
1502  const Expr& D = DorG[0];
1503  const Expr& G = DorG[1];
1504  DebugAssert(D.getKind()==DARK_SHADOW, "D = "+D.toString());
1505  DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
1506  // Set the higher splitter priority for dark shadow
1507  Expr tmp = simplifyExpr(D);
1508  if (!tmp.isBoolConst())
1509  addSplitter(tmp, 5);
1510  // Also set a higher priority to the NEGATION of GRAY_SHADOW
1511  tmp = simplifyExpr(!G);
1512  if (!tmp.isBoolConst())
1513  addSplitter(tmp, 1);
1514  IF_DEBUG(debugger.counter("dark+gray shadows")++;)
1515  }
1516 
1517  //actually normalize the inequalities
1518  if(1 != factor1) {
1519  std::vector<Theorem> thms1;
1520  Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
1521  betaLTt = canonPred(thm2);
1522  ineq1 = betaLTt.getExpr();
1523  }
1524  if(1 != factor2) {
1525  std::vector<Theorem> thms1;
1526  Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
1527  tLTalpha = canonPred(thm2);
1528  ineq2 = tLTalpha.getExpr();
1529  }
1530 
1531  //IF_DEBUG(debugger.counter("real shadows")++;)
1532 
1533  Expr beta(ineq1[0]);
1534  Expr alpha(ineq2[1]);
1535  // In case of alpha <= t <= alpha, we generate t = alpha
1536  if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
1537  Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
1538  TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1539  return result;
1540  }
1541 
1542  // Check if this inequality is a finite interval
1543  if(isInt)
1544  processFiniteInterval(betaLTt, tLTalpha);
1545 
1546  //project the normalized inequalities.
1547 
1548  Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
1549 
1550  // FIXME: Clark's changes. Is 'rewrite' more or less efficient?
1551 // result = iffMP(result, rewrite(result.getExpr()));
1552 // TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1553 
1554  // Now, transform the result into 0 < rhs and see if rhs is a const
1555  Expr e(result.getExpr());
1556  // int kind = e.getKind();
1557  if(!(e[0].isRational() && e[0].getRational() == 0)) {
1558  result = iffMP(result, d_rules->rightMinusLeft(e));
1559  result = canonPred(result);
1560  }
1561 
1562  //result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
1563  Expr right = result.getExpr()[1];
1564  // Check for trivial inequality
1565  if (right.isRational())
1566  result = iffMP(result, d_rules->constPredicate(result.getExpr()));
1567  TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
1568  return result;
1569 }
1570 
1571 Rational TheoryArith3::currentMaxCoefficient(Expr var)
1572 {
1573  bool foundLeft = false;
1574  bool foundRight = false;
1575  Rational leftMax = 1;
1576  Rational rightMax = 1;
1577 
1578  // If the coefitient was found earlier and fixed, just return it
1579  CDMap<Expr, Rational>::iterator findFixed = fixedMaxCoefficient.find(var);
1580  if (findFixed != fixedMaxCoefficient.end())
1581  return (*findFixed).second;
1582 
1583  // Find the biggest left side coefficient
1584  CDMap<Expr, Rational>::iterator findMaxLeft = maxCoefficientLeft.find(var);
1585  if (findMaxLeft != maxCoefficientLeft.end()) {
1586  foundLeft = true;
1587  leftMax = (*findMaxLeft).second;
1588  }
1589 
1590  //
1591  CDMap<Expr, Rational>::iterator findMaxRight = maxCoefficientRight.find(var);
1592  if (findMaxRight != maxCoefficientRight.end()) {
1593  foundRight = true;
1594  rightMax = (*findMaxRight).second;
1595  }
1596 
1597  if (foundLeft && foundRight) {
1598  if (leftMax < rightMax) return rightMax;
1599  else return leftMax;
1600  }
1601 
1602  return Rational(1) / (leftMax * rightMax);
1603 }
1604 
1605 void TheoryArith3::fixCurrentMaxCoefficient(Expr var, Rational max) {
1606  fixedMaxCoefficient[var] = max;
1607 }
1608 
1609 void TheoryArith3::selectSmallestByCoefficient(vector<Expr> input, vector<Expr>& output) {
1610 
1611  // Clear the output vector
1612  output.clear();
1613 
1614  // Get the first variable, and set it as best
1615  Expr best_variable = input[0];
1616  Rational best_coefficient = currentMaxCoefficient(best_variable);
1617  output.push_back(best_variable);
1618 
1619  for(unsigned int i = 1; i < input.size(); i ++) {
1620 
1621  // Get the current variable
1622  Expr current_variable = input[i];
1623  // Get the current variable's max coefficient
1624  Rational current_coefficient = currentMaxCoefficient(current_variable);
1625 
1626  // If strictly better than the current best, remember it
1627  if ((current_coefficient < best_coefficient)) {
1628  best_variable = current_variable;
1629  best_coefficient = current_coefficient;
1630  output.clear();
1631  }
1632 
1633  // If equal to the current best, push it to the stack
1634  if (current_coefficient == best_coefficient)
1635  output.push_back(current_variable);
1636  }
1637 
1638  // Fix the selected best coefficient
1639  fixCurrentMaxCoefficient(best_variable, best_coefficient);
1640 }
1641 
1642 Expr TheoryArith3::pickMonomial(const Expr& right)
1643 {
1644  DebugAssert(isPlus(right), "TheoryArith3::pickMonomial: Wrong Kind: " +
1645  right.toString());
1646  if(theoryCore()->getFlags()["var-order"].getBool()) {
1647  Expr::iterator i = right.begin();
1648  Expr isolatedMonomial = right[1];
1649  //PLUS always has at least two elements and the first element is
1650  //always a constant. hence ++i in the initialization of the for
1651  //loop.
1652  for(++i; i != right.end(); ++i)
1653  if(lessThanVar(isolatedMonomial,*i))
1654  isolatedMonomial = *i;
1655  return isolatedMonomial;
1656  }
1657 
1658  ExprMap<Expr> var2monomial;
1659  vector<Expr> vars;
1660  Expr::iterator i = right.begin(), iend = right.end();
1661  for(;i != iend; ++i) {
1662  if(i->isRational())
1663  continue;
1664  Expr c, var;
1665  separateMonomial(*i, c, var);
1666  var2monomial[var] = *i;
1667  vars.push_back(var);
1668  }
1669 
1670  vector<Expr> largest;
1671  d_graph.selectLargest(vars, largest);
1672  DebugAssert(0 < largest.size(),
1673  "TheoryArith3::pickMonomial: selectLargest: failed!!!!");
1674 
1675  // DEJAN: Rafine the largest by coefficient values
1676  vector<Expr> largest_small_coeff;
1677  selectSmallestByCoefficient(largest, largest_small_coeff);
1678  DebugAssert(0 < largest_small_coeff.size(), "TheoryArith3::pickMonomial: selectLargestByCOefficient: failed!!!!");
1679 
1680  size_t pickedVar = 0;
1681  // Pick the variable which will generate the fewest number of
1682  // projections
1683 
1684  size_t size = largest_small_coeff.size();
1685  int minProjections = -1;
1686  if (size > 1)
1687  for(size_t k=0; k< size; ++k) {
1688  const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
1689  // Grab the counters for the variable
1690  int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
1691  int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
1692  int n(nRight*nLeft);
1693  TRACE("arith ineq", "pickMonomial: var=", var,
1694  ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
1695  if(minProjections < 0 || minProjections > n) {
1696  minProjections = n;
1697  pickedVar = k;
1698  }
1699  TRACE("arith ineq", "Number of projections for "+var.toString()+" = ", n, "");
1700  }
1701 
1702 
1703  const Expr& largestVar = largest_small_coeff[pickedVar];
1704  // FIXME: TODO: update the counters (subtract counts for the vars
1705  // other than largestVar
1706 
1707  // Update the graph (all edges to the largest in the graph, not just the small coefficients).
1708  for(size_t k = 0; k < vars.size(); ++k) {
1709  if(vars[k] != largestVar)
1710  d_graph.addEdge(largestVar, vars[k]);
1711  }
1712 
1713  return var2monomial[largestVar];
1714 }
1715 
1716 void TheoryArith3::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
1717 {
1718  TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
1719  DebugAssert(e1 != e2, "TheoryArith3::VarOrderGraph::addEdge("
1720  +e1.toString()+", "+e2.toString()+")");
1721  d_edges[e1].push_back(e2);
1722 }
1723 
1724 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
1725 //comparable)
1726 bool TheoryArith3::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
1727 {
1728  d_cache.clear();
1729  //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
1730  return dfs(e1,e2);
1731 }
1732 
1733 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
1734 bool TheoryArith3::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
1735 {
1736  if(e1 == e2)
1737  return true;
1738  if(d_cache.count(e2) > 0)
1739  return false;
1740  if(d_edges.count(e2) == 0)
1741  return false;
1742  d_cache[e2] = true;
1743  vector<Expr>& e2Edges = d_edges[e2];
1744  vector<Expr>::iterator i = e2Edges.begin();
1745  vector<Expr>::iterator iend = e2Edges.end();
1746  //if dfs finds e1 then i != iend else i is equal to iend
1747  for(; i != iend && !dfs(e1,*i); ++i);
1748  return (i != iend);
1749 }
1750 
1751 
1752 void TheoryArith3::VarOrderGraph::selectSmallest(vector<Expr>& v1,
1753  vector<Expr>& v2)
1754 {
1755  int v1Size = v1.size();
1756  vector<bool> v3(v1Size);
1757  for(int j=0; j < v1Size; ++j)
1758  v3[j] = false;
1759 
1760  for(int j=0; j < v1Size; ++j) {
1761  if(v3[j]) continue;
1762  for(int i =0; i < v1Size; ++i) {
1763  if((i == j) || v3[i])
1764  continue;
1765  if(lessThan(v1[i],v1[j])) {
1766  v3[j] = true;
1767  break;
1768  }
1769  }
1770  }
1771  vector<Expr> new_v1;
1772 
1773  for(int j = 0; j < v1Size; ++j)
1774  if(!v3[j]) v2.push_back(v1[j]);
1775  else new_v1.push_back(v1[j]);
1776  v1 = new_v1;
1777 }
1778 
1779 
1780 void TheoryArith3::VarOrderGraph::selectLargest(const vector<Expr>& v1,
1781  vector<Expr>& v2)
1782 {
1783  int v1Size = v1.size();
1784  vector<bool> v3(v1Size);
1785  for(int j=0; j < v1Size; ++j)
1786  v3[j] = false;
1787 
1788  for(int j=0; j < v1Size; ++j) {
1789  if(v3[j]) continue;
1790  for(int i =0; i < v1Size; ++i) {
1791  if((i == j) || v3[i])
1792  continue;
1793  if(lessThan(v1[j],v1[i])) {
1794  v3[j] = true;
1795  break;
1796  }
1797  }
1798  }
1799 
1800  for(int j = 0; j < v1Size; ++j)
1801  if(!v3[j]) v2.push_back(v1[j]);
1802 }
1803 
1804 ///////////////////////////////////////////////////////////////////////////////
1805 // TheoryArith3 Public Methods //
1806 ///////////////////////////////////////////////////////////////////////////////
1807 
1808 
1809 TheoryArith3::TheoryArith3(TheoryCore* core)
1810  : TheoryArith(core, "Arithmetic3"),
1811  d_diseq(core->getCM()->getCurrentContext()),
1812  d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
1813  d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
1814  d_freeConstDB(core->getCM()->getCurrentContext()),
1815  d_buffer(core->getCM()->getCurrentContext()),
1816  // Initialize index to 0 at scope 0
1817  d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
1818  d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
1819  d_countRight(core->getCM()->getCurrentContext()),
1820  d_countLeft(core->getCM()->getCurrentContext()),
1821  d_sharedTerms(core->getCM()->getCurrentContext()),
1822  d_sharedVars(core->getCM()->getCurrentContext()),
1823  maxCoefficientLeft(core->getCM()->getCurrentContext()),
1824  maxCoefficientRight(core->getCM()->getCurrentContext()),
1825  fixedMaxCoefficient(core->getCM()->getCurrentContext())
1826 {
1827  IF_DEBUG(d_diseq.setName("CDList[TheoryArith3::d_diseq]");)
1828  IF_DEBUG(d_buffer.setName("CDList[TheoryArith3::d_buffer]");)
1829  IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArith3::d_bufferIdx]");)
1830 
1831  getEM()->newKind(REAL, "_REAL", true);
1832  getEM()->newKind(INT, "_INT", true);
1833  getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
1834 
1835  getEM()->newKind(UMINUS, "_UMINUS");
1836  getEM()->newKind(PLUS, "_PLUS");
1837  getEM()->newKind(MINUS, "_MINUS");
1838  getEM()->newKind(MULT, "_MULT");
1839  getEM()->newKind(DIVIDE, "_DIVIDE");
1840  getEM()->newKind(POW, "_POW");
1841  getEM()->newKind(INTDIV, "_INTDIV");
1842  getEM()->newKind(MOD, "_MOD");
1843  getEM()->newKind(LT, "_LT");
1844  getEM()->newKind(LE, "_LE");
1845  getEM()->newKind(GT, "_GT");
1846  getEM()->newKind(GE, "_GE");
1847  getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
1848  getEM()->newKind(NEGINF, "_NEGINF");
1849  getEM()->newKind(POSINF, "_POSINF");
1850  getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
1851  getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
1852 
1853  getEM()->newKind(REAL_CONST, "_REAL_CONST");
1854 
1855  vector<int> kinds;
1856  kinds.push_back(REAL);
1857  kinds.push_back(INT);
1858  kinds.push_back(SUBRANGE);
1859  kinds.push_back(IS_INTEGER);
1860  kinds.push_back(UMINUS);
1861  kinds.push_back(PLUS);
1862  kinds.push_back(MINUS);
1863  kinds.push_back(MULT);
1864  kinds.push_back(DIVIDE);
1865  kinds.push_back(POW);
1866  kinds.push_back(INTDIV);
1867  kinds.push_back(MOD);
1868  kinds.push_back(LT);
1869  kinds.push_back(LE);
1870  kinds.push_back(GT);
1871  kinds.push_back(GE);
1872  kinds.push_back(RATIONAL_EXPR);
1873  kinds.push_back(NEGINF);
1874  kinds.push_back(POSINF);
1875  kinds.push_back(DARK_SHADOW);
1876  kinds.push_back(GRAY_SHADOW);
1877  kinds.push_back(REAL_CONST);
1878 
1879  registerTheory(this, kinds, true);
1880 
1882 
1883  d_realType = Type(getEM()->newLeafExpr(REAL));
1884  d_intType = Type(getEM()->newLeafExpr(INT));
1885 }
1886 
1887 
1888 // Destructor: delete the proof rules class if it's present
1890  if(d_rules != NULL) delete d_rules;
1891  // Clear the inequality databases
1892  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
1893  iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
1894  delete (i->second);
1895  free(i->second);
1896  }
1897  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
1898  iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
1899  delete (i->second);
1900  free (i->second);
1901  }
1902 }
1903 
1904 void TheoryArith3::collectVars(const Expr& e, vector<Expr>& vars,
1905  set<Expr>& cache) {
1906  // Check the cache first
1907  if(cache.count(e) > 0) return;
1908  // Not processed yet. Cache the expression and proceed
1909  cache.insert(e);
1910  if(isLeaf(e)) vars.push_back(e);
1911  else
1912  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
1913  collectVars(*i, vars, cache);
1914 }
1915 
1916 void
1918  const Theorem& bxLEbeta) {
1919  const Expr& ineq1(alphaLEax.getExpr());
1920  const Expr& ineq2(bxLEbeta.getExpr());
1921  DebugAssert(isLE(ineq1), "TheoryArith3::processFiniteInterval: ineq1 = "
1922  +ineq1.toString());
1923  DebugAssert(isLE(ineq2), "TheoryArith3::processFiniteInterval: ineq2 = "
1924  +ineq2.toString());
1925  // If the inequalities are not integer, just return (nothing to do)
1926  if(!isInteger(ineq1[0])
1927  || !isInteger(ineq1[1])
1928  || !isInteger(ineq2[0])
1929  || !isInteger(ineq2[1]))
1930  return;
1931 
1932  const Expr& ax = ineq1[1];
1933  const Expr& bx = ineq2[0];
1934  DebugAssert(!isPlus(ax) && !isRational(ax),
1935  "TheoryArith3::processFiniteInterval:\n ax = "+ax.toString());
1936  DebugAssert(!isPlus(bx) && !isRational(bx),
1937  "TheoryArith3::processFiniteInterval:\n bx = "+bx.toString());
1938  Expr a = isMult(ax)? ax[0] : rat(1);
1939  Expr b = isMult(bx)? bx[0] : rat(1);
1940 
1941  Theorem thm1(alphaLEax), thm2(bxLEbeta);
1942  // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
1943  if(a != b) {
1944  thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
1945  thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
1946  }
1947  // Check that a*beta - b*alpha == c > 0
1948  const Expr& alphaLEt = thm1.getExpr();
1949  const Expr& alpha = alphaLEt[0];
1950  const Expr& t = alphaLEt[1];
1951  const Expr& beta = thm2.getExpr()[1];
1952  Expr c = canon(beta - alpha).getRHS();
1953 
1954  if(c.isRational() && c.getRational() >= 1) {
1955  // This is a finite interval. First, derive t <= alpha + c:
1956  // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
1957  // Then substitute that in thm2
1958  Theorem bEQac = symmetryRule(canon(alpha + c));
1959  // Substitute beta == alpha+c for the second child of thm2
1960  vector<unsigned> changed;
1961  vector<Theorem> thms;
1962  changed.push_back(1);
1963  thms.push_back(bEQac);
1964  Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
1965  tLEac = iffMP(thm2, tLEac);
1966  // Derive and enqueue the finite interval constraint
1967  Theorem isInta(isIntegerThm(alpha));
1968  Theorem isIntt(isIntegerThm(t));
1969  enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
1970  }
1971 }
1972 
1973 
1974 void
1976  // If x is not integer, do not bother
1977  if(!isInteger(x)) return;
1978  // Process every pair of the opposing inequalities for 'x'
1979  ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
1980  iLeft = d_inequalitiesLeftDB.find(x);
1981  if(iLeft == d_inequalitiesLeftDB.end()) return;
1982  iRight = d_inequalitiesRightDB.find(x);
1983  if(iRight == d_inequalitiesRightDB.end()) return;
1984  // There are some opposing inequalities; get the lists
1985  CDList<Ineq>& ineqsLeft = *(iLeft->second);
1986  CDList<Ineq>& ineqsRight = *(iRight->second);
1987  // Get the sizes of the lists
1988  size_t sizeLeft = ineqsLeft.size();
1989  size_t sizeRight = ineqsRight.size();
1990  // Process all the pairs of the opposing inequalities
1991  for(size_t l=0; l<sizeLeft; ++l)
1992  for(size_t r=0; r<sizeRight; ++r)
1993  processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
1994 }
1995 
1996 /*! This function recursively decends expression tree <strong>without
1997  * caching</strong> until it hits a node that is already setup. Be
1998  * careful on what expressions you are calling it.
1999  */
2000 void
2002  if(e.hasFind()) return;
2003  // First, set up the kids recursively
2004  for (int k = 0; k < e.arity(); ++k) {
2005  setupRec(e[k]);
2006  }
2007  // Create a find pointer for e
2008  e.setFind(reflexivityRule(e));
2009  e.setEqNext(reflexivityRule(e));
2010  // And call our own setup()
2011  setup(e);
2012 }
2013 
2014 
2016  d_sharedTerms[e] = true;
2017 }
2018 
2019 
2021 {
2022  TRACE("arith assert", "assertFact(", e.getExpr().toString(), ")");
2023  const Expr& expr = e.getExpr();
2024  if (expr.isNot() && expr[0].isEq()) {
2025  IF_DEBUG(debugger.counter("[arith] received disequalities")++;)
2026  d_diseq.push_back(e);
2027  }
2028  else if (!expr.isEq()){
2029  if (expr.isNot()) {
2030  // This can only be negation of dark or gray shadows, or
2031  // disequalities, which we ignore. Negations of inequalities
2032  // are handled in rewrite, we don't even receive them here.
2033  }
2034  else if(isDarkShadow(expr)) {
2036  IF_DEBUG(debugger.counter("received DARK_SHADOW")++;)
2037  }
2038  else if(isGrayShadow(expr)) {
2039  IF_DEBUG(debugger.counter("received GRAY_SHADOW")++;)
2040  const Rational& c1 = expr[2].getRational();
2041  const Rational& c2 = expr[3].getRational();
2042  const Expr& v = expr[0];
2043  const Expr& ee = expr[1];
2044  if(c1 == c2)
2046  else {
2047  Theorem gThm(e);
2048  // Check if we can reduce the number of cases in G(ax,c,c1,c2)
2049  if(ee.isRational() && isMult(v)
2050  && v[0].isRational() && v[0].getRational() >= 2) {
2051  IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++;)
2052  gThm = d_rules->grayShadowConst(e);
2053  }
2054  // (Possibly) new gray shadow
2055  const Expr& g = gThm.getExpr();
2056  if(g.isFalse())
2057  setInconsistent(gThm);
2058  else if(g[2].getRational() == g[3].getRational())
2060  else {
2061  // Assert c1+e <= v <= c2+e
2063  // Split G into 2 cases (binary search b/w c1 and c2)
2064  Theorem thm2 = d_rules->splitGrayShadow(gThm);
2065  enqueueFact(thm2);
2066  // Fetch the two gray shadows
2067  DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
2068  "thm2 = "+thm2.getExpr().toString());
2069  const Expr& G1orG2 = thm2.getExpr()[0];
2070  DebugAssert(G1orG2.isOr() && G1orG2.arity()==2,
2071  "G1orG2 = "+G1orG2.toString());
2072  const Expr& G1 = G1orG2[0];
2073  const Expr& G2 = G1orG2[1];
2074  DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString());
2075  DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString());
2076  // Split on the left disjunct first (keep the priority low)
2077  Expr tmp = simplifyExpr(G1);
2078  if (!tmp.isBoolConst())
2079  addSplitter(tmp, 1);
2080  tmp = simplifyExpr(G2);
2081  if (!tmp.isBoolConst())
2082  addSplitter(tmp, -1);
2083  }
2084  }
2085  }
2086  else {
2087  DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr),
2088  "expected LE or LT: "+expr.toString());
2089  if(isLE(expr) || isLT(expr)) {
2090  IF_DEBUG(debugger.counter("recevied inequalities")++;)
2091 
2092  // Assert the equivalent negated inequality
2093  Theorem thm;
2094  if (isLE(expr)) thm = d_rules->negatedInequality(!gtExpr(expr[0],expr[1]));
2095  else thm = d_rules->negatedInequality(!geExpr(expr[0],expr[1]));
2096  thm = symmetryRule(thm);
2097  Theorem thm2 = simplify(thm.getRHS()[0]);
2098  DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite");
2099  thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2);
2100  thm = transitivityRule(thm, thm2);
2101  enqueueFact(iffMP(e, thm));
2102 
2103  // Buffer the inequality
2104  addToBuffer(e);
2105 
2106  TRACE("arith ineq", "buffer.size() = ", d_buffer.size(),
2107  ", index="+int2string(d_bufferIdx)
2108  +", threshold="+int2string(*d_bufferThres));
2109 
2110  if((((int)d_buffer.size()) - (int)d_bufferIdx > *d_bufferThres)
2111  && !d_inModelCreation)
2112  processBuffer();
2113  } else {
2114  IF_DEBUG(debugger.counter("arith IS_INTEGER")++;)
2115  }
2116  }
2117  }
2118  else {
2119  IF_DEBUG(debugger.counter("[arith] received t1=t2")++;)
2120  }
2121 }
2122 
2123 
2124 void TheoryArith3::checkSat(bool fullEffort)
2125 {
2126  // vector<Expr>::const_iterator e;
2127  // vector<Expr>::const_iterator eEnd;
2128  // TODO: convert back to use iterators
2129  TRACE("arith checksat", "checksat(", fullEffort? "true" : "false", ")");
2130  TRACE("arith ineq", "TheoryArith3::checkSat(fullEffort=",
2131  fullEffort? "true" : "false", ")");
2132  if (fullEffort) {
2133  while(!inconsistent() && d_bufferIdx < d_buffer.size())
2134  processBuffer();
2135  if(d_inModelCreation) {
2136  for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
2137  TRACE("model", "[arith] refining diseq: ",
2138  d_diseq[d_diseqIdx].getExpr() , "");
2140  }
2141  }
2142  }
2143 }
2144 
2145 
2146 
2148 {
2149  d_inModelCreation = true;
2150  TRACE("model", "refineCounterExample[TheoryArith3] ", "", "{");
2151  CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
2152  iend = d_sharedTerms.end();
2153  // Add equalities over all pairs of shared terms as suggested
2154  // splitters. Notice, that we want to split on equality
2155  // (positively) first, to reduce the size of the model.
2156  for(; it!=iend; ++it) {
2157  // Copy by value: the elements in the pair from *it are NOT refs in CDMap
2158  Expr e1 = (*it).first;
2159  for(it2 = it, ++it2; it2!=iend; ++it2) {
2160  Expr e2 = (*it2).first;
2162  "TheoryArith3::refineCounterExample: e1 = "+e1.toString()
2163  +"\n type(e1) = "+e1.getType().toString());
2164  if(findExpr(e1) != findExpr(e2)) {
2166  "TheoryArith3::refineCounterExample: e2 = "+e2.toString()
2167  +"\n type(e2) = "+e2.getType().toString());
2168  Expr eq = simplifyExpr(e1.eqExpr(e2));
2169  if (!eq.isBoolConst())
2170  addSplitter(eq);
2171  }
2172  }
2173  }
2174  TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
2175 }
2176 
2177 
2178 void
2179 TheoryArith3::findRationalBound(const Expr& varSide, const Expr& ratSide,
2180  const Expr& var,
2181  Rational &r)
2182 {
2183  Expr c, x;
2184  separateMonomial(varSide, c, x);
2185 
2187  "seperateMonomial failed");
2188  DebugAssert(findExpr(ratSide).isRational(),
2189  "smallest variable in graph, should not have variables"
2190  " in inequalities: ");
2191  DebugAssert(x == var, "separateMonomial found different variable: "
2192  + var.toString());
2193  r = findExpr(ratSide).getRational() / findExpr(c).getRational();
2194 }
2195 
2196 bool
2198 {
2199  bool strictLB=false, strictUB=false;
2200  bool right = (d_inequalitiesRightDB.count(e) > 0
2201  && d_inequalitiesRightDB[e]->size() > 0);
2202  bool left = (d_inequalitiesLeftDB.count(e) > 0
2203  && d_inequalitiesLeftDB[e]->size() > 0);
2204  int numRight = 0, numLeft = 0;
2205  if(right) { //rationals less than e
2206  CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
2207  for(unsigned int i=0; i<ratsLTe->size(); i++) {
2208  DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
2209  Expr ineq = (*ratsLTe)[i].ineq().getExpr();
2210  Expr leftSide = ineq[0], rightSide = ineq[1];
2211  Rational r;
2212  findRationalBound(rightSide, leftSide, e , r);
2213  if(numRight==0 || r>glb){
2214  glb = r;
2215  strictLB = isLT(ineq);
2216  }
2217  numRight++;
2218  }
2219  TRACE("model", " =>Lower bound ", glb.toString(), "");
2220  }
2221  if(left) { //rationals greater than e
2222  CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
2223  for(unsigned int i=0; i<ratsGTe->size(); i++) {
2224  DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
2225  Expr ineq = (*ratsGTe)[i].ineq().getExpr();
2226  Expr leftSide = ineq[0], rightSide = ineq[1];
2227  Rational r;
2228  findRationalBound(leftSide, rightSide, e, r);
2229  if(numLeft==0 || r<lub) {
2230  lub = r;
2231  strictUB = isLT(ineq);
2232  }
2233  numLeft++;
2234  }
2235  TRACE("model", " =>Upper bound ", lub.toString(), "");
2236  }
2237  if(!left && !right) {
2238  lub = 0;
2239  glb = 0;
2240  }
2241  if(!left && right) {lub = glb +2;}
2242  if(!right && left) {glb = lub-2;}
2243  DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
2244  "than least upper bound");
2245  return strictLB;
2246 }
2247 
2248 void TheoryArith3::assignVariables(std::vector<Expr>&v)
2249 {
2250  int count = 0;
2251  while (v.size() > 0) {
2252  std::vector<Expr> bottom;
2253  d_graph.selectSmallest(v, bottom);
2254  TRACE("model", "Finding variables to assign. Iteration # ", count, "");
2255  for(unsigned int i = 0; i<bottom.size(); i++) {
2256  Expr e = bottom[i];
2257  TRACE("model", "Found: ", e, "");
2258  // Check if it is already a concrete constant
2259  if(e.isRational()) continue;
2260 
2261  Rational lub, glb;
2262  bool strictLB;
2263  strictLB = findBounds(e, lub, glb);
2264  Rational mid;
2265  if(isInteger(e)) {
2266  if(strictLB && glb.isInteger())
2267  mid = glb + 1;
2268  else
2269  mid = ceil(glb);
2270  }
2271  else
2272  mid = (lub + glb)/2;
2273  TRACE("model", "Assigning mid = ", mid, " {");
2274  assignValue(e, rat(mid));
2275  TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
2276  if(inconsistent()) return; // Punt immediately if failed
2277  }
2278  count++;
2279  }
2280 }
2281 
2282 void TheoryArith3::computeModelBasic(const std::vector<Expr>& v)
2283 {
2284  d_inModelCreation = true;
2285  vector<Expr> reps;
2286  TRACE("model", "Arith=>computeModel ", "", "{");
2287  for(unsigned int i=0; i <v.size(); ++i) {
2288  const Expr& e = v[i];
2289  if(findExpr(e) == e) {
2290  TRACE("model", "arith variable:", e , "");
2291  reps.push_back(e);
2292  }
2293  else {
2294  TRACE("model", "arith variable:", e , "");
2295  TRACE("model", " ==> is defined by: ", findExpr(e) , "");
2296  }
2297  }
2298  assignVariables(reps);
2299  TRACE("model", "Arith=>computeModel", "", "}");
2300  d_inModelCreation = false;
2301 }
2302 
2303 // For any arith expression 'e', if the subexpressions are assigned
2304 // concrete values, then find(e) must already be a concrete value.
2305 void TheoryArith3::computeModel(const Expr& e, vector<Expr>& vars) {
2306  DebugAssert(findExpr(e).isRational(), "TheoryArith3::computeModel("
2307  +e.toString()+")\n e is not assigned concrete value.\n"
2308  +" find(e) = "+findExpr(e).toString());
2309  assignValue(simplify(e));
2310  vars.push_back(e);
2311 }
2312 
2313 
2314 
2315 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
2316  * and returns a theorem to that effect. assumes e is non-trivial
2317  * i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
2318  */
2320  //e is an eqn or ineqn. e is not a trivial eqn or ineqn
2321  //trivial means 0 = const or 0 <= const.
2322  TRACE("arith", "normalize(", e, ") {");
2323  DebugAssert(e.isEq() || isIneq(e),
2324  "normalize: input must be Eq or Ineq: " + e.toString());
2325  DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
2326  "normalize: if (e is ineq) then e[0] must be 0" +
2327  e.toString());
2328  if(e.isEq()) {
2329  if(e[0].isRational()) {
2330  DebugAssert(0 == e[0].getRational(),
2331  "normalize: if e is Eq and e[0] is rat then e[0]==0");
2332  }
2333  else {
2334  //if e[0] is not rational then e[1] must be rational.
2335  DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
2336  "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
2337  " e = "+e.toString());
2338  }
2339  }
2340 
2341  Expr factor;
2342  if(e[0].isRational())
2343  factor = computeNormalFactor(e[1]);
2344  else
2345  factor = computeNormalFactor(e[0]);
2346 
2347  TRACE("arith", "normalize: factor = ", factor, "");
2348  DebugAssert(factor.getRational() > 0,
2349  "normalize: factor="+ factor.toString());
2350 
2351  Theorem thm(reflexivityRule(e));
2352  // Now multiply the equality by the factor, unless it is 1
2353  if(factor.getRational() != 1) {
2354  int kind = e.getKind();
2355  switch(kind) {
2356  case EQ:
2357  thm = d_rules->multEqn(e[0], e[1], factor);
2358  // And canonize the result
2359  thm = canonPredEquiv(thm);
2360  break;
2361  case LE:
2362  case LT:
2363  case GE:
2364  case GT:
2365  thm = d_rules->multIneqn(e, factor);
2366  // And canonize the result
2367  thm = canonPredEquiv(thm);
2368  break;
2369  default:
2370  // MS .net doesn't accept "..." + int
2371  ostringstream ss;
2372  ss << "normalize: control should not reach here " << kind;
2373  DebugAssert(false, ss.str());
2374  break;
2375  }
2376  }
2377  TRACE("arith", "normalize => ", thm, " }");
2378  return(thm);
2379 }
2380 
2381 
2383  return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
2384 }
2385 
2386 
2388 {
2389  DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
2390  TRACE("arith", "TheoryArith3::rewrite(", e, ") {");
2391  Theorem thm;
2392  if (!e.isTerm()) {
2393  if (!e.isAbsLiteral()) {
2394  e.setRewriteNormal();
2395  thm = reflexivityRule(e);
2396  TRACE("arith", "TheoryArith3::rewrite[non-literal] => ", thm, " }");
2397  return thm;
2398  }
2399  switch(e.getKind()) {
2400  case EQ:
2401  {
2402  // canonical form for an equality of two leaves
2403  // is just l == r instead of 0 + (-1 * l) + r = 0.
2404  if (isLeaf(e[0]) && isLeaf(e[1]))
2405  thm = reflexivityRule(e);
2406  else { // Otherwise, it is "lhs = 0"
2407  //first convert e to the form 0=e'
2408  if((e[0].isRational() && e[0].getRational() == 0)
2409  || (e[1].isRational() && e[1].getRational() == 0))
2410  //already in 0=e' or e'=0 form
2411  thm = reflexivityRule(e);
2412  else {
2413  thm = d_rules->rightMinusLeft(e);
2414  thm = canonPredEquiv(thm);
2415  }
2416  // Check for trivial equation
2417  if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
2418  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
2419  } else {
2420  //else equation is non-trivial
2421  thm = normalize(thm);
2422  // Normalization may yield non-simplified terms
2423  thm = canonPredEquiv(thm);
2424 
2425  }
2426  }
2427 
2428  // Equations must be oriented such that lhs >= rhs as Exprs;
2429  // this ordering is given by operator<(Expr,Expr).
2430  const Expr& eq = thm.getRHS();
2431  if(eq.isEq() && eq[0] < eq[1])
2433  }
2434  break;
2435  case GRAY_SHADOW:
2436  case DARK_SHADOW:
2437  thm = reflexivityRule(e);
2438  break;
2439  case IS_INTEGER: {
2440  Theorem res(isIntegerDerive(e, typePred(e[0])));
2441  if(!res.isNull())
2442  thm = getCommonRules()->iffTrue(res);
2443  else
2444  thm = reflexivityRule(e);
2445  break;
2446  }
2447  case NOT:
2448  if (!isIneq(e[0]))
2449  //in this case we have "NOT of DARK or GRAY_SHADOW."
2450  thm = reflexivityRule(e);
2451  else {
2452  //In this case we have the "NOT of ineq". get rid of NOT
2453  //and then treat like an ineq
2454  thm = d_rules->negatedInequality(e);
2455  DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
2456  "Expected GE or GT");
2457  thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
2458  thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
2459  thm = canonPredEquiv(thm);
2460 
2461  // Check for trivial inequation
2462  if ((thm.getRHS())[1].isRational())
2463  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
2464  else {
2465  //else ineq is non-trivial
2466  thm = normalize(thm);
2467  // Normalization may yield non-simplified terms
2468  thm = canonPredEquiv(thm);
2469  }
2470  }
2471  break;
2472  case LE:
2473  case LT:
2474  case GE:
2475  case GT:
2476  if (isGE(e) || isGT(e)) {
2477  thm = d_rules->flipInequality(e);
2478  thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
2479  }
2480  else
2481  thm = d_rules->rightMinusLeft(e);
2482  thm = canonPredEquiv(thm);
2483 
2484  // Check for trivial inequation
2485  if ((thm.getRHS())[1].isRational())
2486  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
2487  else { // ineq is non-trivial
2488  thm = normalize(thm);
2489  thm = canonPredEquiv(thm);
2490  }
2491  break;
2492  default:
2493  DebugAssert(false,
2494  "Theory_Arith::rewrite: control should not reach here");
2495  break;
2496  }
2497  }
2498  else {
2499  if (e.isAtomic())
2500  thm = canon(e);
2501  else
2502  thm = reflexivityRule(e);
2503  }
2504  // Arith canonization is idempotent
2505  if (theoryOf(thm.getRHS()) == this)
2506  thm.getRHS().setRewriteNormal();
2507  TRACE("arith", "TheoryArith3::rewrite => ", thm, " }");
2508  return thm;
2509 }
2510 
2511 
2513 {
2514  if (!e.isTerm()) {
2515  if (e.isNot() || e.isEq() || isDarkShadow(e) || isGrayShadow(e)) return;
2516  if(e.getKind() == IS_INTEGER) {
2517  e[0].addToNotify(this, e);
2518  return;
2519  }
2520  DebugAssert((isLT(e)||isLE(e)) &&
2521  e[0].isRational() && e[0].getRational() == 0,
2522  "TheoryArith3::setup: expected 0 < rhs:" + e.toString());
2523  e[1].addToNotify(this, e);
2524  return;
2525  }
2526  int k(0), ar(e.arity());
2527  for ( ; k < ar; ++k) {
2528  e[k].addToNotify(this, e);
2529  TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
2530  }
2531 }
2532 
2533 
2534 void TheoryArith3::update(const Theorem& e, const Expr& d)
2535 {
2536  if (inconsistent()) return;
2537  IF_DEBUG(debugger.counter("arith update total")++;)
2538  if (!d.hasFind()) return;
2539  if (isIneq(d)) {
2540  // Substitute e[1] for e[0] in d and enqueue new inequality
2541  DebugAssert(e.getLHS() == d[1], "Mismatch");
2542  Theorem thm = find(d);
2543  // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
2544  vector<unsigned> changed;
2545  vector<Theorem> children;
2546  changed.push_back(1);
2547  children.push_back(e);
2548  Theorem thm2 = substitutivityRule(d, changed, children);
2549  if (thm.getRHS() == trueExpr()) {
2550  enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
2551  }
2552  else {
2553  enqueueFact(getCommonRules()->iffFalseElim(
2554  transitivityRule(symmetryRule(thm2), thm)));
2555  }
2556  IF_DEBUG(debugger.counter("arith update ineq")++;)
2557  }
2558  else if (find(d).getRHS() == d) {
2559  Theorem thm = canonSimp(d);
2560  TRACE("arith", "TheoryArith3::update(): thm = ", thm, "");
2561  DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
2562  +thm.getExpr().toString());
2564  IF_DEBUG(debugger.counter("arith update find(d)=d")++;)
2565  }
2566 }
2567 
2568 
2570 {
2571  DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
2572  const Expr& lhs = thm.getLHS();
2573  const Expr& rhs = thm.getRHS();
2574 
2575  // Check for already solved equalities.
2576 
2577  // Have to be careful about the types: integer variable cannot be
2578  // assigned a real term. Also, watch for e[0] being a subexpression
2579  // of e[1]: this would create an unsimplifiable expression.
2580  if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
2581  && (lhs.getType() != intType() || isInteger(rhs))
2582  // && !e[0].subExprOf(e[1])
2583  )
2584  return thm;
2585 
2586  // Symmetric version is already solved
2587  if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
2588  && (rhs.getType() != intType() || isInteger(lhs))
2589  // && !e[1].subExprOf(e[0])
2590  )
2591  return symmetryRule(thm);
2592 
2593  return doSolve(thm);
2594 }
2595 
2596 
2597 void TheoryArith3::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
2598  switch(e.getKind()) {
2599  case RATIONAL_EXPR: // Skip the constants
2600  break;
2601  case PLUS:
2602  case MULT:
2603  case DIVIDE:
2604  case POW: // This is not a variable; extract the variables from children
2605  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
2606  // getModelTerm(*i, v);
2607  v.push_back(*i);
2608  break;
2609  default: { // Otherwise it's a variable. Check if it has a find pointer
2610  Expr e2(findExpr(e));
2611  if(e==e2) {
2612  TRACE("model", "TheoryArith3::computeModelTerm(", e, "): a variable");
2613  // Leave it alone (it has no descendants)
2614  // v.push_back(e);
2615  } else {
2616  TRACE("model", "TheoryArith3::computeModelTerm("+e.toString()
2617  +"): has find pointer to ", e2, "");
2618  v.push_back(e2);
2619  }
2620  }
2621  }
2622 }
2623 
2624 
2626  Expr tExpr = t.getExpr();
2627  switch(tExpr.getKind()) {
2628  case INT:
2629  return Expr(IS_INTEGER, e);
2630  case SUBRANGE: {
2631  std::vector<Expr> kids;
2632  kids.push_back(Expr(IS_INTEGER, e));
2633  kids.push_back(leExpr(tExpr[0], e));
2634  kids.push_back(leExpr(e, tExpr[1]));
2635  return andExpr(kids);
2636  }
2637  default:
2638  return e.getEM()->trueExpr();
2639  }
2640 }
2641 
2642 
2644 {
2645  if (e.isRewrite()) {
2646  DebugAssert(e.getLHS().isTerm(), "Expected equation");
2647  if (isLeaf(e.getLHS())) {
2648  // should be in solved form
2649  DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
2650  "Not in solved form: lhs appears in rhs");
2651  }
2652  else {
2653  DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
2655  "Expected at least one unsimplified leaf on lhs");
2656  }
2657  DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
2658  "Expected canonSimp(rhs) = canonSimp(rhs)");
2659  }
2660  else {
2661  Expr expr = e.getExpr();
2662  if (expr.isFalse()) return;
2663 
2664  vector<Theorem> eqs;
2665  Theorem thm;
2666  int index, index2;
2667 
2668  for (index = 0; index < expr.arity(); ++index) {
2669  thm = getCommonRules()->andElim(e, index);
2670  eqs.push_back(thm);
2671  if (thm.getExpr().isFalse()) return;
2672  DebugAssert(eqs[index].isRewrite() &&
2673  eqs[index].getLHS().isTerm(), "Expected equation");
2674  }
2675 
2676  // Check for solved form
2677  for (index = 0; index < expr.arity(); ++index) {
2678  DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
2679  DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
2680  "Expected canonSimp(rhs) = canonSimp(rhs)");
2681  DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
2682  "Failed recursive canonSimp check");
2683  for (index2 = 0; index2 < expr.arity(); ++index2) {
2684  DebugAssert(index == index2 ||
2685  eqs[index].getLHS() != eqs[index2].getLHS(),
2686  "Not in solved form: repeated lhs");
2687  DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
2688  "Not in solved form: lhs appears in rhs");
2689  }
2690  }
2691  }
2692 }
2693 
2694 
2696 {
2697  switch (e.getKind()) {
2698  case INT:
2699  case REAL:
2700  if (e.arity() > 0) {
2701  throw Exception("Ill-formed arithmetic type: "+e.toString());
2702  }
2703  break;
2704  case SUBRANGE:
2705  if (e.arity() != 2 ||
2706  !isIntegerConst(e[0]) ||
2707  !isIntegerConst(e[1]) ||
2708  e[0].getRational() > e[1].getRational()) {
2709  throw Exception("bad SUBRANGE type expression"+e.toString());
2710  }
2711  break;
2712  default:
2713  DebugAssert(false, "Unexpected kind in TheoryArith3::checkType"
2714  +getEM()->getKindName(e.getKind()));
2715  }
2716 }
2717 
2718 
2720  bool enumerate, bool computeSize)
2721 {
2722  Cardinality card = CARD_INFINITE;
2723  switch (e.getKind()) {
2724  case SUBRANGE: {
2725  card = CARD_FINITE;
2726  Expr typeExpr = e;
2727  if (enumerate) {
2728  Rational r = typeExpr[0].getRational() + n;
2729  if (r <= typeExpr[1].getRational()) {
2730  e = rat(r);
2731  }
2732  else e = Expr();
2733  }
2734  if (computeSize) {
2735  Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1;
2736  n = r.getUnsigned();
2737  }
2738  break;
2739  }
2740  default:
2741  break;
2742  }
2743  return card;
2744 }
2745 
2746 
2748 {
2749  switch (e.getKind()) {
2750  case REAL_CONST:
2751  e.setType(d_realType);
2752  break;
2753  case RATIONAL_EXPR:
2754  if(e.getRational().isInteger())
2755  e.setType(d_intType);
2756  else
2757  e.setType(d_realType);
2758  break;
2759  case UMINUS:
2760  case PLUS:
2761  case MINUS:
2762  case MULT:
2763  case POW: {
2764  bool isInt = true;
2765  for(int k = 0; k < e.arity(); ++k) {
2766  if(d_realType != getBaseType(e[k]))
2767  throw TypecheckException("Expecting type REAL with `" +
2768  getEM()->getKindName(e.getKind()) + "',\n"+
2769  "but got a " + getBaseType(e[k]).toString()+
2770  " for:\n" + e.toString());
2771  if(isInt && !isInteger(e[k]))
2772  isInt = false;
2773  }
2774  if(isInt)
2775  e.setType(d_intType);
2776  else
2777  e.setType(d_realType);
2778  break;
2779  }
2780  case DIVIDE: {
2781  Expr numerator = e[0];
2782  Expr denominator = e[1];
2783  if (getBaseType(numerator) != d_realType ||
2784  getBaseType(denominator) != d_realType) {
2785  throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
2786  "but got " + getBaseType(numerator).toString()+
2787  " and " + getBaseType(denominator).toString() +
2788  " for:\n" + e.toString());
2789  }
2790  if(denominator.isRational() && 1 == denominator.getRational())
2791  e.setType(numerator.getType());
2792  else
2793  e.setType(d_realType);
2794  break;
2795  }
2796  case LT:
2797  case LE:
2798  case GT:
2799  case GE:
2800  case GRAY_SHADOW:
2801  // Need to know types for all exprs -Clark
2802  // e.setType(boolType());
2803  // break;
2804  case DARK_SHADOW:
2805  for (int k = 0; k < e.arity(); ++k) {
2806  if (d_realType != getBaseType(e[k]))
2807  throw TypecheckException("Expecting type REAL with `" +
2808  getEM()->getKindName(e.getKind()) + "',\n"+
2809  "but got a " + getBaseType(e[k]).toString()+
2810  " for:\n" + e.toString());
2811  }
2812 
2813  e.setType(boolType());
2814  break;
2815  case IS_INTEGER:
2816  if(d_realType != getBaseType(e[0]))
2817  throw TypecheckException("Expected type REAL, but got "
2818  +getBaseType(e[0]).toString()
2819  +"\n\nExpr = "+e.toString());
2820  e.setType(boolType());
2821  break;
2822  default:
2823  DebugAssert(false,"TheoryArith3::computeType: unexpected expression:\n "
2824  +e.toString());
2825  break;
2826  }
2827 }
2828 
2829 
2831  IF_DEBUG(int kind = t.getExpr().getKind();)
2832  DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
2833  "TheoryArith3::computeBaseType("+t.toString()+")");
2834  return realType();
2835 }
2836 
2837 
2838 Expr
2840  Expr tcc(Theory::computeTCC(e));
2841  switch(e.getKind()) {
2842  case DIVIDE:
2843  DebugAssert(e.arity() == 2, "");
2844  return tcc.andExpr(!(e[1].eqExpr(rat(0))));
2845  default:
2846  return tcc;
2847  }
2848 }
2849 
2850 ///////////////////////////////////////////////////////////////////////////////
2851 //parseExprOp:
2852 //translating special Exprs to regular EXPR??
2853 ///////////////////////////////////////////////////////////////////////////////
2854 Expr
2856  TRACE("parser", "TheoryArith3::parseExprOp(", e, ")");
2857  //std::cout << "Were here";
2858  // If the expression is not a list, it must have been already
2859  // parsed, so just return it as is.
2860  switch(e.getKind()) {
2861  case ID: {
2862  int kind = getEM()->getKind(e[0].getString());
2863  switch(kind) {
2864  case NULL_KIND: return e; // nothing to do
2865  case REAL:
2866  case INT:
2867  case NEGINF:
2868  case POSINF: return getEM()->newLeafExpr(kind);
2869  default:
2870  DebugAssert(false, "Bad use of bare keyword: "+e.toString());
2871  return e;
2872  }
2873  }
2874  case RAW_LIST: break; // break out of switch, do the hard work
2875  default:
2876  return e;
2877  }
2878 
2879  DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
2880  "TheoryArith3::parseExprOp:\n e = "+e.toString());
2881 
2882  const Expr& c1 = e[0][0];
2883  int kind = getEM()->getKind(c1.getString());
2884  switch(kind) {
2885  case UMINUS: {
2886  if(e.arity() != 2)
2887  throw ParserException("UMINUS requires exactly one argument: "
2888  +e.toString());
2889  return uminusExpr(parseExpr(e[1]));
2890  }
2891  case PLUS: {
2892  vector<Expr> k;
2893  Expr::iterator i = e.begin(), iend=e.end();
2894  // Skip first element of the vector of kids in 'e'.
2895  // The first element is the operator.
2896  ++i;
2897  // Parse the kids of e and push them into the vector 'k'
2898  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
2899  return plusExpr(k);
2900  }
2901  case MINUS: {
2902  if(e.arity() == 2)
2903  return uminusExpr(parseExpr(e[1]));
2904  else if(e.arity() == 3)
2905  return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
2906  else
2907  throw ParserException("MINUS requires one or two arguments:"
2908  +e.toString());
2909  }
2910  case MULT: {
2911  vector<Expr> k;
2912  Expr::iterator i = e.begin(), iend=e.end();
2913  // Skip first element of the vector of kids in 'e'.
2914  // The first element is the operator.
2915  ++i;
2916  // Parse the kids of e and push them into the vector 'k'
2917  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
2918  return multExpr(k);
2919  }
2920  case POW: {
2921  return powExpr(parseExpr(e[1]), parseExpr(e[2]));
2922  }
2923  case DIVIDE:
2924  { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
2925  case LT:
2926  { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
2927  case LE:
2928  { return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
2929  case GT:
2930  { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
2931  case GE:
2932  { return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
2933  case INTDIV:
2934  case MOD:
2935  case SUBRANGE: {
2936  vector<Expr> k;
2937  Expr::iterator i = e.begin(), iend=e.end();
2938  // Skip first element of the vector of kids in 'e'.
2939  // The first element is the operator.
2940  ++i;
2941  // Parse the kids of e and push them into the vector 'k'
2942  for(; i!=iend; ++i)
2943  k.push_back(parseExpr(*i));
2944  return Expr(kind, k, e.getEM());
2945  }
2946  case IS_INTEGER: {
2947  if(e.arity() != 2)
2948  throw ParserException("IS_INTEGER requires exactly one argument: "
2949  +e.toString());
2950  return Expr(IS_INTEGER, parseExpr(e[1]));
2951  }
2952  default:
2953  DebugAssert(false,
2954  "TheoryArith3::parseExprOp: invalid input " + e.toString());
2955  break;
2956  }
2957  return e;
2958 }
2959 
2960 ///////////////////////////////////////////////////////////////////////////////
2961 // Pretty-printing //
2962 ///////////////////////////////////////////////////////////////////////////////
2963 
2964 
2965 ExprStream&
2967  switch(os.lang()) {
2968  case SIMPLIFY_LANG:
2969  switch(e.getKind()) {
2970  case RATIONAL_EXPR:
2971  e.print(os);
2972  break;
2973  case SUBRANGE:
2974  os <<"ERROR:SUBRANGE:not supported in Simplify\n";
2975  break;
2976  case IS_INTEGER:
2977  os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
2978  break;
2979  case PLUS: {
2980  int i=0, iend=e.arity();
2981  os << "(+ ";
2982  if(i!=iend) os << e[i];
2983  ++i;
2984  for(; i!=iend; ++i) os << " " << e[i];
2985  os << ")";
2986  break;
2987  }
2988  case MINUS:
2989  os << "(- " << e[0] << " " << e[1]<< ")";
2990  break;
2991  case UMINUS:
2992  os << "-" << e[0] ;
2993  break;
2994  case MULT: {
2995  int i=0, iend=e.arity();
2996  os << "(* " ;
2997  if(i!=iend) os << e[i];
2998  ++i;
2999  for(; i!=iend; ++i) os << " " << e[i];
3000  os << ")";
3001  break;
3002  }
3003  case POW:
3004  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
3005  break;
3006  case DIVIDE:
3007  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
3008  break;
3009  case LT:
3010  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
3011  }
3012  os << "(< " << e[0] << " " << e[1] <<")";
3013  break;
3014  case LE:
3015  os << "(<= " << e[0] << " " << e[1] << ")";
3016  break;
3017  case GT:
3018  os << "(> " << e[0] << " " << e[1] << ")";
3019  break;
3020  case GE:
3021  os << "(>= " << e[0] << " " << e[1] << ")";
3022  break;
3023  case DARK_SHADOW:
3024  case GRAY_SHADOW:
3025  os <<"ERROR:SHADOW:not supported in Simplify\n";
3026  break;
3027  default:
3028  // Print the top node in the default LISP format, continue with
3029  // pretty-printing for children.
3030  e.print(os);
3031 
3032  break;
3033  }
3034  break; // end of case SIMPLIFY_LANG
3035 
3036  case TPTP_LANG:
3037  switch(e.getKind()) {
3038  case RATIONAL_EXPR:
3039  e.print(os);
3040  break;
3041  case SUBRANGE:
3042  os <<"ERROR:SUBRANGE:not supported in TPTP\n";
3043  break;
3044  case IS_INTEGER:
3045  os <<"ERROR:IS_INTEGER:not supported in TPTP\n";
3046  break;
3047  case PLUS: {
3048  if(!isInteger(e[0])){
3049  os<<"ERRPR:plus only supports inteters now in TPTP\n";
3050  break;
3051  }
3052 
3053  int i=0, iend=e.arity();
3054  if(iend <=1){
3055  os<<"ERROR,plus must have more than two numbers in TPTP\n";
3056  break;
3057  }
3058 
3059  for(i=0; i <= iend-2; ++i){
3060  os << "$plus_int(";
3061  os << e[i] << ",";
3062  }
3063 
3064  os<< e[iend-1];
3065 
3066  for(i=0 ; i <= iend-2; ++i){
3067  os << ")";
3068  }
3069 
3070  break;
3071  }
3072  case MINUS:
3073  if(!isInteger(e[0])){
3074  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3075  break;
3076  }
3077 
3078  os << "$minus_int(" << e[0] << "," << e[1]<< ")";
3079  break;
3080  case UMINUS:
3081  if(!isInteger(e[0])){
3082  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3083  break;
3084  }
3085 
3086  os << "$uminus_int(" << e[0] <<")" ;
3087  break;
3088  case MULT: {
3089  if(!isInteger(e[0])){
3090  os<<"ERRPR:times only supports inteters now in TPTP\n";
3091  break;
3092  }
3093 
3094  int i=0, iend=e.arity();
3095  if(iend <=1){
3096  os<<"ERROR:times must have more than two numbers in TPTP\n";
3097  break;
3098  }
3099 
3100  for(i=0; i <= iend-2; ++i){
3101  os << "$times_int(";
3102  os << e[i] << ",";
3103  }
3104 
3105  os<< e[iend-1];
3106 
3107  for(i=0 ; i <= iend-2; ++i){
3108  os << ")";
3109  }
3110 
3111  break;
3112  }
3113  case POW:
3114 
3115  if(!isInteger(e[0])){
3116  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3117  break;
3118  }
3119 
3120  os << "$power_int(" << push << e[1] << space << "^ " << e[0] << push << ")";
3121  break;
3122 
3123  case DIVIDE:
3124  if(!isInteger(e[0])){
3125  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3126  break;
3127  }
3128 
3129  os << "divide_int(" <<e[0] << "," << e[1] << ")";
3130  break;
3131 
3132  case LT:
3133  if(!isInteger(e[0])){
3134  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3135  break;
3136  }
3137  os << "$less_int(" << e[0] << "," << e[1] <<")";
3138  break;
3139 
3140  case LE:
3141  if(!isInteger(e[0])){
3142  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3143  break;
3144  }
3145 
3146  os << "$lesseq_int(" << e[0] << "," << e[1] << ")";
3147  break;
3148 
3149  case GT:
3150  if(!isInteger(e[0])){
3151  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3152  break;
3153  }
3154 
3155  os << "$greater_int(" << e[0] << "," << e[1] << ")";
3156  break;
3157 
3158  case GE:
3159  if(!isInteger(e[0])){
3160  os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3161  break;
3162  }
3163 
3164  os << "$greatereq_int(" << e[0] << "," << e[1] << ")";
3165  break;
3166  case DARK_SHADOW:
3167  case GRAY_SHADOW:
3168  os <<"ERROR:SHADOW:not supported in TPTP\n";
3169  break;
3170 
3171  case INT:
3172  os <<"$int";
3173  break;
3174  case REAL:
3175  os <<"ERROR:REAL not supported in TPTP\n";
3176  default:
3177  // Print the top node in the default LISP format, continue with
3178  // pretty-printing for children.
3179  e.print(os);
3180 
3181  break;
3182  }
3183  break; // end of case TPTP_LANG
3184 
3185  case PRESENTATION_LANG:
3186  switch(e.getKind()) {
3187  case REAL:
3188  os << "REAL";
3189  break;
3190  case INT:
3191  os << "INT";
3192  break;
3193  case RATIONAL_EXPR:
3194  e.print(os);
3195  break;
3196  case NEGINF:
3197  os << "NEGINF";
3198  break;
3199  case POSINF:
3200  os << "POSINF";
3201  break;
3202  case SUBRANGE:
3203  if(e.arity() != 2) e.printAST(os);
3204  else
3205  os << "[" << push << e[0] << ".." << e[1] << push << "]";
3206  break;
3207  case IS_INTEGER:
3208  if(e.arity() == 1)
3209  os << "IS_INTEGER(" << push << e[0] << push << ")";
3210  else
3211  e.printAST(os);
3212  break;
3213  case PLUS: {
3214  int i=0, iend=e.arity();
3215  os << "(" << push;
3216  if(i!=iend) os << e[i];
3217  ++i;
3218  for(; i!=iend; ++i) os << space << "+ " << e[i];
3219  os << push << ")";
3220  break;
3221  }
3222  case MINUS:
3223  os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
3224  break;
3225  case UMINUS:
3226  os << "-(" << push << e[0] << push << ")";
3227  break;
3228  case MULT: {
3229  int i=0, iend=e.arity();
3230  os << "(" << push;
3231  if(i!=iend) os << e[i];
3232  ++i;
3233  for(; i!=iend; ++i) os << space << "* " << e[i];
3234  os << push << ")";
3235  break;
3236  }
3237  case POW:
3238  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
3239  break;
3240  case DIVIDE:
3241  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
3242  break;
3243  case LT:
3244  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
3245  }
3246  os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
3247  break;
3248  case LE:
3249  os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
3250  break;
3251  case GT:
3252  os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
3253  break;
3254  case GE:
3255  os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
3256  break;
3257  case DARK_SHADOW:
3258  os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
3259  break;
3260  case GRAY_SHADOW:
3261  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
3262  << "," << space << e[2] << "," << space << e[3] << push << ")";
3263  break;
3264  default:
3265  // Print the top node in the default LISP format, continue with
3266  // pretty-printing for children.
3267  e.printAST(os);
3268 
3269  break;
3270  }
3271  break; // end of case PRESENTATION_LANG
3272  case SMTLIB_LANG:
3273  case SMTLIB_V2_LANG: {
3274  switch(e.getKind()) {
3275  case REAL_CONST:
3276  printRational(os, e[0].getRational(), true);
3277  break;
3278  case RATIONAL_EXPR:
3279  printRational(os, e.getRational());
3280  break;
3281  case REAL:
3282  os << "Real";
3283  break;
3284  case INT:
3285  os << "Int";
3286  break;
3287  case SUBRANGE:
3288  throw SmtlibException("TheoryArith3::print: SMTLIB: SUBRANGE not implemented");
3289 // if(e.arity() != 2) e.print(os);
3290 // else
3291 // os << "(" << push << "SUBRANGE" << space << e[0]
3292 // << space << e[1] << push << ")";
3293  break;
3294  case IS_INTEGER:
3295  if(e.arity() == 1)
3296  os << "(" << push << "IsInt" << space << e[0] << push << ")";
3297  else
3298  throw SmtlibException("TheoryArith3::print: SMTLIB: IS_INTEGER used unexpectedly");
3299  break;
3300  case PLUS: {
3301  if(e.arity() == 1 && os.lang() == SMTLIB_V2_LANG) {
3302  os << e[0];
3303  } else {
3304  os << "(" << push << "+";
3305  Expr::iterator i = e.begin(), iend = e.end();
3306  for(; i!=iend; ++i) {
3307  os << space << (*i);
3308  }
3309  os << push << ")";
3310  }
3311  break;
3312  }
3313  case MINUS: {
3314  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
3315  break;
3316  }
3317  case UMINUS: {
3318  os << "(" << push << "-" << space << e[0] << push << ")";
3319  break;
3320  }
3321  case MULT: {
3322  int i=0, iend=e.arity();
3323  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
3324  os << e[0];
3325  } else {
3326  for(; i!=iend; ++i) {
3327  if (i < iend-1) {
3328  os << "(" << push << "*";
3329  }
3330  os << space << e[i];
3331  }
3332  for (i=0; i < iend-1; ++i) os << push << ")";
3333  }
3334  break;
3335  }
3336  case POW:
3337  throw SmtlibException("TheoryArith3::print: SMTLIB: POW not supported");
3338  // os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
3339  break;
3340  case DIVIDE: {
3341  throw SmtlibException("TheoryArith3::print: SMTLIB: unexpected use of DIVIDE");
3342  break;
3343  }
3344  case LT: {
3345  Rational r;
3346  os << "(" << push << "<" << space;
3347  os << e[0] << space << e[1] << push << ")";
3348  break;
3349  }
3350  case LE: {
3351  Rational r;
3352  os << "(" << push << "<=" << space;
3353  os << e[0] << space << e[1] << push << ")";
3354  break;
3355  }
3356  case GT: {
3357  Rational r;
3358  os << "(" << push << ">" << space;
3359  os << e[0] << space << e[1] << push << ")";
3360  break;
3361  }
3362  case GE: {
3363  Rational r;
3364  os << "(" << push << ">=" << space;
3365  os << e[0] << space << e[1] << push << ")";
3366  break;
3367  }
3368  case DARK_SHADOW:
3369  throw SmtlibException("TheoryArith3::print: SMTLIB: DARK_SHADOW not supported");
3370  os << "(" << push << "DARK_SHADOW" << space << e[0]
3371  << space << e[1] << push << ")";
3372  break;
3373  case GRAY_SHADOW:
3374  throw SmtlibException("TheoryArith3::print: SMTLIB: GRAY_SHADOW not supported");
3375  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
3376  << "," << space << e[2] << "," << space << e[3] << push << ")";
3377  break;
3378  default:
3379  throw SmtlibException("TheoryArith3::print: SMTLIB: default not supported");
3380  // Print the top node in the default LISP format, continue with
3381  // pretty-printing for children.
3382  e.printAST(os);
3383 
3384  break;
3385  }
3386  break; // end of case SMTLIB_LANG
3387  }
3388  case LISP_LANG:
3389  switch(e.getKind()) {
3390  case REAL:
3391  case INT:
3392  case RATIONAL_EXPR:
3393  case NEGINF:
3394  case POSINF:
3395  e.print(os);
3396  break;
3397  case SUBRANGE:
3398  if(e.arity() != 2) e.printAST(os);
3399  else
3400  os << "(" << push << "SUBRANGE" << space << e[0]
3401  << space << e[1] << push << ")";
3402  break;
3403  case IS_INTEGER:
3404  if(e.arity() == 1)
3405  os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
3406  else
3407  e.printAST(os);
3408  break;
3409  case PLUS: {
3410  int i=0, iend=e.arity();
3411  os << "(" << push << "+";
3412  for(; i!=iend; ++i) os << space << e[i];
3413  os << push << ")";
3414  break;
3415  }
3416  case MINUS:
3417  //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
3418  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
3419  break;
3420  case UMINUS:
3421  os << "(" << push << "-" << space << e[0] << push << ")";
3422  break;
3423  case MULT: {
3424  int i=0, iend=e.arity();
3425  os << "(" << push << "*";
3426  for(; i!=iend; ++i) os << space << e[i];
3427  os << push << ")";
3428  break;
3429  }
3430  case POW:
3431  os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
3432  break;
3433  case DIVIDE:
3434  os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
3435  break;
3436  case LT:
3437  os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
3438  break;
3439  case LE:
3440  os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
3441  break;
3442  case GT:
3443  os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
3444  break;
3445  case GE:
3446  os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
3447  break;
3448  case DARK_SHADOW:
3449  os << "(" << push << "DARK_SHADOW" << space << e[0]
3450  << space << e[1] << push << ")";
3451  break;
3452  case GRAY_SHADOW:
3453  os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
3454  << e[1] << space << e[2] << space << e[3] << push << ")";
3455  break;
3456  default:
3457  // Print the top node in the default LISP format, continue with
3458  // pretty-printing for children.
3459  e.printAST(os);
3460 
3461  break;
3462  }
3463  break; // end of case LISP_LANG
3464  default:
3465  // Print the top node in the default LISP format, continue with
3466  // pretty-printing for children.
3467  e.printAST(os);
3468  }
3469  return os;
3470 }
Expr minusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:205
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
Definition: theory.cpp:119
void refineCounterExample()
Process disequalities from the arrangement for model generation.
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
int arity() const
Definition: expr.h:1201
virtual Theorem multEqn(const Expr &x, const Expr &y, const Expr &z)=0
x = y <==> x * z = y * z, where z is a non-zero constant
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
iterator begin() const
Begin iterator.
Definition: expr.h:1211
bool isEq() const
Definition: expr.h:419
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
void checkType(const Expr &e)
Check that e is a valid Type expr.
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
Definition: theory.cpp:557
void setRewriteNormal() const
Definition: expr.h:1457
bool isInt(Type t)
Definition: theory_arith.h:174
Expr ltExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:221
ArithProofRules * d_rules
Definition: theory_arith3.h:31
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem typePred(const Expr &e)
Return BOOLEAN type.
Definition: theory.cpp:918
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
Definition: theory.cpp:148
bool isLeafIn(const Expr &e1, const Expr &e2)
Test if e1 is an i-leaf in e2.
Definition: theory.cpp:546
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
An exception thrown by the parser.
bool isLeaf(const Expr &e)
Test if e is an i-leaf term for the current theory.
Definition: theory.h:556
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
Definition: theory.cpp:103
void computeType(const Expr &e)
Compute and store the type of e.
bool isTrue() const
Definition: expr.h:356
bool isRational() const
Definition: expr.h:431
Rational getNumerator() const
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
virtual Theorem constPredicate(const Expr &e)=0
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem negatedInequality(const Expr &e)=0
Propagating negation over <,<=,>,>=.
bool isIntPred(const Expr &e)
Definition: theory_arith.h:194
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
Definition: expr.cpp:517
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
Definition: expr_map.h:194
Data class for the strongest free constant in separation inqualities.
Definition: theory_arith3.h:35
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
bool isLE(const Expr &e)
Definition: theory_arith.h:187
bool isFalse() const
Definition: expr.h:355
void setFind(const Theorem &e) const
Set the find attribute to e.
Definition: expr.h:1405
for output in TPTP format
Definition: lang.h:46
T max(T a, T b)
Definition: cvc_util.h:56
Theorem canon(const Expr &e)
Canonize the expression e, assuming all children are canonical.
MS C++ specific settings.
Definition: type.h:42
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Definition: theory.cpp:128
CDO< size_t > d_bufferIdx
Buffer index of the next unprocessed inequality.
Definition: theory_arith3.h:93
SMT-LIB v2 format.
Definition: lang.h:52
bool varOnRHS() const
Flag whether var is isolated on the RHS.
Definition: theory_arith3.h:65
STL namespace.
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
static T min(T x, T y)
iterator begin()
Definition: expr_map.h:190
bool isGE(const Expr &e)
Definition: theory_arith.h:189
Lisp-like format for automatically generated specs.
Definition: lang.h:36
Definition: kinds.h:66
void printRational(ExprStream &os, const Rational &r, bool printAsReal=false)
Print a rational in SMT-LIB format.
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
Definition: theory_arith3.h:78
CDO< size_t > d_diseqIdx
Definition: theory_arith3.h:30
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
virtual Theorem rightMinusLeft(const Expr &e)=0
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
std::string toString(int base=10) const
ExprStream & space(ExprStream &os)
Insert a single white space separator.
void assignVariables(std::vector< Expr > &v)
Expr gtExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:225
virtual Theorem splitGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
Theorem canonPredEquiv(const Theorem &thm)
bool hasFind() const
Definition: expr.h:1232
virtual Theorem finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
An exception thrown by the arithmetic decision procedure.
bool isGT(const Expr &e)
Definition: theory_arith.h:188
bool isOr() const
Definition: expr.h:422
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
bool isIntx(const Expr &e, const Rational &x)
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
bool isPlus(const Expr &e)
Definition: theory_arith.h:181
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
Expr andExpr(const Expr &right) const
Definition: expr.h:941
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
Definition: theory_arith.h:177
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
Definition: theory_arith3.h:75
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
const Expr & getExpr() const
Definition: type.h:52
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
Definition: theory.h:714
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
Definition: theory.cpp:162
bool isNot() const
Definition: expr.h:420
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
Definition: theory.h:96
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
const Theorem & ineq() const
Get the inequality.
Definition: theory_arith3.h:61
virtual Theorem iffTrue(const Theorem &e)=0
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
Definition: kinds.h:44
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
bool empty() const
Definition: expr_map.h:170
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
CDList< Theorem > d_buffer
Buffer of input inequalities.
Definition: theory_arith3.h:91
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
bool isInteger() const
std::string toString() const
Definition: theorem.h:404
virtual Theorem expandDarkShadow(const Theorem &darkShadow)=0
DARK_SHADOW(t1, t2) ==> t1 <= t2.
ArithProofRules * createProofRules3()
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
virtual Theorem grayShadowConst(const Theorem &g)=0
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
static int left(int i)
Definition: minisat_heap.h:53
virtual Theorem multIneqn(const Expr &e, const Expr &z)=0
Multiplying inequation by a non-zero constant.
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
virtual Theorem expandGrayShadow0(const Theorem &g)=0
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
bool isBoolConst() const
Definition: expr.h:357
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
Rational getDenominator() const
T abs(T t)
Definition: cvc_util.h:53
std::string int2string(int n)
Definition: cvc_util.h:46
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
Definition: theory.h:430
const Rational & getConst() const
Definition: theory_arith3.h:42
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Definition: theory.h:503
virtual Theorem flipInequality(const Expr &e)=0
"op1 GE|GT op2" <==> op2 LE|LT op1
CDList< Theorem > d_diseq
Definition: theory_arith3.h:29
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)
std::string toString() const
Definition: type.h:80
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
Definition: theory_arith.h:216
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
const int * d_bufferThres
Threshold when the buffer must be processed.
Definition: theory_arith3.h:95
#define IF_DEBUG(code)
Definition: debug.h:406
const Expr & trueExpr()
Return TRUE Expr.
Definition: theory.h:582
unsigned int getUnsigned() const
unsigned size() const
Definition: cdlist.h:64
bool isIntegerConst(const Expr &e)
Definition: theory_arith.h:178
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
bool isIneq(const Expr &e)
Definition: theory_arith.h:192
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
bool isDarkShadow(const Expr &e)
Definition: theory_arith.h:190
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
static int right(int i)
Definition: minisat_heap.h:54
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
Expr rat(Rational r)
Definition: theory_arith.h:156
Private class for an inequality in the Fourier-Motzkin database.
Definition: theory_arith3.h:49
Type boolType()
Return BOOLEAN type.
Definition: theory.h:576
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
const FreeConst & getConst() const
Get the max/min constant.
Definition: theory_arith3.h:63
An exception to be thrown by the smtlib translator.
Expr computeNormalFactor(const Expr &rhs)
Given a canonized term, compute a factor to make all coefficients integer and relatively prime...
Arithmetic proof rules.
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
bool isLT(const Expr &e)
Definition: theory_arith.h:186
SMT-LIB format.
Definition: lang.h:34
Expr plusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:199
bool isGrayShadow(const Expr &e)
Definition: theory_arith.h:191
ostream & operator<<(ostream &os, const TheoryArith3::Ineq &ineq)
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
const Expr & getLHS() const
Definition: theorem.cpp:240
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
Definition: expr.h:1416
const Data & get() const
Definition: cdmap.h:106
Expr geExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:227
void processBuffer()
Process inequalities in the buffer.
void processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)
Check if alpha <= ax & bx <= beta is a finite interval for integer var 'x', and assert the corresponding ...
Definition: kinds.h:61
bool recursiveCanonSimpCheck(const Expr &e)
helper for checkAssertEqInvariant
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
Theorem normalize(const Expr &e)
Normalize an equation (make all coefficients rel. prime integers)
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition: theory.h:686
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
An optional solver.
CDO< bool > d_inModelCreation
Definition: theory_arith3.h:32
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
bool isReal(Type t)
Definition: theory_arith.h:173
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
bool isPow(const Expr &e)
Definition: theory_arith.h:185
Definition: expr.cpp:35
Expr uminusExpr(const Expr &child)
Definition: theory_arith.h:197
Definition: kinds.h:99
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
Expr leExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:223
bool isRewrite() const
Definition: theorem.cpp:224
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
void addToBuffer(const Theorem &thm)
Add an inequality to the input buffer. See also d_buffer.
VarOrderGraph d_graph
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
bool isMult(const Expr &e)
Definition: theory_arith.h:183
Expr divideExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:219
Theorem canonSimp(const Expr &e)
simplify leaves and then canonize
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
virtual Theorem expandGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
Rational ratRoot(const Rational &base, unsigned long int n)
take nth root of base, return result if it is exact, 0 otherwise
Definition: rational.h:172
for output into Simplify format
Definition: lang.h:43
virtual Theorem diseqToIneq(const Theorem &diseq)=0
x /= y ==> (x < y) OR (x > y)
virtual Theorem andElim(const Theorem &e, int i)=0
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Expr multExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:207
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677
Nice SAL-like language for manually written specs.
Definition: lang.h:32
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421