CVC3  2.4.1
theory_arith_new.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith_new.cpp
4  *
5  * Author: Dejan Jovanovic
6  *
7  * Created: Thu Jun 14 13:42:00 2007
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "theory_arith_new.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 // TheoryArithNew::FreeConst Methods //
40 ///////////////////////////////////////////////////////////////////////////////
41 
42 namespace CVC3 {
43 
44 ostream& operator<<(ostream& os, const TheoryArithNew::FreeConst& fc) {
45  os << "FreeConst(r=" << fc.getConst() << ", "
46  << (fc.strict()? "strict" : "non-strict") << ")";
47  return os;
48 }
49 
50 ///////////////////////////////////////////////////////////////////////////////
51 // TheoryArithNew::Ineq Methods //
52 ///////////////////////////////////////////////////////////////////////////////
53 
54 ostream& operator<<(ostream& os, const TheoryArithNew::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 // TheoryArithNew Private Methods //
65 ///////////////////////////////////////////////////////////////////////////////
66 
67 
68 Theorem TheoryArithNew::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 TheoryArithNew::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 
94 bool TheoryArithNew::kidsCanonical(const Expr& e) {
95  if(isLeaf(e)) return true;
96  bool res(true);
97  for(int i=0; res && i<e.arity(); ++i) {
98  Expr simp(canon(e[i]).getRHS());
99  res = (e[i] == simp);
100  IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
101  << "\nsimplified = " << simp << endl;)
102  }
103  return res;
104 }
105 
106 
107 
108 
109 /**
110  * Compute a canonical form for expression e and return a theorem that e is equal to its canonical form.
111  * Note that canonical form for arith expressions is of the following form:
112  *
113  * b + a_1 x_1 + a_2 x_2 + ... + a_n x_n (ONE SUM EXPRESION)
114  *
115  * or just a rational b (RATIONAL EXPRESSION)
116  *
117  * where a_i and b are rationals and x_i are arithmetical leaves (i.e. variables or non arithmetic terms)
118  *
119  * @author Clark Barrett
120  * @author Vijay Ganesh
121  * @since Sat Feb 8 14:46:32 2003
122  */
123 Theorem TheoryArithNew::canon(const Expr& e)
124 {
125  // Trace the arith canon of the expression in the debug version
126  TRACE("arith", "canon(", e , ") {");
127 
128  // The invariant is that the kids of the expression should already be canonised
129  //DebugAssert(kidsCanonical(e), "TheoryArithNew::canon("+e.toString()+")");
130 
131  // The resulting theorem object
132  Theorem result;
133 
134  switch (e.getKind()) {
135 
136  // -E
137  case UMINUS: {
138 
139  // Convert the unary minus to multiplication with -1
140  result = d_rules->uMinusToMult(e[0]);
141 
142  // Get the resulting epression
143  Expr e2 = result.getRHS();
144 
145  // Canonise the resulting expression and combine the theorems
146  result = transitivityRule(result, canon(e2));
147 
148  // UMINUS case break
149  break;
150  }
151 
152  // e[0] + e[1]
153  case PLUS:
154 
155  // Call the canonPlus procedure to canonise +
156  result = d_rules->canonPlus(e);
157 
158  // PLUS case break
159  break;
160 
161  // e[0] - e[1]
162  case MINUS: {
163 
164  // Arity of the minus should be exactly 2 (TODO: looks useless, maybe remove)
165  DebugAssert(e.arity() == 2," ");
166 
167  // This produces e[0] + (-1)*e[1], we have to canonize it in 2 steps
168  Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
169 
170  // The resulting sum expression
171  Expr sum(minus_eq_sum.getRHS());
172 
173  // Canonise the sum[1]
174  Theorem thm(canon(sum[1]));
175 
176  // If the sum[1] sayed the same, canonise the sum expression
177  if(thm.getLHS() == thm.getRHS())
178  result = canonThm(minus_eq_sum);
179  // The sum changed; do the work
180  else {
181 
182  // Substitute and try to canonise again
183  Theorem sum_eq_canon = canonThm(substitutivityRule(sum, 1, thm));
184 
185  // Combine the results, and thats it
186  result = transitivityRule(minus_eq_sum, sum_eq_canon);
187  }
188 
189  // MINUS case break
190  break;
191 
192  }
193 
194  // e[0] * e[1]
195  case MULT:
196 
197  // Canonise using the canonMult() proof rule
198  result = d_rules->canonMult(e);
199 
200  // MULT case break
201  break;
202 
203  // e[0] DIV e[1]
204  case DIVIDE: {
205 
206  // Division by 0 is OK (total extension, protected by TCCs)
207  // if (e[1].isRational() && e[1].getRational() == 0)
208  // throw ArithException("Divide by 0 error in "+e.toString());
209  if (e[1].getKind() == PLUS)
210  throw ArithException("Divide by a PLUS expression not handled in" + e.toString());
211 
212  // Canonise the divite using canonDivide() method
213  result = d_rules->canonDivide(e);
214 
215  // DIVIDE case break
216  break;
217  }
218 
219  // e[0]^e[1]
220  case POW :
221 
222  // If we are raising to a constant rational call canonPowConst() proof rule
223  if(e[1].isRational()) result = d_rules->canonPowConst(e);
224  // Othervise just return the same expression
225  else result = reflexivityRule(e);
226 
227  // POW case break
228  break;
229 
230  default:
231 
232  // How did we get here (TODO: check if need to throw and exception), anyhow, just return the reflexivity rule
233  result = reflexivityRule(e);
234 
235  // Default break
236  break;
237  }
238 
239  // Finished with the canonisation, trace the result in the debug version
240  TRACE("arith","canon => ",result," }");
241 
242  // Return the resulting theorem
243  return result;
244 }
245 
246 Theorem TheoryArithNew::canonSimplify(const Expr& e) {
247  // Trace the function on the arith trace flag
248  TRACE("arith", "canonSimplify(", e, ") {");
249 
250  // Assert that all the kids must be already canonical
251  //DebugAssert(kidsCanonical(e), "TheoryArithNew::canonSimplify("+e.toString()+")");
252  // Assert that all the leaves must be simplified
253  //DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
254 
255  // Make a copy of the expression
256  Expr tmp(e);
257 
258  // Canonise the expresion
259  Theorem thm = canon(e);
260 
261  // If the new simplified expression has a find, use it (TODO: Check whats going on here)
262  if(thm.getRHS().hasFind())
263  thm = transitivityRule(thm, find(thm.getRHS()));
264 
265  // We shouldn't rely on simplification in this function anymore
266  DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()), "canonSimplify("+e.toString()+")\n"+"canon(e) = "+thm.getRHS().toString()+"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
267 
268  // Trace the resulting theorem
269  TRACE("arith", "canonSimplify =>", thm, " }");
270 
271  // Return the theorem
272  return thm;
273 }
274 
275 /*! accepts a theorem, canonizes it, applies iffMP and substituvity to
276  * derive the canonized thm
277  */
278 Theorem
279 TheoryArithNew::canonPred(const Theorem& thm) {
280  vector<Theorem> thms;
281  DebugAssert(thm.getExpr().arity() == 2,
282  "TheoryArithNew::canonPred: bad theorem: "+thm.toString());
283  Expr e(thm.getExpr());
284  thms.push_back(canonSimplify(e[0]));
285  thms.push_back(canonSimplify(e[1]));
286  return iffMP(thm, substitutivityRule(e.getOp(), thms));
287 }
288 
289 /**
290  * Accepts an equivalence theorem, canonizes the subexpressions, applies transitivity and substituvity to derive the canonized theorem.
291  *
292  * @param thm equivalence theorem
293  * @return the canonised expression theorem
294  */
295 Theorem TheoryArithNew::canonPredEquiv(const Theorem& thm) {
296 
297  vector<Theorem> thms; // Vector to hold the simplified versions of e[0] and e[1]
298 
299  // Arity of the expression should be 2
300  DebugAssert(thm.getRHS().arity() == 2, "TheoryArithNew::canonPredEquiv: bad theorem: " + thm.toString());
301 
302  // Get the expression of the theorem
303  Expr e(thm.getRHS());
304 
305  // Simplify both sides of the equivalence
306  thms.push_back(canonSimplify(e[0]));
307  thms.push_back(canonSimplify(e[1]));
308 
309  // Return the theorem substituting e[0] and e[1] with their simplified versions
310  return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
311 }
312 
313 /*! accepts an equivalence theorem whose RHS is a conjunction,
314  * canonizes it, applies iffMP and substituvity to derive the
315  * canonized thm
316  */
317 Theorem
318 TheoryArithNew::canonConjunctionEquiv(const Theorem& thm) {
319  vector<Theorem> thms;
320  return thm;
321 }
322 
323 /*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
324  * -# translate e to the form e' = 0
325  * -# if (e'.isRational()) then {if e' != 0 return false else true}
326  * -# a for loop checks if all the variables are integers.
327  * - if not isolate a suitable real variable and call processRealEq().
328  * - if all variables are integers then isolate suitable variable
329  * and call processIntEq().
330  */
331 Theorem TheoryArithNew::doSolve(const Theorem& thm)
332 {
333  const Expr& e = thm.getExpr();
334  TRACE("arith eq","doSolve(",e,") {");
335  DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
336  Theorem eqnThm;
337  vector<Theorem> thms;
338  // Move LHS to the RHS, if necessary
339  if(e[0].isRational() && e[0].getRational() == 0)
340  eqnThm = thm;
341  else {
342  eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
343  eqnThm = canonPred(eqnThm);
344  }
345  // eqnThm is of the form 0 = e'
346  // 'right' is of the form e'
347  Expr right = eqnThm.getRHS();
348  // Check for trivial equation
349  if (right.isRational()) {
350  Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
351  TRACE("arith eq","doSolve => ",result," }");
352  return result;
353  }
354 
355  //normalize
356  eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
357  right = eqnThm.getRHS();
358 
359  //eqn is of the form 0 = e' and is normalized where 'right' denotes e'
360  //FIXME: change processRealEq to accept equations as well instead of theorems
361  if(!isInteger(right)) {
362  Theorem res;
363  try {
364  res = processRealEq(eqnThm);
365  } catch(ArithException& e) {
366  res = symmetryRule(eqnThm); // Flip to e' = 0
367  TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
368  IF_DEBUG(debugger.counter("FAILED to solve real equalities")++;)
369  setIncomplete("Non-linear arithmetic inequalities");
370  }
371  IF_DEBUG(debugger.counter("solved real equalities")++;)
372  TRACE("arith eq", "doSolve [real] => ", res, " }");
373  return res;
374  }
375  else {
376  Theorem res = processIntEq(eqnThm);
377  IF_DEBUG(debugger.counter("solved int equalities")++;)
378  TRACE("arith eq", "doSolve [int] => ", res, " }");
379  return res;
380  }
381 }
382 
383 /*! pick a monomial for the input equation. This function is used only
384  * if the equation is an integer equation. Choose the monomial with
385  * the smallest absolute value of coefficient.
386  */
387 Expr
388 TheoryArithNew::pickIntEqMonomial(const Expr& right)
389 {
390  DebugAssert(isPlus(right) && right.arity() > 2,
391  "TheoryArithNew::pickIntEqMonomial right is wrong :-): " +
392  right.toString());
393  DebugAssert(right[0].isRational(),
394  "TheoryArithNew::pickIntEqMonomial. right[0] must be const" +
395  right.toString());
396  DebugAssert(isInteger(right),
397  "TheoryArithNew::pickIntEqMonomial: right is of type int: " +
398  right.toString());
399  //right is of the form "C + a1x1 + ... + anxn". min is initialized
400  //to a1
401  Expr::iterator i = right.begin();
402  i++; //skip 'C'
403  Rational min = isMult(*i) ? abs((*i)[0].getRational()) : 1;
404  Expr pickedMon = *i;
405  for(Expr::iterator iend = right.end(); i != iend; ++i) {
406  Rational coeff = isMult(*i) ? abs((*i)[0].getRational()) : 1;
407  if(min > coeff) {
408  min = coeff;
409  pickedMon = *i;
410  }
411  }
412  return pickedMon;
413 }
414 
415 /*! input is e1=e2<==>0=e' Theorem and some of the vars in e' are of
416  * type REAL. isolate one of them and send back to framework. output
417  * is "e1=e2 <==> var = e''" Theorem.
418  */
419 Theorem
420 TheoryArithNew::processRealEq(const Theorem& eqn)
421 {
422  Expr right = eqn.getRHS();
423  // Find variable to isolate and store it in left. Pick the largest
424  // (according to the total ordering) variable. FIXME: change from
425  // total ordering to the ordering we devised for inequalities.
426 
427  // TODO: I have to pick a variable that appears as a variable in the
428  // term but does not appear as a variable anywhere else. The variable
429  // must appear as a single leaf and not in a MULT expression with some
430  // other variables and nor in a POW expression.
431 
432  bool found = false;
433 
434  Expr left;
435 
436  if (isPlus(right)) {
437  for(int i = right.arity()-1; i>=0; --i) {
438  Expr c = right[i];
439  if(isRational(c))
440  continue;
441  if(!isInteger(c)) {
442  if (isLeaf(c) ||
443  ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
444  int numoccurs = 0;
445  Expr leaf = isLeaf(c) ? c : c[1];
446  for (int j = 0; j < right.arity(); ++j) {
447  if (j!= i
448  && isLeafIn(leaf, right[j])
449  // && leaf.subExprOf(right[j])
450  ) {
451  numoccurs++;
452  break;
453  }
454  }
455  if (!numoccurs) {
456  left = c;
457  found = true;
458  break;
459  }
460  }
461  }
462  }
463  }
464  else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
465  isLeaf(right)) {
466  left = right;
467  found = true;
468  }
469 
470  if (!found) {
471  // TODO:
472  // throw an arithmetic exception that this cannot be done.
473  throw
474  ArithException("Can't find a leaf for solve in "+eqn.toString());
475  }
476 
477  Rational r = -1;
478  if (isMult(left)) {
479  DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
480  DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
481  r = -1/left[0].getRational();
482  left = left[1];
483  }
484 
485  DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
486  "TheoryArithNew::ProcessRealEq: left is integer:\n left = "
487  +left.toString());
488  // Normalize equation so that coefficient of the monomial
489  // corresponding to "left" in eqn[1] is -1
490  Theorem result(iffMP(eqn,
491  d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
492  result = canonPred(result);
493 
494  // Isolate left
495  result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
496  result.getRHS(), left, EQ));
497  result = canonPred(result);
498  TRACE("arith","processRealEq => ",result," }");
499  return result;
500 }
501 
502 /*!
503  * \param eqn is a single equation 0 = e
504  * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
505  */
506 Theorem
507 TheoryArithNew::processSimpleIntEq(const Theorem& eqn)
508 {
509  TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
510  DebugAssert(eqn.isRewrite(),
511  "TheoryArithNew::processSimpleIntEq: eqn must be equality" +
512  eqn.getExpr().toString());
513 
514  Expr right = eqn.getRHS();
515 
516  DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
517  "TheoryArithNew::processSimpleIntEq: LHS must be 0:\n" +
518  eqn.getExpr().toString());
519 
520  //recall that 0 = c case is already handled in doSolve() function.
521  if(isMult(right)) {
522  //here we take care of special case 0=c.x
523  Expr c,x;
524  separateMonomial(right, c, x);
525  Theorem isIntx(isIntegerThm(x));
526  DebugAssert(!isIntx.isNull(), "right = "+right.toString());
527  Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
528  TRACE("arith eq", "processSimpleIntEq[0 = a*x] => ", res, " }");
529  return res;
530  } else if(isPlus(right)) {
531  if(2 == right.arity()) {
532  //we take care of special cases like 0 = c + a.x, 0 = c + x,
533  Expr c,x;
534  separateMonomial(right[1], c, x);
535  Theorem isIntx(isIntegerThm(x));
536  DebugAssert(!isIntx.isNull(), "right = "+right.toString()
537  +"\n x = "+x.toString());
538  Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
539  TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
540  return res;
541  }
542  DebugAssert(right.arity() > 2,
543  "TheoryArithNew::processSimpleIntEq: RHS is not in correct form:"
544  +eqn.getExpr().toString());
545  // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
546  Expr isolated = pickIntEqMonomial(right);
547  TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
548 
549  // First, we compute the 'sign factor' with which to multiply the
550  // eqn. if the coeff of isolated is positive (i.e. 'isolated' is
551  // of the form x or a.x where a>0 ) then r must be -1 and if coeff
552  // of 'isolated' is negative, r=1.
553  Rational r = isMult(isolated) ?
554  ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
555  Theorem result;
556  if (-1 == r) {
557  // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
558  // positive. modify eqn (0=e') to the equation (0=canon(-1*e'))
559  result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
560  result = canonPred(result);
561  Expr e = result.getRHS();
562 
563  // Isolate the 'isolated'
564  result = iffMP(result,
565  d_rules->plusPredicate(result.getLHS(),result.getRHS(),
566  isolated, EQ));
567  } else {
568  //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
569  const Rational& minusa = isolated[0].getRational();
570  Rational a = -1*minusa;
571  isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
572 
573  // Isolate the 'isolated'
574  result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
575  right,isolated,EQ));
576  }
577  // Canonize the result
578  result = canonPred(result);
579 
580  //if isolated is 'x' or 1*x, then return result else continue processing.
581  if(!isMult(isolated) || isolated[0].getRational() == 1) {
582  TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
583  return result;
584  } else {
585  DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
586  "TheoryArithNew::processSimpleIntEq: isolated must be mult "
587  "with coeff >= 2.\n isolated = " + isolated.toString());
588 
589  // Compute IS_INTEGER() for lhs and rhs
590  Expr lhs = result.getLHS();
591  Expr rhs = result.getRHS();
592  Expr a, x;
593  separateMonomial(lhs, a, x);
594  Theorem isIntLHS = isIntegerThm(x);
595  vector<Theorem> isIntRHS;
596  if(!isPlus(rhs)) { // rhs is a MULT
597  Expr c, v;
598  separateMonomial(rhs, c, v);
599  isIntRHS.push_back(isIntegerThm(v));
600  DebugAssert(!isIntRHS.back().isNull(), "");
601  } else { // rhs is a PLUS
602  DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
603  DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
604  Expr::iterator i=rhs.begin(), iend=rhs.end();
605  ++i; // Skip the free constant
606  for(; i!=iend; ++i) {
607  Expr c, v;
608  separateMonomial(*i, c, v);
609  isIntRHS.push_back(isIntegerThm(v));
610  DebugAssert(!isIntRHS.back().isNull(), "");
611  }
612  }
613  // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
614  result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
615  // Skolemize the quantifier
616  result = getCommonRules()->skolemize(result);
617  // Canonize t2 and t3 generated by this rule
618  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
619  "processSimpleIntEq: result = "+result.getExpr().toString());
620  Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
621  Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
622  Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
623  if(newRes.getExpr() != result.getExpr()) result = newRes;
624 
625  TRACE("arith eq", "processSimpleIntEq => ", result, " }");
626  return result;
627  }
628  } else {
629  // eqn is 0 = x. Flip it and return
630  Theorem result = symmetryRule(eqn);
631  TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
632  return result;
633  }
634 }
635 
636 /*! input is e1=e2<==>0=e' Theorem and all of the vars in e' are of
637  * type INT. isolate one of them and send back to framework. output
638  * is "e1=e2 <==> var = e''" Theorem and some associated equations in
639  * solved form.
640  */
641 Theorem
642 TheoryArithNew::processIntEq(const Theorem& eqn)
643 {
644  TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
645  // Equations in the solved form.
646  std::vector<Theorem> solvedAndNewEqs;
647  Theorem newEq(eqn), result;
648  bool done(false);
649  do {
650  result = processSimpleIntEq(newEq);
651  // 'result' is of the from (x1=t1) AND 0=t'
652  if(result.isRewrite()) {
653  solvedAndNewEqs.push_back(result);
654  done = true;
655  }
656  else if(!result.getExpr().isFalse()) {
657  DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
658  "TheoryArithNew::processIntEq("+eqn.getExpr().toString()
659  +")\n result = "+result.getExpr().toString());
660  solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
661  newEq = getCommonRules()->andElim(result, 1);
662  } else
663  done = true;
664  } while(!done);
665  Theorem res;
666  if(result.getExpr().isFalse()) res = result;
667  else res = solvedForm(solvedAndNewEqs);
668  TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
669  return res;
670 }
671 
672 /*!
673  * Takes a vector of equations and for every equation x_i=t_i
674  * substitutes t_j for x_j in t_i for all j>i. This turns the system
675  * of equations into a solved form.
676  *
677  * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
678  * i<j, but not for i>=j.
679  */
680 Theorem
681 TheoryArithNew::solvedForm(const vector<Theorem>& solvedEqs)
682 {
683  DebugAssert(solvedEqs.size() > 0, "TheoryArithNew::solvedForm()");
684 
685  // Trace code
686  TRACE_MSG("arith eq", "TheoryArithNew::solvedForm:solvedEqs(\n [");
687  IF_DEBUG(if(debugger.trace("arith eq")) {
688  for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
689  jend=solvedEqs.end(); j!=jend;++j)
690  TRACE("arith eq", "", j->getExpr(), ",\n ");
691  })
692  TRACE_MSG("arith eq", " ]) {");
693  // End of Trace code
694 
695  vector<Theorem>::const_reverse_iterator
696  i = solvedEqs.rbegin(),
697  iend = solvedEqs.rend();
698  // Substitution map: a variable 'x' is mapped to a Theorem x=t.
699  // This map accumulates the resulting solved form.
700  ExprMap<Theorem> subst;
701  for(; i!=iend; ++i) {
702  if(i->isRewrite()) {
703  Theorem thm = substAndCanonize(*i, subst);
704  TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
705  thm.getExpr(), "");
706  subst[i->getLHS()] = thm;
707  }
708  else {
709  // This is the FALSE case: just return the contradiction
710  DebugAssert(i->getExpr().isFalse(),
711  "TheoryArithNew::solvedForm: an element of solvedEqs must "
712  "be either EQ or FALSE: "+i->toString());
713  return *i;
714  }
715  }
716  // Now we've collected the solved form in 'subst'. Wrap it up into
717  // a conjunction and return.
718  vector<Theorem> thms;
719  for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
720  i!=iend; ++i)
721  thms.push_back(i->second);
722  if (thms.size() > 1)
723  return getCommonRules()->andIntro(thms);
724  else
725  return thms.back();
726 }
727 
728 
729 /*!
730  * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
731  * element of subst is a fully canonized equation of the form x=e,
732  * indexed by the LHS variable.
733  */
734 
735 Theorem
736 TheoryArithNew::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
737 {
738  TRACE("arith eq", "substAndCanonize(", t, ") {");
739  // Quick and dirty check: return immediately if subst is empty
740  if(subst.empty()) {
741  Theorem res(reflexivityRule(t));
742  TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
743  return res;
744  }
745  // Check if we can substitute 't' directly
746  ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
747  if(i!=iend) {
748  TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
749  return i->second;
750  }
751  // The base case: t is an i-leaf
752  if(isLeaf(t)) {
753  Theorem res(reflexivityRule(t));
754  TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
755  return res;
756  }
757  // 't' is an arithmetic term; recurse into the children
758  vector<Theorem> thms;
759  vector<unsigned> changed;
760  for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
761  Theorem thm = substAndCanonize(t[j], subst);
762  if(thm.getRHS() != t[j]) {
763  thm = canonThm(thm);
764  thms.push_back(thm);
765  changed.push_back(j);
766  }
767  }
768  // Do the actual substitution and canonize the result
769  Theorem res;
770  if(thms.size() > 0) {
771  res = substitutivityRule(t, changed, thms);
772  res = canonThm(res);
773  }
774  else
775  res = reflexivityRule(t);
776  TRACE("arith eq", "substAndCanonize => ", res, " }");
777  return res;
778 }
779 
780 
781 /*!
782  * ASSUMPTION: 't' is a fully canonized equation of the form x = t,
783  * and so is every element of subst, indexed by the LHS variable.
784  */
785 
786 Theorem
787 TheoryArithNew::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
788 {
789  // Quick and dirty check: return immediately if subst is empty
790  if(subst.empty()) return eq;
791 
792  DebugAssert(eq.isRewrite(), "TheoryArithNew::substAndCanonize: t = "
793  +eq.getExpr().toString());
794  const Expr& t = eq.getRHS();
795  // Do the actual substitution in the term t
796  Theorem thm = substAndCanonize(t, subst);
797  // Substitution had no result: return the original equation
798  if(thm.getRHS() == t) return eq;
799  // Otherwise substitute the result into the equation
800  vector<Theorem> thms;
801  vector<unsigned> changed;
802  thms.push_back(thm);
803  changed.push_back(1);
804  return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
805 }
806 
807 
808 void TheoryArithNew::updateStats(const Rational& c, const Expr& v)
809 {
810  TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
811  if(c > 0) {
812  if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
813  else d_countRight[v] = 1;
814  }
815  else
816  if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
817  else d_countLeft[v] = 1;
818 }
819 
820 
821 void TheoryArithNew::updateStats(const Expr& monomial)
822 {
823  Expr c, m;
824  separateMonomial(monomial, c, m);
825  updateStats(c.getRational(), m);
826 }
827 
828 
829 void TheoryArithNew::addToBuffer(const Theorem& thm) {
830  // First, turn the inequality into 0 < rhs
831  // FIXME: check if this can be optimized away
832  Theorem result(thm);
833  const Expr& e = thm.getExpr();
834  // int kind = e.getKind();
835  if(!(e[0].isRational() && e[0].getRational() == 0)) {
836  result = iffMP(result, d_rules->rightMinusLeft(e));
837  result = canonPred(result);
838  }
839  TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
840  // Push it into the buffer
841  d_buffer.push_back(thm);
842 
843  // Collect the statistics about variables
844  const Expr& rhs = thm.getExpr()[1];
845  if(isPlus(rhs))
846  for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
847  updateStats(*i);
848  else // It's a monomial
849  updateStats(rhs);
850 }
851 
852 
853 Expr TheoryArithNew::computeNormalFactor(const Expr& right, NormalizationType type) {
854  // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is of the form c1/d1*x1 + ... + cn/dn*xn or a rational
855 
856  // The expression must be canonised, i.e. it is a sum or a rational
857  DebugAssert(isRational(right) || isPlus(right),"TheoryArithNew::computeNormalFactor: " + right.toString() + "wrong kind");
858 
859  // The factor we will compute
860  Rational factor;
861 
862  // Sign of the factor
863  int sign = 0;
864 
865  // In case the expression is a PLUS expression find the gcd
866  if(isPlus(right)) {
867 
868  // Vector of numerators and denominators
869  vector<Rational> nums, denoms;
870 
871  // Pass throught the sum and pick up the integers
872  for(int i = 0, iend = right.arity(); i < iend; i ++) {
873 
874  Rational c(1); // The rational constant of the current summand
875 
876  // If rational or multiplicatino set c to be the apropriate rational
877  switch(right[i].getKind()) {
878 
879  case RATIONAL_EXPR:
880 
881  // Sum term is just a rational, so just add it
882  c = abs(right[i].getRational());
883  break;
884 
885  case MULT:
886 
887  // Sum term is involves multiplication
888  c = right[i][0].getRational();
889 
890  // If this is the first one (sign is still not set) set the sign depending on the sign of the term
891  if (!sign) {
892 
893  // If the normalization type is NORMALIZE_UNIT just return the invese of the first
894  if (type == NORMALIZE_UNIT) return rat(1/c);
895 
896  // Set the sign otherwise
897  sign = (c > 0 ? 1 : -1);
898  }
899 
900  // Constant should be positive for lcd and gcd computation
901  c = abs(c);
902 
903  break;
904 
905  default: // Stays 1 or everything else
906 
907  break;
908  }
909 
910  // Add the demoninator and the numerator to the apropriate vectors
911  nums.push_back(c.getNumerator());
912  denoms.push_back(c.getDenominator());
913  }
914 
915  // Compute the gcd of all the numerators
916  Rational gcd_nums = gcd(nums);
917 
918  // x/0 == 0 in our model, as a total extension of arithmetic. The
919  // particular value of x/0 is irrelevant, since the DP is guarded
920  // by the top-level TCCs, and it is safe to return any value in
921  // cases when terms are undefined.
922  factor = (gcd_nums == 0)? 0 : (sign * lcm(denoms) / gcd_nums);
923  } else
924  // The expression is a rational, just return 1
925  factor = 1;
926 
927  // Return the reational expression representing the factor
928  return rat(factor);
929 }
930 
931 
932 bool TheoryArithNew::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
933 {
934  DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
935  "TheoryArithNew::findMaxVar: isolatedMonomial cannot be rational" +
936  isolatedMonomial.toString());
937  Expr c, var0, var1;
938  separateMonomial(isolatedMonomial, c, var0);
939  separateMonomial(var2, c, var1);
940  return var0 < var1;
941 }
942 
943 
944 void TheoryArithNew::separateMonomial(const Expr& e, Expr& c, Expr& var) {
945  TRACE("separateMonomial", "separateMonomial(", e, ")");
946  DebugAssert(!isPlus(e),
947  "TheoryArithNew::separateMonomial(e = "+e.toString()+")");
948  if(isMult(e)) {
949  DebugAssert(e.arity() >= 2,
950  "TheoryArithNew::separateMonomial(e = "+e.toString()+")");
951  c = e[0];
952  if(e.arity() == 2) var = e[1];
953  else {
954  vector<Expr> kids = e.getKids();
955  kids[0] = rat(1);
956  var = multExpr(kids);
957  }
958  } else {
959  c = rat(1);
960  var = e;
961  }
962  DebugAssert(c.isRational(), "TheoryArithNew::separateMonomial(e = "
963  +e.toString()+", c = "+c.toString()+")");
964  DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
965  "TheoryArithNew::separateMonomial(e = "
966  +e.toString()+", var = "+var.toString()+")");
967 }
968 
969 
970 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
971 //comparable)
972 bool TheoryArithNew::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
973 {
974  d_cache.clear();
975  //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
976  return dfs(e1,e2);
977 }
978 
979 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
980 bool TheoryArithNew::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
981 {
982  if(e1 == e2)
983  return true;
984  if(d_cache.count(e2) > 0)
985  return false;
986  if(d_edges.count(e2) == 0)
987  return false;
988  d_cache[e2] = true;
989  vector<Expr>& e2Edges = d_edges[e2];
990  vector<Expr>::iterator i = e2Edges.begin();
991  vector<Expr>::iterator iend = e2Edges.end();
992  //if dfs finds e1 then i != iend else i is equal to iend
993  for(; i != iend && !dfs(e1,*i); ++i);
994  return (i != iend);
995 }
996 
997 
998 void TheoryArithNew::VarOrderGraph::selectSmallest(vector<Expr>& v1,
999  vector<Expr>& v2)
1000 {
1001  int v1Size = v1.size();
1002  vector<bool> v3(v1Size);
1003  for(int j=0; j < v1Size; ++j)
1004  v3[j] = false;
1005 
1006  for(int j=0; j < v1Size; ++j) {
1007  if(v3[j]) continue;
1008  for(int i =0; i < v1Size; ++i) {
1009  if((i == j) || v3[i])
1010  continue;
1011  if(lessThan(v1[i],v1[j])) {
1012  v3[j] = true;
1013  break;
1014  }
1015  }
1016  }
1017  vector<Expr> new_v1;
1018 
1019  for(int j = 0; j < v1Size; ++j)
1020  if(!v3[j]) v2.push_back(v1[j]);
1021  else new_v1.push_back(v1[j]);
1022  v1 = new_v1;
1023 }
1024 
1025 
1026 void TheoryArithNew::VarOrderGraph::selectLargest(const vector<Expr>& v1,
1027  vector<Expr>& v2)
1028 {
1029  int v1Size = v1.size();
1030  vector<bool> v3(v1Size);
1031  for(int j=0; j < v1Size; ++j)
1032  v3[j] = false;
1033 
1034  for(int j=0; j < v1Size; ++j) {
1035  if(v3[j]) continue;
1036  for(int i =0; i < v1Size; ++i) {
1037  if((i == j) || v3[i])
1038  continue;
1039  if(lessThan(v1[j],v1[i])) {
1040  v3[j] = true;
1041  break;
1042  }
1043  }
1044  }
1045 
1046  for(int j = 0; j < v1Size; ++j)
1047  if(!v3[j]) v2.push_back(v1[j]);
1048 }
1049 
1050 ///////////////////////////////////////////////////////////////////////////////
1051 // TheoryArithNew Public Methods //
1052 ///////////////////////////////////////////////////////////////////////////////
1053 
1054 
1055 TheoryArithNew::TheoryArithNew(TheoryCore* core)
1056  : TheoryArith(core, "ArithmeticNew"),
1057  d_diseq(core->getCM()->getCurrentContext()),
1058  d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
1059  d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
1060  d_freeConstDB(core->getCM()->getCurrentContext()),
1061  d_buffer(core->getCM()->getCurrentContext()),
1062  // Initialize index to 0 at scope 0
1063  d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
1064  d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
1065  d_countRight(core->getCM()->getCurrentContext()),
1066  d_countLeft(core->getCM()->getCurrentContext()),
1067  d_sharedTerms(core->getCM()->getCurrentContext()),
1068  d_sharedVars(core->getCM()->getCurrentContext()),
1069  consistent(core->getCM()->getCurrentContext()),
1070  lowerBound(core->getCM()->getCurrentContext()),
1071  upperBound(core->getCM()->getCurrentContext()),
1072  beta(core->getCM()->getCurrentContext()),
1073  assertedExprCount(core->getCM()->getCurrentContext()),
1074  integer_lemma(core->getCM()->getCurrentContext())
1075 {
1076  IF_DEBUG(d_diseq.setName("CDList[TheoryArithNew::d_diseq]");)
1077  IF_DEBUG(d_buffer.setName("CDList[TheoryArithNew::d_buffer]");)
1078  IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArithNew::d_bufferIdx]");)
1079 
1080  getEM()->newKind(REAL, "_REAL", true);
1081  getEM()->newKind(INT, "_INT", true);
1082  getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
1083 
1084  getEM()->newKind(UMINUS, "_UMINUS");
1085  getEM()->newKind(PLUS, "_PLUS");
1086  getEM()->newKind(MINUS, "_MINUS");
1087  getEM()->newKind(MULT, "_MULT");
1088  getEM()->newKind(DIVIDE, "_DIVIDE");
1089  getEM()->newKind(POW, "_POW");
1090  getEM()->newKind(INTDIV, "_INTDIV");
1091  getEM()->newKind(MOD, "_MOD");
1092  getEM()->newKind(LT, "_LT");
1093  getEM()->newKind(LE, "_LE");
1094  getEM()->newKind(GT, "_GT");
1095  getEM()->newKind(GE, "_GE");
1096  getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
1097  getEM()->newKind(NEGINF, "_NEGINF");
1098  getEM()->newKind(POSINF, "_POSINF");
1099  getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
1100  getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
1101 
1102  getEM()->newKind(REAL_CONST, "_REAL_CONST");
1103 
1104  vector<int> kinds;
1105  kinds.push_back(REAL);
1106  kinds.push_back(INT);
1107  kinds.push_back(SUBRANGE);
1108  kinds.push_back(IS_INTEGER);
1109  kinds.push_back(UMINUS);
1110  kinds.push_back(PLUS);
1111  kinds.push_back(MINUS);
1112  kinds.push_back(MULT);
1113  kinds.push_back(DIVIDE);
1114  kinds.push_back(POW);
1115  kinds.push_back(INTDIV);
1116  kinds.push_back(MOD);
1117  kinds.push_back(LT);
1118  kinds.push_back(LE);
1119  kinds.push_back(GT);
1120  kinds.push_back(GE);
1121  kinds.push_back(RATIONAL_EXPR);
1122  kinds.push_back(NEGINF);
1123  kinds.push_back(POSINF);
1124  kinds.push_back(DARK_SHADOW);
1125  kinds.push_back(GRAY_SHADOW);
1126  kinds.push_back(REAL_CONST);
1127 
1128  registerTheory(this, kinds, true);
1129 
1131 
1132  d_realType = Type(getEM()->newLeafExpr(REAL));
1133  d_intType = Type(getEM()->newLeafExpr(INT));
1135  assertedExprCount = 0;
1136 }
1137 
1138 
1139 // Destructor: delete the proof rules class if it's present
1141  if(d_rules != NULL) delete d_rules;
1142  // Clear the inequality databases
1143  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
1144  iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
1145  delete (i->second);
1146  free(i->second);
1147  }
1148  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
1149  iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
1150  delete (i->second);
1151  free (i->second);
1152  }
1153 }
1154 
1155 void TheoryArithNew::collectVars(const Expr& e, vector<Expr>& vars,
1156  set<Expr>& cache) {
1157  // Check the cache first
1158  if(cache.count(e) > 0) return;
1159  // Not processed yet. Cache the expression and proceed
1160  cache.insert(e);
1161  if(isLeaf(e)) vars.push_back(e);
1162  else
1163  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
1164  collectVars(*i, vars, cache);
1165 }
1166 
1167 void
1169  const Theorem& bxLEbeta) {
1170  const Expr& ineq1(alphaLEax.getExpr());
1171  const Expr& ineq2(bxLEbeta.getExpr());
1172  DebugAssert(isLE(ineq1), "TheoryArithNew::processFiniteInterval: ineq1 = "
1173  +ineq1.toString());
1174  DebugAssert(isLE(ineq2), "TheoryArithNew::processFiniteInterval: ineq2 = "
1175  +ineq2.toString());
1176  // If the inequalities are not integer, just return (nothing to do)
1177  if(!isInteger(ineq1[0])
1178  || !isInteger(ineq1[1])
1179  || !isInteger(ineq2[0])
1180  || !isInteger(ineq2[1]))
1181  return;
1182 
1183  const Expr& ax = ineq1[1];
1184  const Expr& bx = ineq2[0];
1185  DebugAssert(!isPlus(ax) && !isRational(ax),
1186  "TheoryArithNew::processFiniteInterval:\n ax = "+ax.toString());
1187  DebugAssert(!isPlus(bx) && !isRational(bx),
1188  "TheoryArithNew::processFiniteInterval:\n bx = "+bx.toString());
1189  Expr a = isMult(ax)? ax[0] : rat(1);
1190  Expr b = isMult(bx)? bx[0] : rat(1);
1191 
1192  Theorem thm1(alphaLEax), thm2(bxLEbeta);
1193  // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
1194  if(a != b) {
1195  thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
1196  thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
1197  }
1198  // Check that a*beta - b*alpha == c > 0
1199  const Expr& alphaLEt = thm1.getExpr();
1200  const Expr& alpha = alphaLEt[0];
1201  const Expr& t = alphaLEt[1];
1202  const Expr& beta = thm2.getExpr()[1];
1203  Expr c = canon(beta - alpha).getRHS();
1204 
1205  if(c.isRational() && c.getRational() >= 1) {
1206  // This is a finite interval. First, derive t <= alpha + c:
1207  // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
1208  // Then substitute that in thm2
1209  Theorem bEQac = symmetryRule(canon(alpha + c));
1210  // Substitute beta == alpha+c for the second child of thm2
1211  vector<unsigned> changed;
1212  vector<Theorem> thms;
1213  changed.push_back(1);
1214  thms.push_back(bEQac);
1215  Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
1216  tLEac = iffMP(thm2, tLEac);
1217  // Derive and enqueue the finite interval constraint
1218  Theorem isInta(isIntegerThm(alpha));
1219  Theorem isIntt(isIntegerThm(t));
1220  enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
1221  }
1222 }
1223 
1224 
1225 void
1227  // If x is not integer, do not bother
1228  if(!isInteger(x)) return;
1229  // Process every pair of the opposing inequalities for 'x'
1230  ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
1231  iLeft = d_inequalitiesLeftDB.find(x);
1232  if(iLeft == d_inequalitiesLeftDB.end()) return;
1233  iRight = d_inequalitiesRightDB.find(x);
1234  if(iRight == d_inequalitiesRightDB.end()) return;
1235  // There are some opposing inequalities; get the lists
1236  CDList<Ineq>& ineqsLeft = *(iLeft->second);
1237  CDList<Ineq>& ineqsRight = *(iRight->second);
1238  // Get the sizes of the lists
1239  size_t sizeLeft = ineqsLeft.size();
1240  size_t sizeRight = ineqsRight.size();
1241  // Process all the pairs of the opposing inequalities
1242  for(size_t l=0; l<sizeLeft; ++l)
1243  for(size_t r=0; r<sizeRight; ++r)
1244  processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
1245 }
1246 
1247 /*! This function recursively decends expression tree <strong>without
1248  * caching</strong> until it hits a node that is already setup. Be
1249  * careful on what expressions you are calling it.
1250  */
1251 void
1253  if(e.hasFind()) return;
1254  // First, set up the kids recursively
1255  for (int k = 0; k < e.arity(); ++k) {
1256  setupRec(e[k]);
1257  }
1258  // Create a find pointer for e
1259  e.setFind(reflexivityRule(e));
1260  e.setEqNext(reflexivityRule(e));
1261  // And call our own setup()
1262  setup(e);
1263 }
1264 
1265 
1266 /*!
1267  * Keep track of all finitely bounded integer variables in shared
1268  * terms.
1269  *
1270  * When a new shared term t is reported, all of its variables x1...xn
1271  * are added to the set d_sharedVars.
1272  *
1273  * For each newly added variable x, check all of its opposing
1274  * inequalities, find out all the finite bounds and assert the
1275  * corresponding GRAY_SHADOW constraints.
1276  *
1277  * When projecting integer inequalities, the database d_sharedVars is
1278  * consulted, and if the variable is in it, check the shadows for
1279  * being a finite interval, and produce the additional GRAY_SHADOW
1280  * constraints.
1281  */
1283  d_sharedTerms[e] = true;
1284  /*
1285  set<Expr> cache; // Aux. cache for collecting i-leaves
1286  vector<Expr> vars; // Vector of vars in e
1287  collectVars(e, vars, cache);
1288  for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
1289  if(d_sharedVars.count(*i) == 0) {
1290  TRACE("arith shared", "TheoryArithNew::addSharedTerm: new var = ", *i, "");
1291  processFiniteIntervals(*i);
1292  d_sharedVars[*i]=true;
1293  }
1294  }
1295  */
1296 }
1297 
1299 {
1300  d_inModelCreation = true;
1301  TRACE("model", "refineCounterExample[TheoryArithNew] ", "", "{");
1302  CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
1303  iend = d_sharedTerms.end();
1304  // Add equalities over all pairs of shared terms as suggested
1305  // splitters. Notice, that we want to split on equality
1306  // (positively) first, to reduce the size of the model.
1307  for(; it!=iend; ++it) {
1308  // Copy by value: the elements in the pair from *it are NOT refs in CDMap
1309  Expr e1 = (*it).first;
1310  for(it2 = it, ++it2; it2!=iend; ++it2) {
1311  Expr e2 = (*it2).first;
1313  "TheoryArithNew::refineCounterExample: e1 = "+e1.toString()
1314  +"\n type(e1) = "+e1.getType().toString());
1315  if(findExpr(e1) != findExpr(e2)) {
1317  "TheoryArithNew::refineCounterExample: e2 = "+e2.toString()
1318  +"\n type(e2) = "+e2.getType().toString());
1319  Expr eq = simplifyExpr(e1.eqExpr(e2));
1320  if (!eq.isBoolConst())
1321  addSplitter(eq);
1322  }
1323  }
1324  }
1325  TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
1326 }
1327 
1328 
1329 void
1330 TheoryArithNew::findRationalBound(const Expr& varSide, const Expr& ratSide,
1331  const Expr& var,
1332  Rational &r)
1333 {
1334  Expr c, x;
1335  separateMonomial(varSide, c, x);
1336 
1338  "seperateMonomial failed");
1339  DebugAssert(findExpr(ratSide).isRational(),
1340  "smallest variable in graph, should not have variables"
1341  " in inequalities: ");
1342  DebugAssert(x == var, "separateMonomial found different variable: "
1343  + var.toString());
1344  r = findExpr(ratSide).getRational() / findExpr(c).getRational();
1345 }
1346 
1347 bool
1349 {
1350  bool strictLB=false, strictUB=false;
1351  bool right = (d_inequalitiesRightDB.count(e) > 0
1352  && d_inequalitiesRightDB[e]->size() > 0);
1353  bool left = (d_inequalitiesLeftDB.count(e) > 0
1354  && d_inequalitiesLeftDB[e]->size() > 0);
1355  int numRight = 0, numLeft = 0;
1356  if(right) { //rationals less than e
1357  CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
1358  for(unsigned int i=0; i<ratsLTe->size(); i++) {
1359  DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
1360  Expr ineq = (*ratsLTe)[i].ineq().getExpr();
1361  Expr leftSide = ineq[0], rightSide = ineq[1];
1362  Rational r;
1363  findRationalBound(rightSide, leftSide, e , r);
1364  if(numRight==0 || r>glb){
1365  glb = r;
1366  strictLB = isLT(ineq);
1367  }
1368  numRight++;
1369  }
1370  TRACE("model", " =>Lower bound ", glb.toString(), "");
1371  }
1372  if(left) { //rationals greater than e
1373  CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
1374  for(unsigned int i=0; i<ratsGTe->size(); i++) {
1375  DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
1376  Expr ineq = (*ratsGTe)[i].ineq().getExpr();
1377  Expr leftSide = ineq[0], rightSide = ineq[1];
1378  Rational r;
1379  findRationalBound(leftSide, rightSide, e, r);
1380  if(numLeft==0 || r<lub) {
1381  lub = r;
1382  strictUB = isLT(ineq);
1383  }
1384  numLeft++;
1385  }
1386  TRACE("model", " =>Upper bound ", lub.toString(), "");
1387  }
1388  if(!left && !right) {
1389  lub = 0;
1390  glb = 0;
1391  }
1392  if(!left && right) {lub = glb +2;}
1393  if(!right && left) {glb = lub-2;}
1394  DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
1395  "than least upper bound");
1396  return strictLB;
1397 }
1398 
1399 void TheoryArithNew::assignVariables(std::vector<Expr>&v)
1400 {
1401  int count = 0;
1402  while (v.size() > 0) {
1403  std::vector<Expr> bottom;
1404  d_graph.selectSmallest(v, bottom);
1405  TRACE("model", "Finding variables to assign. Iteration # ", count, "");
1406  for(unsigned int i = 0; i<bottom.size(); i++) {
1407  Expr e = bottom[i];
1408  TRACE("model", "Found: ", e, "");
1409  // Check if it is already a concrete constant
1410  if(e.isRational()) continue;
1411 
1412  Rational lub, glb;
1413  bool strictLB;
1414  strictLB = findBounds(e, lub, glb);
1415  Rational mid;
1416  if(isInteger(e)) {
1417  if(strictLB && glb.isInteger())
1418  mid = glb + 1;
1419  else
1420  mid = ceil(glb);
1421  }
1422  else
1423  mid = (lub + glb)/2;
1424  TRACE("model", "Assigning mid = ", mid, " {");
1425  assignValue(e, rat(mid));
1426  TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
1427  if(inconsistent()) return; // Punt immediately if failed
1428  }
1429  count++;
1430  }
1431 }
1432 
1433 void TheoryArithNew::computeModelBasic(const std::vector<Expr>& v)
1434 {
1435  d_inModelCreation = true;
1436  vector<Expr> reps;
1437  TRACE("model", "Arith=>computeModel ", "", "{");
1438  for(unsigned int i=0; i <v.size(); ++i) {
1439  const Expr& e = v[i];
1440  if(findExpr(e) == e) {
1441  TRACE("model", "arith variable:", e , "");
1442  reps.push_back(e);
1443  }
1444  else {
1445  TRACE("model", "arith variable:", e , "");
1446  TRACE("model", " ==> is defined by: ", findExpr(e) , "");
1447  }
1448  }
1449  assignVariables(reps);
1450  TRACE("model", "Arith=>computeModel", "", "}");
1451  d_inModelCreation = false;
1452 }
1453 
1454 // For any arith expression 'e', if the subexpressions are assigned
1455 // concrete values, then find(e) must already be a concrete value.
1456 void TheoryArithNew::computeModel(const Expr& e, vector<Expr>& vars) {
1457  DebugAssert(findExpr(e).isRational(), "TheoryArithNew::computeModel("
1458  +e.toString()+")\n e is not assigned concrete value.\n"
1459  +" find(e) = "+findExpr(e).toString());
1460  assignValue(simplify(e));
1461  vars.push_back(e);
1462 }
1463 
1464 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
1465  * and returns a theorem to that effect. assumes e is non-trivial
1466  * i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
1467  */
1469 
1470  //e is an eqn or ineqn. e is not a trivial eqn or ineqn
1471  //trivial means 0 = const or 0 <= const.
1472 
1473  // Trace the normalization on the arithm trace flag
1474  TRACE("arith", "normalize(", e, ") {");
1475 
1476  // The constraint must be an equality or inequality
1477  DebugAssert(isIneq(e), "normalize: input must be an inequality: " + e.toString());
1478 
1479  // The right side must be a sum or a multiplication
1480  DebugAssert(isPlus(e[1]) || (isMult(e[1]) && e[1][0].isRational()), "normalize: right side must be a sum or a mult: " + e.toString());
1481 
1482  // The left side must be 0
1483  DebugAssert(e[0].isRational() && 0 == e[0].getRational(), "normalize: e[0] must be 0" + e.toString());
1484 
1485  // Compute the factor to use for normalizing the inequality
1486  Expr factor;
1487  // If a mult, just take the coefficient
1488  if (isMult(e[1])) factor = rat(1/e[1][0].getRational());
1489  // Otherwise compute it
1490  else factor = computeNormalFactor(e[1], type);
1491 
1492  // Trace the rezult on the arith flag
1493  TRACE("arith", "normalize: factor = ", factor, "");
1494 
1495  // The theorem we will be creating (reflexivity, just in case)
1496  Theorem thm;
1497 
1498  // Now multiply the equality by the factor, unless it is 1
1499  if(factor.getRational() != 1)
1500  switch(e.getKind()) {
1501 
1502  case LE:
1503  case LT:
1504  case GE:
1505  case GT:
1506 
1507  // Multiply inequality by the factor
1508  thm = d_rules->multIneqn(e, factor);
1509 
1510  // And canonize the result
1511  thm = canonPredEquiv(thm);
1512 
1513  // Inequalities case break
1514  break;
1515 
1516  default:
1517 
1518  // How did we get here
1519  FatalAssert(false, "normalize: control should not reach here" + e.toString());
1520 
1521  // Default case break
1522  break;
1523  }
1524  else
1525  // If rational is 1 then nothing to be done
1526  thm = reflexivityRule(e);
1527 
1528 
1529  // Trace the resulting theorem on the arith trace flag
1530  TRACE("arith", "normalize => ", thm, " }");
1531 
1532  // Return the explaining theorem
1533  return(thm);
1534 }
1535 
1536 
1538  return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS(), type));
1539 }
1540 
1542 
1543  // The resulting theorem
1544  Theorem result = thm;
1545 
1546  // Get the constraint
1547  const Expr& constr = result.getRHS();
1548 
1549  // Get the proof that this constraint is an integer constraint
1550  Theorem isIntConstraintThm = isIntegerThm(constr[1]);
1551 
1552  // If not an integer, just return the same theorem
1553  if (isIntConstraintThm.isNull()) return result;
1554 
1555  // Trace the integer
1556  TRACE("integer", "TheoryArithNew::rafineIntegerConstraints(", constr, ")");
1557  TRACE("integer", "TheoryArithNew::rafineIntegerConstraints: int proof:", isIntConstraintThm, "");
1558 
1559  // Get the left-hand of the constraint (the rational)
1560  Rational r = constr[0].getRational();
1561 
1562  // If it is a strict inequality, make it non-strict
1563  if (constr.getKind() == LT || constr.getKind() == GT || !r.isInteger())
1564  result = transitivityRule(result, d_rules->rafineStrictInteger(isIntConstraintThm, constr));
1565 
1566  // Return the result
1567  return result;
1568 }
1569 
1571 
1572  // Leaves are assumeed to be already simplified
1573  //DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
1574 
1575  // Trace the rewrites on the arith flag
1576  TRACE("arith", "TheoryArithNew::rewrite(", e, ") {");
1577 
1578  // The resulting theorem object
1579  Theorem thm;
1580 
1581  // Are we in the NOT expression
1582  bool isNot = false;
1583 
1584  // If the expression is not a term, i.e a literal
1585  if (!e.isTerm()) {
1586 
1587  // If the expression is not a literal just return the reflexivity theorem
1588  if (!e.isAbsLiteral()) {
1589 
1590  // Set the expression REWRITE NORMAL FLAG
1591  e.setRewriteNormal();
1592 
1593  // Create the reflaxivity rule
1594  thm = reflexivityRule(e);
1595 
1596  // Trace the non-literal rewrite
1597  TRACE("arith", "TheoryArithNew::rewrite[non-literal] => ", thm, " }");
1598 
1599  // Return the theorem
1600  return thm;
1601  }
1602 
1603  // Its a literal, switch the arithmetic relations for rewrite
1604  switch(e.getKind()) {
1605 
1606  // Equality
1607  case EQ: {
1608 
1609  // Rewrite equality as two inequalities
1610  thm = d_rules->eqToIneq(e);
1611  Expr andExpr = thm.getRHS();
1612 
1613  // Rewrite the left inequality
1614  Expr leExpr = andExpr[0];
1615  const Theorem& thmLeft = simplify(leExpr);
1616 
1617  // Rewrite the right inequality
1618  Expr geExpr = andExpr[1];
1619  const Theorem& thmRight = simplify(geExpr);
1620 
1621  // Do the substitution
1622  thm = transitivityRule(thm, substitutivityRule(andExpr, thmLeft, thmRight));
1623 
1624  // EQ case break
1625  break;
1626  }
1627 
1628  // Negation of an atomic formula
1629  case NOT:
1630 
1631  // If here, the equality should have already been rewritten as two disequalitites
1632  DebugAssert(e[0].getKind() != EQ, "TheoryArithNew::rewrite, not expecting equality under negation");
1633 
1634  // Negate the inequality and continue with the normal case
1635  thm = d_rules->negatedInequality(e);
1636 
1637  // IMPORTANT, LE, LT, GE, GT MUST BE UNDER THIS
1638  isNot = true;
1639 
1640  case LT:
1641  case GT:
1642  case LE:
1643  case GE:
1644 
1645  // Move everything to the right side
1646  if (isNot)
1647  thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
1648  else
1649  thm = d_rules->rightMinusLeft(e);
1650 
1651  // Canonise children again
1652  thm = canonPredEquiv(thm);
1653 
1654  // If a trivial inequation just return true or false
1655  if ((thm.getRHS())[1].isRational())
1656  thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
1657  else { // It's a non-trivial inequation
1658 
1659  // Normalize the inequality
1660  thm = normalize(thm, NORMALIZE_UNIT);
1661 
1662  // Get the left and right side
1663  const Expr& normalised = thm.getRHS();
1664  const Expr& rightSide = normalised[1];
1665  const Expr& leftSide = normalised[0];
1666 
1667  // If the right side is a sum, move the rational to the right side
1668  if (isPlus(rightSide)) {
1669  // Check if the fist of the sum is a rational
1670  if (rightSide[0].isRational()) {
1671  // Add the negative constant to both sides
1672  thm = transitivityRule(thm, d_rules->plusPredicate(leftSide, rightSide, rat(-rightSide[0].getRational()), thm.getRHS().getKind()));
1673  // Canonize the left side
1674  const Theorem& thmLeft = d_rules->canonPlus(thm.getRHS()[0]);
1675  // Canonize the right side
1676  const Theorem& thmRight = d_rules->canonPlus(thm.getRHS()[1]);
1677  // Sunstitute the canonised into the expression
1678  thm = transitivityRule(thm, substitutivityRule(thm.getRHS(), thmLeft, thmRight));
1679  }
1680  }
1681  }
1682 
1683  // If a strict inequality on integers, or bounded by a non-integer, rafine it to a non-strict one
1684 // thm = rafineIntegerConstraints(thm);
1685 
1686  // EQ, LE, LT, GE, GT case break
1687  break;
1688 
1689  case IS_INTEGER:
1690 
1691  // TRACE
1692  TRACE("integer", "Got ", e.toString(), "");
1693  TRACE("integer", "Type ", e[0].getType().toString(), "");
1694 
1695  // TODO: What with the integers
1696  thm = d_rules->dummyTheorem(e);
1697 
1698  // IS_INTEGER case break
1699  break;
1700 
1701  default:
1702 
1703  // How did we get here
1704  FatalAssert(false, "Theory_Arith::rewrite: control should not reach here");
1705 
1706  // default break
1707  break;
1708 
1709  } // End relation case
1710 
1711  } else { // Expression is a term
1712 
1713  // Terms that don't contain formulas are canonised via the canon() function
1714  if (e.isAtomic()) thm = canon(e);
1715  // Otherwise just return the same expression
1716  else thm = reflexivityRule(e);
1717  }
1718 
1719  // Compact the theorem into one rule
1720  //thm = d_rules->trustedRewrite(e, thm.getRHS());
1721 
1722  // Arith canonization is idempotent, the theory should stay the same
1723  if (theoryOf(thm.getRHS()) == this)
1724  thm.getRHS().setRewriteNormal();
1725 
1726  // Finished, trace the end of rewrite on the arith flag
1727  TRACE("arith", "TheoryArithNew::rewrite => ", thm, " }");
1728 
1729  // Return the final theorem
1730  return thm;
1731 }
1732 
1733 
1735 {
1736  //If the expression is not a term but rather a predicate
1737  if (!e.isTerm()) {
1738 
1739  // If not or equality, just return
1740  if (e.isNot() || e.isEq()) return;
1741 
1742  // TODO: Integer::eqToIneq
1743  if (isIntPred(e)) return;
1744 
1745  // Check if the expression is canonised as (SUM t1 ... tn) @ b
1746  DebugAssert(isIneq(e) && e[0].isRational(), "TheoryArithNew::setup: b @ (sum t1 ... tn) :" + e.toString());
1747 
1748  // Add the sum to the notify list of e
1749  e[1].addToNotify(this, e);
1750 
1751  } else {
1752 
1753  // The arity of the expression
1754  int arity(e.arity());
1755 
1756  // Go through all the children and add this expression to their notify lists
1757  for (int k = 0 ; k < arity; k ++) {
1758 
1759  // Add the to the notify list of the children
1760  e[k].addToNotify(this, e);
1761 
1762  // Trace this notification add
1763  TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
1764  }
1765  }
1766 }
1767 
1768 
1769 void TheoryArithNew::update(const Theorem& e, const Expr& d)
1770 {
1771  if (inconsistent()) return;
1772  IF_DEBUG(debugger.counter("arith update total")++;)
1773  if (!d.hasFind()) return;
1774  if (isIneq(d)) {
1775  // Substitute e[1] for e[0] in d and enqueue new inequality
1776  DebugAssert(e.getLHS() == d[1], "Mismatch");
1777  Theorem thm = find(d);
1778  // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
1779  vector<unsigned> changed;
1780  vector<Theorem> children;
1781  changed.push_back(1);
1782  children.push_back(e);
1783  Theorem thm2 = substitutivityRule(d, changed, children);
1784  if (thm.getRHS() == trueExpr()) {
1785  enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
1786  }
1787  else {
1788  enqueueFact(getCommonRules()->iffFalseElim(
1789  transitivityRule(symmetryRule(thm2), thm)));
1790  }
1791  IF_DEBUG(debugger.counter("arith update ineq")++;)
1792  }
1793  else if (find(d).getRHS() == d) {
1794  // Substitute e[1] for e[0] in d and assert the result equal to d
1795  Theorem thm = canonSimp(d);
1796  TRACE("arith", "TheoryArithNew::update(): thm = ", thm, "");
1797  DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
1798  +thm.getExpr().toString());
1800  IF_DEBUG(debugger.counter("arith update find(d)=d")++;)
1801  }
1802 }
1803 
1804 
1806 {
1807  DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
1808  const Expr& lhs = thm.getLHS();
1809  const Expr& rhs = thm.getRHS();
1810 
1811  // Check for already solved equalities.
1812 
1813  // Have to be careful about the types: integer variable cannot be
1814  // assigned a real term. Also, watch for e[0] being a subexpression
1815  // of e[1]: this would create an unsimplifiable expression.
1816  if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
1817  && (lhs.getType() != intType() || isInteger(rhs))
1818  // && !e[0].subExprOf(e[1])
1819  )
1820  return thm;
1821 
1822  // Symmetric version is already solved
1823  if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
1824  && (rhs.getType() != intType() || isInteger(lhs))
1825  // && !e[1].subExprOf(e[0])
1826  )
1827  return symmetryRule(thm);
1828 
1829  return doSolve(thm);
1830 }
1831 
1832 
1833 void TheoryArithNew::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
1834  switch(e.getKind()) {
1835  case RATIONAL_EXPR: // Skip the constants
1836  break;
1837  case PLUS:
1838  case MULT:
1839  case DIVIDE:
1840  case POW: // This is not a variable; extract the variables from children
1841  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
1842  // getModelTerm(*i, v);
1843  v.push_back(*i);
1844  break;
1845  default: { // Otherwise it's a variable. Check if it has a find pointer
1846  Expr e2(findExpr(e));
1847  if(e==e2) {
1848  TRACE("model", "TheoryArithNew::computeModelTerm(", e, "): a variable");
1849  // Leave it alone (it has no descendants)
1850  // v.push_back(e);
1851  } else {
1852  TRACE("model", "TheoryArithNew::computeModelTerm("+e.toString()
1853  +"): has find pointer to ", e2, "");
1854  v.push_back(e2);
1855  }
1856  }
1857  }
1858 }
1859 
1861  Expr tExpr = t.getExpr();
1862  switch(tExpr.getKind()) {
1863  case INT:
1864  return Expr(IS_INTEGER, e);
1865  case SUBRANGE: {
1866  std::vector<Expr> kids;
1867  kids.push_back(Expr(IS_INTEGER, e));
1868  kids.push_back(leExpr(tExpr[0], e));
1869  kids.push_back(leExpr(e, tExpr[1]));
1870  return andExpr(kids);
1871  }
1872  default:
1873  return e.getEM()->trueExpr();
1874  }
1875 }
1876 
1877 
1879 {
1880  return;
1881 }
1882 
1883 
1885 {
1886  switch (e.getKind()) {
1887  case INT:
1888  case REAL:
1889  if (e.arity() > 0) {
1890  throw Exception("Ill-formed arithmetic type: "+e.toString());
1891  }
1892  break;
1893  case SUBRANGE:
1894  if (e.arity() != 2 ||
1895  !isIntegerConst(e[0]) ||
1896  !isIntegerConst(e[1]) ||
1897  e[0].getRational() > e[1].getRational()) {
1898  throw Exception("bad SUBRANGE type expression"+e.toString());
1899  }
1900  break;
1901  default:
1902  DebugAssert(false, "Unexpected kind in TheoryArithNew::checkType"
1903  +getEM()->getKindName(e.getKind()));
1904  }
1905 }
1906 
1907 
1909  bool enumerate, bool computeSize)
1910 {
1911  Cardinality card = CARD_INFINITE;
1912  switch (e.getKind()) {
1913  case SUBRANGE: {
1914  card = CARD_FINITE;
1915  Expr typeExpr = e;
1916  if (enumerate) {
1917  Rational r = typeExpr[0].getRational() + n;
1918  if (r <= typeExpr[1].getRational()) {
1919  e = rat(r);
1920  }
1921  else e = Expr();
1922  }
1923  if (computeSize) {
1924  Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1;
1925  n = r.getUnsigned();
1926  }
1927  break;
1928  }
1929  default:
1930  break;
1931  }
1932  return card;
1933 }
1934 
1935 
1937 {
1938  switch (e.getKind()) {
1939  case REAL_CONST:
1940  e.setType(d_realType);
1941  break;
1942  case RATIONAL_EXPR:
1943  if(e.getRational().isInteger())
1944  e.setType(d_intType);
1945  else
1946  e.setType(d_realType);
1947  break;
1948  case UMINUS:
1949  case PLUS:
1950  case MINUS:
1951  case MULT:
1952  case POW: {
1953  bool isInt = true;
1954  for(int k = 0; k < e.arity(); ++k) {
1955  if(d_realType != getBaseType(e[k]))
1956  throw TypecheckException("Expecting type REAL with `" +
1957  getEM()->getKindName(e.getKind()) + "',\n"+
1958  "but got a " + getBaseType(e[k]).toString()+
1959  " for:\n" + e.toString());
1960  if(isInt && !isInteger(e[k]))
1961  isInt = false;
1962  }
1963  if(isInt)
1964  e.setType(d_intType);
1965  else
1966  e.setType(d_realType);
1967  break;
1968  }
1969  case DIVIDE: {
1970  Expr numerator = e[0];
1971  Expr denominator = e[1];
1972  if (getBaseType(numerator) != d_realType ||
1973  getBaseType(denominator) != d_realType) {
1974  throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
1975  "but got " + getBaseType(numerator).toString()+
1976  " and " + getBaseType(denominator).toString() +
1977  " for:\n" + e.toString());
1978  }
1979  if(denominator.isRational() && 1 == denominator.getRational())
1980  e.setType(numerator.getType());
1981  else
1982  e.setType(d_realType);
1983  break;
1984  }
1985  case LT:
1986  case LE:
1987  case GT:
1988  case GE:
1989  case GRAY_SHADOW:
1990  // Need to know types for all exprs -Clark
1991  // e.setType(boolType());
1992  // break;
1993  case DARK_SHADOW:
1994  for (int k = 0; k < e.arity(); ++k) {
1995  if (d_realType != getBaseType(e[k]))
1996  throw TypecheckException("Expecting type REAL with `" +
1997  getEM()->getKindName(e.getKind()) + "',\n"+
1998  "but got a " + getBaseType(e[k]).toString()+
1999  " for:\n" + e.toString());
2000  }
2001 
2002  e.setType(boolType());
2003  break;
2004  case IS_INTEGER:
2005  if(d_realType != getBaseType(e[0]))
2006  throw TypecheckException("Expected type REAL, but got "
2007  +getBaseType(e[0]).toString()
2008  +"\n\nExpr = "+e.toString());
2009  e.setType(boolType());
2010  break;
2011  default:
2012  DebugAssert(false,"TheoryArithNew::computeType: unexpected expression:\n "
2013  +e.toString());
2014  break;
2015  }
2016 }
2017 
2019  IF_DEBUG(int kind = t.getExpr().getKind();)
2020  DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
2021  "TheoryArithNew::computeBaseType("+t.toString()+")");
2022  return realType();
2023 }
2024 
2026  Expr tcc(Theory::computeTCC(e));
2027  switch(e.getKind()) {
2028  case DIVIDE:
2029  DebugAssert(e.arity() == 2, "");
2030  return tcc.andExpr(!(e[1].eqExpr(rat(0))));
2031  default:
2032  return tcc;
2033  }
2034 }
2035 
2036 ///////////////////////////////////////////////////////////////////////////////
2037 //parseExprOp:
2038 //translating special Exprs to regular EXPR??
2039 ///////////////////////////////////////////////////////////////////////////////
2041  TRACE("parser", "TheoryArithNew::parseExprOp(", e, ")");
2042  //std::cout << "Were here";
2043  // If the expression is not a list, it must have been already
2044  // parsed, so just return it as is.
2045  switch(e.getKind()) {
2046  case ID: {
2047  int kind = getEM()->getKind(e[0].getString());
2048  switch(kind) {
2049  case NULL_KIND: return e; // nothing to do
2050  case REAL:
2051  case INT:
2052  case NEGINF:
2053  case POSINF: return getEM()->newLeafExpr(kind);
2054  default:
2055  DebugAssert(false, "Bad use of bare keyword: "+e.toString());
2056  return e;
2057  }
2058  }
2059  case RAW_LIST: break; // break out of switch, do the hard work
2060  default:
2061  return e;
2062  }
2063 
2064  DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
2065  "TheoryArithNew::parseExprOp:\n e = "+e.toString());
2066 
2067  const Expr& c1 = e[0][0];
2068  int kind = getEM()->getKind(c1.getString());
2069  switch(kind) {
2070  case UMINUS: {
2071  if(e.arity() != 2)
2072  throw ParserException("UMINUS requires exactly one argument: "
2073  +e.toString());
2074  return uminusExpr(parseExpr(e[1]));
2075  }
2076  case PLUS: {
2077  vector<Expr> k;
2078  Expr::iterator i = e.begin(), iend=e.end();
2079  // Skip first element of the vector of kids in 'e'.
2080  // The first element is the operator.
2081  ++i;
2082  // Parse the kids of e and push them into the vector 'k'
2083  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
2084  return plusExpr(k);
2085  }
2086  case MINUS: {
2087  if(e.arity() == 2)
2088  return uminusExpr(parseExpr(e[1]));
2089  else if(e.arity() == 3)
2090  return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
2091  else
2092  throw ParserException("MINUS requires one or two arguments:"
2093  +e.toString());
2094  }
2095  case MULT: {
2096  vector<Expr> k;
2097  Expr::iterator i = e.begin(), iend=e.end();
2098  // Skip first element of the vector of kids in 'e'.
2099  // The first element is the operator.
2100  ++i;
2101  // Parse the kids of e and push them into the vector 'k'
2102  for(; i!=iend; ++i) k.push_back(parseExpr(*i));
2103  return multExpr(k);
2104  }
2105  case POW: {
2106  return powExpr(parseExpr(e[1]), parseExpr(e[2]));
2107  }
2108  case DIVIDE:
2109  { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
2110  case LT:
2111  { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
2112  case LE:
2113  { return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
2114  case GT:
2115  { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
2116  case GE:
2117  { return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
2118  case INTDIV:
2119  case MOD:
2120  case SUBRANGE: {
2121  vector<Expr> k;
2122  Expr::iterator i = e.begin(), iend=e.end();
2123  // Skip first element of the vector of kids in 'e'.
2124  // The first element is the operator.
2125  ++i;
2126  // Parse the kids of e and push them into the vector 'k'
2127  for(; i!=iend; ++i)
2128  k.push_back(parseExpr(*i));
2129  return Expr(kind, k, e.getEM());
2130  }
2131  case IS_INTEGER: {
2132  if(e.arity() != 2)
2133  throw ParserException("IS_INTEGER requires exactly one argument: "
2134  +e.toString());
2135  return Expr(IS_INTEGER, parseExpr(e[1]));
2136  }
2137  default:
2138  DebugAssert(false,
2139  "TheoryArithNew::parseExprOp: invalid input " + e.toString());
2140  break;
2141  }
2142  return e;
2143 }
2144 
2145 ///////////////////////////////////////////////////////////////////////////////
2146 // Pretty-printing //
2147 ///////////////////////////////////////////////////////////////////////////////
2148 
2149 
2151  switch(os.lang()) {
2152  case SIMPLIFY_LANG:
2153  switch(e.getKind()) {
2154  case RATIONAL_EXPR:
2155  e.print(os);
2156  break;
2157  case SUBRANGE:
2158  os <<"ERROR:SUBRANGE:not supported in Simplify\n";
2159  break;
2160  case IS_INTEGER:
2161  os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
2162  break;
2163  case PLUS: {
2164  int i=0, iend=e.arity();
2165  os << "(+ ";
2166  if(i!=iend) os << e[i];
2167  ++i;
2168  for(; i!=iend; ++i) os << " " << e[i];
2169  os << ")";
2170  break;
2171  }
2172  case MINUS:
2173  os << "(- " << e[0] << " " << e[1]<< ")";
2174  break;
2175  case UMINUS:
2176  os << "-" << e[0] ;
2177  break;
2178  case MULT: {
2179  int i=0, iend=e.arity();
2180  os << "(* " ;
2181  if(i!=iend) os << e[i];
2182  ++i;
2183  for(; i!=iend; ++i) os << " " << e[i];
2184  os << ")";
2185  break;
2186  }
2187  case POW:
2188  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
2189  break;
2190  case DIVIDE:
2191  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
2192  break;
2193  case LT:
2194  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
2195  }
2196  os << "(< " << e[0] << " " << e[1] <<")";
2197  break;
2198  case LE:
2199  os << "(<= " << e[0] << " " << e[1] << ")";
2200  break;
2201  case GT:
2202  os << "(> " << e[0] << " " << e[1] << ")";
2203  break;
2204  case GE:
2205  os << "(>= " << e[0] << " " << e[1] << ")";
2206  break;
2207  case DARK_SHADOW:
2208  case GRAY_SHADOW:
2209  os <<"ERROR:SHADOW:not supported in Simplify\n";
2210  break;
2211  default:
2212  // Print the top node in the default LISP format, continue with
2213  // pretty-printing for children.
2214  e.print(os);
2215 
2216  break;
2217  }
2218  break; // end of case SIMPLIFY_LANG
2219 
2220 
2221  case TPTP_LANG:
2222  switch(e.getKind()) {
2223  case RATIONAL_EXPR:
2224  e.print(os);
2225  break;
2226  case SUBRANGE:
2227  os <<"ERROR:SUBRANGE:not supported in TPTP\n";
2228  break;
2229  case IS_INTEGER:
2230  os <<"ERROR:IS_INTEGER:not supported in TPTP\n";
2231  break;
2232  case PLUS: {
2233  if(!isInteger(e[0])){
2234  os<<"ERRPR:plus only supports inteters now in TPTP\n";
2235  break;
2236  }
2237 
2238  int i=0, iend=e.arity();
2239  if(iend <=1){
2240  os<<"ERROR,plus must have more than two numbers in TPTP\n";
2241  break;
2242  }
2243 
2244  for(i=0; i <= iend-2; ++i){
2245  os << "$plus_int(";
2246  os << e[i] << ",";
2247  }
2248 
2249  os<< e[iend-1];
2250 
2251  for(i=0 ; i <= iend-2; ++i){
2252  os << ")";
2253  }
2254 
2255  break;
2256  }
2257  case MINUS:
2258  os << "(- " << e[0] << " " << e[1]<< ")";
2259  break;
2260  case UMINUS:
2261  os << "-" << e[0] ;
2262  break;
2263  case MULT: {
2264  int i=0, iend=e.arity();
2265  os << "(* " ;
2266  if(i!=iend) os << e[i];
2267  ++i;
2268  for(; i!=iend; ++i) os << " " << e[i];
2269  os << ")";
2270  break;
2271  }
2272  case POW:
2273  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
2274  break;
2275  case DIVIDE:
2276  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
2277  break;
2278  case LT:
2279  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
2280  }
2281  os << "(< " << e[0] << " " << e[1] <<")";
2282  break;
2283  case LE:
2284  os << "(<= " << e[0] << " " << e[1] << ")";
2285  break;
2286  case GT:
2287  os << "(> " << e[0] << " " << e[1] << ")";
2288  break;
2289  case GE:
2290  os << "(>= " << e[0] << " " << e[1] << ")";
2291  break;
2292  case DARK_SHADOW:
2293  case GRAY_SHADOW:
2294  os <<"ERROR:SHADOW:not supported in TPTP\n";
2295  break;
2296  default:
2297  // Print the top node in the default LISP format, continue with
2298  // pretty-printing for children.
2299  e.print(os);
2300 
2301  break;
2302  }
2303  break; // end of case TPTP_LANG
2304 
2305 
2306  case PRESENTATION_LANG:
2307  switch(e.getKind()) {
2308  case REAL:
2309  case INT:
2310  case RATIONAL_EXPR:
2311  case NEGINF:
2312  case POSINF:
2313  e.print(os);
2314  break;
2315  case SUBRANGE:
2316  if(e.arity() != 2) e.printAST(os);
2317  else
2318  os << "[" << push << e[0] << ".." << e[1] << push << "]";
2319  break;
2320  case IS_INTEGER:
2321  if(e.arity() == 1)
2322  os << "IS_INTEGER(" << push << e[0] << push << ")";
2323  else
2324  e.printAST(os);
2325  break;
2326  case PLUS: {
2327  int i=0, iend=e.arity();
2328  os << "(" << push;
2329  if(i!=iend) os << e[i];
2330  ++i;
2331  for(; i!=iend; ++i) os << space << "+ " << e[i];
2332  os << push << ")";
2333  break;
2334  }
2335  case MINUS:
2336  os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
2337  break;
2338  case UMINUS:
2339  os << "-(" << push << e[0] << push << ")";
2340  break;
2341  case MULT: {
2342  int i=0, iend=e.arity();
2343  os << "(" << push;
2344  if(i!=iend) os << e[i];
2345  ++i;
2346  for(; i!=iend; ++i) os << space << "* " << e[i];
2347  os << push << ")";
2348  break;
2349  }
2350  case POW:
2351  os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
2352  break;
2353  case DIVIDE:
2354  os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
2355  break;
2356  case LT:
2357  if (isInt(e[0].getType()) || isInt(e[1].getType())) {
2358  }
2359  os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
2360  break;
2361  case LE:
2362  os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
2363  break;
2364  case GT:
2365  os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
2366  break;
2367  case GE:
2368  os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
2369  break;
2370  case DARK_SHADOW:
2371  os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
2372  break;
2373  case GRAY_SHADOW:
2374  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
2375  << "," << space << e[2] << "," << space << e[3] << push << ")";
2376  break;
2377  default:
2378  // Print the top node in the default LISP format, continue with
2379  // pretty-printing for children.
2380  e.printAST(os);
2381 
2382  break;
2383  }
2384  break; // end of case PRESENTATION_LANG
2385  case SMTLIB_LANG:
2386  case SMTLIB_V2_LANG: {
2387  switch(e.getKind()) {
2388  case REAL_CONST:
2389  printRational(os, e[0].getRational(), true);
2390  break;
2391  case RATIONAL_EXPR:
2392  printRational(os, e.getRational());
2393  break;
2394  case REAL:
2395  os << "Real";
2396  break;
2397  case INT:
2398  os << "Int";
2399  break;
2400  case SUBRANGE:
2401  throw SmtlibException("TheoryArithNew::print: SMTLIB: SUBRANGE not implemented");
2402 // if(e.arity() != 2) e.print(os);
2403 // else
2404 // os << "(" << push << "SUBRANGE" << space << e[0]
2405 // << space << e[1] << push << ")";
2406  break;
2407  case IS_INTEGER:
2408  if(e.arity() == 1)
2409  os << "(" << push << "IsInt" << space << e[0] << push << ")";
2410  else
2411  throw SmtlibException("TheoryArithNew::print: SMTLIB: IS_INTEGER used unexpectedly");
2412  break;
2413  case PLUS: {
2414  if(e.arity() == 1 && os.lang() == SMTLIB_V2_LANG) {
2415  os << e[0];
2416  } else {
2417  os << "(" << push << "+";
2418  Expr::iterator i = e.begin(), iend = e.end();
2419  for(; i!=iend; ++i) {
2420  os << space << (*i);
2421  }
2422  os << push << ")";
2423  }
2424  break;
2425  }
2426  case MINUS: {
2427  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
2428  break;
2429  }
2430  case UMINUS: {
2431  os << "(" << push << "-" << space << e[0] << push << ")";
2432  break;
2433  }
2434  case MULT: {
2435  int i=0, iend=e.arity();
2436  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
2437  os << e[0];
2438  } else {
2439  for(; i!=iend; ++i) {
2440  if (i < iend-1) {
2441  os << "(" << push << "*";
2442  }
2443  os << space << e[i];
2444  }
2445  for (i=0; i < iend-1; ++i) os << push << ")";
2446  }
2447  break;
2448  }
2449  case POW:
2450  throw SmtlibException("TheoryArithNew::print: SMTLIB: POW not supported");
2451  // os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
2452  break;
2453  case DIVIDE: {
2454  throw SmtlibException("TheoryArithNew::print: SMTLIB: unexpected use of DIVIDE");
2455  break;
2456  }
2457  case LT: {
2458  Rational r;
2459  os << "(" << push << "<" << space;
2460  os << e[0] << space << e[1] << push << ")";
2461  break;
2462  }
2463  case LE: {
2464  Rational r;
2465  os << "(" << push << "<=" << space;
2466  os << e[0] << space << e[1] << push << ")";
2467  break;
2468  }
2469  case GT: {
2470  Rational r;
2471  os << "(" << push << ">" << space;
2472  os << e[0] << space << e[1] << push << ")";
2473  break;
2474  }
2475  case GE: {
2476  Rational r;
2477  os << "(" << push << ">=" << space;
2478  os << e[0] << space << e[1] << push << ")";
2479  break;
2480  }
2481  case DARK_SHADOW:
2482  throw SmtlibException("TheoryArithNew::print: SMTLIB: DARK_SHADOW not supported");
2483  os << "(" << push << "DARK_SHADOW" << space << e[0]
2484  << space << e[1] << push << ")";
2485  break;
2486  case GRAY_SHADOW:
2487  throw SmtlibException("TheoryArithNew::print: SMTLIB: GRAY_SHADOW not supported");
2488  os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
2489  << "," << space << e[2] << "," << space << e[3] << push << ")";
2490  break;
2491  default:
2492  throw SmtlibException("TheoryArithNew::print: SMTLIB: default not supported");
2493  // Print the top node in the default LISP format, continue with
2494  // pretty-printing for children.
2495  e.printAST(os);
2496 
2497  break;
2498  }
2499  break; // end of case SMTLIB_LANG
2500  }
2501  case LISP_LANG:
2502  switch(e.getKind()) {
2503  case REAL:
2504  case INT:
2505  case RATIONAL_EXPR:
2506  case NEGINF:
2507  case POSINF:
2508  e.print(os);
2509  break;
2510  case SUBRANGE:
2511  if(e.arity() != 2) e.printAST(os);
2512  else
2513  os << "(" << push << "SUBRANGE" << space << e[0]
2514  << space << e[1] << push << ")";
2515  break;
2516  case IS_INTEGER:
2517  if(e.arity() == 1)
2518  os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
2519  else
2520  e.printAST(os);
2521  break;
2522  case PLUS: {
2523  int i=0, iend=e.arity();
2524  os << "(" << push << "+";
2525  for(; i!=iend; ++i) os << space << e[i];
2526  os << push << ")";
2527  break;
2528  }
2529  case MINUS:
2530  //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
2531  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
2532  break;
2533  case UMINUS:
2534  os << "(" << push << "-" << space << e[0] << push << ")";
2535  break;
2536  case MULT: {
2537  int i=0, iend=e.arity();
2538  os << "(" << push << "*";
2539  for(; i!=iend; ++i) os << space << e[i];
2540  os << push << ")";
2541  break;
2542  }
2543  case POW:
2544  os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
2545  break;
2546  case DIVIDE:
2547  os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
2548  break;
2549  case LT:
2550  os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
2551  break;
2552  case LE:
2553  os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
2554  break;
2555  case GT:
2556  os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
2557  break;
2558  case GE:
2559  os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
2560  break;
2561  case DARK_SHADOW:
2562  os << "(" << push << "DARK_SHADOW" << space << e[0]
2563  << space << e[1] << push << ")";
2564  break;
2565  case GRAY_SHADOW:
2566  os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
2567  << e[1] << space << e[2] << space << e[3] << push << ")";
2568  break;
2569  default:
2570  // Print the top node in the default LISP format, continue with
2571  // pretty-printing for children.
2572  e.printAST(os);
2573 
2574  break;
2575  }
2576  break; // end of case LISP_LANG
2577  default:
2578  // Print the top node in the default LISP format, continue with
2579  // pretty-printing for children.
2580  e.printAST(os);
2581  }
2582  return os;
2583 }
2584 
2585 ///////////////////////////////////////////////////////////////////////////////
2586 // SIMPLEX SOLVER //
2587 ///////////////////////////////////////////////////////////////////////////////
2588 
2589 bool TheoryArithNew::isBasic(const Expr& x) const {
2590  // If it is on the right side of the tableaux the it is basic, non-basic otherwise
2591  return (tableaux.find(x) != tableaux.end());
2592 }
2593 
2594 void TheoryArithNew::pivot(const Expr& x_r, const Expr& x_s) {
2595 
2596  // Check that the variable is non-basic
2597  DebugAssert(isBasic(x_r), "TheoryArithNew::pivot, given variable should be basic" + x_r.toString());
2598  DebugAssert(!isBasic(x_s), "TheoryArithNew::pivot, given variable should be non-basic" + x_s.toString());
2599 
2600  // If trace is on for the simplex, print it out
2601  TRACE("simplex", "TheoryArithNew::pivot(", x_r.toString() + ", " + x_s.toString(), ")");
2602 
2603  // Get the iterator that points to the expression of x_r
2604  TebleauxMap::iterator it = tableaux.find(x_r);
2605 
2606  // Get the expresiion of x_r
2607  Theorem x_r_Theorem = (*it).second;
2608 
2609  // Erase the x_r expression from the tableaux
2610  tableaux.erase(x_r); // TODO: Add erase by iterator to ExprHashMap
2611 
2612  // Update the dependencies
2613  updateDependenciesRemove(x_r, x_r_Theorem.getExpr()[1]);
2614 
2615  // Construct the expresison (theorem) of x_s
2616  const Theorem& x_s_Theorem = pivotRule(x_r_Theorem, x_s);
2617 
2618  // Replace all occurances of x_s with x_s_Expression
2619  substAndCanonizeTableaux(x_s_Theorem);
2620 
2621  // Update the dependencies
2622  updateDependenciesAdd(x_s, x_s_Theorem.getExpr()[1]);
2623 
2624  // Add the expression of x_s to the map
2625  tableaux[x_s] = x_s_Theorem;
2626 }
2627 
2628 void TheoryArithNew::update(const Expr& x_i, const EpsRational& v) {
2629 
2630  // Check that the variable is non-basic
2631  DebugAssert(tableaux.find(x_i) == tableaux.end(), "TheoryArithNew::update, given variable should be non-basic" + x_i.toString());
2632 
2633  // If trace is on for the simplex, print it out
2634  TRACE("simplex", "TheoryArithNew::update(", x_i.toString() + ", " + v.toString(), ")");
2635 
2636  // Remember the value of the x_i variable
2637  EpsRational old_value = getBeta(x_i);
2638 
2639  // If there are dependent variables then do the work
2641  if (find != dependenciesMap.end()) {
2642 
2643  // Go through all the variables that depend on x_i
2644  const set<Expr>& dependent = (*find).second;
2645  set<Expr>::const_iterator it = dependent.begin();
2646  set<Expr>::const_iterator it_end = dependent.end();
2647  // Fix the values of all the variables
2648  while (it != it_end) {
2649 
2650  // Get the current variable
2651  const Expr& x_j = *it;
2652 
2653  // Get the tableaux coefficient of the of x_i in the row of x_j (the right side ofg the tableaux expression)
2654  const Rational& a_ji = getTableauxEntry(x_j, x_i);
2655 
2656  // Update the beta valuation
2657  EpsRational b(getBeta(x_j)); // TODO: not necessary, beta's are all setup now
2658  EpsRational x_j_new = beta[x_j] = b + (v - old_value) * a_ji;
2659 
2660  // Check if the variable is sat or unsat under the new assignment
2661  if (x_j_new < getLowerBound(x_j) || getUpperBound(x_j) < x_j_new)
2662  unsatBasicVariables.insert(x_j);
2663  else
2664  unsatBasicVariables.erase(x_j);
2665 
2666  // Go to the next one
2667  it ++;
2668  }
2669  }
2670 
2671  // Set the new value to x_i (x_i) is non_basic, no need to add to unsat set)
2672  beta[x_i] = v;
2673 }
2674 
2675 void TheoryArithNew::pivotAndUpdate(const Expr& x_i, const Expr& x_j, const EpsRational& v) {
2676 
2677  // Variable x_i should be a basic variable (left side of the tableaux) and x_j should be non_basic
2678  DebugAssert(tableaux.find(x_i) != tableaux.end(), "TheoryArithNew::pivotAndUpdate, " + x_i.toString() + " should be a basic variable");
2679  DebugAssert(tableaux.find(x_j) == tableaux.end(), "TheoryArithNew::pivotAndUpdate, " + x_j.toString() + " should be a non-basic variable");
2680 
2681  // If trace is on for the simplex, print it out
2682  TRACE("simplex", "TheoryArithNew::pivotAndUpdate(", x_i.toString() + ", " + x_j.toString() + ", " + v.toString(), ")");
2683 
2684  // The a_ij coefficient of the tableaux
2685  const Rational& a_ij = getTableauxEntry(x_i, x_j);
2686 
2687  // Let theta be the adjustment coefficient
2688  EpsRational theta((v - getBeta(x_i))/a_ij);
2689 
2690  // Set the new value to x_i (x_i becomes non-basic, hance sat)
2691  beta[x_i] = v;
2692  // x_i becomes non-basic, no need ==> it is sat
2693  unsatBasicVariables.erase(x_i);
2694 
2695  // Set the new value to x_j
2696  EpsRational b = getBeta(x_j);
2697  EpsRational new_x_j = beta[x_j] = b + theta;
2698 
2699  // Check if the variable is sat or unsat under the new assignment
2700  if (new_x_j < getLowerBound(x_j) || getUpperBound(x_j) < new_x_j)
2701  unsatBasicVariables.insert(x_j);
2702  else
2703  unsatBasicVariables.erase(x_j);
2704 
2705  // Go through all the variables that depend on x_j, and update their value (there will be at least one, i.e. x_i) // TODO: maybe optimise
2706  const set<Expr>& dependent = (*dependenciesMap.find(x_j)).second;
2707  set<Expr>::const_iterator it = dependent.begin();
2708  set<Expr>::const_iterator it_end = dependent.end();
2709  // Go throught all the basic variables
2710  while (it != it_end) {
2711 
2712  // Get the current variable
2713  const Expr& x_k = *it;
2714 
2715  // If the basic variable is different from x_i update its value
2716  if (x_k != x_i) {
2717 
2718  // Get the a_kj coefficient from the tableaux
2719  const Rational& a_kj = getTableauxEntry(x_k, x_j);
2720 
2721  // Adjust the value (check fort sat/unsat, x_k is basic)
2722  b = getBeta(x_k);
2723  EpsRational x_k_new = beta[x_k] = b + theta * a_kj;
2724 
2725  // Check if the variable is sat or unsat under the new assignment
2726  if (x_k_new < getLowerBound(x_k) || getUpperBound(x_k) < x_k_new)
2727  unsatBasicVariables.insert(x_k);
2728  else
2729  unsatBasicVariables.erase(x_k);
2730  }
2731 
2732  // Go to the next one
2733  it ++;
2734  }
2735 
2736  // Last thing to do, pivot x_i and x_j
2737  pivot(x_i, x_j);
2738 }
2739 
2741 
2742  // If trace is on for the simplex, print it out
2743  TRACE("simplex", "TheoryArithNew::assertUpper(", x_i.toString() + ", " + c.toString(), ")");
2744 
2745  // Check if the given expression is actually a variable
2746  DebugAssert(isLeaf(x_i), "TheoryArithNew::assertUpper wrong kind, expected an arithmetic leaf (variable) got " + x_i.toString());
2747 
2748  // Check if the upper bound is worse then the last one
2749  if (getUpperBound(x_i) <= c) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
2750 
2751  // If the new bound is lower then the lower bound */
2752  if (c < getLowerBound(x_i)) {
2753  // Create the explaining theorem
2755  // Return unsatisfiable
2756  return UNSATISFIABLE;
2757  }
2758 
2759  // Since it is a tighter bound, propagate what can be
2760  propagate = true;
2761 
2762  // Set the new upper bound */
2763  upperBound[x_i] = BoundInfo(c, thm);
2764 
2765  // If within the new bounds, return the previous state
2766  if (getBeta(x_i) <= c) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
2767 
2768  // Otherwise, if the variable is non-basic then update it's value
2769  if (!isBasic(x_i)) update(x_i, c);
2770  // Else its basic, and non-sat, add to the unsat set
2771  else unsatBasicVariables.insert(x_i);
2772 
2773  // Everything went fine, return OK (not complete, means not UNSAT)
2774  return UNKNOWN;
2775 }
2776 
2778 
2779  // Check if the given expression is actually a variable
2780  DebugAssert(isLeaf(x_i), "TheoryArithNew::assertLower wrong kind, expected an arithmetic leaf (variable) got " + x_i.toString());
2781 
2782  // If trace is on for the simplex, print it out
2783  TRACE("simplex", "TheoryArithNew::assertLower(", x_i.toString() + ", " + c.toString(), ")");
2784 
2785  // Check if the upper bound is worse then the last one
2786  if (c <= getLowerBound(x_i)) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
2787 
2788  // Since it is a tighter bound, propagate what can be
2789  propagate = true;
2790 
2791  // If the new bound is lower then the bound */
2792  if (c > getUpperBound(x_i)) {
2793  // Create the explaining theorem
2795  // Return unsatisfiable
2796  return UNSATISFIABLE;
2797  }
2798 
2799  // Set the new upper bound */
2800  lowerBound[x_i] = BoundInfo(c, thm);
2801 
2802  // If within the new bounds, return the previous state
2803  if (c <= getBeta(x_i)) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
2804 
2805  // Otherwise, if the variable is non-basic then update it's value
2806  if (!isBasic(x_i)) update(x_i, c);
2807  // Else its basic, and non-sat, add to the unsat set
2808  else unsatBasicVariables.insert(x_i);
2809 
2810  // Everything went fine, return OK (not complete, means not UNSAT)
2811  return UNKNOWN;
2812 }
2813 
2815 
2816  // Assert the upper bound
2817  consistent = assertUpper(x_i, c, thm); // TODO: thm: = |- <=
2818 
2819  // If the return value is UNSAT return UNSAT
2820  if (consistent == UNSATISFIABLE) return UNSATISFIABLE;
2821 
2822  // Assert the lower bound
2823  consistent = assertLower(x_i, c, thm); // TODO: thm: = |- >=
2824 
2825  // Return the consistency
2826  return consistent;
2827 }
2828 
2829 
2830 void TheoryArithNew::checkSat(bool fullEffort)
2831 {
2832  // We should not be here if inconsistent
2833  DebugAssert(consistent != UNSATISFIABLE, "TheoryArithNew::checkSat : we are UNSAT before entering?!?!");
2834 
2835  // Trace the check sat if simplex flag is on
2836  TRACE("simplex", "TheoryArithNew::checkSat(fullEffort=",fullEffort? "true" : "false", ")");
2837 
2838  // Check if by backtracking we have more fresh variables than we expect
2839  if (assertedExprCount < assertedExpr.size())
2841 
2842  // Do the simplex search if the database is not satisfiable (if inconsistent, we will not be here);
2843  if (consistent != SATISFIABLE || fullEffort)
2845 
2846  // If the result is inconsistent set the inconsistent flag
2847  if (consistent == UNSATISFIABLE)
2849 
2850  // If we are not - consistent, check the integer satisfiability
2851 // if (consistent == SATISFIABLE) {
2852 // // If we asserted a lemma and it hasn't been processed yet, we just don't do anything
2853 // Theorem integer_lemma_thm = integer_lemma;
2854 // if (!integer_lemma_thm.isNull()) {
2855 // if (simplify(integer_lemma_thm.getExpr()).getRHS() == getEM()->trueExpr())
2856 // consistent = checkSatInteger();
2857 // else
2858 // consistent = UNKNOWN;
2859 // } else
2860 // // Lemma was not asserted, check integer sat
2861 // consistent = checkSatInteger();
2862 // }
2863 
2864  // Trace the check sat if simplex flag is on
2865  TRACE("simplex", "TheoryArithNew::checkSat ==> ", consistent == UNSATISFIABLE? "UNSATISFIABLE" : "SATISFIABLE", "");
2866 }
2867 
2869 
2870  // Trace the check sat if simplex flag is on
2871  TRACE("simplex", "TheoryArithNew::checkSatInteger()", "", "");
2872 
2873  // At this point we are REAL satisfiable, so we have to check the integers
2874  set<Expr>::iterator x_i_it = intVariables.begin();
2875  set<Expr>::iterator x_i_it_end = intVariables.end();
2876 // cerr << "Integer vars: ";
2877 // while (x_i_it != x_i_it_end) {
2878 // cerr << *x_i_it << " ";
2879 // ++ x_i_it;
2880 // }
2881 // cerr << endl;
2882 //
2883 // x_i_it = intVariables.begin();
2884 // x_i_it_end = intVariables.end();
2885  while (x_i_it != x_i_it_end) {
2886 
2887  // Get the left-hand variable of the tableaux
2888  const Expr& x_i = (*x_i_it);
2889 
2890  // Only do work for unsat integer variables
2891  if (isInteger(x_i)) {
2892 
2893  // Get the current assignment of x_i
2894  const EpsRational& beta = getBeta(x_i);
2895 
2896  // Check if it is an integer
2897  if (beta.isInteger()) { ++ x_i_it; continue; }
2898 
2899  // Since the variable is not an integer, split on it being <= [beta] and >= [beta] + 1
2900  integer_lemma = d_rules->integerSplit(x_i, beta.getFloor());
2901  TRACE("integer", "TheoryArithNew::checkSatInteger ==> lemma : ", integer_lemma, "");
2903 
2904  // One split should be enough, return unknown
2905  return UNKNOWN;
2906  }
2907 
2908  // Go to the next row
2909  ++ x_i_it;
2910  }
2911 
2912  // We came through, huh, we are sat
2913  return SATISFIABLE;
2914 }
2915 
2917 
2918  Expr x_i; // The basic variable we will use
2919  EpsRational x_i_Value; // The current value of the variable x_i
2920  Expr x_j; // The non-basic variable we will use
2921  EpsRational x_j_Value; // The current value of the variable x_j
2922  Rational a_ij; // The coefficient wwhen expanding x_i using x_j in the tableaux
2923 
2924  bool x_j_Found; // Did we find a suitable one
2925  EpsRational l_i; // Lower bound of x_i
2926  EpsRational u_i; // Upper bound of x_i
2927 
2928  // Trace the size of the tableaux and the unsat
2929  TRACE("arith_atoms", "Tableaux size: ", tableaux.size(), "");
2930  TRACE("arith_atoms", "UNSAT vars: ", unsatBasicVariables.size(), "");
2931 
2932  // The main loop
2933  while (unsatBasicVariables.size()) {
2934 
2935  // The first unsat variable information
2936  x_i = *unsatBasicVariables.begin();
2937  TebleauxMap::iterator it = tableaux.find(x_i);
2938  x_i_Value = getBeta(x_i);
2939  l_i = getLowerBound(x_i);
2940  u_i = getUpperBound(x_i);
2941 
2942  // If the variable doesn't obey the lower bound
2943  if (l_i > x_i_Value) {
2944 
2945  // Did we find a suitable x_j, NOT YET
2946  x_j_Found = false;
2947 
2948  // Find the smalles non-basic x_j that can improve x_i
2949  const Expr& x_i_RightSide = (*it).second.getExpr()[1];
2950  int non_basics_i_end = x_i_RightSide.arity();
2951  for(int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
2952 
2953  // Get the info on the current variable
2954  x_j = x_i_RightSide[non_basics_i][1];
2955  a_ij = x_i_RightSide[non_basics_i][0].getRational();
2956  x_j_Value = getBeta(x_j);
2957 
2958  // If there is slack for improving x_i using x_j then do it
2959  if (a_ij > 0) {
2960  if (x_j_Value < getUpperBound(x_j)) {
2961  x_j_Found = true;
2962  break;
2963  }
2964  } else {
2965  if (x_j_Value > getLowerBound(x_j)) {
2966  x_j_Found = true;
2967  break;
2968  }
2969  }
2970  }
2971 
2972  // If none of the variables allows for slack, the tableaux is unsatisfiable
2973  if (!x_j_Found) {
2974  // Generate the explanation
2976  // Return unsat
2977  return UNSATISFIABLE;
2978  }
2979 
2980  // Otherwise do pivotAndUpdate and continue with the loop
2981  pivotAndUpdate(x_i, x_j, l_i);
2982  } else
2983  // If the variable doesn't obey the upper bound
2984  if (x_i_Value > u_i) {
2985 
2986  // Did we find a suitable x_j, NOT YET
2987  x_j_Found = false;
2988 
2989  // Find the smalles non-basic x_j that can improve x_i
2990  const Expr& x_i_RightSide = (*it).second.getExpr()[1];
2991  int non_basics_i_end = x_i_RightSide.arity();
2992  for(int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
2993 
2994  // Get the info on the current variable
2995  x_j = x_i_RightSide[non_basics_i][1];
2996  a_ij = x_i_RightSide[non_basics_i][0].getRational();
2997  x_j_Value = getBeta(x_j);
2998 
2999  // If there is slack for improving x_i using x_j then do it
3000  if (a_ij < 0) {
3001  if (x_j_Value < getUpperBound(x_j)) {
3002  x_j_Found = true;
3003  break;
3004  }
3005  } else
3006  if (x_j_Value > getLowerBound(x_j)) {
3007  x_j_Found = true;
3008  break;
3009  }
3010  }
3011 
3012  // If none of the variables allows for slack, the tableaux is unsatisfiable
3013  if (!x_j_Found) {
3014  // Generate the explanation
3016  // Return unsat
3017  return UNSATISFIABLE;
3018  }
3019 
3020  // Otherwise do pivotAndUpdate and continue with the loop
3021  pivotAndUpdate(x_i, x_j, u_i);
3022  } else
3023  // Due to backtracking a unsat might become sat, just erase it
3024  unsatBasicVariables.erase(x_i);
3025 
3026 
3027  // If trace is on, printout the current valuation and the tableaux
3028  TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> new tableaux : \n", tableauxAsString(), "");
3029  TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> new bounds : \n", boundsAsString(), "");
3030  TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> unsat : \n", unsatAsString(), "");
3031 
3032  };
3033 
3034  // Since there is no more unsat constraints we are satisfiable
3035  return SATISFIABLE;
3036 }
3037 
3039  return findCoefficient(x_j, tableaux[x_i].getExpr()[1]);
3040 }
3041 
3042 
3043 const Rational& TheoryArithNew::findCoefficient(const Expr& var, const Expr& expr) {
3044 
3045  // The zero coefficient
3046  static Rational zeroCoefficient(0);
3047 
3048  // The given expression must be a sum
3049  DebugAssert(isPlus(expr), "TheoryArithNew::findCoefficient : expression must be a sum : " + expr.toString());
3050 
3051  // Go through the sum and find the coefficient
3052  int left = 0;
3053  int right = expr.arity() - 1;
3054  int i;
3055  while (left <= right) {
3056 
3057  // Take the middle one
3058  i = (left + right ) / 2;
3059 
3060  // Current expression
3061  const Expr& mult = expr[i];
3062 
3063  // Every summand must be a multiplication with a rational
3064  DebugAssert(isMult(mult) && isRational(mult[0]), "TheoryArithNew::findCoefficient : expression must be a sum of multiplications: " + expr.toString());
3065 
3066  // If the variable is the same return the coefficient
3067  int cmp = compare(mult[1], var);
3068  if (cmp == 0)
3069  return mult[0].getRational();
3070  else
3071  if (cmp > 0)
3072  left = i + 1;
3073  else
3074  right = i - 1;
3075  }
3076 
3077  // Not found, return 0
3078  return zeroCoefficient;
3079 }
3080 
3081 
3083  // Try and find the lower bound in the map
3085  // If not found return +infinity as the default value, othervise return the value
3086  if (find == lowerBound.end()) return EpsRational::MinusInfinity;
3087  else return (*find).second.bound;
3088 }
3089 
3091  // Try and find the upper bound in the map
3093  // If not found return -infinity as the default value, othervise return the value
3094  if (find == upperBound.end()) return EpsRational::PlusInfinity;
3095  else return (*find).second.bound;
3096 }
3097 
3099  // Try and find the upper bound in the map
3101  // It has to be found
3102  DebugAssert(find != lowerBound.end(), "TheoryArithNew::getLowerBoundThm, theorem not found for " + x.toString());
3103  // Return the bound theorem
3104  return (*find).second.theorem;
3105 }
3106 
3108  // Try and find the upper bound in the map
3110  // It has to be found
3111  DebugAssert(find != upperBound.end(), "TheoryArithNew::getUpperBoundThm, theorem not found for " + x.toString());
3112  // Return the bound theorem
3113  return (*find).second.theorem;
3114 }
3115 
3116 
3118 
3119  // Try to find the beta value in the map
3121 
3122  if (find == beta.end()) {
3123  // If not found return 0 (no need for sat/unsat, it's allways sat)
3124  return beta[x] = EpsRational::Zero;
3125 
3126  // Check if the variable is sat or unsat under the new assignment
3128  unsatBasicVariables.insert(x);
3129  else
3130  unsatBasicVariables.erase(x);
3131  }
3132  else
3133  // If found, just return it
3134  return (*find).second;
3135 }
3136 
3137 
3138 void TheoryArithNew::assertFact(const Theorem& assertThm)
3139 {
3140  // Get the expression to be asserted
3141  const Expr& expr = assertThm.getExpr();
3142 
3143  // If tracing arithmetic, print out the expression to be asserted
3144  TRACE("simplex", "TheoryArithNew::assertFact(", expr, ")");
3145  TRACE("simplex", "asserted: ", assertedExpr.size(), "");
3146  TRACE("simplex", "counted: ", assertedExprCount, "");
3147  TRACE("arith_atoms", "Assert: ", expr.toString(), "");
3148 
3149  // Check if by backtracking we have more fresh variables than we expect
3150  if (assertedExprCount < assertedExpr.size())
3152 
3153  // Get the constraint partsreturn
3154  const Expr& leftSide = expr[0]; // The left side of the constraint
3155  const Expr& rightSide = expr[1]; // The right side of the constraint
3156  int kind = expr.getKind(); // The relational symbol, should be one of LT, LE, GT, GE. EQ was rewritten as LE and GE so its not here
3157 
3158  // The expression must be an inequality (sum a_1*x_1 .. a_n*x_n) @ b
3159  DebugAssert(isIneq(expr) , "TheoryArithNew::assertFact wrong kind, expected inequality" + expr.toString());
3160  DebugAssert(isPlus(rightSide) || (isMult(rightSide) && isRational(rightSide[0]) && isLeaf(rightSide[1])), "TheoryArithNew::assertFact wrong kind, expected sum on the right side opr a simple 1*x" + expr.toString());
3161  DebugAssert(isRational(leftSide), "TheoryArithNew::assertFact wrong kind, expected rational on the right side" + expr.toString());
3162 
3163  // Get the rational value on the right side
3164  Rational leftSideValue = leftSide.getRational();
3165 
3166  // The rational bound on the constraint
3167  Rational c = leftSideValue;
3168 
3169  // The variable to be constrained
3170  Expr var;
3171 
3172  // Theorem of the assertion
3173  Theorem assert = assertThm;
3174 
3175  // For now we have that leftSide @ (c1x1 + c2x2 + ... cnxn) = rightSide
3176  // If rightSide is not a sum constraint is atomic (leftSide @ a*x)
3177  if (!isPlus(rightSide)) {
3178 
3179  // Tee left side in this case should be 1*x
3180  DebugAssert(rightSide[0].isRational() && rightSide[0].getRational() == 1, "TheoryArithNew::assertFact, left side should be multiplication by one");
3181 
3182  // Change the assert theorem to remove the 1*x to x
3183  assert = iffMP(assert, substitutivityRule(expr, reflexivityRule(leftSide), d_rules->oneElimination(rightSide)));
3184 
3185  // The variable will just be x1 (if var is not already present in the tableaux, it will be non-basic)
3186  var = rightSide[1]; // IMPORTANT!!!, when giving explanations, it should be of the same form
3187 
3188  // If an integer, add it to the integer set
3189  if (isInteger(var)) intVariables.insert(var);
3190 
3191  } else {
3192  // Get the theorem that corresponds to the introduction of the new variable var = leftSide
3193  const Theorem& introductionThm = getVariableIntroThm(rightSide);
3194 
3195  // Take the new variable out
3196  var = introductionThm.getExpr()[0];
3197 
3198  // Change the theorem for the assertion so that it involves the new variable, i.e. c < rightSide, var = rightSide |- c < var
3199  assert = iffMP(assertThm, substitutivityRule(expr, 1, symmetryRule(introductionThm)));
3200 
3201  // Insert all the integer variables into the integer set
3202  if (isInteger(var)) {
3203  intVariables.insert(var);
3204  int i_end = rightSide.arity();
3205  for(int i = 0; i < i_end; ++ i)
3206  intVariables.insert(rightSide[i][1]);
3207  } else {
3208  int i_end = rightSide.arity();
3209  for(int i = 0; i < i_end; ++ i)
3210  if (isInteger(rightSide[i][1])) intVariables.insert(rightSide[i][1]);
3211  }
3212  }
3213 
3214  // Make the BoundInfo object for theory propagation
3215  EpsRational bound;
3216 
3217  // By default we don't propagate
3218  propagate = false;
3219 
3220  // Remember the old bound
3221  EpsRational oldBound;
3222 
3223  // Finnaly assert the right constraint
3224  switch (kind) {
3225  case LT:
3226  oldBound = getLowerBound(var);
3227  // c < var, convert to c + epsilon <= var and assert it
3228  consistent = assertLower(var, bound = EpsRational(c, +1), assert);
3229  break;
3230  case LE:
3231  oldBound = getLowerBound(var);
3232  // c <= var, assert the lower bound
3233  consistent = assertLower(var, bound = c, assert);
3234  break;
3235  case GT:
3236  oldBound = getUpperBound(var);
3237  // c > var, convert to c - epsilon >= var and assert it
3238  consistent = assertUpper(var, bound = EpsRational(c, -1), assert);
3239  break;
3240  case GE:
3241  oldBound = getUpperBound(var);
3242  // c >= var, assert the upper bound
3243  consistent = assertUpper(var, bound = c, assert);
3244  break;
3245  case EQ:
3246  // c == var, assert the equality
3247  consistent = assertEqual(var, bound = c, assert);
3248  // For now, don't propagate anything
3249  propagate = false; // TODO: some propagation is in place here (negations)
3250  break;
3251  default:
3252  //How did we get here
3253  FatalAssert(false, "Theory_Arith::assertFact, control should not reach here");
3254  break;
3255  }
3256 
3257  // If tracing arithmetic, print out the new tableaux and the current bounds
3258  TRACE("simplex", "TheoryArithNew::assertFact ==> ", consistent == UNSATISFIABLE? "UNSATISFIABLE" : consistent == UNKNOWN? "UNKNOWN" : "SATISFIABLE", "");
3259  TRACE("simplex", "TheoryArithNew::assertFact ==> new tableaux : \n", tableauxAsString(), "");
3260  TRACE("simplex", "TheoryArithNew::assertFact ==> new bounds : \n", boundsAsString(), "");
3261  TRACE("simplex", "TheoryArithNew::assertFact ==> unsat : \n", unsatAsString(), "");
3262 
3263  // If the result is inconsistent set the inconsistent flag
3264  if (consistent == UNSATISFIABLE)
3266 
3267  // Not inconsistent, propagate all from this assertion
3268  if (propagate)
3269  propagateTheory(assertThm.getExpr(), bound, oldBound);
3270 }
3271 
3272 
3274 
3275  // Try to find the expression in the map
3277 
3278  // If not in tableaux, add it and assign it a new variable
3279  if (find == freshVariables.end()) {
3280 
3281  // Get the common rules
3282  CommonProofRules* c_rules = getCommonRules();
3283 
3284  // Create a new variable (\exists x . rightSide = x)
3285  Theorem thm = c_rules->varIntroRule(rightSide);
3286 
3287  // Skolemise it, to get an equality (\exists x . rightSide = x) <==> rightSide = c, then infer |- rightSide = c
3288  thm = c_rules->iffMP(thm, c_rules->skolemizeRewrite(thm.getExpr()));
3289 
3290  // Reverse the equality into standard form
3291  thm = symmetryRule(thm);
3292 
3293  // Add the theorem to the variable introduction map (this is the theorem we return)
3294  Theorem returnThm = freshVariables[rightSide] = thm;
3295 
3296  // Now, flatten the equality modulo tableaux
3297  thm = substAndCanonizeModTableaux(thm);
3298 
3299  // Get the skolem constant that was introduced (|- c = leftSide)
3300  const Expr& var = thm.getExpr()[0];
3301 
3302  // Also add it to the tableaux
3303  tableaux[var] = thm;
3304 
3305  // Update the dependencies
3306  updateDependenciesAdd(var, thm.getExpr()[1]);
3307 
3308  // Add it to the expressions map
3309  assertedExpr.push_back(Expr(EQ, var, rightSide));
3311 
3312  // Compute the value of the new variable using the tableaux
3313  updateValue(var, rightSide);
3314 
3315  // Return the variable
3316  return returnThm;
3317  }
3318 
3319  // Otherwise we have it, so return it
3320  return (*find).second;
3321 }
3322 
3323 void TheoryArithNew::updateValue(const Expr& var, const Expr& e) {
3324 
3325  // The initial value
3326  EpsRational varValue(0);
3327 
3328  // Go through the sum and compute the value
3329  int i_end = e.arity();
3330  for (int i = 0; i < i_end; ++ i)
3331  varValue += getBeta(e[i][1]) * e[i][0].getRational();
3332 
3333  // Update the beta
3334  beta[var] = varValue;
3335 
3336  // Check if the variable is sat or unsat under the new assignment
3337  if (varValue < getLowerBound(var) || getUpperBound(var) < varValue)
3338  unsatBasicVariables.insert(var);
3339  else
3340  unsatBasicVariables.erase(var);
3341 }
3342 
3344 
3345  // The string we are building
3346  string str;
3347 
3348  // Start from the begining
3351 
3352  // Print all the rows
3353  while (row != tableaux.end()) {
3354  // Print the equality
3355  str = str + ((*row).second).getExpr().toString() + "\n";
3356 
3357  // Continue to the next row
3358  row ++;
3359  }
3360 
3361  // Return the string representation
3362  return str;
3363 }
3364 
3366 
3367  // The string we are building
3368  string str;
3369 
3370  // Start from the begining
3371  set<Expr>::const_iterator it = unsatBasicVariables.begin();
3372  set<Expr>::const_iterator it_end = unsatBasicVariables.end();
3373 
3374  // Print all the rows
3375  while (it != it_end) {
3376  // Print the equality
3377  str = str + (*it).toString() + " ";
3378 
3379  // Continue to the next row
3380  it ++;
3381  }
3382 
3383  // Return the string representation
3384  return str;
3385 }
3386 
3387 
3389 
3390  // The string we are building
3391  string str;
3392 
3393  // Set containing all the variables
3394  set<Expr> all_variables;
3395 
3396  // Go throught the tableaux and pick up all the variables
3399  for(; it != it_end; it ++) {
3400 
3401  // Add the basic variable to the set
3402  all_variables.insert((*it).first);
3403 
3404  // Go through all the expression variables and add them to the set
3405  const Expr& rightSide = (*it).second.getExpr()[1];
3406  int term_i_end = rightSide.arity();
3407  for(int term_i = 0; term_i < term_i_end; ++ term_i)
3408  all_variables.insert(rightSide[term_i][1]);
3409  }
3410 
3411  // Go throught the bounds map and pickup all the variables
3413  for (bounds_it = lowerBound.begin(); bounds_it != lowerBound.end(); bounds_it ++)
3414  all_variables.insert((*bounds_it).first);
3415  for (bounds_it = upperBound.begin(); bounds_it != upperBound.end(); bounds_it ++)
3416  all_variables.insert((*bounds_it).first);
3417 
3418  // Start from the begining
3419  set<Expr>::iterator var_it = all_variables.begin();
3420  set<Expr>::iterator var_it_end = all_variables.end();
3421 
3422  // Print all the rows
3423  while (var_it != var_it_end) {
3424 
3425  // The current variable
3426  const Expr& var = *var_it;
3427 
3428  // Print the equality
3429  str += getLowerBound(var).toString() + " <= " + var.toString() + "(" + getBeta(var).toString() + ") <= " + getUpperBound(var).toString() + "\n";
3430 
3431  // Continue to the next variable
3432  var_it ++;
3433  }
3434 
3435  // Return the string representation
3436  return str;
3437 }
3438 
3439 // The infinity constant
3441 // The negative infinity constant
3443 // The negative infinity constant
3445 
3446 
3448 
3449  // If subst is empty, just return
3450  if(tableaux.empty()) return eq;
3451 
3452  // Get the expression of the equality
3453  const Expr& eqExpr = eq.getExpr();
3454 
3455  // Check if the equality if in the canonic form
3456  DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::substAndCanonize, expected equality " + eqExpr.toString());
3457 
3458  // Get the left side of the equality
3459  const Expr& rightSide = eqExpr[1];
3460 
3461  // Do the actual substitution in the eqExpr
3462  Theorem thm = substAndCanonizeModTableaux(rightSide);
3463 
3464  // If the substitution had no result just return the original equation
3465  if(thm.getRHS() == rightSide) return eq;
3466 
3467  // Return the theorem
3468  return iffMP(eq, substitutivityRule(eq.getExpr(), 1, thm));
3469 }
3470 
3472 
3473  Theorem res; // The resulting theorem
3474  vector<Theorem> thms; // The theorems of the changed terms for the substitution
3475  vector<unsigned> changed; // The indices of the changed terms for the substitution
3476 
3477  // Trace the canonisation
3478  TRACE("simplex", "TheoryArithNew::substAndCanonizeModTableaux(", sum, ")");
3479 
3480  // Check if the equality if in the canonic form
3481  DebugAssert(sum.getKind() == PLUS, "TheoryArithNew::substAndCanonize, expected sum " + sum.toString());
3482 
3483  // Go throught the sum and try to substitute the variables
3484  int term_index_end = sum.arity();
3485  for(int term_index = 0; term_index < term_index_end; ++ term_index) {
3486 
3487  const Expr& term = sum[term_index]; // The current term expression (a*x)
3488  const Expr& var = term[1]; // The variable of the current term
3489 
3490  // Find the variable in the map
3492 
3493  // If found, substitute it
3494  if (find != tableaux.end()) {
3495 
3496  // Substitute the variable
3497  Theorem termTheorem = canonThm(substitutivityRule(term, 1, (*find).second));
3498 
3499  // Check that the result is not trivial
3500  DebugAssert(termTheorem.getExpr() != term, "substAndCanonizeModTableaux: got the same term in substitution");
3501 
3502  // Push it to the theorems vector
3503  thms.push_back(termTheorem);
3504 
3505  // Add the index to the changed vector
3506  changed.push_back(term_index);
3507  }
3508  }
3509 
3510  // Do the actual substitution and canonize the result
3511  if(thms.size() > 0) {
3512  // Substitute the changed subterms into the term
3513  res = substitutivityRule(sum, changed, thms);
3514  // Canonise the result
3515  res = canonThm(res);
3516  } else
3517  // Nothing happened, just return the reflexivity
3518  res = reflexivityRule(sum);
3519 
3520  // Return the result
3521  return res;
3522 }
3523 
3525 
3526  Theorem result; // The explaining theorem
3527 
3528  // Trace
3529  TRACE("simplex", "TheoryArithNew::substAndCanonizeTableaux(", eq.getExpr(), ")");
3530 
3531  // Get the expression of the equality
3532  const Expr& eqExpr = eq.getExpr();
3533 
3534  // Check if the equality if in the canonic form
3535  DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::substAndCanonize, expected equality " + eqExpr.toString());
3536 
3537  // Get the variable of the substitution
3538  const Expr& var = eqExpr[0];
3539 
3540  // Check if there are variables that depend on x_j
3542  if (find != dependenciesMap.end()) {
3543 
3544  // Go through all the variables that depend on x_j, and update their value
3545  set<Expr>& dependent = (*find).second;
3546  set<Expr>::iterator it = dependent.begin();
3547  set<Expr>::iterator it_end = dependent.end();
3548  for(; it != it_end; ++ it) {
3549 
3550  // Get the expression and the right side of the row from the tableaux
3551  const Expr& leftSide = *it;
3552  TebleauxMap::iterator row = tableaux.find(leftSide);
3553  const Expr& rowExpr = (*row).second.getExpr();
3554  const Expr& rowRightSide = rowExpr[1];
3555 
3556  // Go through the sum and try to substitute
3557  int right = rowRightSide.arity() - 1;
3558  int left = 0;
3559  int term_i;
3560  while (left <= right) {
3561 
3562  // Get the middle one
3563  term_i = (left + right) / 2;
3564 
3565  // Get the comparison of the variables
3566  int cmp = compare(rowRightSide[term_i][1], var);
3567 
3568  // If the variable is found
3569  if (cmp == 0) {
3570 
3571  // Do the substitution and canonise
3572  result = canonThm(substitutivityRule(rowRightSide[term_i], 1, eq));
3573  // Do the substitution and canonise in the sum
3574  result = canonThm(substitutivityRule(rowRightSide, term_i, result));
3575  // Do the substitution
3576  result = substitutivityRule(rowExpr, 1, result);
3577 
3578  // Get the new expression
3579  const Expr& newRowRightSide = result.getRHS()[1];
3580  // Update the dependencies of the varriables in the expression
3581  updateDependencies(rowRightSide, newRowRightSide, leftSide, var);
3582 
3583  // That's it, remember the new row
3584  (*row).second = iffMP((*row).second, result);
3585 
3586  // Variables don't repeat, we can just break out
3587  break;
3588  } else if (cmp > 0)
3589  left = term_i + 1;
3590  else
3591  right = term_i - 1;
3592  }
3593  }
3594 
3595  // Now nobody depends on var anymore, just erase it
3596  dependent.clear();
3597  }
3598 }
3599 
3601 
3602  Theorem result; // The theorem explaining the result
3603 
3604  // Get the expression
3605  const Expr& eqExpr = eq.getExpr();
3606  const Expr& right_side = eqExpr[1];
3607  const Expr& left_side = eqExpr[0];
3608 
3609  // Trace if askedTheorem canonLeft = d_rules->canonMult(thm.getExpr()[0]);
3610 
3611  TRACE("simplex", "TheoryArithNew::pivotRule(", eqExpr.toString() + ", ", var.toString() + ")");
3612 
3613  // Eq must be an equation with the sum on the left side and a leaf on the right side (variable)
3614  DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::pivotRule, expected an equality : " + eqExpr.toString());
3615  DebugAssert(right_side.getKind() == PLUS, "TheoryArithNew::pivotRule, expected a sum on the left-hand side : " + eqExpr.toString());
3616  DebugAssert(isLeaf(left_side), "TheoryArithNew::pivotRule, expected a leaf (variable) on the right-hand side : " + eqExpr.toString());
3617 
3618  // Find the term of var in the left-hand side of eq
3619  int term_i_end = right_side.arity();
3620  for(int term_i = 0; term_i < term_i_end; ++ term_i)
3621  // If found do the stuff
3622  if (right_side[term_i][1] == var) {
3623 
3624  // This is the term we need and the rational we need
3625  const Expr& termExpr = right_side[term_i];
3626  const Expr& termVar = termExpr[1];
3627  const Rational& termRat = termExpr[0].getRational();
3628 
3629  // Construct the expression we will add to the equality
3630  const Expr& minusTermExpr = multExpr(rat(-termRat), termVar);
3631  const Expr& minusVarExpr = multExpr(rat(-1), left_side);
3632 
3633  // Add the above expressions to the to the equality
3634  result = iffMP(eq, d_rules->plusPredicate(left_side, right_side, plusExpr(minusTermExpr, minusVarExpr), EQ));
3635  // Canonise the right-hand side
3636  result = transitivityRule(result, canon(result.getExpr()[1]));
3637  // Canonise the left-hand side
3638  result = transitivityRule(symmetryRule(canon(result.getExpr()[0])), result);
3639  // Multiply by the inverse of the rational constant (negated and ^-1)
3640  result = iffMP(result, d_rules->multEqn(result.getExpr()[0], result.getExpr()[1], rat(-1/termRat)));
3641  // Canonise the left-hand side
3642  result = transitivityRule(result, canon(result.getExpr()[1]));
3643  // Canonise the right=hand side
3644  result = transitivityRule(symmetryRule(canon(result.getExpr()[0])), result);
3645  // Rewrite 1*x => x in the left-hand side
3646  result = transitivityRule(symmetryRule(d_rules->oneElimination(result.getExpr()[0])), result);
3647 
3648  // Trace the result
3649  TRACE("simplex", "TheoryArithNew::pivotRule ==> ", result.getExpr().toString(), "");
3650 
3651  // We are done, there is just one variable there
3652  return result;
3653  }
3654 
3655  // If not found, there is something wrong
3656  DebugAssert(false, "TheoryArithNew::pivotRule, " + var.toString() + " does not occur in " + eqExpr.toString());
3657 
3658  // Dummy return
3659  return result;
3660 }
3661 
3663 
3664  vector<Theorem> upperBounds; // Vector of the upper-bound theorems
3665 
3666  // Get the tableaux theorem explaining the leftside = var
3667  Theorem tableauxTheorem = (*var_it).second;
3668 
3669  // Get the variable on the right side
3670  const Expr& var = (*var_it).first;
3671 
3672  // Get the expression involved (leftSide = var)
3673  const Expr& rightSide = tableauxTheorem.getExpr()[1];
3674 
3675  // Go through the left side and pick up the apropriate lower and upper bounds
3676  int leftSide_i_end = rightSide.arity();
3677  for(int leftSide_i = 0; leftSide_i < leftSide_i_end; ++ leftSide_i) {
3678 
3679  // Get the rational
3680  const Expr& a = rightSide[leftSide_i][0];
3681 
3682  // Get the variable
3683  const Expr& x = rightSide[leftSide_i][1];
3684 
3685  // The positive ones make up the upper bounds (x < u => a * x < a * u)
3686  if (a.getRational() > 0) {
3687  // Get the upper bound x < u
3688  Theorem thm = getUpperBoundThm(x);
3689 
3690  // Multiply if by a ==> u_i * a > x * a
3691  thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
3692 
3693  // Canonise the left and the right side
3694  Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
3695  Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
3696 
3697  // Substitute the canonised to the inequality
3698  thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
3699 
3700  // Add the bound to the vector of upper bounds (|- c_x > a * x)
3701  upperBounds.push_back(thm);
3702  }
3703  // The negative ones make up the lower bounds (x > l => a * x < a * l)
3704  else {
3705  // Get the lower bound l < x
3706  Theorem thm = getLowerBoundThm(x);
3707 
3708  // Multiply if by a |- l * a < x * a
3709  thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
3710 
3711  // Canonise the left and the right side
3712  Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
3713  Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
3714 
3715  // Substitute the canonised to the inequality
3716  thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
3717 
3718  // Add the bound to the vector of upper bounds (|- c_x > a * x)
3719  upperBounds.push_back(thm);
3720  }
3721  }
3722 
3723  // Add up all the inequalities to get a C = \sum c_i > rightSide
3724  Theorem sumInequalities = upperBounds[0];
3725  for(unsigned int i = 1; i < upperBounds.size(); i ++) {
3726  // Add the inequalities
3727  sumInequalities = d_rules->addInequalities(sumInequalities, upperBounds[i]);
3728 
3729  // Canonise the left and the right side
3730  Theorem canonLeft = d_rules->canonPlus(sumInequalities.getExpr()[0]);
3731  Theorem canonRight = d_rules->canonPlus(sumInequalities.getExpr()[1]);
3732 
3733  // Substitute the canonised to the inequality
3734  sumInequalities = iffMP(sumInequalities, substitutivityRule(sumInequalities.getExpr(), canonLeft, canonRight));
3735  }
3736 
3737  // Substitute to get C > rightSide ==> C > var
3738  Theorem varUpperBound = substitutivityRule(sumInequalities.getExpr(), 1, symmetryRule(tableauxTheorem));
3739  // MP to get C > var
3740  varUpperBound = iffMP(sumInequalities, varUpperBound);
3741 
3742  // Get the lower bound on the rigth side variable (l_var < var)
3743  Theorem varLowerBound = getLowerBoundThm(var);
3744 
3745  // Return the clashing bound theorem
3746  return d_rules->clashingBounds(varLowerBound, varUpperBound);
3747 }
3748 
3750 
3751  vector<Theorem> lowerBounds; // Vector of the upper-bound theorems
3752 
3753  // Get the tableaux theorem explaining the leftside = var
3754  Theorem tableauxTheorem = (*var_it).second;
3755 
3756  // Get the variable on the right side
3757  const Expr& var = (*var_it).first;
3758 
3759  // Get the expression involved (var = rightSide)
3760  const Expr& rightSide = tableauxTheorem.getExpr()[1];
3761 
3762  // Trace if requested
3763  TRACE("explanations", "Generating explanation for the tableaux row ", tableauxTheorem.getExpr(), "");
3764 
3765  // Go through the right side and pick up the apropriate lower and upper bounds
3766  int rightSide_i_end = rightSide.arity();
3767  for(int rightSide_i = 0; rightSide_i < rightSide_i_end; ++ rightSide_i) {
3768 
3769  // Get the rational
3770  const Expr& a = rightSide[rightSide_i][0];
3771 
3772  // Get the variable
3773  const Expr& x = rightSide[rightSide_i][1];
3774 
3775  // The positive ones make up the lower bounds (x > l => a * x > a * l)
3776  if (a.getRational() > 0) {
3777  // Get the lower bound l < x
3778  Theorem thm = getLowerBoundThm(x);
3779  TRACE("explanations", "Got ", thm.getExpr(), "");
3780 
3781  // Multiply if by a ==> l * a < x * a
3782  thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
3783  TRACE("explanations", "Got ", thm.getExpr(), "");
3784 
3785  // Canonise the left and the right side
3786  Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
3787  Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
3788 
3789  // Substitute the canonised to the inequality
3790  thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
3791  TRACE("explanations", "Got ", thm.getExpr(), "");
3792 
3793  // Add the bound to the vector of upper bounds (|- c_x < a * x)
3794  lowerBounds.push_back(thm);
3795  }
3796  // The negative ones make up the upper bounds (x < u => a * x > a * u)
3797  else {
3798  // Get the upper bound u > x
3799  Theorem thm = getUpperBoundThm(x);
3800  TRACE("explanations", "Got ", thm.getExpr(), "");
3801 
3802  // Multiply it by a |- u * a > x * a
3803  thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
3804  TRACE("explanations", "Got ", thm.getExpr(), "");
3805 
3806  // Canonise the left and the right side
3807  Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
3808  Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
3809 
3810  // Substitute the canonised to the inequality
3811  thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
3812  TRACE("explanations", "Got ", thm.getExpr(), "");
3813 
3814  // Add the bound to the vector of upper bounds (|- c_x < a * x)
3815  lowerBounds.push_back(thm);
3816  }
3817  }
3818 
3819  // Add up all the inequalities to get a \sum c_i = C > rightSide
3820  Theorem sumInequalities = lowerBounds[0];
3821  for(unsigned int i = 1; i < lowerBounds.size(); i ++) {
3822  // Add the inequalities
3823  sumInequalities = d_rules->addInequalities(sumInequalities, lowerBounds[i]);
3824 
3825  TRACE("explanations", "Got sum ", sumInequalities.getExpr(), "");
3826 
3827  // Canonise the left and the right side
3828  Theorem canonLeft = d_rules->canonPlus(sumInequalities.getExpr()[0]);
3829  Theorem canonRight = d_rules->canonPlus(sumInequalities.getExpr()[1]);
3830 
3831  // Substitute the canonised to the inequality
3832  sumInequalities = iffMP(sumInequalities, substitutivityRule(sumInequalities.getExpr(), canonLeft, canonRight));
3833  }
3834 
3835  // Trace if requested
3836  TRACE("explanations", "Got sum ", sumInequalities.getExpr(), "");
3837 
3838  // Substitute to get C < leftSide ==> C < var
3839  Theorem varLowerBound = substitutivityRule(sumInequalities.getExpr(), 1, symmetryRule(tableauxTheorem));
3840 
3841  // MP to get C < var
3842  varLowerBound = iffMP(sumInequalities, varLowerBound);
3843 
3844  // Trace if requested
3845  TRACE("explanations", "Got lower bound ", varLowerBound.getExpr(), "");
3846 
3847  // Get the lower bound on the rigth side variable (var > l_var)
3848  Theorem varUpperBound = getUpperBoundThm(var);
3849 
3850  // Trace if requested
3851  TRACE("explanations", "Got upper bound ", varUpperBound.getExpr(), "");
3852 
3853  TRACE("explanations", "The var value (", var, ")" + getBeta(var).toString());
3854 
3855  // Return the clashing bound theorem
3856  return d_rules->clashingBounds(varLowerBound, varUpperBound);
3857 }
3858 
3860 
3861  unsigned int size = assertedExpr.size();
3862  unsigned int i;
3863 
3864  for (i = assertedExprCount; i < size; ++ i)
3865  //Update the value
3866  updateValue(assertedExpr[i][0], assertedExpr[i][1]);
3867 
3868  // Update the asserted count to be the size of the vector
3869  assertedExprCount = i;
3870 
3871 }
3872 
3873 void TheoryArithNew::updateDependenciesAdd(const Expr& var, const Expr& sum) {
3874 
3875  // Trace it
3876  TRACE("tableaux_dep", "updateDependenciesAdd(", var.toString() + ", ", sum.toString() + ")");
3877 
3878  // Go through the sum and add var to the dependencies of that term variable
3879  Expr::iterator term = sum.begin();
3880  Expr::iterator term_end = sum.end();
3881  for(; term != term_end; term ++)
3882  dependenciesMap[(*term)[1]].insert(var);
3883 
3884 }
3885 
3887 
3888  // Trace it
3889  TRACE("tableaux_dep", "updateDependenciesRemove(", var.toString() + ", ", sum.toString() + ")");
3890 
3891  // Go through the sum and remove var to the dependencies of that term variable
3892  Expr::iterator term = sum.begin();
3893  Expr::iterator term_end = sum.end();
3894  for(; term != term_end; term ++)
3895  dependenciesMap[(*term)[1]].erase(var);
3896 
3897 }
3898 
3899 void TheoryArithNew::updateDependencies(const Expr& oldSum, const Expr& newSum, const Expr& dependentVar, const Expr& skipVar) {
3900 
3901  // Trace it
3902  TRACE("tableaux_dep", "updateDependencies(", oldSum.toString() + ", " + newSum.toString() + ", " + dependentVar.toString(), ")");
3903 
3904  // Since the sums are ordered by variables, we can just to a "merge sort"
3905  int oldSum_i = 0, newSum_i = 0;
3906  int oldSum_end = oldSum.arity(), newSum_end = newSum.arity();
3907  // Get the first variables
3908  while (oldSum_i < oldSum_end && newSum_i < newSum_end) {
3909 
3910  // Get the variable references
3911  const Expr oldVar = oldSum[oldSum_i][1];
3912  const Expr newVar = newSum[newSum_i][1];
3913 
3914  // If variables equal, just skip, everything is ok
3915  if (oldVar == newVar) {
3916  ++ oldSum_i; ++ newSum_i; continue;
3917  }
3918 
3919  // Otherwise do the work with the smaller one
3920  if (oldVar > newVar) {
3921  // Old variable has dissapeared, remove dependent from its list
3922  if (oldVar != skipVar)
3923  dependenciesMap[oldVar].erase(dependentVar);
3924  // Move the old variable forward
3925  ++ oldSum_i;
3926  } else {
3927  // New variable has appeared, insert dependent to its list
3928  if (newVar != skipVar)
3929  dependenciesMap[newVar].insert(dependentVar);
3930  // Move the new variable forward
3931  ++ newSum_i;
3932  }
3933  }
3934 
3935  // If there is leftovers in the old sum, just do the removals
3936  while (oldSum_i < oldSum_end) {
3937  // Get the var, and increase the index
3938  const Expr& var = oldSum[oldSum_i ++][1];
3939  // Update the dependency
3940  if (var != skipVar)
3941  dependenciesMap[var].erase(dependentVar);
3942  }
3943 
3944  while (newSum_i < newSum_end) {
3945  // Get the var, and increase the index
3946  const Expr& var = newSum[newSum_i ++][1];
3947  // Update the dependency
3948  if (var != skipVar)
3949  dependenciesMap[var].insert(dependentVar);
3950  }
3951 }
3952 
3954 
3955  // Trace it
3956  TRACE("propagate_arith", "registerAtom(", e.toString(), ")");
3957  TRACE("arith_atoms", "", e.toString(), "");
3958 
3959  // If it is a atomic formula, add it to the map
3960  if (e.isAbsAtomicFormula()) {
3961  Expr rightSide = e[1];
3962  int kind = e.getKind();
3963  Rational leftSide = e[0].getRational();
3964 
3965  // The eps bound we'll be using
3966  EpsRational bound;
3967 
3968  // Depending on the type of the inequality define the bound
3969  switch (kind) {
3970  case LT:
3971  bound = EpsRational(leftSide, +1);
3972  break;
3973  case LE:
3974  bound = leftSide;
3975  break;
3976  case GT:
3977  bound = EpsRational(leftSide, -1);
3978  break;
3979  case GE:
3980  bound = leftSide;
3981  break;
3982  default:
3983  // How did we get here
3984  FatalAssert(false, "TheoryArithNew::registerAtom: control should not reach here" + e.toString());
3985  }
3986 
3987  // Bound has been set, now add the
3988  allBounds.insert(ExprBoundInfo(bound, e));
3989  }
3990 
3991 // // Printout the current set of atoms in the set
3992 // cout << "ALL BOUNDS:" << endl;
3993 // BoundInfoSet::iterator it = allBounds.begin();
3994 // while (it != allBounds.end()) {
3995 // cout << (*it).e << endl;
3996 // ++ it;
3997 // }
3998 }
3999 
4000 void TheoryArithNew::propagateTheory(const Expr& assertExpr, const EpsRational& bound, const EpsRational& oldBound) {
4001 
4002  // Trace it
4003  TRACE("propagate_arith", "propagateTheory(", assertExpr.toString() + ", " + bound.toString(), ")");
4004 
4005  // Make the bound info object, so that we can search for it
4006  ExprBoundInfo boundInfo(bound, assertExpr);
4007 
4008  // Get the exression on the right side hand
4009  Expr rightSide = assertExpr[1];
4010 
4011  // Get the kid of the disequality
4012  int kind = assertExpr.getKind();
4013 
4014  // Check wheather the kind is one of LT, LE, GT, GE
4015  DebugAssert(kind == LT || kind == LE || kind == GT || kind == GE , "TheoryArithNew::propagateTheory : expected an inequality");
4016 
4017  // If the bound is of the type LT or LE we go up
4018  if (kind == LT || kind == LE) {
4019  // Find the asserted fact in the set (it must be there)
4020  BoundInfoSet::iterator find = allBounds.lower_bound(boundInfo);
4021  BoundInfoSet::iterator find_end = allBounds.lower_bound(ExprBoundInfo(oldBound, assertExpr));
4022 
4023  // If we are at the begining, or not found, just exit
4024  if (find == find_end) return;
4025 
4026  // Now, go up until reached wrong right side (skip the first one, its the same as given)
4027  while (find != find_end) {
4028 
4029  // Go up;
4030  -- find;
4031 
4032  // Get the theorem of the find
4033  const Expr& findExpr = (*find).e;
4034 
4035  // Get the bound of the find
4036  const EpsRational findRat = (*find).bound;
4037 
4038  // Get the kind of the expression in the theorem
4039  int findExprKind = findExpr.getKind();
4040 
4041  // Check if the right sides are the same
4042  if (rightSide != findExpr[1]) break;
4043 
4044  // Construct the theorem object
4045  Theorem lemma;
4046 
4047  // Check the type and equeue the lemma
4048  if (findExprKind == LT || findExprKind == LE)
4049  // Imply the weaker inequality
4050  lemma = d_rules->implyWeakerInequality(assertExpr, findExpr);
4051  else
4052  // Imply the negation of the impossible inequality
4053  lemma = d_rules->implyNegatedInequality(assertExpr, findExpr);
4054 
4055 
4056  TRACE("propagate_arith", "lemma ==>", lemma.toString(), "");
4057  TRACE("arith_atoms", "Propagate: ", lemma.getExpr().toString(), "");
4058 
4059  // Put it across
4060  enqueueFact(lemma);
4061  }
4062  }
4063  // If the bound is of the type GT or GE we go down
4064  else {
4065  // Find the asserted fact in the set (it must be there)
4066  BoundInfoSet::iterator find = allBounds.upper_bound(boundInfo);
4067  BoundInfoSet::iterator find_end = allBounds.upper_bound(ExprBoundInfo(oldBound, assertExpr));
4068 
4069  // Now, go down until reached wrong right side (skip the first one, its the same as given)
4070  while (find != find_end) {
4071 
4072  // Get the bound of the find
4073  const EpsRational findRat = (*find).bound;
4074 
4075  // Get the expression in the theorem
4076  const Expr& findExpr = (*find).e;
4077  int findExprKind = findExpr.getKind();
4078 
4079  // Check if the right sides are the same
4080  if (rightSide != findExpr[1]) break;
4081 
4082  // Construct the theorem object
4083  Theorem lemma;
4084 
4085  // Check the type and equeue the lemma
4086  if (findExprKind == GT || findExprKind == GE)
4087  // Imply the weaker inequality
4088  lemma = d_rules->implyWeakerInequality(assertExpr, findExpr);
4089  else
4090  // Imply the negation of the impossible inequality (use oposite than above)
4091  lemma = d_rules->implyNegatedInequality(assertExpr, findExpr);
4092 
4093  TRACE("propagate_arith", "lemma ==>", lemma.toString(), "");
4094  TRACE("arith_atoms", "Propagate: ", lemma.getExpr().toString(), "");
4095 
4096  // Put it across
4097  enqueueFact(lemma);
4098 
4099  // Go to the next one
4100  ++ find;
4101  }
4102  }
4103 }
4104 
4106 
4107  Theorem res;
4108 
4109  // CHECK IF APPLICABLE
4110  DebugAssert(isBasic(x_i), "TheoryArithNew::deriveGomoryCut variable must be a basic variable : " + x_i.toString());
4111  DebugAssert(intVariables.count(x_i) > 0, "TheoryArithNew::deriveGomoryCut variable must be a basic variable : " + x_i.toString());
4112 
4113  // Get the rational value of x_i
4114  Rational x_i_Value = getBeta(x_i).getRational();
4115 
4116  // Compute f_0
4117  Rational f_0 = x_i_Value - floor(x_i_Value);
4118 
4119  return res;
4120 }
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
virtual Theorem eqToIneq(const Expr &e)=0
x = y ==> x <= y and x >= y
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
virtual Theorem implyNegatedInequality(const Expr &expr1, const Expr &expr2)=0
iterator begin() const
Begin iterator.
Definition: expr.h:1211
bool isEq() const
Definition: expr.h:419
EpsRational getLowerBound(const Expr &x) const
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
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
Definition: theory.cpp:557
_hash_table::iterator iterator
Definition: hash_map.h:106
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
Data structure of expressions in CVC3.
Definition: expr.h:133
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
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
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
void updateValue(const Expr &var, const Expr &e)
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
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
size_type size() const
Definition: hash_map.h:227
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
Definition: theory.cpp:103
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
QueryResult
Definition: queryresult.h:32
bool isRational() const
Definition: expr.h:431
Rational getNumerator() const
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
ostream & operator<<(ostream &os, const TheoryArithNew::Ineq &ineq)
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
int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
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
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
virtual Theorem canonMultTermConst(const Expr &c, const Expr &t)=0
t*c ==> c*t, takes constant c and term t
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
const FreeConst & getConst() const
Get the max/min constant.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool isLE(const Expr &e)
Definition: theory_arith.h:187
bool isFalse() const
Definition: expr.h:355
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
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
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
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
SMT-LIB v2 format.
Definition: lang.h:52
static T min(T x, T y)
iterator begin()
Definition: expr_map.h:190
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
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.
const Rational & findCoefficient(const Expr &var, const Expr &expr)
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 {=,<,<=,>,>=}
void registerAtom(const Expr &e)
_hash_table::const_iterator const_iterator
Definition: hash_map.h:107
static const EpsRational MinusInfinity
std::string toString(int base=10) const
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Theorem pivotRule(const Theorem &eq, const Expr &var)
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Definition: expr.h:398
Expr gtExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:225
#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
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
virtual Theorem clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)=0
bool hasFind() const
Definition: expr.h:1232
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
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.
ArithProofRules * d_rules
Rational getTableauxEntry(const Expr &x_i, const Expr &x_j)
virtual Theorem plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind)=0
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
virtual Theorem dummyTheorem(const Expr &e)=0
bool isIntx(const Expr &e, const Rational &x)
bool isPlus(const Expr &e)
Definition: theory_arith.h:181
CDMap< Expr, BoundInfo > lowerBound
QueryResult assertEqual(const Expr &x_i, const EpsRational &c, const Theorem &thm)
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
std::string tableauxAsString() const
iterator find(const key_type &key)
operations
Definition: hash_map.h:171
Expr andExpr(const Expr &right) const
Definition: expr.h:941
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void computeType(const Expr &e)
Compute and store the type of e.
bool isRational(const Expr &e)
Definition: theory_arith.h:177
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
ArithProofRules * createProofRules()
size_type erase(const key_type &key)
Definition: hash_map.h:197
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
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
std::vector< Expr > assertedExpr
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.
void propagateTheory(const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound)
CDMap< Expr, BoundInfo > upperBound
static const EpsRational Zero
void addSharedTerm(const Expr &e)
Theorem substAndCanonizeModTableaux(const Theorem &eq)
virtual Theorem skolemizeRewrite(const Expr &e)=0
Definition: kinds.h:44
CDList< Theorem > d_diseq
bool empty() const
Definition: expr_map.h:170
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
virtual Theorem rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)=0
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
CDMap< Expr, EpsRational > beta
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
bool isInteger() const
std::string toString() const
Definition: theorem.h:404
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
Definition: theory.cpp:569
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
void substAndCanonizeTableaux(const Theorem &eq)
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
DependenciesMap dependenciesMap
std::set< Expr > intVariables
static int left(int i)
Definition: minisat_heap.h:53
iterator begin()
iterators
Definition: hash_map.h:246
virtual Theorem multIneqn(const Expr &e, const Expr &z)=0
Multiplying inequation by a non-zero constant.
CDList< Theorem > d_buffer
Buffer of input inequalities.
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
Private class for an inequality in the Fourier-Motzkin database.
const Rational & getConst() const
Theorem normalize(const Expr &e, NormalizationType type=NORMALIZE_GCD)
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
CDO< bool > d_inModelCreation
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
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
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
QueryResult assertLower(const Expr &x_i, const EpsRational &c, const Theorem &thm)
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
std::pair< iterator, bool > insert(const value_type &entry)
Definition: hash_map.h:190
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
Expr computeNormalFactor(const Expr &rhs, NormalizationType type=NORMALIZE_GCD)
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
Theorem getVariableIntroThm(const Expr &leftSide)
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
#define IF_DEBUG(code)
Definition: debug.h:406
const Expr & trueExpr()
Return TRUE Expr.
Definition: theory.h:582
Theorem rafineIntegerConstraints(const Theorem &thm)
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)
Theorem getUpperBoundThm(const Expr &x) const
void checkType(const Expr &e)
Check that e is a valid Type expr.
unsigned int getUnsigned() const
unsigned size() const
Definition: cdlist.h:64
bool isIntegerConst(const Expr &e)
Definition: theory_arith.h:178
Expr getExpr() const
Definition: theorem.cpp:230
virtual Theorem oneElimination(const Expr &x)=0
bool isNull() const
Definition: theorem.h:164
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 ...
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
bool isIneq(const Expr &e)
Definition: theory_arith.h:192
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
static const EpsRational PlusInfinity
virtual Theorem addInequalities(const Theorem &thm1, const Theorem &thm2)=0
EpsRational getBeta(const Expr &x)
const Theorem & ineq() const
Get the inequality.
CDO< size_t > d_bufferIdx
Buffer index of the next unprocessed inequality.
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
Theorem solve(const Theorem &e)
An optional solver.
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
CDO< QueryResult > consistent
void pivotAndUpdate(const Expr &x_i, const Expr &x_j, const EpsRational &v)
std::set< Expr > unsatBasicVariables
Theorem getLowerBoundThm(const Expr &x) const
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
virtual Theorem canonMultConstConst(const Expr &c1, const Expr &c2)=0
c1*c2 ==> c', takes constant c1*c2
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
Expr rat(Rational r)
Definition: theory_arith.h:156
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.
Theorem getLowerBoundExplanation(const TebleauxMap::iterator &var_it)
An exception to be thrown by the smtlib translator.
Arithmetic proof rules.
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
bool varOnRHS() const
Flag whether var is isolated on the RHS.
bool isLT(const Expr &e)
Definition: theory_arith.h:186
EpsRational getUpperBound(const Expr &x) const
SMT-LIB format.
Definition: lang.h:34
virtual Theorem canonPlus(const Expr &e)=0
Canonize (PLUS t1 ... tn)
Expr plusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:199
virtual Theorem implyWeakerInequality(const Expr &expr1, const Expr &expr2)=0
std::string unsatAsString() const
virtual Theorem integerSplit(const Expr &intVar, const Rational &intPoint)=0
CDO< Theorem > integer_lemma
const Expr & getLHS() const
Definition: theorem.cpp:240
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
Definition: expr.h:1416
virtual Theorem varIntroRule(const Expr &e)=0
|- EXISTS x. e = x
void updateDependenciesAdd(const Expr &var, const Expr &sum)
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
Expr geExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:227
Definition: kinds.h:61
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
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
Theorem canonThm(const Theorem &thm)
Composition of canon(const Expr&) by transitivity: take e0 = e1, canonize e1 to e2, return e0 = e2.
Definition: theory_arith.h:120
bool empty() const
Definition: hash_map.h:222
bool isReal(Type t)
Definition: theory_arith.h:173
Theorem getUpperBoundExplanation(const TebleauxMap::iterator &var_it)
Theorem canon(const Expr &e)
Canonize the expression e, assuming all children are canonical.
Expr uminusExpr(const Expr &child)
Definition: theory_arith.h:197
Definition: kinds.h:99
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Theorem deriveGomoryCut(const Expr &x_i)
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
void updateDependencies(const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar)
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
CDO< unsigned int > assertedExprCount
bool isMult(const Expr &e)
Definition: theory_arith.h:183
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
void assignVariables(std::vector< Expr > &v)
void pivot(const Expr &x_r, const Expr &x_s)
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
void refineCounterExample()
Process disequalities from the arrangement for model generation.
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
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isBasic(const Expr &x) const
QueryResult assertUpper(const Expr &x_i, const EpsRational &c, const Theorem &thm)
for output into Simplify format
Definition: lang.h:43
Theorem canonPredEquiv(const Theorem &thm)
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()
Definition: hash_map.h:257
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421
void updateDependenciesRemove(const Expr &var, const Expr &sum)