00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "theory_arith_new.h"
00023 #include "arith_proof_rules.h"
00024
00025 #include "arith_exception.h"
00026 #include "typecheck_exception.h"
00027 #include "eval_exception.h"
00028 #include "parser_exception.h"
00029 #include "smtlib_exception.h"
00030 #include "theory_core.h"
00031 #include "command_line_flags.h"
00032
00033
00034 using namespace std;
00035 using namespace CVC3;
00036
00037
00038
00039
00040
00041
00042 namespace CVC3 {
00043
00044 ostream& operator<<(ostream& os, const TheoryArithNew::FreeConst& fc) {
00045 os << "FreeConst(r=" << fc.getConst() << ", "
00046 << (fc.strict()? "strict" : "non-strict") << ")";
00047 return os;
00048 }
00049
00050
00051
00052
00053
00054 ostream& operator<<(ostream& os, const TheoryArithNew::Ineq& ineq) {
00055 os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
00056 << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
00057 << ineq.getConst() << ")";
00058 return os;
00059 }
00060 }
00061
00062
00063
00064
00065
00066
00067
00068 Theorem TheoryArithNew::isIntegerThm(const Expr& e) {
00069
00070 if(isReal(e.getType())) return Theorem();
00071
00072 return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
00073 }
00074
00075
00076 Theorem TheoryArithNew::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
00077 const Expr& e = thm.getExpr();
00078
00079 if(e == isIntE) return thm;
00080
00081 Theorem res;
00082
00083 if(e.isAnd()) {
00084 int i, iend=e.arity();
00085 for(i=0; i<iend; ++i) {
00086 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
00087 if(!res.isNull()) return res;
00088 }
00089 }
00090 return res;
00091 }
00092
00093
00094 bool TheoryArithNew::kidsCanonical(const Expr& e) {
00095 if(isLeaf(e)) return true;
00096 bool res(true);
00097 for(int i=0; res && i<e.arity(); ++i) {
00098 Expr simp(canon(e[i]).getRHS());
00099 res = (e[i] == simp);
00100 IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
00101 << "\nsimplified = " << simp << endl);
00102 }
00103 return res;
00104 }
00105
00106
00107
00108
00109
00110
00111
00112
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123 Theorem TheoryArithNew::canon(const Expr& e)
00124 {
00125
00126 TRACE("arith", "canon(", e , ") {");
00127
00128
00129
00130
00131
00132 Theorem result;
00133
00134 switch (e.getKind()) {
00135
00136
00137 case UMINUS: {
00138
00139
00140 result = d_rules->uMinusToMult(e[0]);
00141
00142
00143 Expr e2 = result.getRHS();
00144
00145
00146 result = transitivityRule(result, canon(e2));
00147
00148
00149 break;
00150 }
00151
00152
00153 case PLUS:
00154
00155
00156 result = d_rules->canonPlus(e);
00157
00158
00159 break;
00160
00161
00162 case MINUS: {
00163
00164
00165 DebugAssert(e.arity() == 2," ");
00166
00167
00168 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
00169
00170
00171 Expr sum(minus_eq_sum.getRHS());
00172
00173
00174 Theorem thm(canon(sum[1]));
00175
00176
00177 if(thm.getLHS() == thm.getRHS())
00178 result = canonThm(minus_eq_sum);
00179
00180 else {
00181
00182
00183 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, 1, thm));
00184
00185
00186 result = transitivityRule(minus_eq_sum, sum_eq_canon);
00187 }
00188
00189
00190 break;
00191
00192 }
00193
00194
00195 case MULT:
00196
00197
00198 result = d_rules->canonMult(e);
00199
00200
00201 break;
00202
00203
00204 case DIVIDE: {
00205
00206
00207
00208
00209 if (e[1].getKind() == PLUS)
00210 throw ArithException("Divide by a PLUS expression not handled in" + e.toString());
00211
00212
00213 result = d_rules->canonDivide(e);
00214
00215
00216 break;
00217 }
00218
00219
00220 case POW :
00221
00222
00223 if(e[1].isRational()) result = d_rules->canonPowConst(e);
00224
00225 else result = reflexivityRule(e);
00226
00227
00228 break;
00229
00230 case RATIONAL_EXPR:
00231 result = reflexivityRule(e);
00232 break;
00233
00234 default:
00235
00236 DebugAssert(isLeaf(e), "unexpected case");
00237 result = reflexivityRule(e);
00238
00239
00240 break;
00241 }
00242
00243
00244 TRACE("arith","canon => ",result," }");
00245
00246
00247 return result;
00248 }
00249
00250 Theorem TheoryArithNew::canonSimplify(const Expr& e) {
00251
00252 TRACE("arith", "canonSimplify(", e, ") {");
00253
00254
00255
00256
00257
00258
00259
00260 Expr tmp(e);
00261
00262
00263 Theorem thm = canon(e);
00264
00265
00266 if(thm.getRHS().hasFind())
00267 thm = transitivityRule(thm, find(thm.getRHS()));
00268
00269
00270 DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()), "canonSimplify("+e.toString()+")\n"+"canon(e) = "+thm.getRHS().toString()+"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
00271
00272
00273 TRACE("arith", "canonSimplify =>", thm, " }");
00274
00275
00276 return thm;
00277 }
00278
00279
00280
00281
00282 Theorem
00283 TheoryArithNew::canonPred(const Theorem& thm) {
00284 vector<Theorem> thms;
00285 DebugAssert(thm.getExpr().arity() == 2,
00286 "TheoryArithNew::canonPred: bad theorem: "+thm.toString());
00287 Expr e(thm.getExpr());
00288 thms.push_back(canonSimplify(e[0]));
00289 thms.push_back(canonSimplify(e[1]));
00290 return iffMP(thm, substitutivityRule(e.getOp(), thms));
00291 }
00292
00293
00294
00295
00296
00297
00298
00299 Theorem TheoryArithNew::canonPredEquiv(const Theorem& thm) {
00300
00301 vector<Theorem> thms;
00302
00303
00304 DebugAssert(thm.getRHS().arity() == 2, "TheoryArithNew::canonPredEquiv: bad theorem: " + thm.toString());
00305
00306
00307 Expr e(thm.getRHS());
00308
00309
00310 DebugAssert(kidsCanonical(e[0]), "TheoryArithNew::canon("+e.toString()+")");
00311 DebugAssert(kidsCanonical(e[1]), "TheoryArithNew::canon("+e.toString()+")");
00312 thms.push_back(canon(e[0]));
00313 thms.push_back(canon(e[1]));
00314
00315
00316 return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
00317 }
00318
00319
00320
00321
00322
00323 Theorem
00324 TheoryArithNew::canonConjunctionEquiv(const Theorem& thm) {
00325 vector<Theorem> thms;
00326 return thm;
00327 }
00328
00329
00330
00331
00332
00333
00334
00335
00336
00337 Theorem TheoryArithNew::doSolve(const Theorem& thm)
00338 {
00339 const Expr& e = thm.getExpr();
00340 TRACE("arith eq","doSolve(",e,") {");
00341 DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
00342 Theorem eqnThm;
00343 vector<Theorem> thms;
00344
00345 if(e[0].isRational() && e[0].getRational() == 0)
00346 eqnThm = thm;
00347 else {
00348 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
00349 eqnThm = canonPred(eqnThm);
00350 }
00351
00352
00353 Expr right = eqnThm.getRHS();
00354
00355 if (right.isRational()) {
00356 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
00357 TRACE("arith eq","doSolve => ",result," }");
00358 return result;
00359 }
00360
00361
00362 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
00363 right = eqnThm.getRHS();
00364
00365
00366
00367 if(!isInteger(right)) {
00368 Theorem res;
00369 try {
00370 res = processRealEq(eqnThm);
00371 } catch(ArithException& e) {
00372 res = symmetryRule(eqnThm);
00373 TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
00374 IF_DEBUG(debugger.counter("FAILED to solve real equalities")++);
00375 setIncomplete("Non-linear arithmetic inequalities");
00376 }
00377 IF_DEBUG(debugger.counter("solved real equalities")++);
00378 TRACE("arith eq", "doSolve [real] => ", res, " }");
00379 return res;
00380 }
00381 else {
00382 Theorem res = processIntEq(eqnThm);
00383 IF_DEBUG(debugger.counter("solved int equalities")++);
00384 TRACE("arith eq", "doSolve [int] => ", res, " }");
00385 return res;
00386 }
00387 }
00388
00389
00390
00391
00392
00393 Expr
00394 TheoryArithNew::pickIntEqMonomial(const Expr& right)
00395 {
00396 DebugAssert(isPlus(right) && right.arity() > 2,
00397 "TheoryArithNew::pickIntEqMonomial right is wrong :-): " +
00398 right.toString());
00399 DebugAssert(right[0].isRational(),
00400 "TheoryArithNew::pickIntEqMonomial. right[0] must be const" +
00401 right.toString());
00402 DebugAssert(isInteger(right),
00403 "TheoryArithNew::pickIntEqMonomial: right is of type int: " +
00404 right.toString());
00405
00406
00407 Expr::iterator i = right.begin();
00408 i++;
00409 Rational min = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00410 Expr pickedMon = *i;
00411 for(Expr::iterator iend = right.end(); i != iend; ++i) {
00412 Rational coeff = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00413 if(min > coeff) {
00414 min = coeff;
00415 pickedMon = *i;
00416 }
00417 }
00418 return pickedMon;
00419 }
00420
00421
00422
00423
00424
00425 Theorem
00426 TheoryArithNew::processRealEq(const Theorem& eqn)
00427 {
00428 Expr right = eqn.getRHS();
00429
00430
00431
00432
00433
00434
00435
00436
00437
00438 bool found = false;
00439
00440 Expr left;
00441
00442 if (isPlus(right)) {
00443 for(int i = right.arity()-1; i>=0; --i) {
00444 Expr c = right[i];
00445 if(isRational(c))
00446 continue;
00447 if(!isInteger(c)) {
00448 if (isLeaf(c) ||
00449 ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
00450 int numoccurs = 0;
00451 Expr leaf = isLeaf(c) ? c : c[1];
00452 for (int j = 0; j < right.arity(); ++j) {
00453 if (j!= i
00454 && isLeafIn(leaf, right[j])
00455
00456 ) {
00457 numoccurs++;
00458 break;
00459 }
00460 }
00461 if (!numoccurs) {
00462 left = c;
00463 found = true;
00464 break;
00465 }
00466 }
00467 }
00468 }
00469 }
00470 else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
00471 isLeaf(right)) {
00472 left = right;
00473 found = true;
00474 }
00475
00476 if (!found) {
00477
00478
00479 throw
00480 ArithException("Can't find a leaf for solve in "+eqn.toString());
00481 }
00482
00483 Rational r = -1;
00484 if (isMult(left)) {
00485 DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
00486 DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
00487 r = -1/left[0].getRational();
00488 left = left[1];
00489 }
00490
00491 DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
00492 "TheoryArithNew::ProcessRealEq: left is integer:\n left = "
00493 +left.toString());
00494
00495
00496 Theorem result(iffMP(eqn,
00497 d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
00498 result = canonPred(result);
00499
00500
00501 result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
00502 result.getRHS(), left, EQ));
00503 result = canonPred(result);
00504 TRACE("arith","processRealEq => ",result," }");
00505 return result;
00506 }
00507
00508
00509
00510
00511
00512 Theorem
00513 TheoryArithNew::processSimpleIntEq(const Theorem& eqn)
00514 {
00515 TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
00516 DebugAssert(eqn.isRewrite(),
00517 "TheoryArithNew::processSimpleIntEq: eqn must be equality" +
00518 eqn.getExpr().toString());
00519
00520 Expr right = eqn.getRHS();
00521
00522 DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
00523 "TheoryArithNew::processSimpleIntEq: LHS must be 0:\n" +
00524 eqn.getExpr().toString());
00525
00526
00527 if(isMult(right)) {
00528
00529 Expr c,x;
00530 separateMonomial(right, c, x);
00531 Theorem isIntx(isIntegerThm(x));
00532 DebugAssert(!isIntx.isNull(), "right = "+right.toString());
00533 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00534 TRACE("arith eq", "processSimpleIntEq[0 = a*x] => ", res, " }");
00535 return res;
00536 } else if(isPlus(right)) {
00537 if(2 == right.arity()) {
00538
00539 Expr c,x;
00540 separateMonomial(right[1], c, x);
00541 Theorem isIntx(isIntegerThm(x));
00542 DebugAssert(!isIntx.isNull(), "right = "+right.toString()
00543 +"\n x = "+x.toString());
00544 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00545 TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
00546 return res;
00547 }
00548 DebugAssert(right.arity() > 2,
00549 "TheoryArithNew::processSimpleIntEq: RHS is not in correct form:"
00550 +eqn.getExpr().toString());
00551
00552 Expr isolated = pickIntEqMonomial(right);
00553 TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
00554
00555
00556
00557
00558
00559 Rational r = isMult(isolated) ?
00560 ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
00561 Theorem result;
00562 if (-1 == r) {
00563
00564
00565 result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
00566 result = canonPred(result);
00567 Expr e = result.getRHS();
00568
00569
00570 result = iffMP(result,
00571 d_rules->plusPredicate(result.getLHS(),result.getRHS(),
00572 isolated, EQ));
00573 } else {
00574
00575 const Rational& minusa = isolated[0].getRational();
00576 Rational a = -1*minusa;
00577 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
00578
00579
00580 result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
00581 right,isolated,EQ));
00582 }
00583
00584 result = canonPred(result);
00585
00586
00587 if(!isMult(isolated) || isolated[0].getRational() == 1) {
00588 TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
00589 return result;
00590 } else {
00591 DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
00592 "TheoryArithNew::processSimpleIntEq: isolated must be mult "
00593 "with coeff >= 2.\n isolated = " + isolated.toString());
00594
00595
00596 Expr lhs = result.getLHS();
00597 Expr rhs = result.getRHS();
00598 Expr a, x;
00599 separateMonomial(lhs, a, x);
00600 Theorem isIntLHS = isIntegerThm(x);
00601 vector<Theorem> isIntRHS;
00602 if(!isPlus(rhs)) {
00603 Expr c, v;
00604 separateMonomial(rhs, c, v);
00605 isIntRHS.push_back(isIntegerThm(v));
00606 DebugAssert(!isIntRHS.back().isNull(), "");
00607 } else {
00608 DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
00609 DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
00610 Expr::iterator i=rhs.begin(), iend=rhs.end();
00611 ++i;
00612 for(; i!=iend; ++i) {
00613 Expr c, v;
00614 separateMonomial(*i, c, v);
00615 isIntRHS.push_back(isIntegerThm(v));
00616 DebugAssert(!isIntRHS.back().isNull(), "");
00617 }
00618 }
00619
00620 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
00621
00622 result = getCommonRules()->skolemize(result);
00623
00624 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00625 "processSimpleIntEq: result = "+result.getExpr().toString());
00626 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
00627 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
00628 Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
00629 if(newRes.getExpr() != result.getExpr()) result = newRes;
00630
00631 TRACE("arith eq", "processSimpleIntEq => ", result, " }");
00632 return result;
00633 }
00634 } else {
00635
00636 Theorem result = symmetryRule(eqn);
00637 TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
00638 return result;
00639 }
00640 }
00641
00642
00643
00644
00645
00646
00647 Theorem
00648 TheoryArithNew::processIntEq(const Theorem& eqn)
00649 {
00650 TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
00651
00652 std::vector<Theorem> solvedAndNewEqs;
00653 Theorem newEq(eqn), result;
00654 bool done(false);
00655 do {
00656 result = processSimpleIntEq(newEq);
00657
00658 if(result.isRewrite()) {
00659 solvedAndNewEqs.push_back(result);
00660 done = true;
00661 }
00662 else if(!result.getExpr().isFalse()) {
00663 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00664 "TheoryArithNew::processIntEq("+eqn.getExpr().toString()
00665 +")\n result = "+result.getExpr().toString());
00666 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
00667 newEq = getCommonRules()->andElim(result, 1);
00668 } else
00669 done = true;
00670 } while(!done);
00671 Theorem res;
00672 if(result.getExpr().isFalse()) res = result;
00673 else res = solvedForm(solvedAndNewEqs);
00674 TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
00675 return res;
00676 }
00677
00678
00679
00680
00681
00682
00683
00684
00685
00686 Theorem
00687 TheoryArithNew::solvedForm(const vector<Theorem>& solvedEqs)
00688 {
00689 DebugAssert(solvedEqs.size() > 0, "TheoryArithNew::solvedForm()");
00690
00691
00692 TRACE_MSG("arith eq", "TheoryArithNew::solvedForm:solvedEqs(\n [");
00693 IF_DEBUG(if(debugger.trace("arith eq")) {
00694 for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
00695 jend=solvedEqs.end(); j!=jend;++j)
00696 TRACE("arith eq", "", j->getExpr(), ",\n ");
00697 });
00698 TRACE_MSG("arith eq", " ]) {");
00699
00700
00701 vector<Theorem>::const_reverse_iterator
00702 i = solvedEqs.rbegin(),
00703 iend = solvedEqs.rend();
00704
00705
00706 ExprMap<Theorem> subst;
00707 for(; i!=iend; ++i) {
00708 if(i->isRewrite()) {
00709 Theorem thm = substAndCanonize(*i, subst);
00710 TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
00711 thm.getExpr(), "");
00712 subst[i->getLHS()] = thm;
00713 }
00714 else {
00715
00716 DebugAssert(i->getExpr().isFalse(),
00717 "TheoryArithNew::solvedForm: an element of solvedEqs must "
00718 "be either EQ or FALSE: "+i->toString());
00719 return *i;
00720 }
00721 }
00722
00723
00724 vector<Theorem> thms;
00725 for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
00726 i!=iend; ++i)
00727 thms.push_back(i->second);
00728 return getCommonRules()->andIntro(thms);
00729 }
00730
00731
00732
00733
00734
00735
00736
00737
00738 Theorem
00739 TheoryArithNew::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
00740 {
00741 TRACE("arith eq", "substAndCanonize(", t, ") {");
00742
00743 if(subst.empty()) {
00744 Theorem res(reflexivityRule(t));
00745 TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
00746 return res;
00747 }
00748
00749 ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
00750 if(i!=iend) {
00751 TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
00752 return i->second;
00753 }
00754
00755 if(isLeaf(t)) {
00756 Theorem res(reflexivityRule(t));
00757 TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
00758 return res;
00759 }
00760
00761 vector<Theorem> thms;
00762 vector<unsigned> changed;
00763 for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
00764 Theorem thm = substAndCanonize(t[j], subst);
00765 if(thm.getRHS() != t[j]) {
00766 thm = canonThm(thm);
00767 thms.push_back(thm);
00768 changed.push_back(j);
00769 }
00770 }
00771
00772 Theorem res;
00773 if(thms.size() > 0) {
00774 res = substitutivityRule(t, changed, thms);
00775 res = canonThm(res);
00776 }
00777 else
00778 res = reflexivityRule(t);
00779 TRACE("arith eq", "substAndCanonize => ", res, " }");
00780 return res;
00781 }
00782
00783
00784
00785
00786
00787
00788
00789 Theorem
00790 TheoryArithNew::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
00791 {
00792
00793 if(subst.empty()) return eq;
00794
00795 DebugAssert(eq.isRewrite(), "TheoryArithNew::substAndCanonize: t = "
00796 +eq.getExpr().toString());
00797 const Expr& t = eq.getRHS();
00798
00799 Theorem thm = substAndCanonize(t, subst);
00800
00801 if(thm.getRHS() == t) return eq;
00802
00803 vector<Theorem> thms;
00804 vector<unsigned> changed;
00805 thms.push_back(thm);
00806 changed.push_back(1);
00807 return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
00808 }
00809
00810
00811 void TheoryArithNew::updateStats(const Rational& c, const Expr& v)
00812 {
00813 TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
00814 if(c > 0) {
00815 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
00816 else d_countRight[v] = 1;
00817 }
00818 else
00819 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
00820 else d_countLeft[v] = 1;
00821 }
00822
00823
00824 void TheoryArithNew::updateStats(const Expr& monomial)
00825 {
00826 Expr c, m;
00827 separateMonomial(monomial, c, m);
00828 updateStats(c.getRational(), m);
00829 }
00830
00831
00832 void TheoryArithNew::addToBuffer(const Theorem& thm) {
00833
00834
00835 Theorem result(thm);
00836 const Expr& e = thm.getExpr();
00837
00838 if(!(e[0].isRational() && e[0].getRational() == 0)) {
00839 result = iffMP(result, d_rules->rightMinusLeft(e));
00840 result = canonPred(result);
00841 }
00842 TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
00843
00844 d_buffer.push_back(thm);
00845
00846
00847 const Expr& rhs = thm.getExpr()[1];
00848 if(isPlus(rhs))
00849 for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
00850 updateStats(*i);
00851 else
00852 updateStats(rhs);
00853 }
00854
00855
00856 Expr TheoryArithNew::computeNormalFactor(const Expr& right, NormalizationType type) {
00857
00858
00859
00860 DebugAssert(isRational(right) || isPlus(right),"TheoryArithNew::computeNormalFactor: " + right.toString() + "wrong kind");
00861
00862
00863 Rational factor;
00864
00865
00866 int sign = 0;
00867
00868
00869 if(isPlus(right)) {
00870
00871
00872 vector<Rational> nums, denoms;
00873
00874
00875 for(int i = 0, iend = right.arity(); i < iend; i ++) {
00876
00877 Rational c(1);
00878
00879
00880 switch(right[i].getKind()) {
00881
00882 case RATIONAL_EXPR:
00883
00884
00885 c = abs(right[i].getRational());
00886 break;
00887
00888 case MULT:
00889
00890
00891 c = right[i][0].getRational();
00892
00893
00894 if (!sign) {
00895
00896
00897 if (type == NORMALIZE_UNIT) return rat(1/c);
00898
00899
00900 sign = (c > 0 ? 1 : -1);
00901 }
00902
00903
00904 c = abs(c);
00905
00906 break;
00907
00908 default:
00909
00910 break;
00911 }
00912
00913
00914 nums.push_back(c.getNumerator());
00915 denoms.push_back(c.getDenominator());
00916 }
00917
00918
00919 Rational gcd_nums = gcd(nums);
00920
00921
00922
00923
00924
00925 factor = (gcd_nums == 0)? 0 : (sign * lcm(denoms) / gcd_nums);
00926 } else
00927
00928 factor = 1;
00929
00930
00931 return rat(factor);
00932 }
00933
00934
00935 bool TheoryArithNew::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
00936 {
00937 DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
00938 "TheoryArithNew::findMaxVar: isolatedMonomial cannot be rational" +
00939 isolatedMonomial.toString());
00940 Expr c, var0, var1;
00941 separateMonomial(isolatedMonomial, c, var0);
00942 separateMonomial(var2, c, var1);
00943 return var0 < var1;
00944 }
00945
00946
00947 void TheoryArithNew::separateMonomial(const Expr& e, Expr& c, Expr& var) {
00948 TRACE("separateMonomial", "separateMonomial(", e, ")");
00949 DebugAssert(!isPlus(e),
00950 "TheoryArithNew::separateMonomial(e = "+e.toString()+")");
00951 if(isMult(e)) {
00952 DebugAssert(e.arity() >= 2,
00953 "TheoryArithNew::separateMonomial(e = "+e.toString()+")");
00954 c = e[0];
00955 if(e.arity() == 2) var = e[1];
00956 else {
00957 vector<Expr> kids = e.getKids();
00958 kids[0] = rat(1);
00959 var = multExpr(kids);
00960 }
00961 } else {
00962 c = rat(1);
00963 var = e;
00964 }
00965 DebugAssert(c.isRational(), "TheoryArithNew::separateMonomial(e = "
00966 +e.toString()+", c = "+c.toString()+")");
00967 DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
00968 "TheoryArithNew::separateMonomial(e = "
00969 +e.toString()+", var = "+var.toString()+")");
00970 }
00971
00972
00973
00974
00975 bool TheoryArithNew::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
00976 {
00977 d_cache.clear();
00978
00979 return dfs(e1,e2);
00980 }
00981
00982
00983 bool TheoryArithNew::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
00984 {
00985 if(e1 == e2)
00986 return true;
00987 if(d_cache.count(e2) > 0)
00988 return false;
00989 if(d_edges.count(e2) == 0)
00990 return false;
00991 d_cache[e2] = true;
00992 vector<Expr>& e2Edges = d_edges[e2];
00993 vector<Expr>::iterator i = e2Edges.begin();
00994 vector<Expr>::iterator iend = e2Edges.end();
00995
00996 for(; i != iend && !dfs(e1,*i); ++i);
00997 return (i != iend);
00998 }
00999
01000
01001 void TheoryArithNew::VarOrderGraph::selectSmallest(vector<Expr>& v1,
01002 vector<Expr>& v2)
01003 {
01004 int v1Size = v1.size();
01005 vector<bool> v3(v1Size);
01006 for(int j=0; j < v1Size; ++j)
01007 v3[j] = false;
01008
01009 for(int j=0; j < v1Size; ++j) {
01010 if(v3[j]) continue;
01011 for(int i =0; i < v1Size; ++i) {
01012 if((i == j) || v3[i])
01013 continue;
01014 if(lessThan(v1[i],v1[j])) {
01015 v3[j] = true;
01016 break;
01017 }
01018 }
01019 }
01020 vector<Expr> new_v1;
01021
01022 for(int j = 0; j < v1Size; ++j)
01023 if(!v3[j]) v2.push_back(v1[j]);
01024 else new_v1.push_back(v1[j]);
01025 v1 = new_v1;
01026 }
01027
01028
01029 void TheoryArithNew::VarOrderGraph::selectLargest(const vector<Expr>& v1,
01030 vector<Expr>& v2)
01031 {
01032 int v1Size = v1.size();
01033 vector<bool> v3(v1Size);
01034 for(int j=0; j < v1Size; ++j)
01035 v3[j] = false;
01036
01037 for(int j=0; j < v1Size; ++j) {
01038 if(v3[j]) continue;
01039 for(int i =0; i < v1Size; ++i) {
01040 if((i == j) || v3[i])
01041 continue;
01042 if(lessThan(v1[j],v1[i])) {
01043 v3[j] = true;
01044 break;
01045 }
01046 }
01047 }
01048
01049 for(int j = 0; j < v1Size; ++j)
01050 if(!v3[j]) v2.push_back(v1[j]);
01051 }
01052
01053
01054
01055
01056
01057
01058 TheoryArithNew::TheoryArithNew(TheoryCore* core)
01059 : TheoryArith(core, "ArithmeticNew"),
01060 d_diseq(core->getCM()->getCurrentContext()),
01061 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
01062 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
01063 d_freeConstDB(core->getCM()->getCurrentContext()),
01064 d_buffer(core->getCM()->getCurrentContext()),
01065
01066 d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
01067 d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
01068 d_countRight(core->getCM()->getCurrentContext()),
01069 d_countLeft(core->getCM()->getCurrentContext()),
01070 d_sharedTerms(core->getCM()->getCurrentContext()),
01071 d_sharedTermsList(core->getCM()->getCurrentContext()),
01072 d_index1(core->getCM()->getCurrentContext(), 0, 0),
01073 d_sharedVars(core->getCM()->getCurrentContext()),
01074 consistent(core->getCM()->getCurrentContext()),
01075 lowerBound(core->getCM()->getCurrentContext()),
01076 upperBound(core->getCM()->getCurrentContext()),
01077 beta(core->getCM()->getCurrentContext()),
01078 assertedExprCount(core->getCM()->getCurrentContext()),
01079 integer_lemma(core->getCM()->getCurrentContext())
01080 {
01081 IF_DEBUG(d_diseq.setName("CDList[TheoryArithNew::d_diseq]"));
01082 IF_DEBUG(d_buffer.setName("CDList[TheoryArithNew::d_buffer]"));
01083 IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArithNew::d_bufferIdx]"));
01084
01085 getEM()->newKind(REAL, "_REAL", true);
01086 getEM()->newKind(INT, "_INT", true);
01087 getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
01088
01089 getEM()->newKind(UMINUS, "_UMINUS");
01090 getEM()->newKind(PLUS, "_PLUS");
01091 getEM()->newKind(MINUS, "_MINUS");
01092 getEM()->newKind(MULT, "_MULT");
01093 getEM()->newKind(DIVIDE, "_DIVIDE");
01094 getEM()->newKind(POW, "_POW");
01095 getEM()->newKind(INTDIV, "_INTDIV");
01096 getEM()->newKind(MOD, "_MOD");
01097 getEM()->newKind(LT, "_LT");
01098 getEM()->newKind(LE, "_LE");
01099 getEM()->newKind(GT, "_GT");
01100 getEM()->newKind(GE, "_GE");
01101 getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
01102 getEM()->newKind(NEGINF, "_NEGINF");
01103 getEM()->newKind(POSINF, "_POSINF");
01104 getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
01105 getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
01106
01107 getEM()->newKind(REAL_CONST, "_REAL_CONST");
01108
01109 vector<int> kinds;
01110 kinds.push_back(REAL);
01111 kinds.push_back(INT);
01112 kinds.push_back(SUBRANGE);
01113 kinds.push_back(IS_INTEGER);
01114 kinds.push_back(UMINUS);
01115 kinds.push_back(PLUS);
01116 kinds.push_back(MINUS);
01117 kinds.push_back(MULT);
01118 kinds.push_back(DIVIDE);
01119 kinds.push_back(POW);
01120 kinds.push_back(INTDIV);
01121 kinds.push_back(MOD);
01122 kinds.push_back(LT);
01123 kinds.push_back(LE);
01124 kinds.push_back(GT);
01125 kinds.push_back(GE);
01126 kinds.push_back(RATIONAL_EXPR);
01127 kinds.push_back(NEGINF);
01128 kinds.push_back(POSINF);
01129 kinds.push_back(DARK_SHADOW);
01130 kinds.push_back(GRAY_SHADOW);
01131 kinds.push_back(REAL_CONST);
01132
01133 registerTheory(this, kinds, true);
01134
01135 d_rules = createProofRules();
01136
01137 d_realType = Type(getEM()->newLeafExpr(REAL));
01138 d_intType = Type(getEM()->newLeafExpr(INT));
01139 consistent = SATISFIABLE;
01140 assertedExprCount = 0;
01141 }
01142
01143
01144
01145 TheoryArithNew::~TheoryArithNew() {
01146 if(d_rules != NULL) delete d_rules;
01147
01148 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
01149 iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
01150 delete (i->second);
01151 free(i->second);
01152 }
01153 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
01154 iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
01155 delete (i->second);
01156 free (i->second);
01157 }
01158 }
01159
01160 void TheoryArithNew::collectVars(const Expr& e, vector<Expr>& vars,
01161 set<Expr>& cache) {
01162
01163 if(cache.count(e) > 0) return;
01164
01165 cache.insert(e);
01166 if(isLeaf(e)) vars.push_back(e);
01167 else
01168 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01169 collectVars(*i, vars, cache);
01170 }
01171
01172 void
01173 TheoryArithNew::processFiniteInterval(const Theorem& alphaLEax,
01174 const Theorem& bxLEbeta) {
01175 const Expr& ineq1(alphaLEax.getExpr());
01176 const Expr& ineq2(bxLEbeta.getExpr());
01177 DebugAssert(isLE(ineq1), "TheoryArithNew::processFiniteInterval: ineq1 = "
01178 +ineq1.toString());
01179 DebugAssert(isLE(ineq2), "TheoryArithNew::processFiniteInterval: ineq2 = "
01180 +ineq2.toString());
01181
01182 if(!isInteger(ineq1[0])
01183 || !isInteger(ineq1[1])
01184 || !isInteger(ineq2[0])
01185 || !isInteger(ineq2[1]))
01186 return;
01187
01188 const Expr& ax = ineq1[1];
01189 const Expr& bx = ineq2[0];
01190 DebugAssert(!isPlus(ax) && !isRational(ax),
01191 "TheoryArithNew::processFiniteInterval:\n ax = "+ax.toString());
01192 DebugAssert(!isPlus(bx) && !isRational(bx),
01193 "TheoryArithNew::processFiniteInterval:\n bx = "+bx.toString());
01194 Expr a = isMult(ax)? ax[0] : rat(1);
01195 Expr b = isMult(bx)? bx[0] : rat(1);
01196
01197 Theorem thm1(alphaLEax), thm2(bxLEbeta);
01198
01199 if(a != b) {
01200 thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
01201 thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
01202 }
01203
01204 const Expr& alphaLEt = thm1.getExpr();
01205 const Expr& alpha = alphaLEt[0];
01206 const Expr& t = alphaLEt[1];
01207 const Expr& beta = thm2.getExpr()[1];
01208 Expr c = canon(beta - alpha).getRHS();
01209
01210 if(c.isRational() && c.getRational() >= 1) {
01211
01212
01213
01214 Theorem bEQac = symmetryRule(canon(alpha + c));
01215
01216 vector<unsigned> changed;
01217 vector<Theorem> thms;
01218 changed.push_back(1);
01219 thms.push_back(bEQac);
01220 Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
01221 tLEac = iffMP(thm2, tLEac);
01222
01223 Theorem isInta(isIntegerThm(alpha));
01224 Theorem isIntt(isIntegerThm(t));
01225 enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
01226 }
01227 }
01228
01229
01230 void
01231 TheoryArithNew::processFiniteIntervals(const Expr& x) {
01232
01233 if(!isInteger(x)) return;
01234
01235 ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
01236 iLeft = d_inequalitiesLeftDB.find(x);
01237 if(iLeft == d_inequalitiesLeftDB.end()) return;
01238 iRight = d_inequalitiesRightDB.find(x);
01239 if(iRight == d_inequalitiesRightDB.end()) return;
01240
01241 CDList<Ineq>& ineqsLeft = *(iLeft->second);
01242 CDList<Ineq>& ineqsRight = *(iRight->second);
01243
01244 size_t sizeLeft = ineqsLeft.size();
01245 size_t sizeRight = ineqsRight.size();
01246
01247 for(size_t l=0; l<sizeLeft; ++l)
01248 for(size_t r=0; r<sizeRight; ++r)
01249 processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
01250 }
01251
01252
01253
01254
01255
01256 void
01257 TheoryArithNew::setupRec(const Expr& e) {
01258 if(e.hasFind()) return;
01259
01260 for (int k = 0; k < e.arity(); ++k) {
01261 setupRec(e[k]);
01262 }
01263
01264 e.setFind(reflexivityRule(e));
01265
01266 setup(e);
01267 }
01268
01269
01270
01271
01272
01273
01274
01275
01276
01277
01278
01279
01280
01281
01282
01283
01284
01285
01286 void TheoryArithNew::addSharedTerm(const Expr& e) {
01287 if (d_sharedTerms.count(e) > 0) return;
01288 d_sharedTerms[e] = e;
01289 d_sharedTermsList.push_back(e);
01290 e.addToNotify(this, Expr());
01291
01292
01293
01294
01295
01296
01297
01298
01299
01300
01301
01302
01303 }
01304
01305 void TheoryArithNew::refineCounterExample()
01306 {
01307 d_inModelCreation = true;
01308 TRACE("model", "refineCounterExample[TheoryArithNew] ", "", "{");
01309 CDMap<Expr, Expr>::iterator it = d_sharedTerms.begin(), it2,
01310 iend = d_sharedTerms.end();
01311
01312
01313
01314 for(; it!=iend; ++it) {
01315
01316 Expr e1 = (*it).first;
01317 for(it2 = it, ++it2; it2!=iend; ++it2) {
01318 Expr e2 = (*it2).first;
01319 DebugAssert(isReal(getBaseType(e1)),
01320 "TheoryArithNew::refineCounterExample: e1 = "+e1.toString()
01321 +"\n type(e1) = "+e1.getType().toString());
01322 if(findExpr(e1) != findExpr(e2)) {
01323 DebugAssert(isReal(getBaseType(e2)),
01324 "TheoryArithNew::refineCounterExample: e2 = "+e2.toString()
01325 +"\n type(e2) = "+e2.getType().toString());
01326 Expr eq = simplifyExpr(e1.eqExpr(e2));
01327 if (!eq.isBoolConst())
01328 addSplitter(eq);
01329 }
01330 }
01331 }
01332 TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
01333 }
01334
01335
01336 void TheoryArithNew::findRationalBound(const Expr& varSide, const Expr& ratSide,
01337 const Expr& var,
01338 Rational &r)
01339 {
01340 Expr c, x;
01341 separateMonomial(varSide, c, x);
01342
01343 DebugAssert(findExpr(c).isRational(),
01344 "seperateMonomial failed");
01345 DebugAssert(findExpr(ratSide).isRational(),
01346 "smallest variable in graph, should not have variables"
01347 " in inequalities: ");
01348 DebugAssert(x == var, "separateMonomial found different variable: "
01349 + var.toString());
01350 r = findExpr(ratSide).getRational() / findExpr(c).getRational();
01351 }
01352
01353
01354 bool TheoryArithNew::findBounds(const Expr& e, Rational& lub, Rational& glb)
01355 {
01356 bool strictLB=false, strictUB=false;
01357 bool right = (d_inequalitiesRightDB.count(e) > 0
01358 && d_inequalitiesRightDB[e]->size() > 0);
01359 bool left = (d_inequalitiesLeftDB.count(e) > 0
01360 && d_inequalitiesLeftDB[e]->size() > 0);
01361 int numRight = 0, numLeft = 0;
01362 if(right) {
01363 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
01364 for(unsigned int i=0; i<ratsLTe->size(); i++) {
01365 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
01366 Expr ineq = (*ratsLTe)[i].ineq().getExpr();
01367 Expr leftSide = ineq[0], rightSide = ineq[1];
01368 Rational r;
01369 findRationalBound(rightSide, leftSide, e , r);
01370 if(numRight==0 || r>glb){
01371 glb = r;
01372 strictLB = isLT(ineq);
01373 }
01374 numRight++;
01375 }
01376 TRACE("model", " =>Lower bound ", glb.toString(), "");
01377 }
01378 if(left) {
01379 CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
01380 for(unsigned int i=0; i<ratsGTe->size(); i++) {
01381 DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
01382 Expr ineq = (*ratsGTe)[i].ineq().getExpr();
01383 Expr leftSide = ineq[0], rightSide = ineq[1];
01384 Rational r;
01385 findRationalBound(leftSide, rightSide, e, r);
01386 if(numLeft==0 || r<lub) {
01387 lub = r;
01388 strictUB = isLT(ineq);
01389 }
01390 numLeft++;
01391 }
01392 TRACE("model", " =>Upper bound ", lub.toString(), "");
01393 }
01394 if(!left && !right) {
01395 lub = 0;
01396 glb = 0;
01397 }
01398 if(!left && right) {lub = glb +2;}
01399 if(!right && left) {glb = lub-2;}
01400 DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
01401 "than least upper bound");
01402 return strictLB;
01403 }
01404
01405
01406 void TheoryArithNew::assignVariables(std::vector<Expr>&v)
01407 {
01408 int count = 0;
01409 while (v.size() > 0) {
01410 std::vector<Expr> bottom;
01411 d_graph.selectSmallest(v, bottom);
01412 TRACE("model", "Finding variables to assign. Iteration # ", count, "");
01413 for(unsigned int i = 0; i<bottom.size(); i++) {
01414 Expr e = bottom[i];
01415 TRACE("model", "Found: ", e, "");
01416
01417 if(e.isRational()) continue;
01418
01419 Rational lub, glb;
01420 bool strictLB;
01421 strictLB = findBounds(e, lub, glb);
01422 Rational mid;
01423 if(isInteger(e)) {
01424 if(strictLB && glb.isInteger())
01425 mid = glb + 1;
01426 else
01427 mid = ceil(glb);
01428 }
01429 else
01430 mid = (lub + glb)/2;
01431 TRACE("model", "Assigning mid = ", mid, " {");
01432 assignValue(e, rat(mid));
01433 TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
01434 if(inconsistent()) return;
01435 }
01436 count++;
01437 }
01438 }
01439
01440
01441 void TheoryArithNew::computeModelBasic(const std::vector<Expr>& v)
01442 {
01443 d_inModelCreation = true;
01444 vector<Expr> reps;
01445 TRACE("model", "Arith=>computeModel ", "", "{");
01446 for(unsigned int i=0; i <v.size(); ++i) {
01447 const Expr& e = v[i];
01448 if(findExpr(e) == e) {
01449 TRACE("model", "arith variable:", e , "");
01450 reps.push_back(e);
01451 }
01452 else {
01453 TRACE("model", "arith variable:", e , "");
01454 TRACE("model", " ==> is defined by: ", findExpr(e) , "");
01455 }
01456 }
01457 assignVariables(reps);
01458 TRACE("model", "Arith=>computeModel", "", "}");
01459 d_inModelCreation = false;
01460 }
01461
01462
01463
01464
01465 void TheoryArithNew::computeModel(const Expr& e, vector<Expr>& vars) {
01466 DebugAssert(findExpr(e).isRational(), "TheoryArithNew::computeModel("
01467 +e.toString()+")\n e is not assigned concrete value.\n"
01468 +" find(e) = "+findExpr(e).toString());
01469 assignValue(simplify(e));
01470 vars.push_back(e);
01471 }
01472
01473
01474
01475
01476
01477
01478 Theorem TheoryArithNew::normalize(const Expr& e, NormalizationType type) {
01479
01480
01481
01482
01483
01484 TRACE("arith", "normalize(", e, ") {");
01485
01486
01487 DebugAssert(isIneq(e) || e.isEq(), "normalize: input must be an equality or inequality: " + e.toString());
01488
01489
01490 DebugAssert(isPlus(e[1]) || (isMult(e[1]) && e[1][0].isRational()), "normalize: right side must be a sum or a mult: " + e.toString());
01491
01492
01493 DebugAssert(e[0].isRational() && 0 == e[0].getRational(), "normalize: e[0] must be 0" + e.toString());
01494
01495
01496 Expr factor;
01497
01498 if (isMult(e[1])) factor = rat(1/e[1][0].getRational());
01499
01500 else factor = computeNormalFactor(e[1], type);
01501
01502
01503 TRACE("arith", "normalize: factor = ", factor, "");
01504
01505
01506 Theorem thm;
01507
01508
01509 if(factor.getRational() != 1)
01510 switch(e.getKind()) {
01511
01512 case EQ:
01513 thm = d_rules->multEqn(e[0], e[1], factor);
01514
01515 thm = canonPredEquiv(thm);
01516 break;
01517
01518 case LE:
01519 case LT:
01520 case GE:
01521 case GT:
01522
01523
01524 thm = d_rules->multIneqn(e, factor);
01525
01526
01527 thm = canonPredEquiv(thm);
01528
01529
01530 break;
01531
01532 default:
01533
01534
01535 FatalAssert(false, "normalize: control should not reach here" + e.toString());
01536
01537
01538 break;
01539 }
01540 else
01541
01542 thm = reflexivityRule(e);
01543
01544
01545
01546 TRACE("arith", "normalize => ", thm, " }");
01547
01548
01549 return(thm);
01550 }
01551
01552
01553 Theorem TheoryArithNew::normalize(const Theorem& eIffEqn, NormalizationType type) {
01554 return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS(), type));
01555 }
01556
01557
01558 Theorem TheoryArithNew::rafineIntegerConstraints(const Theorem& thm) {
01559
01560
01561 Theorem result = thm;
01562
01563
01564 const Expr& constr = result.getRHS();
01565
01566 if (!isIneq(constr)) return thm;
01567
01568
01569 Theorem isIntConstraintThm = isIntegerThm(constr[1]);
01570
01571
01572 if (isIntConstraintThm.isNull()) return result;
01573
01574
01575 TRACE("integer", "TheoryArithNew::rafineIntegerConstraints(", constr, ")");
01576 TRACE("integer", "TheoryArithNew::rafineIntegerConstraints: int proof:", isIntConstraintThm, "");
01577
01578
01579 Rational r = constr[0].getRational();
01580
01581
01582 if (constr.getKind() == LT || constr.getKind() == GT || !r.isInteger())
01583 result = transitivityRule(result, d_rules->rafineStrictInteger(isIntConstraintThm, constr));
01584
01585
01586 return result;
01587 }
01588
01589
01590 Theorem TheoryArithNew::rewrite(const Expr& e) {
01591
01592
01593
01594
01595
01596 TRACE("arith", "TheoryArithNew::rewrite(", e, ") {");
01597
01598
01599 Theorem thm;
01600
01601
01602 bool isNot = false;
01603
01604
01605 if (!e.isTerm()) {
01606
01607
01608 if (!e.isAbsLiteral()) {
01609
01610
01611 e.setRewriteNormal();
01612
01613
01614 thm = reflexivityRule(e);
01615
01616
01617 TRACE("arith", "TheoryArithNew::rewrite[non-literal] => ", thm, " }");
01618
01619
01620 return thm;
01621 }
01622
01623
01624 switch(e.getKind()) {
01625
01626
01627 case EQ: {
01628
01629
01630
01631
01632
01633
01634
01635
01636
01637
01638
01639
01640
01641
01642
01643
01644
01645
01646
01647 thm = reflexivityRule(e);
01648 break;
01649 }
01650
01651
01652 case NOT:
01653
01654 if (e[0].getKind() == EQ) {
01655 thm = reflexivityRule(e);
01656 break;
01657 }
01658
01659 DebugAssert(e[0].getKind() != EQ, "TheoryArithNew::rewrite, not expecting equality under negation");
01660
01661
01662 thm = d_rules->negatedInequality(e);
01663
01664
01665 isNot = true;
01666
01667 case LT:
01668 case GT:
01669 case LE:
01670 case GE:
01671
01672
01673 if (isNot)
01674 thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
01675 else
01676 thm = d_rules->rightMinusLeft(e);
01677
01678
01679 thm = canonPredEquiv(thm);
01680
01681
01682 if ((thm.getRHS())[1].isRational())
01683 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
01684 else {
01685
01686
01687 thm = normalize(thm, NORMALIZE_UNIT);
01688
01689
01690 const Expr& normalised = thm.getRHS();
01691 const Expr& rightSide = normalised[1];
01692 const Expr& leftSide = normalised[0];
01693
01694
01695 if (isPlus(rightSide)) {
01696
01697 if (rightSide[0].isRational()) {
01698
01699 thm = transitivityRule(thm, d_rules->plusPredicate(leftSide, rightSide, rat(-rightSide[0].getRational()), thm.getRHS().getKind()));
01700
01701 const Theorem& thmLeft = d_rules->canonPlus(thm.getRHS()[0]);
01702
01703 const Theorem& thmRight = d_rules->canonPlus(thm.getRHS()[1]);
01704
01705 thm = transitivityRule(thm, substitutivityRule(thm.getRHS(), thmLeft, thmRight));
01706 }
01707 }
01708 }
01709
01710
01711 thm = rafineIntegerConstraints(thm);
01712
01713
01714 break;
01715
01716 case IS_INTEGER:
01717
01718
01719 TRACE("integer", "Got ", e.toString(), "");
01720 TRACE("integer", "Type ", e[0].getType().toString(), "");
01721
01722
01723 thm = d_rules->dummyTheorem(e);
01724
01725
01726 break;
01727
01728 default:
01729
01730
01731 FatalAssert(false, "Theory_Arith::rewrite: control should not reach here");
01732
01733
01734 break;
01735
01736 }
01737
01738 } else {
01739
01740
01741 if (e.isAtomic()) thm = canon(e);
01742
01743 else thm = reflexivityRule(e);
01744 }
01745
01746
01747
01748
01749
01750 if (theoryOf(thm.getRHS()) == this)
01751 thm.getRHS().setRewriteNormal();
01752
01753
01754 TRACE("arith", "TheoryArithNew::rewrite => ", thm, " }");
01755
01756
01757 return thm;
01758 }
01759
01760
01761 void TheoryArithNew::setup(const Expr& e)
01762 {
01763
01764 if (!e.isTerm()) {
01765
01766
01767 if (e.isNot() || e.isEq()) return;
01768
01769
01770 if (isIntPred(e)) return;
01771
01772
01773 DebugAssert(isIneq(e) && e[0].isRational(), "TheoryArithNew::setup: b @ (sum t1 ... tn) :" + e.toString());
01774
01775
01776 e[1].addToNotify(this, e);
01777
01778 } else {
01779
01780
01781 int arity(e.arity());
01782
01783
01784 for (int k = 0 ; k < arity; k ++) {
01785
01786
01787 e[k].addToNotify(this, e);
01788
01789
01790 TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
01791 }
01792 }
01793 }
01794
01795
01796 void TheoryArithNew::update(const Theorem& e, const Expr& d)
01797 {
01798 if (inconsistent()) return;
01799
01800 if (d.isNull()) {
01801 DebugAssert(!e.getLHS().isRational(),
01802 "TheoryArithNew::update(e="+e.getExpr().toString()
01803 +", d="+d.toString());
01804 Expr lhs = e.getLHS();
01805 Expr rhs = e.getRHS();
01806
01807 CDMap<Expr,Expr>::iterator it = d_sharedTerms.find(lhs);
01808 DebugAssert(it != d_sharedTerms.end(), "Expected lhs to be shared");
01809 CDMap<Expr,Expr>::iterator it2 = d_sharedTerms.find(rhs);
01810 if (it2 != d_sharedTerms.end()) {
01811
01812 if ((*it).second != lhs) {
01813 lhs = (*it).second;
01814 it = d_sharedTerms.find(lhs);
01815 DebugAssert(it != d_sharedTerms.end() && (*it).second == lhs,
01816 "Invariant violated in TheoryBitvector::update");
01817 }
01818 if ((*it2).second != rhs) {
01819 rhs = (*it2).second;
01820 it2 = d_sharedTerms.find(rhs);
01821 DebugAssert(it2 != d_sharedTerms.end() && (*it2).second == rhs,
01822 "Invariant violated in TheoryBitvector::update");
01823 }
01824 DebugAssert(findExpr(lhs) == e.getRHS() &&
01825 findExpr(rhs) == e.getRHS(), "Unexpected value for finds");
01826 Theorem thm = transitivityRule(find(lhs),symmetryRule(find(rhs)));
01827 if (thm == e && theoryOf(e.getLHS()) == this) return;
01828 assertFact(thm);
01829 }
01830 else {
01831 d_sharedTerms[rhs] = (*it).second;
01832 }
01833 return;
01834 }
01835
01836 IF_DEBUG(debugger.counter("arith update total")++);
01837 if (!d.hasFind()) return;
01838 if (isIneq(d)) {
01839
01840 DebugAssert(e.getLHS() == d[1], "Mismatch");
01841 Theorem thm = find(d);
01842
01843 vector<unsigned> changed;
01844 vector<Theorem> children;
01845 changed.push_back(1);
01846 children.push_back(e);
01847 Theorem thm2 = substitutivityRule(d, changed, children);
01848 if (thm.getRHS() == trueExpr()) {
01849 enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
01850 }
01851 else {
01852 enqueueFact(getCommonRules()->iffFalseElim(
01853 transitivityRule(symmetryRule(thm2), thm)));
01854 }
01855 IF_DEBUG(debugger.counter("arith update ineq")++);
01856 }
01857 else if (find(d).getRHS() == d) {
01858
01859 Theorem thm = canonSimp(d);
01860 TRACE("arith", "TheoryArithNew::update(): thm = ", thm, "");
01861 DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
01862 +thm.getExpr().toString());
01863 assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
01864 IF_DEBUG(debugger.counter("arith update find(d)=d")++);
01865 }
01866 }
01867
01868
01869 Theorem TheoryArithNew::solve(const Theorem& thm)
01870 {
01871 DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
01872 const Expr& lhs = thm.getLHS();
01873 const Expr& rhs = thm.getRHS();
01874
01875
01876
01877
01878
01879
01880 if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
01881 && (lhs.getType() != intType() || isInteger(rhs))
01882
01883 )
01884 return thm;
01885
01886
01887 if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
01888 && (rhs.getType() != intType() || isInteger(lhs))
01889
01890 )
01891 return symmetryRule(thm);
01892
01893 return doSolve(thm);
01894 }
01895
01896
01897 void TheoryArithNew::checkAssertEqInvariant(const Theorem& e)
01898 {
01899 return;
01900 }
01901
01902
01903 void TheoryArithNew::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
01904 switch(e.getKind()) {
01905 case RATIONAL_EXPR:
01906 break;
01907 case PLUS:
01908 case MULT:
01909 case DIVIDE:
01910 case POW:
01911 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01912
01913 v.push_back(*i);
01914 break;
01915 default: {
01916 Expr e2(findExpr(e));
01917 if(e==e2) {
01918 TRACE("model", "TheoryArithNew::computeModelTerm(", e, "): a variable");
01919
01920
01921 } else {
01922 TRACE("model", "TheoryArithNew::computeModelTerm("+e.toString()
01923 +"): has find pointer to ", e2, "");
01924 v.push_back(e2);
01925 }
01926 }
01927 }
01928 }
01929
01930 Expr TheoryArithNew::computeTypePred(const Type& t, const Expr& e) {
01931 Expr tExpr = t.getExpr();
01932 switch(tExpr.getKind()) {
01933 case INT:
01934 return Expr(IS_INTEGER, e);
01935 case SUBRANGE: {
01936 std::vector<Expr> kids;
01937 kids.push_back(Expr(IS_INTEGER, e));
01938 kids.push_back(leExpr(tExpr[0], e));
01939 kids.push_back(leExpr(e, tExpr[1]));
01940 return andExpr(kids);
01941 }
01942 default:
01943 return e.getEM()->trueExpr();
01944 }
01945 }
01946
01947 void TheoryArithNew::checkType(const Expr& e)
01948 {
01949 switch (e.getKind()) {
01950 case INT:
01951 case REAL:
01952 if (e.arity() > 0) {
01953 throw Exception("Ill-formed arithmetic type: "+e.toString());
01954 }
01955 break;
01956 case SUBRANGE:
01957 if (e.arity() != 2 ||
01958 !isIntegerConst(e[0]) ||
01959 !isIntegerConst(e[1]) ||
01960 e[0].getRational() > e[1].getRational()) {
01961 throw Exception("bad SUBRANGE type expression"+e.toString());
01962 }
01963 break;
01964 default:
01965 DebugAssert(false, "Unexpected kind in TheoryArithNew::checkType"
01966 +getEM()->getKindName(e.getKind()));
01967 }
01968 }
01969
01970 void TheoryArithNew::computeType(const Expr& e)
01971 {
01972 switch (e.getKind()) {
01973 case REAL_CONST:
01974 e.setType(d_realType);
01975 break;
01976 case RATIONAL_EXPR:
01977 if(e.getRational().isInteger())
01978 e.setType(d_intType);
01979 else
01980 e.setType(d_realType);
01981 break;
01982 case UMINUS:
01983 case PLUS:
01984 case MINUS:
01985 case MULT:
01986 case POW: {
01987 bool isInt = true;
01988 for(int k = 0; k < e.arity(); ++k) {
01989 if(d_realType != getBaseType(e[k]))
01990 throw TypecheckException("Expecting type REAL with `" +
01991 getEM()->getKindName(e.getKind()) + "',\n"+
01992 "but got a " + getBaseType(e[k]).toString()+
01993 " for:\n" + e.toString());
01994 if(isInt && !isInteger(e[k]))
01995 isInt = false;
01996 }
01997 if(isInt)
01998 e.setType(d_intType);
01999 else
02000 e.setType(d_realType);
02001 break;
02002 }
02003 case DIVIDE: {
02004 Expr numerator = e[0];
02005 Expr denominator = e[1];
02006 if (getBaseType(numerator) != d_realType ||
02007 getBaseType(denominator) != d_realType) {
02008 throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
02009 "but got " + getBaseType(numerator).toString()+
02010 " and " + getBaseType(denominator).toString() +
02011 " for:\n" + e.toString());
02012 }
02013 if(denominator.isRational() && 1 == denominator.getRational())
02014 e.setType(numerator.getType());
02015 else
02016 e.setType(d_realType);
02017 break;
02018 }
02019 case LT:
02020 case LE:
02021 case GT:
02022 case GE:
02023 case GRAY_SHADOW:
02024
02025
02026
02027 case DARK_SHADOW:
02028 for (int k = 0; k < e.arity(); ++k) {
02029 if (d_realType != getBaseType(e[k]))
02030 throw TypecheckException("Expecting type REAL with `" +
02031 getEM()->getKindName(e.getKind()) + "',\n"+
02032 "but got a " + getBaseType(e[k]).toString()+
02033 " for:\n" + e.toString());
02034 }
02035
02036 e.setType(boolType());
02037 break;
02038 case IS_INTEGER:
02039 if(d_realType != getBaseType(e[0]))
02040 throw TypecheckException("Expected type REAL, but got "
02041 +getBaseType(e[0]).toString()
02042 +"\n\nExpr = "+e.toString());
02043 e.setType(boolType());
02044 break;
02045 default:
02046 DebugAssert(false,"TheoryArithNew::computeType: unexpected expression:\n "
02047 +e.toString());
02048 break;
02049 }
02050 }
02051
02052 Type TheoryArithNew::computeBaseType(const Type& t) {
02053 IF_DEBUG(int kind = t.getExpr().getKind());
02054 DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
02055 "TheoryArithNew::computeBaseType("+t.toString()+")");
02056 return realType();
02057 }
02058
02059 Expr TheoryArithNew::computeTCC(const Expr& e) {
02060 Expr tcc(Theory::computeTCC(e));
02061 switch(e.getKind()) {
02062 case DIVIDE:
02063 DebugAssert(e.arity() == 2, "");
02064 return tcc.andExpr(!(e[1].eqExpr(rat(0))));
02065 default:
02066 return tcc;
02067 }
02068 }
02069
02070
02071
02072
02073
02074 Expr TheoryArithNew::parseExprOp(const Expr& e) {
02075 TRACE("parser", "TheoryArithNew::parseExprOp(", e, ")");
02076
02077
02078
02079 switch(e.getKind()) {
02080 case ID: {
02081 int kind = getEM()->getKind(e[0].getString());
02082 switch(kind) {
02083 case NULL_KIND: return e;
02084 case REAL:
02085 case INT:
02086 case NEGINF:
02087 case POSINF: return getEM()->newLeafExpr(kind);
02088 default:
02089 DebugAssert(false, "Bad use of bare keyword: "+e.toString());
02090 return e;
02091 }
02092 }
02093 case RAW_LIST: break;
02094 default:
02095 return e;
02096 }
02097
02098 DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
02099 "TheoryArithNew::parseExprOp:\n e = "+e.toString());
02100
02101 const Expr& c1 = e[0][0];
02102 int kind = getEM()->getKind(c1.getString());
02103 switch(kind) {
02104 case UMINUS: {
02105 if(e.arity() != 2)
02106 throw ParserException("UMINUS requires exactly one argument: "
02107 +e.toString());
02108 return uminusExpr(parseExpr(e[1]));
02109 }
02110 case PLUS: {
02111 vector<Expr> k;
02112 Expr::iterator i = e.begin(), iend=e.end();
02113
02114
02115 ++i;
02116
02117 for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02118 return plusExpr(k);
02119 }
02120 case MINUS: {
02121 if(e.arity() == 2)
02122 return uminusExpr(parseExpr(e[1]));
02123 else if(e.arity() == 3)
02124 return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
02125 else
02126 throw ParserException("MINUS requires one or two arguments:"
02127 +e.toString());
02128 }
02129 case MULT: {
02130 vector<Expr> k;
02131 Expr::iterator i = e.begin(), iend=e.end();
02132
02133
02134 ++i;
02135
02136 for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02137 return multExpr(k);
02138 }
02139 case POW: {
02140 return powExpr(parseExpr(e[1]), parseExpr(e[2]));
02141 }
02142 case DIVIDE:
02143 { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
02144 case LT:
02145 { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
02146 case LE:
02147 { return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
02148 case GT:
02149 { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
02150 case GE:
02151 { return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
02152 case INTDIV:
02153 case MOD:
02154 case SUBRANGE: {
02155 vector<Expr> k;
02156 Expr::iterator i = e.begin(), iend=e.end();
02157
02158
02159 ++i;
02160
02161 for(; i!=iend; ++i)
02162 k.push_back(parseExpr(*i));
02163 return Expr(kind, k, e.getEM());
02164 }
02165 case IS_INTEGER: {
02166 if(e.arity() != 2)
02167 throw ParserException("IS_INTEGER requires exactly one argument: "
02168 +e.toString());
02169 return Expr(IS_INTEGER, parseExpr(e[1]));
02170 }
02171 default:
02172 DebugAssert(false,
02173 "TheoryArithNew::parseExprOp: invalid input " + e.toString());
02174 break;
02175 }
02176 return e;
02177 }
02178
02179
02180
02181
02182
02183
02184 ExprStream& TheoryArithNew::print(ExprStream& os, const Expr& e) {
02185 switch(os.lang()) {
02186 case SIMPLIFY_LANG:
02187 switch(e.getKind()) {
02188 case RATIONAL_EXPR:
02189 e.print(os);
02190 break;
02191 case SUBRANGE:
02192 os <<"ERROR:SUBRANGE:not supported in Simplify\n";
02193 break;
02194 case IS_INTEGER:
02195 os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
02196 break;
02197 case PLUS: {
02198 int i=0, iend=e.arity();
02199 os << "(+ ";
02200 if(i!=iend) os << e[i];
02201 ++i;
02202 for(; i!=iend; ++i) os << " " << e[i];
02203 os << ")";
02204 break;
02205 }
02206 case MINUS:
02207 os << "(- " << e[0] << " " << e[1]<< ")";
02208 break;
02209 case UMINUS:
02210 os << "-" << e[0] ;
02211 break;
02212 case MULT: {
02213 int i=0, iend=e.arity();
02214 os << "(* " ;
02215 if(i!=iend) os << e[i];
02216 ++i;
02217 for(; i!=iend; ++i) os << " " << e[i];
02218 os << ")";
02219 break;
02220 }
02221 case POW:
02222 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02223 break;
02224 case DIVIDE:
02225 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02226 break;
02227 case LT:
02228 if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02229 }
02230 os << "(< " << e[0] << " " << e[1] <<")";
02231 break;
02232 case LE:
02233 os << "(<= " << e[0] << " " << e[1] << ")";
02234 break;
02235 case GT:
02236 os << "(> " << e[0] << " " << e[1] << ")";
02237 break;
02238 case GE:
02239 os << "(>= " << e[0] << " " << e[1] << ")";
02240 break;
02241 case DARK_SHADOW:
02242 case GRAY_SHADOW:
02243 os <<"ERROR:SHADOW:not supported in Simplify\n";
02244 break;
02245 default:
02246
02247
02248 e.print(os);
02249
02250 break;
02251 }
02252 break;
02253
02254 case PRESENTATION_LANG:
02255 switch(e.getKind()) {
02256 case REAL:
02257 case INT:
02258 case RATIONAL_EXPR:
02259 case NEGINF:
02260 case POSINF:
02261 e.print(os);
02262 break;
02263 case SUBRANGE:
02264 if(e.arity() != 2) e.printAST(os);
02265 else
02266 os << "[" << push << e[0] << ".." << e[1] << push << "]";
02267 break;
02268 case IS_INTEGER:
02269 if(e.arity() == 1)
02270 os << "IS_INTEGER(" << push << e[0] << push << ")";
02271 else
02272 e.printAST(os);
02273 break;
02274 case PLUS: {
02275 int i=0, iend=e.arity();
02276 os << "(" << push;
02277 if(i!=iend) os << e[i];
02278 ++i;
02279 for(; i!=iend; ++i) os << space << "+ " << e[i];
02280 os << push << ")";
02281 break;
02282 }
02283 case MINUS:
02284 os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
02285 break;
02286 case UMINUS:
02287 os << "-(" << push << e[0] << push << ")";
02288 break;
02289 case MULT: {
02290 int i=0, iend=e.arity();
02291 os << "(" << push;
02292 if(i!=iend) os << e[i];
02293 ++i;
02294 for(; i!=iend; ++i) os << space << "* " << e[i];
02295 os << push << ")";
02296 break;
02297 }
02298 case POW:
02299 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02300 break;
02301 case DIVIDE:
02302 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02303 break;
02304 case LT:
02305 if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02306 }
02307 os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
02308 break;
02309 case LE:
02310 os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
02311 break;
02312 case GT:
02313 os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
02314 break;
02315 case GE:
02316 os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
02317 break;
02318 case DARK_SHADOW:
02319 os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
02320 break;
02321 case GRAY_SHADOW:
02322 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
02323 << "," << space << e[2] << "," << space << e[3] << push << ")";
02324 break;
02325 default:
02326
02327
02328 e.printAST(os);
02329
02330 break;
02331 }
02332 break;
02333 case SMTLIB_LANG: {
02334 switch(e.getKind()) {
02335 case REAL_CONST:
02336 printRational(os, e[0].getRational(), true);
02337 break;
02338 case RATIONAL_EXPR:
02339 printRational(os, e.getRational());
02340 break;
02341 case REAL:
02342 os << "Real";
02343 break;
02344 case INT:
02345 os << "Int";
02346 break;
02347 case SUBRANGE:
02348 throw SmtlibException("TheoryArithNew::print: SMTLIB: SUBRANGE not implemented");
02349
02350
02351
02352
02353 break;
02354 case IS_INTEGER:
02355 if(e.arity() == 1)
02356 os << "(" << push << "IsInt" << space << e[0] << push << ")";
02357 else
02358 throw SmtlibException("TheoryArithNew::print: SMTLIB: IS_INTEGER used unexpectedly");
02359 break;
02360 case PLUS: {
02361 os << "(" << push << "+";
02362 Expr::iterator i = e.begin(), iend = e.end();
02363 for(; i!=iend; ++i) {
02364 os << space << (*i);
02365 }
02366 os << push << ")";
02367 break;
02368 }
02369 case MINUS: {
02370 os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02371 break;
02372 }
02373 case UMINUS: {
02374 os << "(" << push << "-" << space << e[0] << push << ")";
02375 break;
02376 }
02377 case MULT: {
02378 int i=0, iend=e.arity();
02379 for(; i!=iend; ++i) {
02380 if (i < iend-1) {
02381 os << "(" << push << "*";
02382 }
02383 os << space << e[i];
02384 }
02385 for (i=0; i < iend-1; ++i) os << push << ")";
02386 break;
02387 }
02388 case POW:
02389 throw SmtlibException("TheoryArithNew::print: SMTLIB: POW not supported");
02390
02391 break;
02392 case DIVIDE: {
02393 throw SmtlibException("TheoryArithNew::print: SMTLIB: unexpected use of DIVIDE");
02394 break;
02395 }
02396 case LT: {
02397 Rational r;
02398 os << "(" << push << "<" << space;
02399 os << e[0] << space << e[1] << push << ")";
02400 break;
02401 }
02402 case LE: {
02403 Rational r;
02404 os << "(" << push << "<=" << space;
02405 os << e[0] << space << e[1] << push << ")";
02406 break;
02407 }
02408 case GT: {
02409 Rational r;
02410 os << "(" << push << ">" << space;
02411 os << e[0] << space << e[1] << push << ")";
02412 break;
02413 }
02414 case GE: {
02415 Rational r;
02416 os << "(" << push << ">=" << space;
02417 os << e[0] << space << e[1] << push << ")";
02418 break;
02419 }
02420 case DARK_SHADOW:
02421 throw SmtlibException("TheoryArithNew::print: SMTLIB: DARK_SHADOW not supported");
02422 os << "(" << push << "DARK_SHADOW" << space << e[0]
02423 << space << e[1] << push << ")";
02424 break;
02425 case GRAY_SHADOW:
02426 throw SmtlibException("TheoryArithNew::print: SMTLIB: GRAY_SHADOW not supported");
02427 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
02428 << "," << space << e[2] << "," << space << e[3] << push << ")";
02429 break;
02430 default:
02431 throw SmtlibException("TheoryArithNew::print: SMTLIB: default not supported");
02432
02433
02434 e.printAST(os);
02435
02436 break;
02437 }
02438 break;
02439 }
02440 case LISP_LANG:
02441 switch(e.getKind()) {
02442 case REAL:
02443 case INT:
02444 case RATIONAL_EXPR:
02445 case NEGINF:
02446 case POSINF:
02447 e.print(os);
02448 break;
02449 case SUBRANGE:
02450 if(e.arity() != 2) e.printAST(os);
02451 else
02452 os << "(" << push << "SUBRANGE" << space << e[0]
02453 << space << e[1] << push << ")";
02454 break;
02455 case IS_INTEGER:
02456 if(e.arity() == 1)
02457 os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
02458 else
02459 e.printAST(os);
02460 break;
02461 case PLUS: {
02462 int i=0, iend=e.arity();
02463 os << "(" << push << "+";
02464 for(; i!=iend; ++i) os << space << e[i];
02465 os << push << ")";
02466 break;
02467 }
02468 case MINUS:
02469
02470 os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02471 break;
02472 case UMINUS:
02473 os << "(" << push << "-" << space << e[0] << push << ")";
02474 break;
02475 case MULT: {
02476 int i=0, iend=e.arity();
02477 os << "(" << push << "*";
02478 for(; i!=iend; ++i) os << space << e[i];
02479 os << push << ")";
02480 break;
02481 }
02482 case POW:
02483 os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
02484 break;
02485 case DIVIDE:
02486 os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
02487 break;
02488 case LT:
02489 os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
02490 break;
02491 case LE:
02492 os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
02493 break;
02494 case GT:
02495 os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
02496 break;
02497 case GE:
02498 os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
02499 break;
02500 case DARK_SHADOW:
02501 os << "(" << push << "DARK_SHADOW" << space << e[0]
02502 << space << e[1] << push << ")";
02503 break;
02504 case GRAY_SHADOW:
02505 os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
02506 << e[1] << space << e[2] << space << e[3] << push << ")";
02507 break;
02508 default:
02509
02510
02511 e.printAST(os);
02512
02513 break;
02514 }
02515 break;
02516 default:
02517
02518
02519 e.printAST(os);
02520 }
02521 return os;
02522 }
02523
02524
02525
02526
02527
02528 bool TheoryArithNew::isBasic(const Expr& x) const {
02529
02530 return (tableaux.find(x) != tableaux.end());
02531 }
02532
02533 void TheoryArithNew::pivot(const Expr& x_r, const Expr& x_s) {
02534
02535
02536 DebugAssert(isBasic(x_r), "TheoryArithNew::pivot, given variable should be basic" + x_r.toString());
02537 DebugAssert(!isBasic(x_s), "TheoryArithNew::pivot, given variable should be non-basic" + x_s.toString());
02538
02539
02540 TRACE("simplex", "TheoryArithNew::pivot(", x_r.toString() + ", " + x_s.toString(), ")");
02541
02542
02543 TebleauxMap::iterator it = tableaux.find(x_r);
02544
02545
02546 Theorem x_r_Theorem = (*it).second;
02547
02548
02549 tableaux.erase(x_r);
02550
02551
02552 updateDependenciesRemove(x_r, x_r_Theorem.getExpr()[1]);
02553
02554
02555 const Theorem& x_s_Theorem = pivotRule(x_r_Theorem, x_s);
02556
02557
02558 substAndCanonizeTableaux(x_s_Theorem);
02559
02560
02561 updateDependenciesAdd(x_s, x_s_Theorem.getExpr()[1]);
02562
02563
02564 tableaux[x_s] = x_s_Theorem;
02565 }
02566
02567 void TheoryArithNew::update(const Expr& x_i, const EpsRational& v) {
02568
02569
02570 DebugAssert(tableaux.find(x_i) == tableaux.end(), "TheoryArithNew::update, given variable should be non-basic" + x_i.toString());
02571
02572
02573 TRACE("simplex", "TheoryArithNew::update(", x_i.toString() + ", " + v.toString(), ")");
02574
02575
02576 EpsRational old_value = getBeta(x_i);
02577
02578
02579 DependenciesMap::iterator find = dependenciesMap.find(x_i);
02580 if (find != dependenciesMap.end()) {
02581
02582
02583 const set<Expr>& dependent = (*find).second;
02584 set<Expr>::iterator it = dependent.begin();
02585 set<Expr>::iterator it_end = dependent.end();
02586
02587 while (it != it_end) {
02588
02589
02590 const Expr& x_j = *it;
02591
02592
02593 const Rational& a_ji = getTableauxEntry(x_j, x_i);
02594
02595
02596 EpsRational b(getBeta(x_j));
02597 EpsRational x_j_new = beta[x_j] = b + (v - old_value) * a_ji;
02598
02599
02600 if (x_j_new < getLowerBound(x_j) || getUpperBound(x_j) < x_j_new)
02601 unsatBasicVariables.insert(x_j);
02602 else
02603 unsatBasicVariables.erase(x_j);
02604
02605
02606 it ++;
02607 }
02608 }
02609
02610
02611 beta[x_i] = v;
02612 }
02613
02614 void TheoryArithNew::pivotAndUpdate(const Expr& x_i, const Expr& x_j, const EpsRational& v) {
02615
02616
02617 DebugAssert(tableaux.find(x_i) != tableaux.end(), "TheoryArithNew::pivotAndUpdate, " + x_i.toString() + " should be a basic variable");
02618 DebugAssert(tableaux.find(x_j) == tableaux.end(), "TheoryArithNew::pivotAndUpdate, " + x_j.toString() + " should be a non-basic variable");
02619
02620
02621 TRACE("simplex", "TheoryArithNew::pivotAndUpdate(", x_i.toString() + ", " + x_j.toString() + ", " + v.toString(), ")");
02622
02623
02624 const Rational& a_ij = getTableauxEntry(x_i, x_j);
02625
02626
02627 EpsRational theta((v - getBeta(x_i))/a_ij);
02628
02629
02630 beta[x_i] = v;
02631
02632 unsatBasicVariables.erase(x_i);
02633
02634
02635 EpsRational b = getBeta(x_j);
02636 EpsRational new_x_j = beta[x_j] = b + theta;
02637
02638
02639 if (new_x_j < getLowerBound(x_j) || getUpperBound(x_j) < new_x_j)
02640 unsatBasicVariables.insert(x_j);
02641 else
02642 unsatBasicVariables.erase(x_j);
02643
02644
02645 const set<Expr>& dependent = (*dependenciesMap.find(x_j)).second;
02646 set<Expr>::iterator it = dependent.begin();
02647 set<Expr>::iterator it_end = dependent.end();
02648
02649 while (it != it_end) {
02650
02651
02652 const Expr& x_k = *it;
02653
02654
02655 if (x_k != x_i) {
02656
02657
02658 const Rational& a_kj = getTableauxEntry(x_k, x_j);
02659
02660
02661 b = getBeta(x_k);
02662 EpsRational x_k_new = beta[x_k] = b + theta * a_kj;
02663
02664
02665 if (x_k_new < getLowerBound(x_k) || getUpperBound(x_k) < x_k_new)
02666 unsatBasicVariables.insert(x_k);
02667 else
02668 unsatBasicVariables.erase(x_k);
02669 }
02670
02671
02672 it ++;
02673 }
02674
02675
02676 pivot(x_i, x_j);
02677 }
02678
02679 QueryResult TheoryArithNew::assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm) {
02680
02681
02682 TRACE("simplex", "TheoryArithNew::assertUpper(", x_i.toString() + ", " + c.toString(), ")");
02683
02684
02685 DebugAssert(isLeaf(x_i), "TheoryArithNew::assertUpper wronk kind, expected an arithmetic leaf (variable) got " + x_i.toString());
02686
02687
02688 if (getUpperBound(x_i) <= c) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
02689
02690
02691 if (c < getLowerBound(x_i)) {
02692
02693 explanation = d_rules->clashingBounds(getLowerBoundThm(x_i), thm);
02694
02695 return UNSATISFIABLE;
02696 }
02697
02698
02699 propagate = true;
02700
02701
02702 upperBound[x_i] = BoundInfo(c, thm);
02703
02704
02705 if (getBeta(x_i) <= c) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
02706
02707
02708 if (!isBasic(x_i)) update(x_i, c);
02709
02710 else unsatBasicVariables.insert(x_i);
02711
02712
02713 return UNKNOWN;
02714 }
02715
02716 QueryResult TheoryArithNew::assertLower(const Expr& x_i, const EpsRational& c, const Theorem& thm) {
02717
02718
02719 DebugAssert(isLeaf(x_i), "TheoryArithNew::assertLower wronk kind, expected an arithmetic leaf (variable) got " + x_i.toString());
02720
02721
02722 TRACE("simplex", "TheoryArithNew::assertLower(", x_i.toString() + ", " + c.toString(), ")");
02723
02724
02725 if (c <= getLowerBound(x_i)) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
02726
02727
02728 propagate = true;
02729
02730
02731 if (c > getUpperBound(x_i)) {
02732
02733 explanation = d_rules->clashingBounds(thm, getUpperBoundThm(x_i));
02734
02735 return UNSATISFIABLE;
02736 }
02737
02738
02739 lowerBound[x_i] = BoundInfo(c, thm);
02740
02741
02742 if (c <= getBeta(x_i)) return (consistent == UNKNOWN? UNKNOWN : SATISFIABLE);
02743
02744
02745 if (!isBasic(x_i)) update(x_i, c);
02746
02747 else unsatBasicVariables.insert(x_i);
02748
02749
02750 return UNKNOWN;
02751 }
02752
02753 QueryResult TheoryArithNew::assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm) {
02754
02755
02756 consistent = assertUpper(x_i, c, thm);
02757
02758
02759 if (consistent == UNSATISFIABLE) return UNSATISFIABLE;
02760
02761
02762 consistent = assertLower(x_i, c, thm);
02763
02764
02765 return consistent;
02766 }
02767
02768
02769 void TheoryArithNew::checkSat(bool fullEffort)
02770 {
02771
02772 DebugAssert(consistent != UNSATISFIABLE, "TheoryArithNew::checkSat : we are UNSAT before entering?!?!");
02773
02774
02775 TRACE("simplex", "TheoryArithNew::checkSat(fullEffort=",fullEffort? "true" : "false", ")");
02776
02777
02778 if (assertedExprCount < assertedExpr.size())
02779 updateFreshVariables();
02780
02781
02782 if (consistent != SATISFIABLE || fullEffort)
02783 consistent = checkSatSimplex();
02784
02785
02786 if (consistent == UNSATISFIABLE)
02787 setInconsistent(explanation);
02788
02789
02790 if (consistent == SATISFIABLE) {
02791
02792 Theorem integer_lemma_thm = integer_lemma;
02793 if (!integer_lemma_thm.isNull()) {
02794 if (simplify(integer_lemma_thm.getExpr()).getRHS() == getEM()->trueExpr())
02795 consistent = checkSatInteger();
02796 else
02797 consistent = UNKNOWN;
02798 } else
02799
02800 consistent = checkSatInteger();
02801 }
02802
02803
02804 if (consistent == SATISFIABLE && fullEffort) {
02805 unsigned size = d_sharedTermsList.size(), j;
02806 Theorem thm;
02807 for (; d_index1 < size; d_index1 = d_index1 + 1) {
02808 const Expr& e1 = d_sharedTermsList[d_index1];
02809 if (e1.getKind() == RATIONAL_EXPR) continue;
02810 if (find(e1).getRHS() != e1) continue;
02811 Expr var(e1);
02812 if (isPlus(e1)) {
02813 TebleauxMap::iterator findt = freshVariables.find(e1);
02814 DebugAssert(findt != freshVariables.end(), "expected to find in tableaux");
02815 var = (*findt).second.getExpr()[0];
02816 }
02817 else {
02818 DebugAssert(isLeaf(e1), "expected leaf");
02819 }
02820 CDMap<Expr, EpsRational>::iterator findb = beta.find(var);
02821 if (findb == beta.end()) continue;
02822 EpsRational val = (*findb).second;
02823
02824 for (j = 0; j < size; ++j) {
02825 const Expr& e2 = d_sharedTermsList[j];
02826 if (j < d_index1 && e2.getKind() != RATIONAL_EXPR) continue;
02827 else if (j == d_index1) continue;
02828 if (find(e2).getRHS() != e2) continue;
02829 DebugAssert(e1 != e2, "should be distinct");
02830
02831 if (isPlus(e2)) {
02832 TebleauxMap::iterator findt = freshVariables.find(e2);
02833 DebugAssert(findt != freshVariables.end(), "expected to find in tableaux");
02834 var = (*findt).second.getExpr()[0];
02835 }
02836 else {
02837 var = e2;
02838 DebugAssert(isLeaf(e2), "expected leaf");
02839 }
02840 findb = beta.find(var);
02841 if (findb == beta.end()) continue;
02842 if (!(val == (*findb).second)) continue;
02843 addSplitter(e1.eqExpr(e2));
02844 return;
02845 }
02846 }
02847
02848 }
02849
02850
02851 TRACE("simplex", "TheoryArithNew::checkSat ==> ", consistent == UNSATISFIABLE? "UNSATISFIABLE" : "SATISFIABLE", "");
02852 }
02853
02854 QueryResult TheoryArithNew::checkSatInteger() {
02855
02856
02857 TRACE("simplex", "TheoryArithNew::checkSatInteger()", "", "");
02858
02859
02860 set<Expr>::iterator x_i_it = intVariables.begin();
02861 set<Expr>::iterator x_i_it_end = intVariables.end();
02862
02863
02864
02865
02866
02867
02868
02869
02870
02871 while (x_i_it != x_i_it_end) {
02872
02873
02874 const Expr& x_i = (*x_i_it);
02875
02876
02877 if (isInteger(x_i)) {
02878
02879
02880 const EpsRational& beta = getBeta(x_i);
02881
02882
02883 if (beta.isInteger()) { ++ x_i_it; continue; }
02884
02885
02886 integer_lemma = d_rules->integerSplit(x_i, beta.getFloor());
02887 TRACE("integer", "TheoryArithNew::checkSatInteger ==> lemma : ", integer_lemma, "");
02888 enqueueFact(integer_lemma);
02889
02890
02891 return UNKNOWN;
02892 }
02893
02894
02895 ++ x_i_it;
02896 }
02897
02898
02899 return SATISFIABLE;
02900 }
02901
02902 QueryResult TheoryArithNew::checkSatSimplex() {
02903
02904 Expr x_i;
02905 EpsRational x_i_Value;
02906 Expr x_j;
02907 EpsRational x_j_Value;
02908 Rational a_ij;
02909
02910 bool x_j_Found;
02911 EpsRational l_i;
02912 EpsRational u_i;
02913
02914
02915 TRACE("arith_atoms", "Tableaux size: ", tableaux.size(), "");
02916 TRACE("arith_atoms", "UNSAT vars: ", unsatBasicVariables.size(), "");
02917
02918
02919 while (unsatBasicVariables.size()) {
02920
02921
02922 x_i = *unsatBasicVariables.begin();
02923 TebleauxMap::iterator it = tableaux.find(x_i);
02924 x_i_Value = getBeta(x_i);
02925 l_i = getLowerBound(x_i);
02926 u_i = getUpperBound(x_i);
02927
02928
02929 if (l_i > x_i_Value) {
02930
02931
02932 x_j_Found = false;
02933
02934
02935 const Expr& x_i_RightSide = (*it).second.getExpr()[1];
02936 int non_basics_i_end = x_i_RightSide.arity();
02937 for(int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
02938
02939
02940 x_j = x_i_RightSide[non_basics_i][1];
02941 a_ij = x_i_RightSide[non_basics_i][0].getRational();
02942 x_j_Value = getBeta(x_j);
02943
02944
02945 if (a_ij > 0) {
02946 if (x_j_Value < getUpperBound(x_j)) {
02947 x_j_Found = true;
02948 break;
02949 }
02950 } else {
02951 if (x_j_Value > getLowerBound(x_j)) {
02952 x_j_Found = true;
02953 break;
02954 }
02955 }
02956 }
02957
02958
02959 if (!x_j_Found) {
02960
02961 explanation = getLowerBoundExplanation(it);
02962
02963 return UNSATISFIABLE;
02964 }
02965
02966
02967 pivotAndUpdate(x_i, x_j, l_i);
02968 } else
02969
02970 if (x_i_Value > u_i) {
02971
02972
02973 x_j_Found = false;
02974
02975
02976 const Expr& x_i_RightSide = (*it).second.getExpr()[1];
02977 int non_basics_i_end = x_i_RightSide.arity();
02978 for(int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
02979
02980
02981 x_j = x_i_RightSide[non_basics_i][1];
02982 a_ij = x_i_RightSide[non_basics_i][0].getRational();
02983 x_j_Value = getBeta(x_j);
02984
02985
02986 if (a_ij < 0) {
02987 if (x_j_Value < getUpperBound(x_j)) {
02988 x_j_Found = true;
02989 break;
02990 }
02991 } else
02992 if (x_j_Value > getLowerBound(x_j)) {
02993 x_j_Found = true;
02994 break;
02995 }
02996 }
02997
02998
02999 if (!x_j_Found) {
03000
03001 explanation = getUpperBoundExplanation(it);
03002
03003 return UNSATISFIABLE;
03004 }
03005
03006
03007 pivotAndUpdate(x_i, x_j, u_i);
03008 } else
03009
03010 unsatBasicVariables.erase(x_i);
03011
03012
03013
03014 TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> new tableaux : \n", tableauxAsString(), "");
03015 TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> new bounds : \n", boundsAsString(), "");
03016 TRACE("simplex", "TheoryArithNew::checkSatSimplex ==> unsat : \n", unsatAsString(), "");
03017
03018 };
03019
03020
03021 return SATISFIABLE;
03022 }
03023
03024 Rational TheoryArithNew::getTableauxEntry(const Expr& x_i, const Expr& x_j) {
03025 return findCoefficient(x_j, tableaux[x_i].getExpr()[1]);
03026 }
03027
03028
03029 const Rational& TheoryArithNew::findCoefficient(const Expr& var, const Expr& expr) {
03030
03031
03032 static Rational zeroCoefficient(0);
03033
03034
03035 DebugAssert(isPlus(expr), "TheoryArithNew::findCoefficient : expression must be a sum : " + expr.toString());
03036
03037
03038 int left = 0;
03039 int right = expr.arity() - 1;
03040 int i;
03041 while (left <= right) {
03042
03043
03044 i = (left + right ) / 2;
03045
03046
03047 const Expr& mult = expr[i];
03048
03049
03050 DebugAssert(isMult(mult) && isRational(mult[0]), "TheoryArithNew::findCoefficient : expression must be a sum of multiplications: " + expr.toString());
03051
03052
03053 int cmp = compare(mult[1], var);
03054 if (cmp == 0)
03055 return mult[0].getRational();
03056 else
03057 if (cmp > 0)
03058 left = i + 1;
03059 else
03060 right = i - 1;
03061 }
03062
03063
03064 return zeroCoefficient;
03065 }
03066
03067
03068 TheoryArithNew::EpsRational TheoryArithNew::getLowerBound(const Expr& x) const {
03069
03070 CDMap<Expr, BoundInfo>::iterator find = lowerBound.find(x);
03071
03072 if (find == lowerBound.end()) return EpsRational::MinusInfinity;
03073 else return (*find).second.bound;
03074 }
03075
03076 TheoryArithNew::EpsRational TheoryArithNew::getUpperBound(const Expr& x) const {
03077
03078 CDMap<Expr, BoundInfo>::iterator find = upperBound.find(x);
03079
03080 if (find == upperBound.end()) return EpsRational::PlusInfinity;
03081 else return (*find).second.bound;
03082 }
03083
03084 Theorem TheoryArithNew::getLowerBoundThm(const Expr& x) const {
03085
03086 CDMap<Expr, BoundInfo>::iterator find = lowerBound.find(x);
03087
03088 DebugAssert(find != lowerBound.end(), "TheoryArithNew::getLowerBoundThm, theorem not found for " + x.toString());
03089
03090 return (*find).second.theorem;
03091 }
03092
03093 Theorem TheoryArithNew::getUpperBoundThm(const Expr& x) const {
03094
03095 CDMap<Expr, BoundInfo>::iterator find = upperBound.find(x);
03096
03097 DebugAssert(find != upperBound.end(), "TheoryArithNew::getUpperBoundThm, theorem not found for " + x.toString());
03098
03099 return (*find).second.theorem;
03100 }
03101
03102
03103 TheoryArithNew::EpsRational TheoryArithNew::getBeta(const Expr& x) {
03104
03105
03106 CDMap<Expr, EpsRational>::iterator find = beta.find(x);
03107
03108 if (find == beta.end()) {
03109
03110 return beta[x] = EpsRational::Zero;
03111
03112
03113 if (EpsRational::Zero < getLowerBound(x) || getUpperBound(x) < EpsRational::Zero)
03114 unsatBasicVariables.insert(x);
03115 else
03116 unsatBasicVariables.erase(x);
03117 }
03118 else
03119
03120 return (*find).second;
03121 }
03122
03123
03124 void TheoryArithNew::assertFact(const Theorem& assertThm)
03125 {
03126
03127 const Expr& expr = assertThm.getExpr();
03128
03129
03130 if (expr.isEq()) {
03131 Theorem thm = iffMP(assertThm, d_rules->eqToIneq(assertThm.getExpr()));
03132 Theorem thm1 = getCommonRules()->andElim(thm, 0);
03133 Theorem thm2 = getCommonRules()->andElim(thm, 1);
03134 thm1 = iffMP(thm1, rewrite(thm1.getExpr()));
03135 if (thm1.getExpr().isBoolConst()) enqueueFact(thm1);
03136 else assertFact(thm1);
03137 thm2 = iffMP(thm2, rewrite(thm2.getExpr()));
03138 if (thm2.getExpr().isBoolConst()) enqueueFact(thm2);
03139 else assertFact(thm2);
03140 return;
03141 }
03142
03143
03144 if (expr.isNot() && expr[0].isEq()) {
03145 enqueueFact(d_rules->diseqToIneq(assertThm));
03146 return;
03147 }
03148
03149
03150 TRACE("simplex", "TheoryArithNew::assertFact(", expr, ")");
03151 TRACE("simplex", "asserted: ", assertedExpr.size(), "");
03152 TRACE("simplex", "counted: ", assertedExprCount, "");
03153 TRACE("arith_atoms", "Assert: ", expr.toString(), "");
03154
03155
03156 if (assertedExprCount < assertedExpr.size())
03157 updateFreshVariables();
03158
03159
03160 const Expr& leftSide = expr[0];
03161 const Expr& rightSide = expr[1];
03162 int kind = expr.getKind();
03163
03164
03165 DebugAssert(isIneq(expr) , "TheoryArithNew::assertFact wronk kind, expected inequality" + expr.toString());
03166 DebugAssert(isPlus(rightSide) || (isMult(rightSide) && isRational(rightSide[0]) && isLeaf(rightSide[1])), "TheoryArithNew::assertFact wronk kind, expected sum on the right side opr a simple 1*x" + expr.toString());
03167 DebugAssert(isRational(leftSide), "TheoryArithNew::assertFact wronk kind, expected rational on the right side" + expr.toString());
03168
03169
03170 Rational leftSideValue = leftSide.getRational();
03171
03172
03173 Rational c = leftSideValue;
03174
03175
03176 Expr var;
03177
03178
03179 Theorem assert = assertThm;
03180
03181
03182
03183 if (!isPlus(rightSide)) {
03184
03185
03186 DebugAssert(rightSide[0].isRational() && rightSide[0].getRational() == 1, "TheoryArithNew::assertFact, left side should be multiplication by one");
03187
03188
03189 assert = iffMP(assert, substitutivityRule(expr, reflexivityRule(leftSide), d_rules->oneElimination(rightSide)));
03190
03191
03192 var = rightSide[1];
03193
03194
03195 if (isInteger(var)) intVariables.insert(var);
03196
03197 } else {
03198
03199 const Theorem& introductionThm = getVariableIntroThm(rightSide);
03200
03201
03202 var = introductionThm.getExpr()[0];
03203
03204
03205 assert = iffMP(assertThm, substitutivityRule(expr, 1, symmetryRule(introductionThm)));
03206
03207
03208 if (isInteger(var)) {
03209 intVariables.insert(var);
03210 int i_end = rightSide.arity();
03211 for(int i = 0; i < i_end; ++ i)
03212 intVariables.insert(rightSide[i][1]);
03213 } else {
03214 int i_end = rightSide.arity();
03215 for(int i = 0; i < i_end; ++ i)
03216 if (isInteger(rightSide[i][1])) intVariables.insert(rightSide[i][1]);
03217 }
03218 }
03219
03220
03221 EpsRational bound;
03222
03223
03224 propagate = false;
03225
03226
03227 EpsRational oldBound;
03228
03229
03230 switch (kind) {
03231 case LT:
03232 oldBound = getLowerBound(var);
03233
03234 consistent = assertLower(var, bound = EpsRational(c, +1), assert);
03235 break;
03236 case LE:
03237 oldBound = getLowerBound(var);
03238
03239 consistent = assertLower(var, bound = c, assert);
03240 break;
03241 case GT:
03242 oldBound = getUpperBound(var);
03243
03244 consistent = assertUpper(var, bound = EpsRational(c, -1), assert);
03245 break;
03246 case GE:
03247 oldBound = getUpperBound(var);
03248
03249 consistent = assertUpper(var, bound = c, assert);
03250 break;
03251 case EQ:
03252
03253 consistent = assertEqual(var, bound = c, assert);
03254
03255 propagate = false;
03256 break;
03257 default:
03258
03259 FatalAssert(false, "Theory_Arith::assertFact, control should not reach here");
03260 break;
03261 }
03262
03263
03264 TRACE("simplex", "TheoryArithNew::assertFact ==> ", consistent == UNSATISFIABLE? "UNSATISFIABLE" : consistent == UNKNOWN? "UNKNOWN" : "SATISFIABLE", "");
03265 TRACE("simplex", "TheoryArithNew::assertFact ==> new tableaux : \n", tableauxAsString(), "");
03266 TRACE("simplex", "TheoryArithNew::assertFact ==> new bounds : \n", boundsAsString(), "");
03267 TRACE("simplex", "TheoryArithNew::assertFact ==> unsat : \n", unsatAsString(), "");
03268
03269
03270 if (consistent == UNSATISFIABLE)
03271 setInconsistent(explanation);
03272
03273
03274 if (propagate)
03275 propagateTheory(assertThm.getExpr(), bound, oldBound);
03276 }
03277
03278
03279 Theorem TheoryArithNew::getVariableIntroThm(const Expr& rightSide) {
03280
03281
03282 TebleauxMap::iterator find = freshVariables.find(rightSide);
03283
03284
03285 if (find == freshVariables.end()) {
03286
03287
03288 CommonProofRules* c_rules = getCommonRules();
03289
03290
03291 Theorem thm = c_rules->varIntroRule(rightSide);
03292
03293
03294 thm = c_rules->iffMP(thm, c_rules->skolemizeRewrite(thm.getExpr()));
03295
03296
03297 thm = symmetryRule(thm);
03298
03299
03300 Theorem returnThm = freshVariables[rightSide] = thm;
03301
03302
03303 thm = substAndCanonizeModTableaux(thm);
03304
03305
03306 const Expr& var = thm.getExpr()[0];
03307
03308
03309 tableaux[var] = thm;
03310
03311
03312 updateDependenciesAdd(var, thm.getExpr()[1]);
03313
03314
03315 assertedExpr.push_back(Expr(EQ, var, rightSide));
03316 assertedExprCount = assertedExprCount + 1;
03317
03318
03319 updateValue(var, rightSide);
03320
03321
03322 return returnThm;
03323 }
03324
03325
03326 return (*find).second;
03327 }
03328
03329 void TheoryArithNew::updateValue(const Expr& var, const Expr& e) {
03330
03331
03332 EpsRational varValue(0);
03333
03334
03335 int i_end = e.arity();
03336 for (int i = 0; i < i_end; ++ i)
03337 varValue += getBeta(e[i][1]) * e[i][0].getRational();
03338
03339
03340 beta[var] = varValue;
03341
03342
03343 if (varValue < getLowerBound(var) || getUpperBound(var) < varValue)
03344 unsatBasicVariables.insert(var);
03345 else
03346 unsatBasicVariables.erase(var);
03347 }
03348
03349 string TheoryArithNew::tableauxAsString() const {
03350
03351
03352 string str;
03353
03354
03355 TebleauxMap::const_iterator row = tableaux.begin();
03356 TebleauxMap::const_iterator row_end = tableaux.end();
03357
03358
03359 while (row != tableaux.end()) {
03360
03361 str = str + ((*row).second).getExpr().toString() + "\n";
03362
03363
03364 row ++;
03365 }
03366
03367
03368 return str;
03369 }
03370
03371 string TheoryArithNew::unsatAsString() const {
03372
03373
03374 string str;
03375
03376
03377 set<Expr>::const_iterator it = unsatBasicVariables.begin();
03378 set<Expr>::const_iterator it_end = unsatBasicVariables.end();
03379
03380
03381 while (it != it_end) {
03382
03383 str = str + (*it).toString() + " ";
03384
03385
03386 it ++;
03387 }
03388
03389
03390 return str;
03391 }
03392
03393
03394 string TheoryArithNew::boundsAsString() {
03395
03396
03397 string str;
03398
03399
03400 set<Expr> all_variables;
03401
03402
03403 TebleauxMap::const_iterator it = tableaux.begin();
03404 TebleauxMap::const_iterator it_end = tableaux.end();
03405 for(; it != it_end; it ++) {
03406
03407
03408 all_variables.insert((*it).first);
03409
03410
03411 const Expr& rightSide = (*it).second.getExpr()[1];
03412 int term_i_end = rightSide.arity();
03413 for(int term_i = 0; term_i < term_i_end; ++ term_i)
03414 all_variables.insert(rightSide[term_i][1]);
03415 }
03416
03417
03418 CDMap<Expr, BoundInfo>::iterator bounds_it;
03419 for (bounds_it = lowerBound.begin(); bounds_it != lowerBound.end(); bounds_it ++)
03420 all_variables.insert((*bounds_it).first);
03421 for (bounds_it = upperBound.begin(); bounds_it != upperBound.end(); bounds_it ++)
03422 all_variables.insert((*bounds_it).first);
03423
03424
03425 set<Expr>::iterator var_it = all_variables.begin();
03426 set<Expr>::iterator var_it_end = all_variables.end();
03427
03428
03429 while (var_it != var_it_end) {
03430
03431
03432 const Expr& var = *var_it;
03433
03434
03435 str += getLowerBound(var).toString() + " <= " + var.toString() + "(" + getBeta(var).toString() + ") <= " + getUpperBound(var).toString() + "\n";
03436
03437
03438 var_it ++;
03439 }
03440
03441
03442 return str;
03443 }
03444
03445
03446 const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::PlusInfinity(PLUS_INFINITY);
03447
03448 const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::MinusInfinity(MINUS_INFINITY);
03449
03450 const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::Zero;
03451
03452
03453 Theorem TheoryArithNew::substAndCanonizeModTableaux(const Theorem& eq) {
03454
03455
03456 if(tableaux.empty()) return eq;
03457
03458
03459 const Expr& eqExpr = eq.getExpr();
03460
03461
03462 DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::substAndCanonize, expected equality " + eqExpr.toString());
03463
03464
03465 const Expr& rightSide = eqExpr[1];
03466
03467
03468 Theorem thm = substAndCanonizeModTableaux(rightSide);
03469
03470
03471 if(thm.getRHS() == rightSide) return eq;
03472
03473
03474 return iffMP(eq, substitutivityRule(eq.getExpr(), 1, thm));
03475 }
03476
03477 Theorem TheoryArithNew::substAndCanonizeModTableaux(const Expr& sum) {
03478
03479 Theorem res;
03480 vector<Theorem> thms;
03481 vector<unsigned> changed;
03482
03483
03484 TRACE("simplex", "TheoryArithNew::substAndCanonizeModTableaux(", sum, ")");
03485
03486
03487 DebugAssert(sum.getKind() == PLUS, "TheoryArithNew::substAndCanonize, expected sum " + sum.toString());
03488
03489
03490 int term_index_end = sum.arity();
03491 for(int term_index = 0; term_index < term_index_end; ++ term_index) {
03492
03493 const Expr& term = sum[term_index];
03494 const Expr& var = term[1];
03495
03496
03497 TebleauxMap::iterator find = tableaux.find(var);
03498
03499
03500 if (find != tableaux.end()) {
03501
03502
03503 Theorem termTheorem = canonThm(substitutivityRule(term, 1, (*find).second));
03504
03505
03506 DebugAssert(termTheorem.getExpr() != term, "substAndCanonizeModTableaux: got the same term in substitution");
03507
03508
03509 thms.push_back(termTheorem);
03510
03511
03512 changed.push_back(term_index);
03513 }
03514 }
03515
03516
03517 if(thms.size() > 0) {
03518
03519 res = substitutivityRule(sum, changed, thms);
03520
03521 res = canonThm(res);
03522 } else
03523
03524 res = reflexivityRule(sum);
03525
03526
03527 return res;
03528 }
03529
03530 void TheoryArithNew::substAndCanonizeTableaux(const Theorem& eq) {
03531
03532 Theorem result;
03533
03534
03535 TRACE("simplex", "TheoryArithNew::substAndCanonizeTableaux(", eq.getExpr(), ")");
03536
03537
03538 const Expr& eqExpr = eq.getExpr();
03539
03540
03541 DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::substAndCanonize, expected equality " + eqExpr.toString());
03542
03543
03544 const Expr& var = eqExpr[0];
03545
03546
03547 DependenciesMap::iterator find = dependenciesMap.find(var);
03548 if (find != dependenciesMap.end()) {
03549
03550
03551 set<Expr>& dependent = (*find).second;
03552 set<Expr>::iterator it = dependent.begin();
03553 set<Expr>::iterator it_end = dependent.end();
03554 for(; it != it_end; ++ it) {
03555
03556
03557 const Expr& leftSide = *it;
03558 TebleauxMap::iterator row = tableaux.find(leftSide);
03559 const Expr& rowExpr = (*row).second.getExpr();
03560 const Expr& rowRightSide = rowExpr[1];
03561
03562
03563 int right = rowRightSide.arity() - 1;
03564 int left = 0;
03565 int term_i;
03566 while (left <= right) {
03567
03568
03569 term_i = (left + right) / 2;
03570
03571
03572 int cmp = compare(rowRightSide[term_i][1], var);
03573
03574
03575 if (cmp == 0) {
03576
03577
03578 result = canonThm(substitutivityRule(rowRightSide[term_i], 1, eq));
03579
03580 result = canonThm(substitutivityRule(rowRightSide, term_i, result));
03581
03582 result = substitutivityRule(rowExpr, 1, result);
03583
03584
03585 const Expr& newRowRightSide = result.getRHS()[1];
03586
03587 updateDependencies(rowRightSide, newRowRightSide, leftSide, var);
03588
03589
03590 (*row).second = iffMP((*row).second, result);
03591
03592
03593 break;
03594 } else if (cmp > 0)
03595 left = term_i + 1;
03596 else
03597 right = term_i - 1;
03598 }
03599 }
03600
03601
03602 dependent.clear();
03603 }
03604 }
03605
03606 Theorem TheoryArithNew::pivotRule(const Theorem& eq, const Expr& var) {
03607
03608 Theorem result;
03609
03610
03611 const Expr& eqExpr = eq.getExpr();
03612 const Expr& right_side = eqExpr[1];
03613 const Expr& left_side = eqExpr[0];
03614
03615
03616
03617 TRACE("simplex", "TheoryArithNew::pivotRule(", eqExpr.toString() + ", ", var.toString() + ")");
03618
03619
03620 DebugAssert(eqExpr.getKind() == EQ, "TheoryArithNew::pivotRule, expected an equality : " + eqExpr.toString());
03621 DebugAssert(right_side.getKind() == PLUS, "TheoryArithNew::pivotRule, expected a sum on the left-hand side : " + eqExpr.toString());
03622 DebugAssert(isLeaf(left_side), "TheoryArithNew::pivotRule, expected a leaf (variable) on the right-hand side : " + eqExpr.toString());
03623
03624
03625 int term_i_end = right_side.arity();
03626 for(int term_i = 0; term_i < term_i_end; ++ term_i)
03627
03628 if (right_side[term_i][1] == var) {
03629
03630
03631 const Expr& termExpr = right_side[term_i];
03632 const Expr& termVar = termExpr[1];
03633 const Rational& termRat = termExpr[0].getRational();
03634
03635
03636 const Expr& minusTermExpr = multExpr(rat(-termRat), termVar);
03637 const Expr& minusVarExpr = multExpr(rat(-1), left_side);
03638
03639
03640 result = iffMP(eq, d_rules->plusPredicate(left_side, right_side, plusExpr(minusTermExpr, minusVarExpr), EQ));
03641
03642 result = transitivityRule(result, canon(result.getExpr()[1]));
03643
03644 result = transitivityRule(symmetryRule(canon(result.getExpr()[0])), result);
03645
03646 result = iffMP(result, d_rules->multEqn(result.getExpr()[0], result.getExpr()[1], rat(-1/termRat)));
03647
03648 result = transitivityRule(result, canon(result.getExpr()[1]));
03649
03650 result = transitivityRule(symmetryRule(canon(result.getExpr()[0])), result);
03651
03652 result = transitivityRule(symmetryRule(d_rules->oneElimination(result.getExpr()[0])), result);
03653
03654
03655 TRACE("simplex", "TheoryArithNew::pivotRule ==> ", result.getExpr().toString(), "");
03656
03657
03658 return result;
03659 }
03660
03661
03662 DebugAssert(false, "TheoryArithNew::pivotRule, " + var.toString() + " does not occur in " + eqExpr.toString());
03663
03664
03665 return result;
03666 }
03667
03668 Theorem TheoryArithNew::getLowerBoundExplanation(const TebleauxMap::iterator& var_it) {
03669
03670 vector<Theorem> upperBounds;
03671
03672
03673 Theorem tableauxTheorem = (*var_it).second;
03674
03675
03676 const Expr& var = (*var_it).first;
03677
03678
03679 const Expr& rightSide = tableauxTheorem.getExpr()[1];
03680
03681
03682 int leftSide_i_end = rightSide.arity();
03683 for(int leftSide_i = 0; leftSide_i < leftSide_i_end; ++ leftSide_i) {
03684
03685
03686 const Expr& a = rightSide[leftSide_i][0];
03687
03688
03689 const Expr& x = rightSide[leftSide_i][1];
03690
03691
03692 if (a.getRational() > 0) {
03693
03694 Theorem thm = getUpperBoundThm(x);
03695
03696
03697 thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
03698
03699
03700 Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
03701 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
03702
03703
03704 thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
03705
03706
03707 upperBounds.push_back(thm);
03708 }
03709
03710 else {
03711
03712 Theorem thm = getLowerBoundThm(x);
03713
03714
03715 thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
03716
03717
03718 Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
03719 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
03720
03721
03722 thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
03723
03724
03725 upperBounds.push_back(thm);
03726 }
03727 }
03728
03729
03730 Theorem sumInequalities = upperBounds[0];
03731 for(unsigned int i = 1; i < upperBounds.size(); i ++) {
03732
03733 sumInequalities = d_rules->addInequalities(sumInequalities, upperBounds[i]);
03734
03735
03736 Theorem canonLeft = d_rules->canonPlus(sumInequalities.getExpr()[0]);
03737 Theorem canonRight = d_rules->canonPlus(sumInequalities.getExpr()[1]);
03738
03739
03740 sumInequalities = iffMP(sumInequalities, substitutivityRule(sumInequalities.getExpr(), canonLeft, canonRight));
03741 }
03742
03743
03744 Theorem varUpperBound = substitutivityRule(sumInequalities.getExpr(), 1, symmetryRule(tableauxTheorem));
03745
03746 varUpperBound = iffMP(sumInequalities, varUpperBound);
03747
03748
03749 Theorem varLowerBound = getLowerBoundThm(var);
03750
03751
03752 return d_rules->clashingBounds(varLowerBound, varUpperBound);
03753 }
03754
03755 Theorem TheoryArithNew::getUpperBoundExplanation(const TebleauxMap::iterator& var_it) {
03756
03757 vector<Theorem> lowerBounds;
03758
03759
03760 Theorem tableauxTheorem = (*var_it).second;
03761
03762
03763 const Expr& var = (*var_it).first;
03764
03765
03766 const Expr& rightSide = tableauxTheorem.getExpr()[1];
03767
03768
03769 TRACE("explanations", "Generating explanation for the tableaux row ", tableauxTheorem.getExpr(), "");
03770
03771
03772 int rightSide_i_end = rightSide.arity();
03773 for(int rightSide_i = 0; rightSide_i < rightSide_i_end; ++ rightSide_i) {
03774
03775
03776 const Expr& a = rightSide[rightSide_i][0];
03777
03778
03779 const Expr& x = rightSide[rightSide_i][1];
03780
03781
03782 if (a.getRational() > 0) {
03783
03784 Theorem thm = getLowerBoundThm(x);
03785 TRACE("explanations", "Got ", thm.getExpr(), "");
03786
03787
03788 thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
03789 TRACE("explanations", "Got ", thm.getExpr(), "");
03790
03791
03792 Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
03793 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
03794
03795
03796 thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
03797 TRACE("explanations", "Got ", thm.getExpr(), "");
03798
03799
03800 lowerBounds.push_back(thm);
03801 }
03802
03803 else {
03804
03805 Theorem thm = getUpperBoundThm(x);
03806 TRACE("explanations", "Got ", thm.getExpr(), "");
03807
03808
03809 thm = iffMP(thm, d_rules->multIneqn(thm.getExpr(), a));
03810 TRACE("explanations", "Got ", thm.getExpr(), "");
03811
03812
03813 Theorem canonRight = d_rules->canonMultTermConst(thm.getExpr()[1][1], thm.getExpr()[1][0]);
03814 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]);
03815
03816
03817 thm = iffMP(thm, substitutivityRule(thm.getExpr(), canonLeft, canonRight));
03818 TRACE("explanations", "Got ", thm.getExpr(), "");
03819
03820
03821 lowerBounds.push_back(thm);
03822 }
03823 }
03824
03825
03826 Theorem sumInequalities = lowerBounds[0];
03827 for(unsigned int i = 1; i < lowerBounds.size(); i ++) {
03828
03829 sumInequalities = d_rules->addInequalities(sumInequalities, lowerBounds[i]);
03830
03831 TRACE("explanations", "Got sum ", sumInequalities.getExpr(), "");
03832
03833
03834 Theorem canonLeft = d_rules->canonPlus(sumInequalities.getExpr()[0]);
03835 Theorem canonRight = d_rules->canonPlus(sumInequalities.getExpr()[1]);
03836
03837
03838 sumInequalities = iffMP(sumInequalities, substitutivityRule(sumInequalities.getExpr(), canonLeft, canonRight));
03839 }
03840
03841
03842 TRACE("explanations", "Got sum ", sumInequalities.getExpr(), "");
03843
03844
03845 Theorem varLowerBound = substitutivityRule(sumInequalities.getExpr(), 1, symmetryRule(tableauxTheorem));
03846
03847
03848 varLowerBound = iffMP(sumInequalities, varLowerBound);
03849
03850
03851 TRACE("explanations", "Got lower bound ", varLowerBound.getExpr(), "");
03852
03853
03854 Theorem varUpperBound = getUpperBoundThm(var);
03855
03856
03857 TRACE("explanations", "Got upper bound ", varUpperBound.getExpr(), "");
03858
03859 TRACE("explanations", "The var value (", var, ")" + getBeta(var).toString());
03860
03861
03862 return d_rules->clashingBounds(varLowerBound, varUpperBound);
03863 }
03864
03865 void TheoryArithNew::updateFreshVariables() {
03866
03867 unsigned int size = assertedExpr.size();
03868 unsigned int i;
03869
03870 for (i = assertedExprCount; i < size; ++ i)
03871
03872 updateValue(assertedExpr[i][0], assertedExpr[i][1]);
03873
03874
03875 assertedExprCount = i;
03876
03877 }
03878
03879 void TheoryArithNew::updateDependenciesAdd(const Expr& var, const Expr& sum) {
03880
03881
03882 TRACE("tableaux_dep", "updateDependenciesAdd(", var.toString() + ", ", sum.toString() + ")");
03883
03884
03885 Expr::iterator term = sum.begin();
03886 Expr::iterator term_end = sum.end();
03887 for(; term != term_end; term ++)
03888 dependenciesMap[(*term)[1]].insert(var);
03889
03890 }
03891
03892 void TheoryArithNew::updateDependenciesRemove(const Expr& var, const Expr& sum) {
03893
03894
03895 TRACE("tableaux_dep", "updateDependenciesRemove(", var.toString() + ", ", sum.toString() + ")");
03896
03897
03898 Expr::iterator term = sum.begin();
03899 Expr::iterator term_end = sum.end();
03900 for(; term != term_end; term ++)
03901 dependenciesMap[(*term)[1]].erase(var);
03902
03903 }
03904
03905 void TheoryArithNew::updateDependencies(const Expr& oldSum, const Expr& newSum, const Expr& dependentVar, const Expr& skipVar) {
03906
03907
03908 TRACE("tableaux_dep", "updateDependencies(", oldSum.toString() + ", " + newSum.toString() + ", " + dependentVar.toString(), ")");
03909
03910
03911 int oldSum_i = 0, newSum_i = 0;
03912 int oldSum_end = oldSum.arity(), newSum_end = newSum.arity();
03913
03914 while (oldSum_i < oldSum_end && newSum_i < newSum_end) {
03915
03916
03917 const Expr oldVar = oldSum[oldSum_i][1];
03918 const Expr newVar = newSum[newSum_i][1];
03919
03920
03921 if (oldVar == newVar) {
03922 ++ oldSum_i; ++ newSum_i; continue;
03923 }
03924
03925
03926 if (oldVar > newVar) {
03927
03928 if (oldVar != skipVar)
03929 dependenciesMap[oldVar].erase(dependentVar);
03930
03931 ++ oldSum_i;
03932 } else {
03933
03934 if (newVar != skipVar)
03935 dependenciesMap[newVar].insert(dependentVar);
03936
03937 ++ newSum_i;
03938 }
03939 }
03940
03941
03942 while (oldSum_i < oldSum_end) {
03943
03944 const Expr& var = oldSum[oldSum_i ++][1];
03945
03946 if (var != skipVar)
03947 dependenciesMap[var].erase(dependentVar);
03948 }
03949
03950 while (newSum_i < newSum_end) {
03951
03952 const Expr& var = newSum[newSum_i ++][1];
03953
03954 if (var != skipVar)
03955 dependenciesMap[var].insert(dependentVar);
03956 }
03957 }
03958
03959 void TheoryArithNew::registerAtom(const Expr& e) {
03960
03961 if (e.isEq()) return;
03962
03963 TRACE("propagate_arith", "registerAtom(", e.toString(), ")");
03964 TRACE("arith_atoms", "", e.toString(), "");
03965
03966
03967 if (e.isAbsAtomicFormula()) {
03968 Expr rightSide = e[1];
03969 int kind = e.getKind();
03970 Rational leftSide = e[0].getRational();
03971
03972
03973 EpsRational bound;
03974
03975
03976 switch (kind) {
03977 case LT:
03978 bound = EpsRational(leftSide, +1);
03979 break;
03980 case LE:
03981 bound = leftSide;
03982 break;
03983 case GT:
03984 bound = EpsRational(leftSide, -1);
03985 break;
03986 case GE:
03987 bound = leftSide;
03988 break;
03989 default:
03990
03991 FatalAssert(false, "TheoryArithNew::registerAtom: control should not reach here" + e.toString());
03992 }
03993
03994
03995 allBounds.insert(ExprBoundInfo(bound, e));
03996 }
03997
03998
03999
04000
04001
04002
04003
04004
04005 }
04006
04007 void TheoryArithNew::propagateTheory(const Expr& assertExpr, const EpsRational& bound, const EpsRational& oldBound) {
04008
04009
04010 TRACE("propagate_arith", "propagateTheory(", assertExpr.toString() + ", " + bound.toString(), ")");
04011
04012
04013 ExprBoundInfo boundInfo(bound, assertExpr);
04014
04015
04016 Expr rightSide = assertExpr[1];
04017
04018
04019 int kind = assertExpr.getKind();
04020
04021
04022 DebugAssert(kind == LT || kind == LE || kind == GT || kind == GE , "TheoryArithNew::propagateTheory : expected an inequality");
04023
04024
04025 if (kind == LT || kind == LE) {
04026
04027 BoundInfoSet::iterator find = allBounds.lower_bound(boundInfo);
04028 BoundInfoSet::iterator find_end = allBounds.lower_bound(ExprBoundInfo(oldBound, assertExpr));
04029
04030
04031 if (find == find_end) return;
04032
04033
04034 while (find != find_end) {
04035
04036
04037 -- find;
04038
04039
04040 const Expr& findExpr = (*find).e;
04041
04042
04043 const EpsRational findRat = (*find).bound;
04044
04045
04046 int findExprKind = findExpr.getKind();
04047
04048
04049 if (rightSide != findExpr[1]) break;
04050
04051
04052 Theorem lemma;
04053
04054
04055 if (findExprKind == LT || findExprKind == LE)
04056
04057 lemma = d_rules->implyWeakerInequality(assertExpr, findExpr);
04058 else
04059
04060 lemma = d_rules->implyNegatedInequality(assertExpr, findExpr);
04061
04062
04063 TRACE("propagate_arith", "lemma ==>", lemma.toString(), "");
04064 TRACE("arith_atoms", "Propagate: ", lemma.getExpr().toString(), "");
04065
04066
04067 enqueueFact(lemma);
04068 }
04069 }
04070
04071 else {
04072
04073 BoundInfoSet::iterator find = allBounds.upper_bound(boundInfo);
04074 BoundInfoSet::iterator find_end = allBounds.upper_bound(ExprBoundInfo(oldBound, assertExpr));
04075
04076
04077 while (find != find_end) {
04078
04079
04080 const EpsRational findRat = (*find).bound;
04081
04082
04083 const Expr& findExpr = (*find).e;
04084 int findExprKind = findExpr.getKind();
04085
04086
04087 if (rightSide != findExpr[1]) break;
04088
04089
04090 Theorem lemma;
04091
04092
04093 if (findExprKind == GT || findExprKind == GE)
04094
04095 lemma = d_rules->implyWeakerInequality(assertExpr, findExpr);
04096 else
04097
04098 lemma = d_rules->implyNegatedInequality(assertExpr, findExpr);
04099
04100 TRACE("propagate_arith", "lemma ==>", lemma.toString(), "");
04101 TRACE("arith_atoms", "Propagate: ", lemma.getExpr().toString(), "");
04102
04103
04104 enqueueFact(lemma);
04105
04106
04107 ++ find;
04108 }
04109 }
04110 }
04111
04112 Theorem TheoryArithNew::deriveGomoryCut(const Expr& x_i) {
04113
04114 Theorem res;
04115
04116
04117 DebugAssert(isBasic(x_i), "TheoryArithNew::deriveGomoryCut variable must be a basic variable : " + x_i.toString());
04118 DebugAssert(intVariables.count(x_i) > 0, "TheoryArithNew::deriveGomoryCut variable must be a basic variable : " + x_i.toString());
04119
04120
04121 Rational x_i_Value = getBeta(x_i).getRational();
04122
04123
04124 Rational f_0 = x_i_Value - floor(x_i_Value);
04125
04126 return res;
04127 }