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