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_old.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 TheoryArithOld::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 TheoryArithOld::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 TheoryArithOld::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 TheoryArithOld::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 const Rational& TheoryArithOld::freeConstIneq(const Expr& ineq, bool varOnRHS) {
00094 DebugAssert(isIneq(ineq), "TheoryArithOld::freeConstIneq("+ineq.toString()+")");
00095 const Expr& e = varOnRHS? ineq[0] : ineq[1];
00096
00097 switch(e.getKind()) {
00098 case PLUS:
00099 return e[0].getRational();
00100 case RATIONAL_EXPR:
00101 return e.getRational();
00102 default: {
00103 static Rational zero(0);
00104 return zero;
00105 }
00106 }
00107 }
00108
00109
00110 const TheoryArithOld::FreeConst&
00111 TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00112 bool& subsumed) {
00113 TRACE("arith ineq", "TheoryArithOld::updateSubsumptionDB(", ineq,
00114 ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
00115 DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArithOld::updateSubsumptionDB("
00116 +ineq.toString()+")");
00117
00118 Expr index;
00119 const Expr& t = varOnRHS? ineq[0] : ineq[1];
00120 bool strict(isLT(ineq));
00121 Rational c(0);
00122 if(isPlus(t)) {
00123 DebugAssert(t.arity() >= 2, "TheoryArithOld::updateSubsumptionDB("
00124 +ineq.toString()+")");
00125 c = t[0].getRational();
00126 Expr newT;
00127 if(t.arity() == 2) {
00128 newT = t[1];
00129 } else {
00130 vector<Expr> kids;
00131 Expr::iterator i=t.begin(), iend=t.end();
00132 for(++i; i!=iend; ++i) kids.push_back(*i);
00133 DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
00134 +", ineq = "+ineq.toString());
00135 newT = plusExpr(kids);
00136 }
00137 if(varOnRHS)
00138 index = leExpr(newT, ineq[1]);
00139 else
00140 index = leExpr(ineq[0], newT);
00141 } else if(isRational(t)) {
00142 c = t.getRational();
00143 if(varOnRHS)
00144 index = leExpr(rat(0), ineq[1]);
00145 else
00146 index = leExpr(ineq[0], rat(0));
00147 } else if(isLT(ineq))
00148 index = leExpr(ineq[0], ineq[1]);
00149 else
00150 index = ineq;
00151
00152 CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index),
00153 iend=d_freeConstDB.end();
00154 if(i == iend) {
00155 subsumed = false;
00156
00157 CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
00158 obj = FreeConst(c,strict);
00159 TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
00160 return obj.get();
00161 } else {
00162 CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
00163 const FreeConst& fc = obj.get();
00164 if(varOnRHS) {
00165 subsumed = (c < fc.getConst() ||
00166 (c == fc.getConst() && (!strict || fc.strict())));
00167 } else {
00168 subsumed = (c > fc.getConst() ||
00169 (c == fc.getConst() && (strict || !fc.strict())));
00170 }
00171 if(!subsumed) {
00172 obj = FreeConst(c,strict);
00173 TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
00174 }
00175 return obj.get();
00176 }
00177 }
00178
00179
00180 bool TheoryArithOld::kidsCanonical(const Expr& e) {
00181 if(isLeaf(e)) return true;
00182 bool res(true);
00183 for(int i=0; res && i<e.arity(); ++i) {
00184 Expr simp(canon(e[i]).getRHS());
00185 res = (e[i] == simp);
00186 IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
00187 << "\nsimplified = " << simp << endl);
00188 }
00189 return res;
00190 }
00191
00192
00193
00194
00195
00196
00197
00198
00199
00200
00201
00202
00203
00204
00205
00206
00207
00208
00209
00210
00211
00212 Theorem TheoryArithOld::canon(const Expr& e)
00213 {
00214 TRACE("arith canon","canon(",e,") {");
00215 DebugAssert(kidsCanonical(e), "TheoryArithOld::canon("+e.toString()+")");
00216 Theorem result;
00217 switch (e.getKind()) {
00218 case UMINUS: {
00219 Theorem thm = d_rules->uMinusToMult(e[0]);
00220 Expr e2 = thm.getRHS();
00221 result = transitivityRule(thm, canon(e2));
00222 }
00223 break;
00224 case PLUS:
00225
00226
00227
00228
00229
00230
00231 result = d_rules->canonPlus(e);
00232 break;
00233 case MINUS: {
00234 DebugAssert(e.arity() == 2,"");
00235 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
00236
00237 Expr sum(minus_eq_sum.getRHS());
00238 Theorem thm(canon(sum[1]));
00239 if(thm.getLHS() == thm.getRHS())
00240 result = canonThm(minus_eq_sum);
00241
00242 else {
00243 vector<unsigned> changed;
00244 vector<Theorem> thms;
00245 changed.push_back(1);
00246 thms.push_back(thm);
00247 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
00248 result = transitivityRule(minus_eq_sum, sum_eq_canon);
00249 }
00250 break;
00251 }
00252
00253 case MULT:
00254 result = d_rules->canonMult(e);
00255 break;
00256
00257
00258
00259
00260
00261
00262
00263
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273
00274
00275
00276
00277
00278
00279
00280
00281
00282
00283
00284
00285
00286
00287
00288
00289
00290
00291
00292
00293
00294
00295
00296
00297
00298
00299
00300
00301
00302
00303
00304
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314
00315
00316
00317 case DIVIDE:{
00318
00319
00320
00321
00322
00323
00324
00325
00326
00327
00328
00329
00330
00331
00332
00333
00334
00335
00336
00337
00338
00339 if (e[1].getKind() == PLUS)
00340 throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
00341 result = d_rules->canonDivide(e);
00342 break;
00343 }
00344 case POW:
00345 if(e[1].isRational())
00346 result = d_rules->canonPowConst(e);
00347 else
00348 result = reflexivityRule(e);
00349 break;
00350 default:
00351 result = reflexivityRule(e);
00352 break;
00353 }
00354 TRACE("arith canon","canon => ",result," }");
00355 return result;
00356 }
00357
00358
00359 Theorem
00360 TheoryArithOld::canonSimplify(const Expr& e) {
00361 TRACE("arith", "canonSimplify(", e, ") {");
00362 DebugAssert(kidsCanonical(e),
00363 "TheoryArithOld::canonSimplify("+e.toString()+")");
00364 DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
00365 Expr tmp(e);
00366 Theorem thm = canon(e);
00367 if(thm.getRHS().hasFind())
00368 thm = transitivityRule(thm, find(thm.getRHS()));
00369
00370 DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
00371 "canonSimplify("+e.toString()+")\n"
00372 +"canon(e) = "+thm.getRHS().toString()
00373 +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
00374
00375
00376
00377
00378
00379
00380
00381
00382 TRACE("arith", "canonSimplify =>", thm, " }");
00383 return thm;
00384 }
00385
00386
00387
00388
00389 Theorem
00390 TheoryArithOld::canonPred(const Theorem& thm) {
00391 vector<Theorem> thms;
00392 DebugAssert(thm.getExpr().arity() == 2,
00393 "TheoryArithOld::canonPred: bad theorem: "+thm.toString());
00394 Expr e(thm.getExpr());
00395 thms.push_back(canonSimplify(e[0]));
00396 thms.push_back(canonSimplify(e[1]));
00397 return iffMP(thm, substitutivityRule(e.getOp(), thms));
00398 }
00399
00400
00401
00402
00403 Theorem
00404 TheoryArithOld::canonPredEquiv(const Theorem& thm) {
00405 vector<Theorem> thms;
00406 DebugAssert(thm.getRHS().arity() == 2,
00407 "TheoryArithOld::canonPredEquiv: bad theorem: "+thm.toString());
00408 Expr e(thm.getRHS());
00409 thms.push_back(canonSimplify(e[0]));
00410 thms.push_back(canonSimplify(e[1]));
00411 return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
00412 }
00413
00414
00415
00416
00417
00418 Theorem
00419 TheoryArithOld::canonConjunctionEquiv(const Theorem& thm) {
00420 vector<Theorem> thms;
00421 return thm;
00422 }
00423
00424
00425
00426
00427
00428
00429
00430
00431
00432 Theorem TheoryArithOld::doSolve(const Theorem& thm)
00433 {
00434 const Expr& e = thm.getExpr();
00435 TRACE("arith eq","doSolve(",e,") {");
00436 DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
00437 Theorem eqnThm;
00438 vector<Theorem> thms;
00439
00440 if(e[0].isRational() && e[0].getRational() == 0)
00441 eqnThm = thm;
00442 else {
00443 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
00444 eqnThm = canonPred(eqnThm);
00445 }
00446
00447
00448 Expr right = eqnThm.getRHS();
00449
00450 if (right.isRational()) {
00451 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
00452 TRACE("arith eq","doSolve => ",result," }");
00453 return result;
00454 }
00455
00456
00457 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
00458 right = eqnThm.getRHS();
00459
00460
00461
00462 if(!isInteger(right)) {
00463 Theorem res;
00464 try {
00465 res = processRealEq(eqnThm);
00466 } catch(ArithException& e) {
00467 res = symmetryRule(eqnThm);
00468 TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
00469 IF_DEBUG(debugger.counter("FAILED to solve real equalities")++);
00470 setIncomplete("Non-linear arithmetic inequalities");
00471 }
00472 IF_DEBUG(debugger.counter("solved real equalities")++);
00473 TRACE("arith eq", "doSolve [real] => ", res, " }");
00474 return res;
00475 }
00476 else {
00477 Theorem res = processIntEq(eqnThm);
00478 IF_DEBUG(debugger.counter("solved int equalities")++);
00479 TRACE("arith eq", "doSolve [int] => ", res, " }");
00480 return res;
00481 }
00482 }
00483
00484
00485
00486
00487
00488 Expr
00489 TheoryArithOld::pickIntEqMonomial(const Expr& right)
00490 {
00491 DebugAssert(isPlus(right) && right.arity() > 2,
00492 "TheoryArithOld::pickIntEqMonomial right is wrong :-): " +
00493 right.toString());
00494 DebugAssert(right[0].isRational(),
00495 "TheoryArithOld::pickIntEqMonomial. right[0] must be const" +
00496 right.toString());
00497 DebugAssert(isInteger(right),
00498 "TheoryArithOld::pickIntEqMonomial: right is of type int: " +
00499 right.toString());
00500
00501
00502 Expr::iterator i = right.begin();
00503 i++;
00504 Rational min = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00505 Expr pickedMon = *i;
00506 for(Expr::iterator iend = right.end(); i != iend; ++i) {
00507 Rational coeff = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00508 if(min > coeff) {
00509 min = coeff;
00510 pickedMon = *i;
00511 }
00512 }
00513 return pickedMon;
00514 }
00515
00516
00517
00518
00519
00520 Theorem
00521 TheoryArithOld::processRealEq(const Theorem& eqn)
00522 {
00523 Expr right = eqn.getRHS();
00524
00525
00526
00527
00528
00529
00530
00531
00532
00533 bool found = false;
00534
00535 Expr left;
00536
00537 if (isPlus(right)) {
00538 for(int i = right.arity()-1; i>=0; --i) {
00539 Expr c = right[i];
00540 if(isRational(c))
00541 continue;
00542 if(!isInteger(c)) {
00543 if (isLeaf(c) ||
00544 ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
00545 int numoccurs = 0;
00546 Expr leaf = isLeaf(c) ? c : c[1];
00547 for (int j = 0; j < right.arity(); ++j) {
00548 if (j!= i
00549 && isLeafIn(leaf, right[j])
00550
00551 ) {
00552 numoccurs++;
00553 break;
00554 }
00555 }
00556 if (!numoccurs) {
00557 left = c;
00558 found = true;
00559 break;
00560 }
00561 }
00562 }
00563 }
00564 }
00565 else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
00566 isLeaf(right)) {
00567 left = right;
00568 found = true;
00569 }
00570
00571 if (!found) {
00572
00573
00574 throw
00575 ArithException("Can't find a leaf for solve in "+eqn.toString());
00576 }
00577
00578 Rational r = -1;
00579 if (isMult(left)) {
00580 DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
00581 DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
00582 r = -1/left[0].getRational();
00583 left = left[1];
00584 }
00585
00586 DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
00587 "TheoryArithOld::ProcessRealEq: left is integer:\n left = "
00588 +left.toString());
00589
00590
00591 Theorem result(iffMP(eqn,
00592 d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
00593 result = canonPred(result);
00594
00595
00596 result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
00597 result.getRHS(), left, EQ));
00598 result = canonPred(result);
00599 TRACE("arith","processRealEq => ",result," }");
00600 return result;
00601 }
00602
00603
00604
00605
00606
00607 Theorem
00608 TheoryArithOld::processSimpleIntEq(const Theorem& eqn)
00609 {
00610 TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
00611 DebugAssert(eqn.isRewrite(),
00612 "TheoryArithOld::processSimpleIntEq: eqn must be equality" +
00613 eqn.getExpr().toString());
00614
00615 Expr right = eqn.getRHS();
00616
00617 DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
00618 "TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" +
00619 eqn.getExpr().toString());
00620
00621
00622 if(isMult(right)) {
00623
00624 Expr c,x;
00625 separateMonomial(right, c, x);
00626 Theorem isIntx(isIntegerThm(x));
00627 DebugAssert(!isIntx.isNull(), "right = "+right.toString());
00628 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00629 TRACE("arith eq", "processSimpleIntEq[0 = a*x] => ", res, " }");
00630 return res;
00631 } else if(isPlus(right)) {
00632 if(2 == right.arity()) {
00633
00634 Expr c,x;
00635 separateMonomial(right[1], c, x);
00636 Theorem isIntx(isIntegerThm(x));
00637 DebugAssert(!isIntx.isNull(), "right = "+right.toString()
00638 +"\n x = "+x.toString());
00639 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00640 TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
00641 return res;
00642 }
00643 DebugAssert(right.arity() > 2,
00644 "TheoryArithOld::processSimpleIntEq: RHS is not in correct form:"
00645 +eqn.getExpr().toString());
00646
00647 Expr isolated = pickIntEqMonomial(right);
00648 TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
00649
00650
00651
00652
00653
00654 Rational r = isMult(isolated) ?
00655 ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
00656 Theorem result;
00657 if (-1 == r) {
00658
00659
00660 result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
00661 result = canonPred(result);
00662 Expr e = result.getRHS();
00663
00664
00665 result = iffMP(result,
00666 d_rules->plusPredicate(result.getLHS(),result.getRHS(),
00667 isolated, EQ));
00668 } else {
00669
00670 const Rational& minusa = isolated[0].getRational();
00671 Rational a = -1*minusa;
00672 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
00673
00674
00675 result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
00676 right,isolated,EQ));
00677 }
00678
00679 result = canonPred(result);
00680
00681
00682 if(!isMult(isolated) || isolated[0].getRational() == 1) {
00683 TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
00684 return result;
00685 } else {
00686 DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
00687 "TheoryArithOld::processSimpleIntEq: isolated must be mult "
00688 "with coeff >= 2.\n isolated = " + isolated.toString());
00689
00690
00691 Expr lhs = result.getLHS();
00692 Expr rhs = result.getRHS();
00693 Expr a, x;
00694 separateMonomial(lhs, a, x);
00695 Theorem isIntLHS = isIntegerThm(x);
00696 vector<Theorem> isIntRHS;
00697 if(!isPlus(rhs)) {
00698 Expr c, v;
00699 separateMonomial(rhs, c, v);
00700 isIntRHS.push_back(isIntegerThm(v));
00701 DebugAssert(!isIntRHS.back().isNull(), "");
00702 } else {
00703 DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
00704 DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
00705 Expr::iterator i=rhs.begin(), iend=rhs.end();
00706 ++i;
00707 for(; i!=iend; ++i) {
00708 Expr c, v;
00709 separateMonomial(*i, c, v);
00710 isIntRHS.push_back(isIntegerThm(v));
00711 DebugAssert(!isIntRHS.back().isNull(), "");
00712 }
00713 }
00714
00715 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
00716
00717 result = getCommonRules()->skolemize(result);
00718
00719 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00720 "processSimpleIntEq: result = "+result.getExpr().toString());
00721 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
00722 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
00723 Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
00724 if(newRes.getExpr() != result.getExpr()) result = newRes;
00725
00726 TRACE("arith eq", "processSimpleIntEq => ", result, " }");
00727 return result;
00728 }
00729 } else {
00730
00731 Theorem result = symmetryRule(eqn);
00732 TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
00733 return result;
00734 }
00735 }
00736
00737
00738
00739
00740
00741
00742 Theorem
00743 TheoryArithOld::processIntEq(const Theorem& eqn)
00744 {
00745 TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
00746
00747 std::vector<Theorem> solvedAndNewEqs;
00748 Theorem newEq(eqn), result;
00749 bool done(false);
00750 do {
00751 result = processSimpleIntEq(newEq);
00752
00753 if(result.isRewrite()) {
00754 solvedAndNewEqs.push_back(result);
00755 done = true;
00756 }
00757 else if(!result.getExpr().isFalse()) {
00758 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00759 "TheoryArithOld::processIntEq("+eqn.getExpr().toString()
00760 +")\n result = "+result.getExpr().toString());
00761 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
00762 newEq = getCommonRules()->andElim(result, 1);
00763 } else
00764 done = true;
00765 } while(!done);
00766 Theorem res;
00767 if(result.getExpr().isFalse()) res = result;
00768 else res = solvedForm(solvedAndNewEqs);
00769 TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
00770 return res;
00771 }
00772
00773
00774
00775
00776
00777
00778
00779
00780
00781 Theorem
00782 TheoryArithOld::solvedForm(const vector<Theorem>& solvedEqs)
00783 {
00784 DebugAssert(solvedEqs.size() > 0, "TheoryArithOld::solvedForm()");
00785
00786
00787 TRACE_MSG("arith eq", "TheoryArithOld::solvedForm:solvedEqs(\n [");
00788 IF_DEBUG(if(debugger.trace("arith eq")) {
00789 for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
00790 jend=solvedEqs.end(); j!=jend;++j)
00791 TRACE("arith eq", "", j->getExpr(), ",\n ");
00792 });
00793 TRACE_MSG("arith eq", " ]) {");
00794
00795
00796 vector<Theorem>::const_reverse_iterator
00797 i = solvedEqs.rbegin(),
00798 iend = solvedEqs.rend();
00799
00800
00801 ExprMap<Theorem> subst;
00802 for(; i!=iend; ++i) {
00803 if(i->isRewrite()) {
00804 Theorem thm = substAndCanonize(*i, subst);
00805 TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
00806 thm.getExpr(), "");
00807 subst[i->getLHS()] = thm;
00808 }
00809 else {
00810
00811 DebugAssert(i->getExpr().isFalse(),
00812 "TheoryArithOld::solvedForm: an element of solvedEqs must "
00813 "be either EQ or FALSE: "+i->toString());
00814 return *i;
00815 }
00816 }
00817
00818
00819 vector<Theorem> thms;
00820 for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
00821 i!=iend; ++i)
00822 thms.push_back(i->second);
00823 return getCommonRules()->andIntro(thms);
00824 }
00825
00826
00827
00828
00829
00830
00831
00832
00833 Theorem
00834 TheoryArithOld::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
00835 {
00836 TRACE("arith eq", "substAndCanonize(", t, ") {");
00837
00838 if(subst.empty()) {
00839 Theorem res(reflexivityRule(t));
00840 TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
00841 return res;
00842 }
00843
00844 ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
00845 if(i!=iend) {
00846 TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
00847 return i->second;
00848 }
00849
00850 if(isLeaf(t)) {
00851 Theorem res(reflexivityRule(t));
00852 TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
00853 return res;
00854 }
00855
00856 vector<Theorem> thms;
00857 vector<unsigned> changed;
00858 for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
00859 Theorem thm = substAndCanonize(t[j], subst);
00860 if(thm.getRHS() != t[j]) {
00861 thm = canonThm(thm);
00862 thms.push_back(thm);
00863 changed.push_back(j);
00864 }
00865 }
00866
00867 Theorem res;
00868 if(thms.size() > 0) {
00869 res = substitutivityRule(t, changed, thms);
00870 res = canonThm(res);
00871 }
00872 else
00873 res = reflexivityRule(t);
00874 TRACE("arith eq", "substAndCanonize => ", res, " }");
00875 return res;
00876 }
00877
00878
00879
00880
00881
00882
00883
00884 Theorem
00885 TheoryArithOld::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
00886 {
00887
00888 if(subst.empty()) return eq;
00889
00890 DebugAssert(eq.isRewrite(), "TheoryArithOld::substAndCanonize: t = "
00891 +eq.getExpr().toString());
00892 const Expr& t = eq.getRHS();
00893
00894 Theorem thm = substAndCanonize(t, subst);
00895
00896 if(thm.getRHS() == t) return eq;
00897
00898 vector<Theorem> thms;
00899 vector<unsigned> changed;
00900 thms.push_back(thm);
00901 changed.push_back(1);
00902 return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
00903 }
00904
00905
00906 void TheoryArithOld::processBuffer()
00907 {
00908
00909 bool varOnRHS;
00910 for(; !inconsistent() && d_bufferIdx < d_buffer.size();
00911 d_bufferIdx = d_bufferIdx+1) {
00912 const Theorem& ineqThm = d_buffer[d_bufferIdx];
00913
00914 if(isStale(ineqThm.getExpr())) continue;
00915 Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
00916 const Expr& ineq = thm1.getExpr();
00917 if((ineq).isFalse())
00918 setInconsistent(thm1);
00919 else if(!ineq.isTrue()) {
00920
00921 DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]),
00922 "TheoryArithOld::processBuffer(): bad result from "
00923 "isolateVariable:\nineq = "+ineq.toString());
00924
00925 projectInequalities(thm1, varOnRHS);
00926 }
00927 }
00928 }
00929
00930
00931 void TheoryArithOld::updateStats(const Rational& c, const Expr& v)
00932 {
00933 TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
00934 if(c > 0) {
00935 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
00936 else d_countRight[v] = 1;
00937 }
00938 else
00939 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
00940 else d_countLeft[v] = 1;
00941 }
00942
00943
00944 void TheoryArithOld::updateStats(const Expr& monomial)
00945 {
00946 Expr c, m;
00947 separateMonomial(monomial, c, m);
00948 updateStats(c.getRational(), m);
00949 }
00950
00951
00952 void TheoryArithOld::addToBuffer(const Theorem& thm) {
00953
00954
00955 Theorem result(thm);
00956 const Expr& e = thm.getExpr();
00957
00958 if(!(e[0].isRational() && e[0].getRational() == 0)) {
00959 result = iffMP(result, d_rules->rightMinusLeft(e));
00960 result = canonPred(result);
00961 }
00962 TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
00963
00964 d_buffer.push_back(thm);
00965
00966
00967 const Expr& rhs = thm.getExpr()[1];
00968 if(isPlus(rhs))
00969 for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
00970 updateStats(*i);
00971 else
00972 updateStats(rhs);
00973 }
00974
00975
00976 Theorem TheoryArithOld::isolateVariable(const Theorem& inputThm,
00977 bool& isolatedVarOnRHS)
00978 {
00979 Theorem result(inputThm);
00980 const Expr& e = inputThm.getExpr();
00981 TRACE("arith","isolateVariable(",e,") {");
00982 TRACE("arith ineq", "isolateVariable(", e, ") {");
00983
00984 DebugAssert(isLT(e)||isLE(e),
00985 "TheoryArithOld::isolateVariable: " + e.toString() +
00986 " wrong kind");
00987 int kind = e.getKind();
00988 DebugAssert(e[0].isRational() && e[0].getRational() == 0,
00989 "TheoryArithOld::isolateVariable: theorem must be of "
00990 "the form 0 < rhs: " + inputThm.toString());
00991
00992 const Expr& zero = e[0];
00993 Expr right = e[1];
00994
00995 if (right.isRational()) {
00996 result = iffMP(result, d_rules->constPredicate(e));
00997 TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
00998 TRACE("arith","isolateVariable => ",result," }");
00999 return result;
01000 }
01001
01002
01003
01004
01005 Expr factor(computeNormalFactor(right));
01006 TRACE("arith", "isolateVariable: factor = ", factor, "");
01007 DebugAssert(factor.getRational() > 0,
01008 "isolateVariable: factor="+factor.toString());
01009
01010 if(factor.getRational() != 1) {
01011 result = iffMP(result, d_rules->multIneqn(e, factor));
01012
01013 result = canonPred(result);
01014 right = result.getExpr()[1];
01015 }
01016
01017
01018 Expr isolatedMonomial = right;
01019
01020 if (isPlus(right))
01021 isolatedMonomial = pickMonomial(right);
01022
01023 Rational r = -1;
01024 isolatedVarOnRHS = true;
01025 if (isMult(isolatedMonomial)) {
01026 r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
01027 isolatedVarOnRHS =
01028 ((isolatedMonomial[0].getRational()) >= 0)? true : false;
01029 }
01030 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
01031
01032 result = iffMP(result, d_rules->plusPredicate(zero, right,
01033 isolatedMonomial, kind));
01034
01035 result = canonPred(result);
01036 if(1 != r) {
01037 result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
01038 result = canonPred(result);
01039 }
01040 TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
01041 TRACE("arith","isolateVariable => ",result," }");
01042 return result;
01043 }
01044
01045 Expr
01046 TheoryArithOld::computeNormalFactor(const Expr& right) {
01047
01048
01049 Rational factor;
01050 if(isPlus(right)) {
01051 vector<Rational> nums, denoms;
01052 for(int i=0, iend=right.arity(); i<iend; ++i) {
01053 switch(right[i].getKind()) {
01054 case RATIONAL_EXPR: {
01055 Rational c(abs(right[i].getRational()));
01056 nums.push_back(c.getNumerator());
01057 denoms.push_back(c.getDenominator());
01058 break;
01059 }
01060 case MULT: {
01061 Rational c(abs(right[i][0].getRational()));
01062 nums.push_back(c.getNumerator());
01063 denoms.push_back(c.getDenominator());
01064 break;
01065 }
01066 default:
01067 nums.push_back(1);
01068 denoms.push_back(1);
01069 break;
01070 }
01071 }
01072 Rational gcd_nums = gcd(nums);
01073
01074
01075
01076
01077 factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
01078 } else if(isMult(right)) {
01079 const Rational& r = right[0].getRational();
01080 factor = (r==0)? 0 : (1/abs(r));
01081 }
01082 else
01083 factor = 1;
01084 return rat(factor);
01085 }
01086
01087
01088 bool TheoryArithOld::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
01089 {
01090 DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
01091 "TheoryArithOld::findMaxVar: isolatedMonomial cannot be rational" +
01092 isolatedMonomial.toString());
01093 Expr c, var0, var1;
01094 separateMonomial(isolatedMonomial, c, var0);
01095 separateMonomial(var2, c, var1);
01096 return var0 < var1;
01097 }
01098
01099
01100
01101
01102
01103
01104 bool TheoryArithOld::isStale(const Expr& e) {
01105 if(e.isTerm())
01106 return e != find(e).getRHS();
01107
01108
01109 bool stale=false;
01110 for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
01111 stale = isStale(*i);
01112 return stale;
01113 }
01114
01115
01116 bool TheoryArithOld::isStale(const TheoryArithOld::Ineq& ineq) {
01117 TRACE("arith ineq", "isStale(", ineq, ") {");
01118 const Expr& ineqExpr = ineq.ineq().getExpr();
01119 const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
01120 bool strict(isLT(ineqExpr));
01121 const FreeConst& fc = ineq.getConst();
01122
01123 bool subsumed;
01124
01125 if(ineq.varOnRHS()) {
01126 subsumed = (c < fc.getConst() ||
01127 (c == fc.getConst() && !strict && fc.strict()));
01128 } else {
01129 subsumed = (c > fc.getConst() ||
01130 (c == fc.getConst() && strict && !fc.strict()));
01131 }
01132
01133 bool res;
01134 if(subsumed) {
01135 res = true;
01136 TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
01137 }
01138 else {
01139 res = isStale(ineqExpr);
01140 TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
01141 }
01142 return res;
01143 }
01144
01145
01146 void TheoryArithOld::separateMonomial(const Expr& e, Expr& c, Expr& var) {
01147 TRACE("separateMonomial", "separateMonomial(", e, ")");
01148 DebugAssert(!isPlus(e),
01149 "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
01150 if(isMult(e)) {
01151 DebugAssert(e.arity() >= 2,
01152 "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
01153 c = e[0];
01154 if(e.arity() == 2) var = e[1];
01155 else {
01156 vector<Expr> kids = e.getKids();
01157 kids[0] = rat(1);
01158 var = multExpr(kids);
01159 }
01160 } else {
01161 c = rat(1);
01162 var = e;
01163 }
01164 DebugAssert(c.isRational(), "TheoryArithOld::separateMonomial(e = "
01165 +e.toString()+", c = "+c.toString()+")");
01166 DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
01167 "TheoryArithOld::separateMonomial(e = "
01168 +e.toString()+", var = "+var.toString()+")");
01169 }
01170
01171
01172 void TheoryArithOld::projectInequalities(const Theorem& theInequality,
01173 bool isolatedVarOnRHS)
01174 {
01175 TRACE("arith ineq", "projectInequalities(", theInequality.getExpr(),
01176 ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
01177 +") {");
01178 DebugAssert(isLE(theInequality.getExpr()) ||
01179 isLT(theInequality.getExpr()),
01180 "TheoryArithOld::projectIsolatedVar: "\
01181 "theInequality is of the wrong form: " +
01182 theInequality.toString());
01183
01184
01185 Theorem theIneqThm(theInequality);
01186 Expr theIneq = theIneqThm.getExpr();
01187
01188 Theorem isIntLHS(isIntegerThm(theIneq[0]));
01189 Theorem isIntRHS(isIntegerThm(theIneq[1]));
01190 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
01191
01192 if(isLT(theIneq) && isInt) {
01193 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
01194 !isolatedVarOnRHS);
01195 theIneqThm = canonPred(iffMP(theIneqThm, thm));
01196 theIneq = theIneqThm.getExpr();
01197 }
01198 Expr isolatedMonomial =
01199 isolatedVarOnRHS ? theIneq[1] : theIneq[0];
01200
01201 Expr monomialVar, a;
01202 separateMonomial(isolatedMonomial, a, monomialVar);
01203
01204 bool subsumed;
01205 const FreeConst& bestConst =
01206 updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
01207
01208 if(subsumed) {
01209 IF_DEBUG(debugger.counter("subsumed inequalities")++);
01210 TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
01211 } else {
01212
01213
01214 if(isMult(monomialVar) || isPow(monomialVar))
01215 setIncomplete("Non-linear arithmetic inequalities");
01216
01217
01218
01219
01220
01221 theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
01222 theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
01223
01224 ExprMap<CDList<Ineq> *>& db1 =
01225 isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
01226 ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
01227 if(it1 == db1.end()) {
01228 CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
01229 list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01230 db1[monomialVar] = list;
01231 }
01232 else
01233 ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01234
01235 ExprMap<CDList<Ineq> *>& db2 =
01236 isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
01237 ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
01238 if(it == db2.end()) {
01239 TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
01240 return;
01241 }
01242
01243 CDList<Ineq>& listOfDBIneqs = *((*it).second);
01244 Theorem betaLTt, tLTalpha, thm;
01245 for(size_t i = 0, iend=listOfDBIneqs.size(); i!=iend; ++i) {
01246 const Ineq& ineqEntry = listOfDBIneqs[i];
01247 const Theorem& ineqThm = ineqEntry.ineq();
01248 if(!isStale(ineqEntry)) {
01249 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
01250 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
01251 thm = normalizeProjectIneqs(betaLTt, tLTalpha);
01252
01253 IF_DEBUG(debugger.counter("real shadows")++);
01254
01255
01256 Expr e(thm.getExpr()); if(e.isFalse()) {
01257 setInconsistent(thm);
01258 TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
01259 return;
01260 }
01261 else {
01262 if(!e.isTrue() && !e.isEq())
01263 addToBuffer(thm);
01264 else if(e.isEq())
01265 enqueueFact(thm);
01266 }
01267 } else {
01268 IF_DEBUG(debugger.counter("stale inequalities")++);
01269 }
01270 }
01271 }
01272 TRACE_MSG("arith ineq", "projectInequalities => }");
01273 }
01274
01275 Theorem TheoryArithOld::normalizeProjectIneqs(const Theorem& ineqThm1,
01276 const Theorem& ineqThm2)
01277 {
01278
01279
01280 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
01281 Expr ineq1 = betaLTt.getExpr();
01282 Expr ineq2 = tLTalpha.getExpr();
01283 Expr c,x;
01284 separateMonomial(ineq2[0], c, x);
01285 Theorem isIntx(isIntegerThm(x));
01286 Theorem isIntBeta(isIntegerThm(ineq1[0]));
01287 Theorem isIntAlpha(isIntegerThm(ineq2[1]));
01288 bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
01289
01290 TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
01291 ", "+ineq2.toString()+") {");
01292 DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
01293 (isLE(ineq2) || isLT(ineq2)),
01294 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
01295 ineq1.toString() + ineq2.toString());
01296 DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
01297 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
01298 ineq1.toString() + ineq2.toString());
01299
01300
01301
01302 Rational factor1 = 1, factor2 = 1;
01303 Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
01304 Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
01305 if(b != a) {
01306 factor1 = a;
01307 factor2 = b;
01308 }
01309
01310
01311
01312
01313
01314
01315
01316 if(isInt && (a >= 2 || b >= 2)) {
01317 Theorem intResult;
01318 if(a <= b)
01319 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
01320 isIntAlpha, isIntBeta, isIntx);
01321 else
01322 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
01323 isIntAlpha, isIntBeta, isIntx);
01324 enqueueFact(intResult);
01325
01326 DebugAssert(intResult.getExpr().isAnd() && intResult.getExpr().arity()==2,
01327 "intResult = "+intResult.getExpr().toString());
01328 const Expr& DorG = intResult.getExpr()[0];
01329 DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
01330 const Expr& D = DorG[0];
01331 const Expr& G = DorG[1];
01332 DebugAssert(D.getKind()==DARK_SHADOW, "D = "+D.toString());
01333 DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
01334
01335 Expr tmp = simplifyExpr(D);
01336 if (!tmp.isBoolConst())
01337 addSplitter(tmp, 5);
01338
01339 tmp = simplifyExpr(!G);
01340 if (!tmp.isBoolConst())
01341 addSplitter(tmp, 1);
01342 IF_DEBUG(debugger.counter("dark+gray shadows")++);
01343 }
01344
01345
01346 if(1 != factor1) {
01347 std::vector<Theorem> thms1;
01348 Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
01349 betaLTt = canonPred(thm2);
01350 ineq1 = betaLTt.getExpr();
01351 }
01352 if(1 != factor2) {
01353 std::vector<Theorem> thms1;
01354 Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
01355 tLTalpha = canonPred(thm2);
01356 ineq2 = tLTalpha.getExpr();
01357 }
01358
01359
01360
01361 Expr beta(ineq1[0]);
01362 Expr alpha(ineq2[1]);
01363
01364 if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
01365 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
01366 TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01367 return result;
01368 }
01369
01370
01371 if(isInt)
01372 processFiniteInterval(betaLTt, tLTalpha);
01373
01374
01375
01376 Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
01377
01378
01379
01380
01381
01382
01383 Expr e(result.getExpr());
01384
01385 if(!(e[0].isRational() && e[0].getRational() == 0)) {
01386 result = iffMP(result, d_rules->rightMinusLeft(e));
01387 result = canonPred(result);
01388 }
01389
01390
01391 Expr right = result.getExpr()[1];
01392
01393 if (right.isRational())
01394 result = iffMP(result, d_rules->constPredicate(result.getExpr()));
01395 TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01396 return result;
01397 }
01398
01399
01400 Expr TheoryArithOld::pickMonomial(const Expr& right)
01401 {
01402 DebugAssert(isPlus(right), "TheoryArithOld::pickMonomial: Wrong Kind: " +
01403 right.toString());
01404 if(theoryCore()->getFlags()["var-order"].getBool()) {
01405 Expr::iterator i = right.begin();
01406 Expr isolatedMonomial = right[1];
01407
01408
01409
01410 for(++i; i != right.end(); ++i)
01411 if(lessThanVar(isolatedMonomial,*i))
01412 isolatedMonomial = *i;
01413 return isolatedMonomial;
01414 }
01415 ExprMap<Expr> var2monomial;
01416 vector<Expr> vars;
01417 Expr::iterator i = right.begin(), iend = right.end();
01418 for(;i != iend; ++i) {
01419 if(i->isRational())
01420 continue;
01421 Expr c, var;
01422 separateMonomial(*i, c, var);
01423 var2monomial[var] = *i;
01424 vars.push_back(var);
01425 }
01426 vector<Expr> largest;
01427 d_graph.selectLargest(vars, largest);
01428 DebugAssert(0 < largest.size(),
01429 "TheoryArithOld::pickMonomial: selectLargest: failed!!!!");
01430 if(1 == largest.size())
01431 return var2monomial[largest[0] ];
01432 else {
01433 size_t pickedVar = 0;
01434
01435
01436 int minProjections(-1);
01437 for(size_t k=0; k< largest.size(); ++k) {
01438 const Expr& var(largest[k]), monom(var2monomial[var]);
01439
01440 int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
01441 int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
01442 int n(nRight*nLeft);
01443 TRACE("arith ineq", "pickMonomial: var=", var,
01444 ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
01445 if(minProjections < 0 || minProjections > n) {
01446 minProjections = n;
01447 pickedVar = k;
01448 }
01449 TRACE("arith ineq", "Number of projections for "+var.toString()+" = ",
01450 n, "");
01451 }
01452
01453 const Expr& largestVar = largest[pickedVar];
01454
01455
01456
01457
01458 for(size_t k = 0; k < largest.size(); ++k) {
01459 if(k != pickedVar)
01460 d_graph.addEdge(largestVar, largest[k]);
01461 }
01462 return var2monomial[largestVar];
01463 }
01464 }
01465
01466 void TheoryArithOld::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
01467 {
01468 TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
01469 DebugAssert(e1 != e2, "TheoryArithOld::VarOrderGraph::addEdge("
01470 +e1.toString()+", "+e2.toString()+")");
01471 d_edges[e1].push_back(e2);
01472 }
01473
01474
01475
01476 bool TheoryArithOld::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
01477 {
01478 d_cache.clear();
01479
01480 return dfs(e1,e2);
01481 }
01482
01483
01484 bool TheoryArithOld::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
01485 {
01486 if(e1 == e2)
01487 return true;
01488 if(d_cache.count(e2) > 0)
01489 return false;
01490 if(d_edges.count(e2) == 0)
01491 return false;
01492 d_cache[e2] = true;
01493 vector<Expr>& e2Edges = d_edges[e2];
01494 vector<Expr>::iterator i = e2Edges.begin();
01495 vector<Expr>::iterator iend = e2Edges.end();
01496
01497 for(; i != iend && !dfs(e1,*i); ++i);
01498 return (i != iend);
01499 }
01500
01501
01502 void TheoryArithOld::VarOrderGraph::selectSmallest(vector<Expr>& v1,
01503 vector<Expr>& v2)
01504 {
01505 int v1Size = v1.size();
01506 vector<bool> v3(v1Size);
01507 for(int j=0; j < v1Size; ++j)
01508 v3[j] = false;
01509
01510 for(int j=0; j < v1Size; ++j) {
01511 if(v3[j]) continue;
01512 for(int i =0; i < v1Size; ++i) {
01513 if((i == j) || v3[i])
01514 continue;
01515 if(lessThan(v1[i],v1[j])) {
01516 v3[j] = true;
01517 break;
01518 }
01519 }
01520 }
01521 vector<Expr> new_v1;
01522
01523 for(int j = 0; j < v1Size; ++j)
01524 if(!v3[j]) v2.push_back(v1[j]);
01525 else new_v1.push_back(v1[j]);
01526 v1 = new_v1;
01527 }
01528
01529
01530 void TheoryArithOld::VarOrderGraph::selectLargest(const vector<Expr>& v1,
01531 vector<Expr>& v2)
01532 {
01533 int v1Size = v1.size();
01534 vector<bool> v3(v1Size);
01535 for(int j=0; j < v1Size; ++j)
01536 v3[j] = false;
01537
01538 for(int j=0; j < v1Size; ++j) {
01539 if(v3[j]) continue;
01540 for(int i =0; i < v1Size; ++i) {
01541 if((i == j) || v3[i])
01542 continue;
01543 if(lessThan(v1[j],v1[i])) {
01544 v3[j] = true;
01545 break;
01546 }
01547 }
01548 }
01549
01550 for(int j = 0; j < v1Size; ++j)
01551 if(!v3[j]) v2.push_back(v1[j]);
01552 }
01553
01554
01555
01556
01557
01558
01559 TheoryArithOld::TheoryArithOld(TheoryCore* core)
01560 : TheoryArith(core, "ArithmeticOld"),
01561 d_diseq(core->getCM()->getCurrentContext()),
01562 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
01563 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
01564 d_freeConstDB(core->getCM()->getCurrentContext()),
01565 d_buffer(core->getCM()->getCurrentContext()),
01566
01567 d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
01568 d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
01569 d_countRight(core->getCM()->getCurrentContext()),
01570 d_countLeft(core->getCM()->getCurrentContext()),
01571 d_sharedTerms(core->getCM()->getCurrentContext()),
01572 d_sharedVars(core->getCM()->getCurrentContext())
01573 {
01574 IF_DEBUG(d_diseq.setName("CDList[TheoryArithOld::d_diseq]"));
01575 IF_DEBUG(d_buffer.setName("CDList[TheoryArithOld::d_buffer]"));
01576 IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArithOld::d_bufferIdx]"));
01577
01578 getEM()->newKind(REAL, "_REAL", true);
01579 getEM()->newKind(INT, "_INT", true);
01580 getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
01581
01582 getEM()->newKind(UMINUS, "_UMINUS");
01583 getEM()->newKind(PLUS, "_PLUS");
01584 getEM()->newKind(MINUS, "_MINUS");
01585 getEM()->newKind(MULT, "_MULT");
01586 getEM()->newKind(DIVIDE, "_DIVIDE");
01587 getEM()->newKind(POW, "_POW");
01588 getEM()->newKind(INTDIV, "_INTDIV");
01589 getEM()->newKind(MOD, "_MOD");
01590 getEM()->newKind(LT, "_LT");
01591 getEM()->newKind(LE, "_LE");
01592 getEM()->newKind(GT, "_GT");
01593 getEM()->newKind(GE, "_GE");
01594 getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
01595 getEM()->newKind(NEGINF, "_NEGINF");
01596 getEM()->newKind(POSINF, "_POSINF");
01597 getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
01598 getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
01599
01600 getEM()->newKind(REAL_CONST, "_REAL_CONST");
01601
01602 vector<int> kinds;
01603 kinds.push_back(REAL);
01604 kinds.push_back(INT);
01605 kinds.push_back(SUBRANGE);
01606 kinds.push_back(IS_INTEGER);
01607 kinds.push_back(UMINUS);
01608 kinds.push_back(PLUS);
01609 kinds.push_back(MINUS);
01610 kinds.push_back(MULT);
01611 kinds.push_back(DIVIDE);
01612 kinds.push_back(POW);
01613 kinds.push_back(INTDIV);
01614 kinds.push_back(MOD);
01615 kinds.push_back(LT);
01616 kinds.push_back(LE);
01617 kinds.push_back(GT);
01618 kinds.push_back(GE);
01619 kinds.push_back(RATIONAL_EXPR);
01620 kinds.push_back(NEGINF);
01621 kinds.push_back(POSINF);
01622 kinds.push_back(DARK_SHADOW);
01623 kinds.push_back(GRAY_SHADOW);
01624 kinds.push_back(REAL_CONST);
01625
01626 registerTheory(this, kinds, true);
01627
01628 d_rules = createProofRulesOld();
01629
01630 d_realType = Type(getEM()->newLeafExpr(REAL));
01631 d_intType = Type(getEM()->newLeafExpr(INT));
01632 }
01633
01634
01635
01636 TheoryArithOld::~TheoryArithOld() {
01637 if(d_rules != NULL) delete d_rules;
01638
01639 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
01640 iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
01641 delete (i->second);
01642 free(i->second);
01643 }
01644 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
01645 iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
01646 delete (i->second);
01647 free (i->second);
01648 }
01649 }
01650
01651 void TheoryArithOld::collectVars(const Expr& e, vector<Expr>& vars,
01652 set<Expr>& cache) {
01653
01654 if(cache.count(e) > 0) return;
01655
01656 cache.insert(e);
01657 if(isLeaf(e)) vars.push_back(e);
01658 else
01659 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01660 collectVars(*i, vars, cache);
01661 }
01662
01663 void
01664 TheoryArithOld::processFiniteInterval(const Theorem& alphaLEax,
01665 const Theorem& bxLEbeta) {
01666 const Expr& ineq1(alphaLEax.getExpr());
01667 const Expr& ineq2(bxLEbeta.getExpr());
01668 DebugAssert(isLE(ineq1), "TheoryArithOld::processFiniteInterval: ineq1 = "
01669 +ineq1.toString());
01670 DebugAssert(isLE(ineq2), "TheoryArithOld::processFiniteInterval: ineq2 = "
01671 +ineq2.toString());
01672
01673 if(!isInteger(ineq1[0])
01674 || !isInteger(ineq1[1])
01675 || !isInteger(ineq2[0])
01676 || !isInteger(ineq2[1]))
01677 return;
01678
01679 const Expr& ax = ineq1[1];
01680 const Expr& bx = ineq2[0];
01681 DebugAssert(!isPlus(ax) && !isRational(ax),
01682 "TheoryArithOld::processFiniteInterval:\n ax = "+ax.toString());
01683 DebugAssert(!isPlus(bx) && !isRational(bx),
01684 "TheoryArithOld::processFiniteInterval:\n bx = "+bx.toString());
01685 Expr a = isMult(ax)? ax[0] : rat(1);
01686 Expr b = isMult(bx)? bx[0] : rat(1);
01687
01688 Theorem thm1(alphaLEax), thm2(bxLEbeta);
01689
01690 if(a != b) {
01691 thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
01692 thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
01693 }
01694
01695 const Expr& alphaLEt = thm1.getExpr();
01696 const Expr& alpha = alphaLEt[0];
01697 const Expr& t = alphaLEt[1];
01698 const Expr& beta = thm2.getExpr()[1];
01699 Expr c = canon(beta - alpha).getRHS();
01700
01701 if(c.isRational() && c.getRational() >= 1) {
01702
01703
01704
01705 Theorem bEQac = symmetryRule(canon(alpha + c));
01706
01707 vector<unsigned> changed;
01708 vector<Theorem> thms;
01709 changed.push_back(1);
01710 thms.push_back(bEQac);
01711 Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
01712 tLEac = iffMP(thm2, tLEac);
01713
01714 Theorem isInta(isIntegerThm(alpha));
01715 Theorem isIntt(isIntegerThm(t));
01716 enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
01717 }
01718 }
01719
01720
01721 void
01722 TheoryArithOld::processFiniteIntervals(const Expr& x) {
01723
01724 if(!isInteger(x)) return;
01725
01726 ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
01727 iLeft = d_inequalitiesLeftDB.find(x);
01728 if(iLeft == d_inequalitiesLeftDB.end()) return;
01729 iRight = d_inequalitiesRightDB.find(x);
01730 if(iRight == d_inequalitiesRightDB.end()) return;
01731
01732 CDList<Ineq>& ineqsLeft = *(iLeft->second);
01733 CDList<Ineq>& ineqsRight = *(iRight->second);
01734
01735 size_t sizeLeft = ineqsLeft.size();
01736 size_t sizeRight = ineqsRight.size();
01737
01738 for(size_t l=0; l<sizeLeft; ++l)
01739 for(size_t r=0; r<sizeRight; ++r)
01740 processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
01741 }
01742
01743
01744
01745
01746
01747 void
01748 TheoryArithOld::setupRec(const Expr& e) {
01749 if(e.hasFind()) return;
01750
01751 for (int k = 0; k < e.arity(); ++k) {
01752 setupRec(e[k]);
01753 }
01754
01755 e.setFind(reflexivityRule(e));
01756
01757 setup(e);
01758 }
01759
01760
01761
01762
01763
01764
01765
01766
01767
01768
01769
01770
01771
01772
01773
01774
01775
01776
01777 void TheoryArithOld::addSharedTerm(const Expr& e) {
01778 d_sharedTerms[e] = true;
01779
01780
01781
01782
01783
01784
01785
01786
01787
01788
01789
01790
01791 }
01792
01793
01794 void TheoryArithOld::assertFact(const Theorem& e)
01795 {
01796 const Expr& expr = e.getExpr();
01797 if (expr.isNot() && expr[0].isEq()) {
01798 IF_DEBUG(debugger.counter("[arith] received disequalities")++);
01799 d_diseq.push_back(e);
01800 }
01801 else if (!expr.isEq()){
01802 if (expr.isNot()) {
01803
01804
01805
01806 }
01807 else if(isDarkShadow(expr)) {
01808 enqueueFact(d_rules->expandDarkShadow(e));
01809 IF_DEBUG(debugger.counter("received DARK_SHADOW")++);
01810 }
01811 else if(isGrayShadow(expr)) {
01812 IF_DEBUG(debugger.counter("received GRAY_SHADOW")++);
01813 const Rational& c1 = expr[2].getRational();
01814 const Rational& c2 = expr[3].getRational();
01815 const Expr& v = expr[0];
01816 const Expr& ee = expr[1];
01817 if(c1 == c2)
01818 enqueueFact(d_rules->expandGrayShadow0(e));
01819 else {
01820 Theorem gThm(e);
01821
01822 if(ee.isRational() && isMult(v)
01823 && v[0].isRational() && v[0].getRational() >= 2) {
01824 IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++);
01825 gThm = d_rules->grayShadowConst(e);
01826 }
01827
01828 const Expr& g = gThm.getExpr();
01829 if(g.isFalse())
01830 setInconsistent(gThm);
01831 else if(g[2].getRational() == g[3].getRational())
01832 enqueueFact(d_rules->expandGrayShadow0(gThm));
01833 else {
01834
01835 enqueueFact(d_rules->expandGrayShadow(gThm));
01836
01837 Theorem thm2 = d_rules->splitGrayShadow(gThm);
01838 enqueueFact(thm2);
01839
01840 DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
01841 "thm2 = "+thm2.getExpr().toString());
01842 const Expr& G1orG2 = thm2.getExpr()[0];
01843 DebugAssert(G1orG2.isOr() && G1orG2.arity()==2,
01844 "G1orG2 = "+G1orG2.toString());
01845 const Expr& G1 = G1orG2[0];
01846 const Expr& G2 = G1orG2[1];
01847 DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString());
01848 DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString());
01849
01850 Expr tmp = simplifyExpr(G1);
01851 if (!tmp.isBoolConst())
01852 addSplitter(tmp, 1);
01853 tmp = simplifyExpr(G2);
01854 if (!tmp.isBoolConst())
01855 addSplitter(tmp, -1);
01856 }
01857 }
01858 }
01859 else {
01860 DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr),
01861 "expected LE or LT: "+expr.toString());
01862 if(isLE(expr) || isLT(expr)) {
01863 IF_DEBUG(debugger.counter("recevied inequalities")++);
01864
01865
01866 Theorem thm;
01867 if (isLE(expr)) thm = d_rules->negatedInequality(!gtExpr(expr[0],expr[1]));
01868 else thm = d_rules->negatedInequality(!geExpr(expr[0],expr[1]));
01869 thm = symmetryRule(thm);
01870 Theorem thm2 = simplify(thm.getRHS()[0]);
01871 DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite");
01872 thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2);
01873 thm = transitivityRule(thm, thm2);
01874 enqueueFact(iffMP(e, thm));
01875
01876
01877 addToBuffer(e);
01878
01879 TRACE("arith ineq", "buffer.size() = ", d_buffer.size(),
01880 ", index="+int2string(d_bufferIdx)
01881 +", threshold="+int2string(*d_bufferThres));
01882
01883 if((((int)d_buffer.size()) - (int)d_bufferIdx > *d_bufferThres)
01884 && !d_inModelCreation)
01885 processBuffer();
01886 } else {
01887 IF_DEBUG(debugger.counter("arith IS_INTEGER")++);
01888 }
01889 }
01890 }
01891 else {
01892 IF_DEBUG(debugger.counter("[arith] received t1=t2")++);
01893 }
01894 }
01895
01896
01897 void TheoryArithOld::checkSat(bool fullEffort)
01898 {
01899
01900
01901
01902 TRACE("arith ineq", "TheoryArithOld::checkSat(fullEffort=",
01903 fullEffort? "true" : "false", ")");
01904 if (fullEffort) {
01905 while(!inconsistent() && d_bufferIdx < d_buffer.size())
01906 processBuffer();
01907 if(d_inModelCreation) {
01908 for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
01909 TRACE("model", "[arith] refining diseq: ",
01910 d_diseq[d_diseqIdx].getExpr() , "");
01911 enqueueFact(d_rules->diseqToIneq(d_diseq[d_diseqIdx]));
01912 }
01913 }
01914 }
01915 }
01916
01917
01918
01919 void TheoryArithOld::refineCounterExample()
01920 {
01921 d_inModelCreation = true;
01922 TRACE("model", "refineCounterExample[TheoryArithOld] ", "", "{");
01923 CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
01924 iend = d_sharedTerms.end();
01925
01926
01927
01928 for(; it!=iend; ++it) {
01929
01930 Expr e1 = (*it).first;
01931 for(it2 = it, ++it2; it2!=iend; ++it2) {
01932 Expr e2 = (*it2).first;
01933 DebugAssert(isReal(getBaseType(e1)),
01934 "TheoryArithOld::refineCounterExample: e1 = "+e1.toString()
01935 +"\n type(e1) = "+e1.getType().toString());
01936 if(findExpr(e1) != findExpr(e2)) {
01937 DebugAssert(isReal(getBaseType(e2)),
01938 "TheoryArithOld::refineCounterExample: e2 = "+e2.toString()
01939 +"\n type(e2) = "+e2.getType().toString());
01940 Expr eq = simplifyExpr(e1.eqExpr(e2));
01941 if (!eq.isBoolConst())
01942 addSplitter(eq);
01943 }
01944 }
01945 }
01946 TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
01947 }
01948
01949
01950 void
01951 TheoryArithOld::findRationalBound(const Expr& varSide, const Expr& ratSide,
01952 const Expr& var,
01953 Rational &r)
01954 {
01955 Expr c, x;
01956 separateMonomial(varSide, c, x);
01957
01958 DebugAssert(findExpr(c).isRational(),
01959 "seperateMonomial failed");
01960 DebugAssert(findExpr(ratSide).isRational(),
01961 "smallest variable in graph, should not have variables"
01962 " in inequalities: ");
01963 DebugAssert(x == var, "separateMonomial found different variable: "
01964 + var.toString());
01965 r = findExpr(ratSide).getRational() / findExpr(c).getRational();
01966 }
01967
01968 bool
01969 TheoryArithOld::findBounds(const Expr& e, Rational& lub, Rational& glb)
01970 {
01971 bool strictLB=false, strictUB=false;
01972 bool right = (d_inequalitiesRightDB.count(e) > 0
01973 && d_inequalitiesRightDB[e]->size() > 0);
01974 bool left = (d_inequalitiesLeftDB.count(e) > 0
01975 && d_inequalitiesLeftDB[e]->size() > 0);
01976 int numRight = 0, numLeft = 0;
01977 if(right) {
01978 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
01979 for(unsigned int i=0; i<ratsLTe->size(); i++) {
01980 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
01981 Expr ineq = (*ratsLTe)[i].ineq().getExpr();
01982 Expr leftSide = ineq[0], rightSide = ineq[1];
01983 Rational r;
01984 findRationalBound(rightSide, leftSide, e , r);
01985 if(numRight==0 || r>glb){
01986 glb = r;
01987 strictLB = isLT(ineq);
01988 }
01989 numRight++;
01990 }
01991 TRACE("model", " =>Lower bound ", glb.toString(), "");
01992 }
01993 if(left) {
01994 CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
01995 for(unsigned int i=0; i<ratsGTe->size(); i++) {
01996 DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
01997 Expr ineq = (*ratsGTe)[i].ineq().getExpr();
01998 Expr leftSide = ineq[0], rightSide = ineq[1];
01999 Rational r;
02000 findRationalBound(leftSide, rightSide, e, r);
02001 if(numLeft==0 || r<lub) {
02002 lub = r;
02003 strictUB = isLT(ineq);
02004 }
02005 numLeft++;
02006 }
02007 TRACE("model", " =>Upper bound ", lub.toString(), "");
02008 }
02009 if(!left && !right) {
02010 lub = 0;
02011 glb = 0;
02012 }
02013 if(!left && right) {lub = glb +2;}
02014 if(!right && left) {glb = lub-2;}
02015 DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
02016 "than least upper bound");
02017 return strictLB;
02018 }
02019
02020 void TheoryArithOld::assignVariables(std::vector<Expr>&v)
02021 {
02022 int count = 0;
02023 while (v.size() > 0) {
02024 std::vector<Expr> bottom;
02025 d_graph.selectSmallest(v, bottom);
02026 TRACE("model", "Finding variables to assign. Iteration # ", count, "");
02027 for(unsigned int i = 0; i<bottom.size(); i++) {
02028 Expr e = bottom[i];
02029 TRACE("model", "Found: ", e, "");
02030
02031 if(e.isRational()) continue;
02032
02033 Rational lub, glb;
02034 bool strictLB;
02035 strictLB = findBounds(e, lub, glb);
02036 Rational mid;
02037 if(isInteger(e)) {
02038 if(strictLB && glb.isInteger())
02039 mid = glb + 1;
02040 else
02041 mid = ceil(glb);
02042 }
02043 else
02044 mid = (lub + glb)/2;
02045 TRACE("model", "Assigning mid = ", mid, " {");
02046 assignValue(e, rat(mid));
02047 TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
02048 if(inconsistent()) return;
02049 }
02050 count++;
02051 }
02052 }
02053
02054 void TheoryArithOld::computeModelBasic(const std::vector<Expr>& v)
02055 {
02056 d_inModelCreation = true;
02057 vector<Expr> reps;
02058 TRACE("model", "Arith=>computeModel ", "", "{");
02059 for(unsigned int i=0; i <v.size(); ++i) {
02060 const Expr& e = v[i];
02061 if(findExpr(e) == e) {
02062 TRACE("model", "arith variable:", e , "");
02063 reps.push_back(e);
02064 }
02065 else {
02066 TRACE("model", "arith variable:", e , "");
02067 TRACE("model", " ==> is defined by: ", findExpr(e) , "");
02068 }
02069 }
02070 assignVariables(reps);
02071 TRACE("model", "Arith=>computeModel", "", "}");
02072 d_inModelCreation = false;
02073 }
02074
02075
02076
02077 void TheoryArithOld::computeModel(const Expr& e, vector<Expr>& vars) {
02078 DebugAssert(findExpr(e).isRational(), "TheoryArithOld::computeModel("
02079 +e.toString()+")\n e is not assigned concrete value.\n"
02080 +" find(e) = "+findExpr(e).toString());
02081 assignValue(simplify(e));
02082 vars.push_back(e);
02083 }
02084
02085
02086
02087
02088
02089
02090
02091 Theorem TheoryArithOld::normalize(const Expr& e) {
02092
02093
02094 TRACE("arith", "normalize(", e, ") {");
02095 DebugAssert(e.isEq() || isIneq(e),
02096 "normalize: input must be Eq or Ineq: " + e.toString());
02097 DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
02098 "normalize: if (e is ineq) then e[0] must be 0" +
02099 e.toString());
02100 if(e.isEq()) {
02101 if(e[0].isRational()) {
02102 DebugAssert(0 == e[0].getRational(),
02103 "normalize: if e is Eq and e[0] is rat then e[0]==0");
02104 }
02105 else {
02106
02107 DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
02108 "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
02109 " e = "+e.toString());
02110 }
02111 }
02112
02113 Expr factor;
02114 if(e[0].isRational())
02115 factor = computeNormalFactor(e[1]);
02116 else
02117 factor = computeNormalFactor(e[0]);
02118
02119 TRACE("arith", "normalize: factor = ", factor, "");
02120 DebugAssert(factor.getRational() > 0,
02121 "normalize: factor="+ factor.toString());
02122
02123 Theorem thm(reflexivityRule(e));
02124
02125 if(factor.getRational() != 1) {
02126 int kind = e.getKind();
02127 switch(kind) {
02128 case EQ:
02129 thm = d_rules->multEqn(e[0], e[1], factor);
02130
02131 thm = canonPredEquiv(thm);
02132 break;
02133 case LE:
02134 case LT:
02135 case GE:
02136 case GT:
02137 thm = d_rules->multIneqn(e, factor);
02138
02139 thm = canonPredEquiv(thm);
02140 break;
02141 default:
02142
02143 ostringstream ss;
02144 ss << "normalize: control should not reach here " << kind;
02145 DebugAssert(false, ss.str());
02146 break;
02147 }
02148 }
02149 TRACE("arith", "normalize => ", thm, " }");
02150 return(thm);
02151 }
02152
02153
02154 Theorem TheoryArithOld::normalize(const Theorem& eIffEqn) {
02155 return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
02156 }
02157
02158
02159 Theorem TheoryArithOld::rewrite(const Expr& e)
02160 {
02161 DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
02162 TRACE("arith", "TheoryArithOld::rewrite(", e, ") {");
02163 Theorem thm;
02164 if (!e.isTerm()) {
02165 if (!e.isAbsLiteral()) {
02166 e.setRewriteNormal();
02167 thm = reflexivityRule(e);
02168 TRACE("arith", "TheoryArithOld::rewrite[non-literal] => ", thm, " }");
02169 return thm;
02170 }
02171 switch(e.getKind()) {
02172 case EQ:
02173 {
02174
02175
02176 if (isLeaf(e[0]) && isLeaf(e[1]))
02177 thm = reflexivityRule(e);
02178 else {
02179
02180 if((e[0].isRational() && e[0].getRational() == 0)
02181 || (e[1].isRational() && e[1].getRational() == 0))
02182
02183 thm = reflexivityRule(e);
02184 else {
02185 thm = d_rules->rightMinusLeft(e);
02186 thm = canonPredEquiv(thm);
02187 }
02188
02189 if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
02190 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02191 } else {
02192
02193 thm = normalize(thm);
02194
02195 thm = canonPredEquiv(thm);
02196
02197 }
02198 }
02199
02200
02201
02202 const Expr& eq = thm.getRHS();
02203 if(eq.isEq() && eq[0] < eq[1])
02204 thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq));
02205 }
02206 break;
02207 case GRAY_SHADOW:
02208 case DARK_SHADOW:
02209 thm = reflexivityRule(e);
02210 break;
02211 case IS_INTEGER: {
02212 Theorem res(isIntegerDerive(e, typePred(e[0])));
02213 if(!res.isNull())
02214 thm = getCommonRules()->iffTrue(res);
02215 else
02216 thm = reflexivityRule(e);
02217 break;
02218 }
02219 case NOT:
02220 if (!isIneq(e[0]))
02221
02222 thm = reflexivityRule(e);
02223 else {
02224
02225
02226 thm = d_rules->negatedInequality(e);
02227 DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
02228 "Expected GE or GT");
02229 thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
02230 thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02231 thm = canonPredEquiv(thm);
02232
02233
02234 if ((thm.getRHS())[1].isRational())
02235 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02236 else {
02237
02238 thm = normalize(thm);
02239
02240 thm = canonPredEquiv(thm);
02241 }
02242 }
02243 break;
02244 case LE:
02245 case LT:
02246 case GE:
02247 case GT:
02248 if (isGE(e) || isGT(e)) {
02249 thm = d_rules->flipInequality(e);
02250 thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02251 }
02252 else
02253 thm = d_rules->rightMinusLeft(e);
02254 thm = canonPredEquiv(thm);
02255
02256
02257 if ((thm.getRHS())[1].isRational())
02258 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02259 else {
02260 thm = normalize(thm);
02261 thm = canonPredEquiv(thm);
02262 }
02263 break;
02264 default:
02265 DebugAssert(false,
02266 "Theory_Arith::rewrite: control should not reach here");
02267 break;
02268 }
02269 }
02270 else {
02271 if (e.isAtomic())
02272 thm = canon(e);
02273 else
02274 thm = reflexivityRule(e);
02275 }
02276
02277 if (theoryOf(thm.getRHS()) == this)
02278 thm.getRHS().setRewriteNormal();
02279 TRACE("arith", "TheoryArithOld::rewrite => ", thm, " }");
02280 return thm;
02281 }
02282
02283
02284 void TheoryArithOld::setup(const Expr& e)
02285 {
02286 if (!e.isTerm()) {
02287 if (e.isNot() || e.isEq() || isDarkShadow(e) || isGrayShadow(e)) return;
02288 if(e.getKind() == IS_INTEGER) {
02289 e[0].addToNotify(this, e);
02290 return;
02291 }
02292 DebugAssert((isLT(e)||isLE(e)) &&
02293 e[0].isRational() && e[0].getRational() == 0,
02294 "TheoryArithOld::setup: expected 0 < rhs:" + e.toString());
02295 e[1].addToNotify(this, e);
02296 return;
02297 }
02298 int k(0), ar(e.arity());
02299 for ( ; k < ar; ++k) {
02300 e[k].addToNotify(this, e);
02301 TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
02302 }
02303 }
02304
02305
02306 void TheoryArithOld::update(const Theorem& e, const Expr& d)
02307 {
02308 if (inconsistent()) return;
02309 IF_DEBUG(debugger.counter("arith update total")++);
02310 if (!d.hasFind()) return;
02311 if (isIneq(d)) {
02312
02313 DebugAssert(e.getLHS() == d[1], "Mismatch");
02314 Theorem thm = find(d);
02315
02316 vector<unsigned> changed;
02317 vector<Theorem> children;
02318 changed.push_back(1);
02319 children.push_back(e);
02320 Theorem thm2 = substitutivityRule(d, changed, children);
02321 if (thm.getRHS() == trueExpr()) {
02322 enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
02323 }
02324 else {
02325 enqueueFact(getCommonRules()->iffFalseElim(
02326 transitivityRule(symmetryRule(thm2), thm)));
02327 }
02328 IF_DEBUG(debugger.counter("arith update ineq")++);
02329 }
02330 else if (find(d).getRHS() == d) {
02331
02332 Theorem thm = canonSimp(d);
02333 TRACE("arith", "TheoryArithOld::update(): thm = ", thm, "");
02334 DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
02335 +thm.getExpr().toString());
02336 assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
02337 IF_DEBUG(debugger.counter("arith update find(d)=d")++);
02338 }
02339 }
02340
02341
02342 Theorem TheoryArithOld::solve(const Theorem& thm)
02343 {
02344 DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
02345 const Expr& lhs = thm.getLHS();
02346 const Expr& rhs = thm.getRHS();
02347
02348
02349
02350
02351
02352
02353 if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
02354 && (lhs.getType() != intType() || isInteger(rhs))
02355
02356 )
02357 return thm;
02358
02359
02360 if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
02361 && (rhs.getType() != intType() || isInteger(lhs))
02362
02363 )
02364 return symmetryRule(thm);
02365
02366 return doSolve(thm);
02367 }
02368
02369
02370 void TheoryArithOld::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
02371 switch(e.getKind()) {
02372 case RATIONAL_EXPR:
02373 break;
02374 case PLUS:
02375 case MULT:
02376 case DIVIDE:
02377 case POW:
02378 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
02379
02380 v.push_back(*i);
02381 break;
02382 default: {
02383 Expr e2(findExpr(e));
02384 if(e==e2) {
02385 TRACE("model", "TheoryArithOld::computeModelTerm(", e, "): a variable");
02386
02387
02388 } else {
02389 TRACE("model", "TheoryArithOld::computeModelTerm("+e.toString()
02390 +"): has find pointer to ", e2, "");
02391 v.push_back(e2);
02392 }
02393 }
02394 }
02395 }
02396
02397
02398 Expr TheoryArithOld::computeTypePred(const Type& t, const Expr& e) {
02399 Expr tExpr = t.getExpr();
02400 switch(tExpr.getKind()) {
02401 case INT:
02402 return Expr(IS_INTEGER, e);
02403 case SUBRANGE: {
02404 std::vector<Expr> kids;
02405 kids.push_back(Expr(IS_INTEGER, e));
02406 kids.push_back(leExpr(tExpr[0], e));
02407 kids.push_back(leExpr(e, tExpr[1]));
02408 return andExpr(kids);
02409 }
02410 default:
02411 return e.getEM()->trueExpr();
02412 }
02413 }
02414
02415
02416 void TheoryArithOld::checkAssertEqInvariant(const Theorem& e)
02417 {
02418 if (e.isRewrite()) {
02419 DebugAssert(e.getLHS().isTerm(), "Expected equation");
02420 if (isLeaf(e.getLHS())) {
02421
02422 DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
02423 "Not in solved form: lhs appears in rhs");
02424 }
02425 else {
02426 DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
02427 DebugAssert(!leavesAreSimp(e.getLHS()),
02428 "Expected at least one unsimplified leaf on lhs");
02429 }
02430 DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
02431 "Expected canonSimp(rhs) = canonSimp(rhs)");
02432 }
02433 else {
02434 Expr expr = e.getExpr();
02435 if (expr.isFalse()) return;
02436
02437 vector<Theorem> eqs;
02438 Theorem thm;
02439 int index, index2;
02440
02441 for (index = 0; index < expr.arity(); ++index) {
02442 thm = getCommonRules()->andElim(e, index);
02443 eqs.push_back(thm);
02444 if (thm.getExpr().isFalse()) return;
02445 DebugAssert(eqs[index].isRewrite() &&
02446 eqs[index].getLHS().isTerm(), "Expected equation");
02447 }
02448
02449
02450 for (index = 0; index < expr.arity(); ++index) {
02451 DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
02452 DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
02453 "Expected canonSimp(rhs) = canonSimp(rhs)");
02454 DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
02455 "Failed recursive canonSimp check");
02456 for (index2 = 0; index2 < expr.arity(); ++index2) {
02457 DebugAssert(index == index2 ||
02458 eqs[index].getLHS() != eqs[index2].getLHS(),
02459 "Not in solved form: repeated lhs");
02460 DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
02461 "Not in solved form: lhs appears in rhs");
02462 }
02463 }
02464 }
02465 }
02466
02467
02468 void TheoryArithOld::checkType(const Expr& e)
02469 {
02470 switch (e.getKind()) {
02471 case INT:
02472 case REAL:
02473 if (e.arity() > 0) {
02474 throw Exception("Ill-formed arithmetic type: "+e.toString());
02475 }
02476 break;
02477 case SUBRANGE:
02478 if (e.arity() != 2 ||
02479 !isIntegerConst(e[0]) ||
02480 !isIntegerConst(e[1]) ||
02481 e[0].getRational() > e[1].getRational()) {
02482 throw Exception("bad SUBRANGE type expression"+e.toString());
02483 }
02484 break;
02485 default:
02486 DebugAssert(false, "Unexpected kind in TheoryArithOld::checkType"
02487 +getEM()->getKindName(e.getKind()));
02488 }
02489 }
02490
02491
02492 void TheoryArithOld::computeType(const Expr& e)
02493 {
02494 switch (e.getKind()) {
02495 case REAL_CONST:
02496 e.setType(d_realType);
02497 break;
02498 case RATIONAL_EXPR:
02499 if(e.getRational().isInteger())
02500 e.setType(d_intType);
02501 else
02502 e.setType(d_realType);
02503 break;
02504 case UMINUS:
02505 case PLUS:
02506 case MINUS:
02507 case MULT:
02508 case POW: {
02509 bool isInt = true;
02510 for(int k = 0; k < e.arity(); ++k) {
02511 if(d_realType != getBaseType(e[k]))
02512 throw TypecheckException("Expecting type REAL with `" +
02513 getEM()->getKindName(e.getKind()) + "',\n"+
02514 "but got a " + getBaseType(e[k]).toString()+
02515 " for:\n" + e.toString());
02516 if(isInt && !isInteger(e[k]))
02517 isInt = false;
02518 }
02519 if(isInt)
02520 e.setType(d_intType);
02521 else
02522 e.setType(d_realType);
02523 break;
02524 }
02525 case DIVIDE: {
02526 Expr numerator = e[0];
02527 Expr denominator = e[1];
02528 if (getBaseType(numerator) != d_realType ||
02529 getBaseType(denominator) != d_realType) {
02530 throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
02531 "but got " + getBaseType(numerator).toString()+
02532 " and " + getBaseType(denominator).toString() +
02533 " for:\n" + e.toString());
02534 }
02535 if(denominator.isRational() && 1 == denominator.getRational())
02536 e.setType(numerator.getType());
02537 else
02538 e.setType(d_realType);
02539 break;
02540 }
02541 case LT:
02542 case LE:
02543 case GT:
02544 case GE:
02545 case GRAY_SHADOW:
02546
02547
02548
02549 case DARK_SHADOW:
02550 for (int k = 0; k < e.arity(); ++k) {
02551 if (d_realType != getBaseType(e[k]))
02552 throw TypecheckException("Expecting type REAL with `" +
02553 getEM()->getKindName(e.getKind()) + "',\n"+
02554 "but got a " + getBaseType(e[k]).toString()+
02555 " for:\n" + e.toString());
02556 }
02557
02558 e.setType(boolType());
02559 break;
02560 case IS_INTEGER:
02561 if(d_realType != getBaseType(e[0]))
02562 throw TypecheckException("Expected type REAL, but got "
02563 +getBaseType(e[0]).toString()
02564 +"\n\nExpr = "+e.toString());
02565 e.setType(boolType());
02566 break;
02567 default:
02568 DebugAssert(false,"TheoryArithOld::computeType: unexpected expression:\n "
02569 +e.toString());
02570 break;
02571 }
02572 }
02573
02574
02575 Type TheoryArithOld::computeBaseType(const Type& t) {
02576 IF_DEBUG(int kind = t.getExpr().getKind());
02577 DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
02578 "TheoryArithOld::computeBaseType("+t.toString()+")");
02579 return realType();
02580 }
02581
02582
02583 Expr
02584 TheoryArithOld::computeTCC(const Expr& e) {
02585 Expr tcc(Theory::computeTCC(e));
02586 switch(e.getKind()) {
02587 case DIVIDE:
02588 DebugAssert(e.arity() == 2, "");
02589 return tcc.andExpr(!(e[1].eqExpr(rat(0))));
02590 default:
02591 return tcc;
02592 }
02593 }
02594
02595
02596
02597
02598
02599 Expr
02600 TheoryArithOld::parseExprOp(const Expr& e) {
02601 TRACE("parser", "TheoryArithOld::parseExprOp(", e, ")");
02602
02603
02604
02605 switch(e.getKind()) {
02606 case ID: {
02607 int kind = getEM()->getKind(e[0].getString());
02608 switch(kind) {
02609 case NULL_KIND: return e;
02610 case REAL:
02611 case INT:
02612 case NEGINF:
02613 case POSINF: return getEM()->newLeafExpr(kind);
02614 default:
02615 DebugAssert(false, "Bad use of bare keyword: "+e.toString());
02616 return e;
02617 }
02618 }
02619 case RAW_LIST: break;
02620 default:
02621 return e;
02622 }
02623
02624 DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
02625 "TheoryArithOld::parseExprOp:\n e = "+e.toString());
02626
02627 const Expr& c1 = e[0][0];
02628 int kind = getEM()->getKind(c1.getString());
02629 switch(kind) {
02630 case UMINUS: {
02631 if(e.arity() != 2)
02632 throw ParserException("UMINUS requires exactly one argument: "
02633 +e.toString());
02634 return uminusExpr(parseExpr(e[1]));
02635 }
02636 case PLUS: {
02637 vector<Expr> k;
02638 Expr::iterator i = e.begin(), iend=e.end();
02639
02640
02641 ++i;
02642
02643 for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02644 return plusExpr(k);
02645 }
02646 case MINUS: {
02647 if(e.arity() == 2)
02648 return uminusExpr(parseExpr(e[1]));
02649 else if(e.arity() == 3)
02650 return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
02651 else
02652 throw ParserException("MINUS requires one or two arguments:"
02653 +e.toString());
02654 }
02655 case MULT: {
02656 vector<Expr> k;
02657 Expr::iterator i = e.begin(), iend=e.end();
02658
02659
02660 ++i;
02661
02662 for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02663 return multExpr(k);
02664 }
02665 case POW: {
02666 return powExpr(parseExpr(e[1]), parseExpr(e[2]));
02667 }
02668 case DIVIDE:
02669 { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
02670 case LT:
02671 { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
02672 case LE:
02673 { return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
02674 case GT:
02675 { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
02676 case GE:
02677 { return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
02678 case INTDIV:
02679 case MOD:
02680 case SUBRANGE: {
02681 vector<Expr> k;
02682 Expr::iterator i = e.begin(), iend=e.end();
02683
02684
02685 ++i;
02686
02687 for(; i!=iend; ++i)
02688 k.push_back(parseExpr(*i));
02689 return Expr(kind, k, e.getEM());
02690 }
02691 case IS_INTEGER: {
02692 if(e.arity() != 2)
02693 throw ParserException("IS_INTEGER requires exactly one argument: "
02694 +e.toString());
02695 return Expr(IS_INTEGER, parseExpr(e[1]));
02696 }
02697 default:
02698 DebugAssert(false,
02699 "TheoryArithOld::parseExprOp: invalid input " + e.toString());
02700 break;
02701 }
02702 return e;
02703 }
02704
02705
02706
02707
02708
02709
02710 ExprStream&
02711 TheoryArithOld::print(ExprStream& os, const Expr& e) {
02712 switch(os.lang()) {
02713 case SIMPLIFY_LANG:
02714 switch(e.getKind()) {
02715 case RATIONAL_EXPR:
02716 e.print(os);
02717 break;
02718 case SUBRANGE:
02719 os <<"ERROR:SUBRANGE:not supported in Simplify\n";
02720 break;
02721 case IS_INTEGER:
02722 os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
02723 break;
02724 case PLUS: {
02725 int i=0, iend=e.arity();
02726 os << "(+ ";
02727 if(i!=iend) os << e[i];
02728 ++i;
02729 for(; i!=iend; ++i) os << " " << e[i];
02730 os << ")";
02731 break;
02732 }
02733 case MINUS:
02734 os << "(- " << e[0] << " " << e[1]<< ")";
02735 break;
02736 case UMINUS:
02737 os << "-" << e[0] ;
02738 break;
02739 case MULT: {
02740 int i=0, iend=e.arity();
02741 os << "(* " ;
02742 if(i!=iend) os << e[i];
02743 ++i;
02744 for(; i!=iend; ++i) os << " " << e[i];
02745 os << ")";
02746 break;
02747 }
02748 case POW:
02749 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02750 break;
02751 case DIVIDE:
02752 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02753 break;
02754 case LT:
02755 if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02756 }
02757 os << "(< " << e[0] << " " << e[1] <<")";
02758 break;
02759 case LE:
02760 os << "(<= " << e[0] << " " << e[1] << ")";
02761 break;
02762 case GT:
02763 os << "(> " << e[0] << " " << e[1] << ")";
02764 break;
02765 case GE:
02766 os << "(>= " << e[0] << " " << e[1] << ")";
02767 break;
02768 case DARK_SHADOW:
02769 case GRAY_SHADOW:
02770 os <<"ERROR:SHADOW:not supported in Simplify\n";
02771 break;
02772 default:
02773
02774
02775 e.print(os);
02776
02777 break;
02778 }
02779 break;
02780
02781 case PRESENTATION_LANG:
02782 switch(e.getKind()) {
02783 case REAL:
02784 case INT:
02785 case RATIONAL_EXPR:
02786 case NEGINF:
02787 case POSINF:
02788 e.print(os);
02789 break;
02790 case SUBRANGE:
02791 if(e.arity() != 2) e.printAST(os);
02792 else
02793 os << "[" << push << e[0] << ".." << e[1] << push << "]";
02794 break;
02795 case IS_INTEGER:
02796 if(e.arity() == 1)
02797 os << "IS_INTEGER(" << push << e[0] << push << ")";
02798 else
02799 e.printAST(os);
02800 break;
02801 case PLUS: {
02802 int i=0, iend=e.arity();
02803 os << "(" << push;
02804 if(i!=iend) os << e[i];
02805 ++i;
02806 for(; i!=iend; ++i) os << space << "+ " << e[i];
02807 os << push << ")";
02808 break;
02809 }
02810 case MINUS:
02811 os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
02812 break;
02813 case UMINUS:
02814 os << "-(" << push << e[0] << push << ")";
02815 break;
02816 case MULT: {
02817 int i=0, iend=e.arity();
02818 os << "(" << push;
02819 if(i!=iend) os << e[i];
02820 ++i;
02821 for(; i!=iend; ++i) os << space << "* " << e[i];
02822 os << push << ")";
02823 break;
02824 }
02825 case POW:
02826 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02827 break;
02828 case DIVIDE:
02829 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02830 break;
02831 case LT:
02832 if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02833 }
02834 os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
02835 break;
02836 case LE:
02837 os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
02838 break;
02839 case GT:
02840 os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
02841 break;
02842 case GE:
02843 os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
02844 break;
02845 case DARK_SHADOW:
02846 os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
02847 break;
02848 case GRAY_SHADOW:
02849 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
02850 << "," << space << e[2] << "," << space << e[3] << push << ")";
02851 break;
02852 default:
02853
02854
02855 e.printAST(os);
02856
02857 break;
02858 }
02859 break;
02860 case SMTLIB_LANG: {
02861 switch(e.getKind()) {
02862 case REAL_CONST:
02863 printRational(os, e[0].getRational(), true);
02864 break;
02865 case RATIONAL_EXPR:
02866 printRational(os, e.getRational());
02867 break;
02868 case REAL:
02869 os << "Real";
02870 break;
02871 case INT:
02872 os << "Int";
02873 break;
02874 case SUBRANGE:
02875 throw SmtlibException("TheoryArithOld::print: SMTLIB: SUBRANGE not implemented");
02876
02877
02878
02879
02880 break;
02881 case IS_INTEGER:
02882 if(e.arity() == 1)
02883 os << "(" << push << "IsInt" << space << e[0] << push << ")";
02884 else
02885 throw SmtlibException("TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly");
02886 break;
02887 case PLUS: {
02888 os << "(" << push << "+";
02889 Expr::iterator i = e.begin(), iend = e.end();
02890 for(; i!=iend; ++i) {
02891 os << space << (*i);
02892 }
02893 os << push << ")";
02894 break;
02895 }
02896 case MINUS: {
02897 os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02898 break;
02899 }
02900 case UMINUS: {
02901 os << "(" << push << "-" << space << e[0] << push << ")";
02902 break;
02903 }
02904 case MULT: {
02905 int i=0, iend=e.arity();
02906 for(; i!=iend; ++i) {
02907 if (i < iend-1) {
02908 os << "(" << push << "*";
02909 }
02910 os << space << e[i];
02911 }
02912 for (i=0; i < iend-1; ++i) os << push << ")";
02913 break;
02914 }
02915 case POW:
02916 throw SmtlibException("TheoryArithOld::print: SMTLIB: POW not supported");
02917
02918 break;
02919 case DIVIDE: {
02920 throw SmtlibException("TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE");
02921 break;
02922 }
02923 case LT: {
02924 Rational r;
02925 os << "(" << push << "<" << space;
02926 os << e[0] << space << e[1] << push << ")";
02927 break;
02928 }
02929 case LE: {
02930 Rational r;
02931 os << "(" << push << "<=" << space;
02932 os << e[0] << space << e[1] << push << ")";
02933 break;
02934 }
02935 case GT: {
02936 Rational r;
02937 os << "(" << push << ">" << space;
02938 os << e[0] << space << e[1] << push << ")";
02939 break;
02940 }
02941 case GE: {
02942 Rational r;
02943 os << "(" << push << ">=" << space;
02944 os << e[0] << space << e[1] << push << ")";
02945 break;
02946 }
02947 case DARK_SHADOW:
02948 throw SmtlibException("TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported");
02949 os << "(" << push << "DARK_SHADOW" << space << e[0]
02950 << space << e[1] << push << ")";
02951 break;
02952 case GRAY_SHADOW:
02953 throw SmtlibException("TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported");
02954 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
02955 << "," << space << e[2] << "," << space << e[3] << push << ")";
02956 break;
02957 default:
02958 throw SmtlibException("TheoryArithOld::print: SMTLIB: default not supported");
02959
02960
02961 e.printAST(os);
02962
02963 break;
02964 }
02965 break;
02966 }
02967 case LISP_LANG:
02968 switch(e.getKind()) {
02969 case REAL:
02970 case INT:
02971 case RATIONAL_EXPR:
02972 case NEGINF:
02973 case POSINF:
02974 e.print(os);
02975 break;
02976 case SUBRANGE:
02977 if(e.arity() != 2) e.printAST(os);
02978 else
02979 os << "(" << push << "SUBRANGE" << space << e[0]
02980 << space << e[1] << push << ")";
02981 break;
02982 case IS_INTEGER:
02983 if(e.arity() == 1)
02984 os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
02985 else
02986 e.printAST(os);
02987 break;
02988 case PLUS: {
02989 int i=0, iend=e.arity();
02990 os << "(" << push << "+";
02991 for(; i!=iend; ++i) os << space << e[i];
02992 os << push << ")";
02993 break;
02994 }
02995 case MINUS:
02996
02997 os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02998 break;
02999 case UMINUS:
03000 os << "(" << push << "-" << space << e[0] << push << ")";
03001 break;
03002 case MULT: {
03003 int i=0, iend=e.arity();
03004 os << "(" << push << "*";
03005 for(; i!=iend; ++i) os << space << e[i];
03006 os << push << ")";
03007 break;
03008 }
03009 case POW:
03010 os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
03011 break;
03012 case DIVIDE:
03013 os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
03014 break;
03015 case LT:
03016 os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
03017 break;
03018 case LE:
03019 os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
03020 break;
03021 case GT:
03022 os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
03023 break;
03024 case GE:
03025 os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
03026 break;
03027 case DARK_SHADOW:
03028 os << "(" << push << "DARK_SHADOW" << space << e[0]
03029 << space << e[1] << push << ")";
03030 break;
03031 case GRAY_SHADOW:
03032 os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
03033 << e[1] << space << e[2] << space << e[3] << push << ")";
03034 break;
03035 default:
03036
03037
03038 e.printAST(os);
03039
03040 break;
03041 }
03042 break;
03043 default:
03044
03045
03046 e.printAST(os);
03047 }
03048 return os;
03049 }
03050
03051
03052
03053
03054
03055
03056
03057
03058
03059
03060
03061
03062
03063
03064
03065
03066
03067
03068
03069
03070
03071
03072
03073
03074
03075
03076
03077
03078
03079
03080
03081
03082
03083
03084
03085
03086
03087
03088
03089
03090
03091
03092
03093