00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030 #define _CVC3_TRUSTED_
00031
00032 #include "arith_theorem_producer_old.h"
00033 #include "theory_core.h"
00034 #include "theory_arith_old.h"
00035
00036 using namespace std;
00037 using namespace CVC3;
00038
00039
00040
00041
00042
00043 ArithProofRules* TheoryArithOld::createProofRulesOld() {
00044 return new ArithTheoremProducerOld(theoryCore()->getTM(), this);
00045 }
00046
00047
00048
00049
00050
00051
00052 #define CLASS_NAME "ArithTheoremProducerOld"
00053
00054
00055
00056 Theorem ArithTheoremProducerOld::varToMult(const Expr& e) {
00057 Proof pf;
00058 if(withProof()) pf = newPf("var_to_mult", e);
00059 return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
00060 }
00061
00062
00063
00064 Theorem ArithTheoremProducerOld::uMinusToMult(const Expr& e) {
00065 Proof pf;
00066 if(withProof()) pf = newPf("uminus_to_mult", e);
00067 return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
00068 }
00069
00070
00071
00072 Theorem ArithTheoremProducerOld::minusToPlus(const Expr& x, const Expr& y)
00073 {
00074 Proof pf;
00075 if(withProof()) pf = newPf("minus_to_plus", x, y);
00076 return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
00077 }
00078
00079
00080
00081
00082 Theorem ArithTheoremProducerOld::canonUMinusToDivide(const Expr& e) {
00083 Proof pf;
00084 if(withProof()) pf = newPf("canon_uminus", e);
00085 return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
00086 }
00087
00088
00089
00090
00091 Theorem ArithTheoremProducerOld::canonDivideConst(const Expr& c,
00092 const Expr& d) {
00093
00094 if(CHECK_PROOFS) {
00095 CHECK_SOUND(isRational(c),
00096 CLASS_NAME "::canonDivideConst:\n c not a constant: "
00097 + c.toString());
00098 CHECK_SOUND(isRational(d),
00099 CLASS_NAME "::canonDivideConst:\n d not a constant: "
00100 + d.toString());
00101 }
00102 Proof pf;
00103 if(withProof())
00104 pf = newPf("canon_divide_const", c, d, d_hole);
00105 const Rational& dr = d.getRational();
00106 return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf);
00107 }
00108
00109
00110 Theorem ArithTheoremProducerOld::canonDivideMult(const Expr& cx,
00111 const Expr& d) {
00112
00113 if(CHECK_PROOFS) {
00114 CHECK_SOUND(isMult(cx) && isRational(cx[0]),
00115 CLASS_NAME "::canonDivideMult:\n "
00116 "Not a (c * x) expression: "
00117 + cx.toString());
00118 CHECK_SOUND(isRational(d),
00119 CLASS_NAME "::canonDivideMult:\n "
00120 "d is not a constant: " + d.toString());
00121 }
00122 const Rational& dr = d.getRational();
00123 Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
00124 Expr cd(rat(cdr));
00125 Proof pf;
00126 if(withProof())
00127 pf = newPf("canon_divide_mult", cx[0], cx[1], d);
00128
00129 if(cdr == 1)
00130 return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
00131 else if(cdr == 0)
00132 return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
00133 else
00134 return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
00135 }
00136
00137
00138 Theorem ArithTheoremProducerOld::canonDividePlus(const Expr& sum, const Expr& d) {
00139 if(CHECK_PROOFS) {
00140 CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]),
00141 CLASS_NAME "::canonUMinusPlus:\n "
00142 "Expr is not a canonical sum: "
00143 + sum.toString());
00144 CHECK_SOUND(isRational(d),
00145 CLASS_NAME "::canonUMinusPlus:\n "
00146 "d is not a const: " + d.toString());
00147 }
00148
00149 Proof pf;
00150 if(withProof())
00151 pf = newPf("canon_divide_plus", rat(sum.arity()),
00152 sum.begin(), sum.end());
00153 vector<Expr> newKids;
00154 for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i)
00155 newKids.push_back((*i)/d);
00156
00157 return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf);
00158 }
00159
00160
00161 Theorem ArithTheoremProducerOld::canonDivideVar(const Expr& e, const Expr& d) {
00162 if(CHECK_PROOFS) {
00163 CHECK_SOUND(isRational(d),
00164 CLASS_NAME "::canonDivideVar:\n "
00165 "d is not a const: " + d.toString());
00166 }
00167 Proof pf;
00168
00169 if(withProof())
00170 pf = newPf("canon_divide_var", e);
00171
00172 const Rational& dr = d.getRational();
00173 if(dr == 1)
00174 return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
00175 if(dr == 0)
00176 return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
00177 else
00178 return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
00179 }
00180
00181
00182
00183
00184
00185
00186
00187
00188
00189
00190
00191
00192
00193
00194
00195
00196 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids)
00197 {
00198 DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), "");
00199 if (mulKids.size() == 1) {
00200 return mulKids[0];
00201 }
00202 if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
00203 return mulKids[1];
00204 }
00205 else
00206 return multExpr(mulKids);
00207 }
00208
00209 Expr ArithTheoremProducerOld::canonMultConstMult(const Expr & c,
00210 const Expr & e)
00211 {
00212
00213
00214
00215 DebugAssert(c.isRational() && e.getKind() == MULT, "");
00216 std::vector<Expr> mulKids;
00217 DebugAssert ((e.arity() > 1) && (e[0].isRational()),
00218 "ArithTheoremProducerOld::canonMultConstMult: "
00219 "a canonized MULT expression must have arity "
00220 "greater than 1: and first child must be "
00221 "rational " + e.toString());
00222 Expr::iterator i = e.begin();
00223 mulKids.push_back(rat(c.getRational() * (*i).getRational()));
00224 ++i;
00225 for(; i != e.end(); ++i) {
00226 mulKids.push_back(*i);
00227 }
00228 return simplifiedMultExpr(mulKids);
00229 }
00230
00231 Expr ArithTheoremProducerOld::canonMultConstPlus(const Expr & e1,
00232 const Expr & e2)
00233 {
00234 DebugAssert(e1.isRational() && e2.getKind() == PLUS &&
00235 e2.arity() > 0, "");
00236
00237
00238
00239 std::vector<Theorem> thmPlusVector;
00240 Expr::iterator i = e2.begin();
00241 for(; i!= e2.end(); ++i) {
00242 thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
00243 }
00244
00245 Theorem thmPlus1 =
00246 d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector);
00247 return thmPlus1.getRHS();
00248 }
00249
00250 Expr ArithTheoremProducerOld::canonMultPowPow(const Expr & e1,
00251 const Expr & e2)
00252 {
00253 DebugAssert(e1.getKind() == POW && e2.getKind() == POW, "");
00254
00255 Expr leaf1 = e1[1];
00256 Expr leaf2 = e2[1];
00257 Expr can_expr;
00258 if (leaf1 == leaf2) {
00259 Rational rsum = e1[0].getRational() + e2[0].getRational();
00260 if (rsum == 0) {
00261 return rat(1);
00262 }
00263 else if (rsum == 1) {
00264 return leaf1;
00265 }
00266 else
00267 {
00268 return powExpr(rat(rsum), leaf1);
00269 }
00270 }
00271 else
00272 {
00273 std::vector<Expr> mulKids;
00274 mulKids.push_back(rat(1));
00275
00276 if (leaf1 < leaf2) {
00277 mulKids.push_back(e2);
00278 mulKids.push_back(e1);
00279 }
00280 else
00281 {
00282 mulKids.push_back(e1);
00283 mulKids.push_back(e2);
00284 }
00285
00286 return simplifiedMultExpr(mulKids);
00287 }
00288 }
00289
00290 Expr ArithTheoremProducerOld::canonMultPowLeaf(const Expr & e1,
00291 const Expr & e2)
00292 {
00293 DebugAssert(e1.getKind() == POW, "");
00294
00295 Expr leaf1 = e1[1];
00296 Expr leaf2 = e2;
00297 Expr can_expr;
00298 if (leaf1 == leaf2) {
00299 Rational rsum = e1[0].getRational() + 1;
00300 if (rsum == 0) {
00301 return rat(1);
00302 }
00303 else if (rsum == 1) {
00304 return leaf1;
00305 }
00306 else
00307 {
00308 return powExpr(rat(rsum), leaf1);
00309 }
00310 }
00311 else
00312 {
00313 std::vector<Expr> mulKids;
00314 mulKids.push_back(rat(1));
00315
00316 if (leaf1 < leaf2) {
00317 mulKids.push_back(e2);
00318 mulKids.push_back(e1);
00319 }
00320 else
00321 {
00322 mulKids.push_back(e1);
00323 mulKids.push_back(e2);
00324 }
00325 return simplifiedMultExpr(mulKids);
00326 }
00327 }
00328
00329 Expr ArithTheoremProducerOld::canonMultLeafLeaf(const Expr & e1,
00330 const Expr & e2)
00331 {
00332
00333 Expr leaf1 = e1;
00334 Expr leaf2 = e2;
00335 Expr can_expr;
00336 if (leaf1 == leaf2) {
00337 return powExpr(rat(2), leaf1);
00338 }
00339 else
00340 {
00341 std::vector<Expr> mulKids;
00342 mulKids.push_back(rat(1));
00343
00344 if (leaf1 < leaf2) {
00345 mulKids.push_back(e2);
00346 mulKids.push_back(e1);
00347 }
00348 else
00349 {
00350 mulKids.push_back(e1);
00351 mulKids.push_back(e2);
00352 }
00353 return simplifiedMultExpr(mulKids);
00354 }
00355 }
00356
00357 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(const Expr & e1,
00358 const Expr & e2)
00359 {
00360 DebugAssert(e2.getKind() == MULT, "");
00361
00362
00363
00364
00365 Expr leaf1 = e1.getKind() == POW ? e1[1] : e1;
00366 std::vector<Expr> mulKids;
00367 DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more");
00368 Expr::iterator i = e2.begin();
00369
00370 mulKids.push_back(*i);
00371 ++i;
00372
00373 for(; i != e2.end(); ++i) {
00374 Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i);
00375 if (leaf1 == leaf2) {
00376 Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1;
00377 Rational r2 =
00378 ((*i).getKind() == POW ? (*i)[0].getRational() : 1);
00379
00380
00381 if (r1 + r2 != 0) {
00382 if (r1 + r2 == 1) {
00383 mulKids.push_back(leaf1);
00384 }
00385 else
00386 {
00387 mulKids.push_back(powExpr(rat(r1 + r2), leaf1));
00388 }
00389 }
00390 break;
00391 }
00392
00393
00394
00395
00396 else if (leaf2 < leaf1) {
00397 mulKids.push_back(e1);
00398 mulKids.push_back(*i);
00399 break;
00400 }
00401 else
00402 mulKids.push_back(*i);
00403 }
00404 if (i == e2.end()) {
00405 mulKids.push_back(e1);
00406 }
00407 else
00408 {
00409
00410 for (++i; i != e2.end(); ++i) {
00411 mulKids.push_back(*i);
00412 }
00413 }
00414 return simplifiedMultExpr(mulKids);
00415 }
00416
00417
00418
00419 class MonomialLess {
00420 public:
00421 bool operator()(const Expr& e1, const Expr& e2) const {
00422 return ArithTheoremProducerOld::greaterthan(e1,e2);
00423 }
00424 };
00425
00426 typedef map<Expr,Rational,MonomialLess> MonomMap;
00427
00428 Expr
00429 ArithTheoremProducerOld::canonCombineLikeTerms(const std::vector<Expr> & sumExprs)
00430 {
00431 Rational constant = 0;
00432 MonomMap sumHashMap;
00433 vector<Expr> sumKids;
00434
00435
00436
00437 std::vector<Expr>::const_iterator i = sumExprs.begin();
00438 for (; i != sumExprs.end(); ++i) {
00439 Expr mul = *i;
00440 if (mul.isRational()) {
00441 constant = constant + mul.getRational();
00442 }
00443 else {
00444 switch (mul.getKind()) {
00445 case MULT: {
00446 std::vector<Expr> mulKids;
00447 DebugAssert(mul.arity() > 1 && mul[0].isRational(),"");
00448 mulKids.push_back(rat(1));
00449 Expr::iterator j = mul.begin();
00450 ++j;
00451 for (; j!= mul.end(); ++j) {
00452 mulKids.push_back(*j);
00453 }
00454
00455
00456 Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1];
00457 MonomMap::iterator i=sumHashMap.find(tempExpr);
00458 if (i == sumHashMap.end()) {
00459 sumHashMap[tempExpr] = mul[0].getRational();
00460 }
00461 else {
00462 (*i).second += mul[0].getRational();
00463 }
00464 }
00465 break;
00466 default: {
00467 MonomMap::iterator i=sumHashMap.find(mul);
00468
00469 if (i == sumHashMap.end()) {
00470 sumHashMap[mul] = 1;
00471 }
00472 else {
00473 (*i).second += 1;
00474 }
00475 break;
00476 }
00477 }
00478 }
00479 }
00480
00481 sumKids.push_back(rat(constant));
00482 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
00483 for(; j != jend; ++j) {
00484 if ((*j).second != 0)
00485 sumKids.push_back
00486 (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
00487 }
00488
00489
00490
00491
00492
00493
00494
00495
00496
00497
00498
00499
00500 if ((constant == 0) && (sumKids.size() == 2)) {
00501 return sumKids[1];
00502 }
00503 else if (sumKids.size() == 1) {
00504 return sumKids[0];
00505 }
00506 else
00507 return plusExpr(sumKids);
00508 }
00509
00510 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(const Expr & e1,
00511 const Expr & e2)
00512 {
00513 DebugAssert(e2.getKind() == PLUS, "");
00514
00515
00516
00517
00518
00519
00520 std::vector<Expr> sumExprs;
00521
00522 Expr::iterator i = e2.begin();
00523 for (; i != e2.end(); ++i) {
00524 sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
00525 }
00526 return canonCombineLikeTerms(sumExprs);
00527 }
00528
00529 Expr ArithTheoremProducerOld::canonMultPlusPlus(const Expr & e1,
00530 const Expr & e2)
00531 {
00532 DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, "");
00533
00534
00535
00536 std::vector<Expr> sumExprs;
00537
00538 Expr::iterator i = e1.begin();
00539 for (; i != e1.end(); ++i) {
00540 Expr::iterator j = e2.begin();
00541 for (; j != e2.end(); ++j) {
00542 sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
00543 }
00544 }
00545 return canonCombineLikeTerms(sumExprs);
00546 }
00547
00548
00549
00550
00551
00552 Theorem
00553 ArithTheoremProducerOld::canonMultMtermMterm(const Expr& e)
00554 {
00555 if(CHECK_PROOFS) {
00556 CHECK_SOUND(isMult(e) && e.arity() == 2,
00557 "canonMultMtermMterm: e = "+e.toString());
00558 }
00559 Proof pf;
00560 Expr rhs;
00561 const Expr& e1 = e[0];
00562 const Expr& e2 = e[1];
00563 string cmmm = "canon_mult_mterm_mterm";
00564
00565 if (e1.isRational()) {
00566
00567 const Rational& c = e1.getRational();
00568 if (c == 0)
00569 return canonMultZero(e2);
00570 else if (c == 1)
00571 return canonMultOne(e2);
00572 else {
00573 switch (e2.getKind()) {
00574 case RATIONAL_EXPR :
00575
00576 return canonMultConstConst(e1,e2);
00577 break;
00578
00579 case POW:
00580
00581
00582 return d_theoryArith->reflexivityRule (e);
00583
00584 break;
00585 case MULT:
00586 rhs = canonMultConstMult(e1,e2);
00587 if(withProof()) pf = newPf(cmmm,e,rhs);
00588 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00589 break;
00590 case PLUS:
00591 rhs = canonMultConstPlus(e1,e2);
00592 if(withProof()) pf = newPf(cmmm,e,rhs);
00593 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00594 break;
00595 default:
00596
00597
00598 return d_theoryArith->reflexivityRule(e);
00599 break;
00600 }
00601 }
00602 }
00603 else if (e1.getKind() == POW) {
00604 switch (e2.getKind()) {
00605 case RATIONAL_EXPR:
00606
00607 return canonMultMtermMterm(e2 * e1);
00608 break;
00609 case POW:
00610 rhs = canonMultPowPow(e1,e2);
00611 if(withProof()) pf = newPf(cmmm,e,rhs);
00612 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00613 break;
00614 case MULT:
00615 rhs = canonMultLeafOrPowMult(e1,e2);
00616 if(withProof()) pf = newPf(cmmm,e,rhs);
00617 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00618 break;
00619 case PLUS:
00620 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00621 if(withProof()) pf = newPf(cmmm,e,rhs);
00622 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00623 break;
00624 default:
00625 rhs = canonMultPowLeaf(e1,e2);
00626 if(withProof()) pf = newPf(cmmm,e,rhs);
00627 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00628 break;
00629 }
00630 }
00631 else if (e1.getKind() == MULT) {
00632 switch (e2.getKind()) {
00633 case RATIONAL_EXPR:
00634 case POW:
00635
00636 return canonMultMtermMterm(e2 * e1);
00637 break;
00638 case MULT:
00639 {
00640
00641 Expr result = e2;
00642 Expr::iterator i = e1.begin();
00643 for (; i != e1.end(); ++i) {
00644 result = canonMultMtermMterm((*i) * result).getRHS();
00645 }
00646 if(withProof()) pf = newPf(cmmm,e,result);
00647 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00648 }
00649 break;
00650 case PLUS:
00651 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00652 if(withProof()) pf = newPf(cmmm,e,rhs);
00653 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00654 break;
00655 default:
00656
00657
00658 return canonMultMtermMterm(e2 * e1);
00659 break;
00660 }
00661 }
00662 else if (e1.getKind() == PLUS) {
00663 switch (e2.getKind()) {
00664 case RATIONAL_EXPR:
00665 case POW:
00666 case MULT:
00667
00668 return canonMultMtermMterm(e2 * e1);
00669 break;
00670 case PLUS:
00671 rhs = canonMultPlusPlus(e1,e2);
00672 if(withProof()) pf = newPf(cmmm,e,rhs);
00673 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00674 break;
00675 default:
00676
00677
00678 return canonMultMtermMterm(e2 * e1);
00679 break;
00680 }
00681 }
00682 else {
00683
00684 switch (e2.getKind()) {
00685 case RATIONAL_EXPR:
00686
00687 return canonMultMtermMterm(e2 * e1);
00688 break;
00689 case POW:
00690 rhs = canonMultPowLeaf(e2,e1);
00691 if(withProof()) pf = newPf(cmmm,e,rhs);
00692 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00693 break;
00694 case MULT:
00695 rhs = canonMultLeafOrPowMult(e1,e2);;
00696 if(withProof()) pf = newPf(cmmm,e,rhs);
00697 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00698 break;
00699 case PLUS:
00700 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00701 if(withProof()) pf = newPf(cmmm,e,rhs);
00702 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00703 break;
00704 default:
00705
00706 rhs = canonMultLeafLeaf(e1,e2);
00707 if(withProof()) pf = newPf(cmmm,e,rhs);
00708 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00709 break;
00710 }
00711 }
00712 FatalAssert(false, "Unreachable");
00713 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00714 }
00715
00716
00717 Theorem
00718 ArithTheoremProducerOld::canonPlus(const Expr& e)
00719 {
00720 Proof pf;
00721
00722 if (withProof()) {
00723 pf = newPf("canon_plus", e);
00724 }
00725 DebugAssert(e.getKind() == PLUS, "");
00726
00727
00728
00729 std::vector<Expr> sumKids;
00730 Expr::iterator i = e.begin();
00731 for(; i != e.end(); ++i) {
00732 if ((*i).getKind() != PLUS) {
00733 sumKids.push_back(*i);
00734 }
00735 else
00736 {
00737 Expr::iterator j = (*i).begin();
00738 for(; j != (*i).end(); ++j)
00739 sumKids.push_back(*j);
00740 }
00741 }
00742 Expr val = canonCombineLikeTerms(sumKids);
00743 if (withProof()) {
00744 pf = newPf("canon_plus", e, val);
00745 }
00746 return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
00747 }
00748
00749
00750 Theorem
00751 ArithTheoremProducerOld::canonMult(const Expr& e)
00752 {
00753 Proof pf;
00754 DebugAssert(e.getKind() == MULT && e.arity() > 1, "");
00755 Expr::iterator i = e.begin();
00756 Expr result = *i;
00757 ++i;
00758 for (; i != e.end(); ++i) {
00759 result = canonMultMtermMterm(result * (*i)).getRHS();
00760 }
00761 if (withProof()) {
00762 pf = newPf("canon_mult", e,result);
00763 }
00764 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00765 }
00766
00767
00768 Theorem
00769 ArithTheoremProducerOld::canonInvertConst(const Expr& e)
00770 {
00771 if(CHECK_PROOFS)
00772 CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString());
00773
00774 Proof pf;
00775
00776 if (withProof()) {
00777 pf = newPf("canon_invert_const", e);
00778 }
00779 const Rational& er = e.getRational();
00780 return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
00781 }
00782
00783
00784 Theorem
00785 ArithTheoremProducerOld::canonInvertLeaf(const Expr& e)
00786 {
00787 Proof pf;
00788
00789 if (withProof()) {
00790 pf = newPf("canon_invert_leaf", e);
00791 }
00792 return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
00793 }
00794
00795
00796 Theorem
00797 ArithTheoremProducerOld::canonInvertPow(const Expr& e)
00798 {
00799 DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString());
00800
00801 Proof pf;
00802
00803 if (withProof()) {
00804 pf = newPf("canon_invert_pow", e);
00805 }
00806 if (e[0].getRational() == -1)
00807 return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
00808 else
00809 return newRWTheorem((rat(1)/e),
00810 powExpr(rat(-e[0].getRational()), e),
00811 Assumptions::emptyAssump(),
00812 pf);
00813 }
00814
00815 Theorem
00816 ArithTheoremProducerOld::canonInvertMult(const Expr& e)
00817 {
00818 DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString());
00819
00820 Proof pf;
00821
00822 if (withProof()) {
00823 pf = newPf("canon_invert_mult", e);
00824 }
00825
00826 DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString());
00827 Expr result = canonInvert(e[0]).getRHS();
00828 for (int i = 1; i < e.arity(); ++i) {
00829 result =
00830 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
00831 }
00832 return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
00833 }
00834
00835
00836
00837
00838 Theorem
00839 ArithTheoremProducerOld::canonInvert(const Expr& e)
00840 {
00841 DebugAssert(e.getKind() != PLUS,
00842 "Cannot do inverse on a PLUS"+e.toString());
00843 switch (e.getKind()) {
00844 case RATIONAL_EXPR:
00845 return canonInvertConst(e);
00846 break;
00847 case POW:
00848 return canonInvertPow(e);
00849 break;
00850 case MULT:
00851 return canonInvertMult(e);
00852 break;
00853 default:
00854
00855 return canonInvertLeaf(e);
00856 break;
00857 }
00858 }
00859
00860
00861 Theorem ArithTheoremProducerOld::moveSumConstantRight(const Expr& e) {
00862
00863
00864 if (CHECK_PROOFS) {
00865 CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString());
00866 CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString());
00867 CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString());
00868 }
00869
00870
00871 Rational r = 0;
00872
00873
00874 Expr right = e[0];
00875
00876
00877 vector<Expr> sumTerms;
00878
00879
00880 if (!right.isRational())
00881 for(Expr::iterator it = right.begin(); it != right.end(); it ++) {
00882
00883 if ((*it).isRational()) r = r + (*it).getRational();
00884
00885 else sumTerms.push_back((*it));
00886 }
00887
00888
00889 Expr transformed;
00890 if (sumTerms.size() > 1)
00891
00892 transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r));
00893 else
00894
00895 transformed = Expr(e.getKind(), sumTerms[0], rat(-r));
00896
00897
00898
00899 Proof pf;
00900 if (withProof()) pf = newPf("arithm_sum_constant_right", e);
00901
00902
00903 return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
00904 }
00905
00906 Theorem
00907 ArithTheoremProducerOld::canonDivide(const Expr& e)
00908 {
00909 DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString());
00910 Proof pf;
00911
00912 if (withProof()) {
00913 pf = newPf("canon_invert_divide", e);
00914 }
00915
00916 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
00917
00918 return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS()));
00919 }
00920
00921
00922
00923
00924 Theorem
00925 ArithTheoremProducerOld::canonMultTermConst(const Expr& c, const Expr& t) {
00926 Proof pf;
00927 if(CHECK_PROOFS) {
00928 CHECK_SOUND(isRational(c),
00929 CLASS_NAME "::canonMultTermConst:\n "
00930 "c is not a constant: " + c.toString());
00931 }
00932 if(withProof()) pf = newPf("canon_mult_term_const", c, t);
00933 return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
00934 }
00935
00936
00937
00938 Theorem
00939 ArithTheoremProducerOld::canonMultTerm1Term2(const Expr& t1, const Expr& t2) {
00940
00941
00942 if(CHECK_PROOFS) {
00943 CHECK_SOUND(false, "Fatal Error: We don't support multiplication"
00944 "of two non constant terms at this time "
00945 + t1.toString() + " and " + t2.toString());
00946 }
00947 return Theorem();
00948 }
00949
00950
00951
00952 Theorem ArithTheoremProducerOld::canonMultZero(const Expr& e) {
00953 Proof pf;
00954 if(withProof()) pf = newPf("canon_mult_zero", e);
00955 return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
00956 }
00957
00958
00959
00960 Theorem ArithTheoremProducerOld::canonMultOne(const Expr& e) {
00961 Proof pf;
00962 if(withProof()) pf = newPf("canon_mult_one", e);
00963 return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
00964 }
00965
00966
00967
00968 Theorem
00969 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) {
00970 Proof pf;
00971 if(CHECK_PROOFS) {
00972 CHECK_SOUND(isRational(c1),
00973 CLASS_NAME "::canonMultConstConst:\n "
00974 "c1 is not a constant: " + c1.toString());
00975 CHECK_SOUND(isRational(c2),
00976 CLASS_NAME "::canonMultConstConst:\n "
00977 "c2 is not a constant: " + c2.toString());
00978 }
00979 if(withProof()) pf = newPf("canon_mult_const_const", c1, c2);
00980 return
00981 newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
00982 }
00983
00984
00985
00986 Theorem
00987 ArithTheoremProducerOld::canonMultConstTerm(const Expr& c1,
00988 const Expr& c2,const Expr& t) {
00989 Proof pf;
00990 if(CHECK_PROOFS) {
00991 CHECK_SOUND(isRational(c1),
00992 CLASS_NAME "::canonMultConstTerm:\n "
00993 "c1 is not a constant: " + c1.toString());
00994 CHECK_SOUND(isRational(c2),
00995 CLASS_NAME "::canonMultConstTerm:\n "
00996 "c2 is not a constant: " + c2.toString());
00997 }
00998
00999 if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t);
01000 return
01001 newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf);
01002 }
01003
01004
01005
01006 Theorem
01007 ArithTheoremProducerOld::canonMultConstSum(const Expr& c1, const Expr& sum) {
01008 Proof pf;
01009 std::vector<Expr> sumKids;
01010
01011 if(CHECK_PROOFS) {
01012 CHECK_SOUND(isRational(c1),
01013 CLASS_NAME "::canonMultConstTerm:\n "
01014 "c1 is not a constant: " + c1.toString());
01015 CHECK_SOUND(PLUS == sum.getKind(),
01016 CLASS_NAME "::canonMultConstTerm:\n "
01017 "the kind must be a PLUS: " + sum.toString());
01018 }
01019 Expr::iterator i = sum.begin();
01020 for(; i != sum.end(); ++i)
01021 sumKids.push_back(c1*(*i));
01022 Expr ret = plusExpr(sumKids);
01023 if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret);
01024 return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
01025 }
01026
01027
01028
01029 Theorem
01030 ArithTheoremProducerOld::canonPowConst(const Expr& e) {
01031 if(CHECK_PROOFS) {
01032 CHECK_SOUND(e.getKind() == POW && e.arity() == 2
01033 && e[0].isRational() && e[1].isRational(),
01034 "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01035 }
01036 const Rational& p = e[0].getRational();
01037 const Rational& base = e[1].getRational();
01038 if(CHECK_PROOFS) {
01039 CHECK_SOUND(p.isInteger(),
01040 "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01041 }
01042 Expr res;
01043 if (base == 0 && p < 0) {
01044 res = rat(0);
01045 }
01046 else res = rat(pow(p, base));
01047 Proof pf;
01048 if(withProof())
01049 pf = newPf("canon_pow_const", e);
01050 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01051 }
01052
01053
01054
01055
01056 Theorem
01057 ArithTheoremProducerOld::canonFlattenSum(const Expr& e) {
01058 Proof pf;
01059 std::vector<Expr> sumKids;
01060 if(CHECK_PROOFS) {
01061 CHECK_SOUND(PLUS == e.getKind(),
01062 CLASS_NAME "::canonFlattenSum:\n"
01063 "input must be a PLUS:" + e.toString());
01064 }
01065
01066 Expr::iterator i = e.begin();
01067 for(; i != e.end(); ++i){
01068 if (PLUS != (*i).getKind())
01069 sumKids.push_back(*i);
01070 else {
01071 Expr::iterator j = (*i).begin();
01072 for(; j != (*i).end(); ++j)
01073 sumKids.push_back(*j);
01074 }
01075 }
01076 Expr ret = plusExpr(sumKids);
01077 if(withProof()) pf = newPf("canon_flatten_sum", e,ret);
01078 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01079 }
01080
01081
01082
01083 Theorem
01084 ArithTheoremProducerOld::canonComboLikeTerms(const Expr& e) {
01085 Proof pf;
01086 std::vector<Expr> sumKids;
01087 ExprMap<Rational> sumHashMap;
01088 Rational constant = 0;
01089
01090 if(CHECK_PROOFS) {
01091 Expr::iterator k = e.begin();
01092 for(; k != e.end(); ++k)
01093 CHECK_SOUND(!isPlus(*k),
01094 CLASS_NAME "::canonComboLikeTerms:\n"
01095 "input must be a flattened PLUS:" + k->toString());
01096 }
01097 Expr::iterator i = e.begin();
01098 for(; i != e.end(); ++i){
01099 if(i->isRational())
01100 constant = constant + i->getRational();
01101 else {
01102 if (!isMult(*i)) {
01103 if(0 == sumHashMap.count((*i)))
01104 sumHashMap[*i] = 1;
01105 else
01106 sumHashMap[*i] += 1;
01107 }
01108 else {
01109 if(0 == sumHashMap.count((*i)[1]))
01110 sumHashMap[(*i)[1]] = (*i)[0].getRational();
01111 else
01112 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
01113 }
01114 }
01115 }
01116
01117 sumKids.push_back(rat(constant));
01118 ExprMap<Rational>::iterator j = sumHashMap.begin();
01119 for(; j != sumHashMap.end(); ++j) {
01120 if(0 == (*j).second)
01121 ;
01122 else if (1 == (*j).second)
01123 sumKids.push_back((*j).first);
01124 else
01125 sumKids.push_back(rat((*j).second) * (*j).first);
01126 }
01127
01128
01129
01130
01131 Expr ret;
01132 if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
01133 else if (1 == sumKids.size()) ret = sumKids[0];
01134 else ret = plusExpr(sumKids);
01135
01136 if(withProof()) pf = newPf("canon_combo_like_terms",e,ret);
01137 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01138 }
01139
01140
01141
01142
01143
01144
01145
01146 Theorem ArithTheoremProducerOld::constPredicate(const Expr& e) {
01147 if(CHECK_PROOFS) {
01148 CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
01149 CLASS_NAME "::constPredicate:\n "
01150 "non-const parameters: " + e.toString());
01151 }
01152 Proof pf;
01153 bool result(false);
01154 int kind = e.getKind();
01155 Rational r1 = e[0].getRational(), r2 = e[1].getRational();
01156 switch(kind) {
01157 case EQ:
01158 result = (r1 == r2)?true : false;
01159 break;
01160 case LT:
01161 result = (r1 < r2)?true : false;
01162 break;
01163 case LE:
01164 result = (r1 <= r2)?true : false;
01165 break;
01166 case GT:
01167 result = (r1 > r2)?true : false;
01168 break;
01169 case GE:
01170 result = (r1 >= r2)?true : false;
01171 break;
01172 default:
01173 if(CHECK_PROOFS) {
01174 CHECK_SOUND(false,
01175 "ArithTheoremProducerOld::constPredicate: wrong kind");
01176 }
01177 break;
01178 }
01179 Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
01180 if(withProof()) pf = newPf("const_predicate", e,ret);
01181 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01182 }
01183
01184
01185 Theorem ArithTheoremProducerOld::rightMinusLeft(const Expr& e)
01186 {
01187 Proof pf;
01188 int kind = e.getKind();
01189 if(CHECK_PROOFS) {
01190 CHECK_SOUND((EQ==kind) ||
01191 (LT==kind) ||
01192 (LE==kind) ||
01193 (GE==kind) ||
01194 (GT==kind),
01195 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01196 }
01197 if(withProof()) pf = newPf("right_minus_left",e);
01198 return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
01199 }
01200
01201
01202
01203 Theorem ArithTheoremProducerOld::leftMinusRight(const Expr& e)
01204 {
01205 Proof pf;
01206 int kind = e.getKind();
01207 if(CHECK_PROOFS) {
01208 CHECK_SOUND((EQ==kind) ||
01209 (LT==kind) ||
01210 (LE==kind) ||
01211 (GE==kind) ||
01212 (GT==kind),
01213 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01214 }
01215 if(withProof()) pf = newPf("left_minus_right",e);
01216 return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
01217 }
01218
01219
01220
01221 Theorem ArithTheoremProducerOld::plusPredicate(const Expr& x,
01222 const Expr& y,
01223 const Expr& z, int kind) {
01224 if(CHECK_PROOFS) {
01225 CHECK_SOUND((EQ==kind) ||
01226 (LT==kind) ||
01227 (LE==kind) ||
01228 (GE==kind) ||
01229 (GT==kind),
01230 "ArithTheoremProducerOld::plusPredicate: wrong kind");
01231 }
01232 Proof pf;
01233 Expr left = Expr(kind, x, y);
01234 Expr right = Expr(kind, x + z, y + z);
01235 if(withProof()) pf = newPf("plus_predicate",left,right);
01236 return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
01237 }
01238
01239
01240 Theorem ArithTheoremProducerOld::multEqn(const Expr& x,
01241 const Expr& y,
01242 const Expr& z) {
01243 Proof pf;
01244 if(CHECK_PROOFS)
01245 CHECK_SOUND(z.isRational() && z.getRational() != 0,
01246 "ArithTheoremProducerOld::multEqn(): multiplying equation by 0");
01247 if(withProof()) pf = newPf("mult_eqn", x, y, z);
01248 return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
01249 }
01250
01251
01252
01253
01254 Theorem ArithTheoremProducerOld::multIneqn(const Expr& e, const Expr& z)
01255 {
01256 int kind = e.getKind();
01257
01258 if(CHECK_PROOFS) {
01259 CHECK_SOUND((LT==kind) ||
01260 (LE==kind) ||
01261 (GE==kind) ||
01262 (GT==kind),
01263 "ArithTheoremProducerOld::multIneqn: wrong kind");
01264 CHECK_SOUND(z.isRational() && z.getRational() != 0,
01265 "ArithTheoremProducerOld::multIneqn: "
01266 "z must be non-zero rational: " + z.toString());
01267 }
01268 Op op(e.getOp());
01269 Proof pf;
01270
01271 Expr ret;
01272 if(0 < z.getRational())
01273 ret = Expr(op, e[0]*z, e[1]*z);
01274 else
01275 ret = Expr(op, e[1]*z, e[0]*z);
01276 if(withProof()) pf = newPf("mult_ineqn", e, ret);
01277 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01278 }
01279
01280
01281 Theorem ArithTheoremProducerOld::eqToIneq(const Expr& e) {
01282
01283
01284 if (CHECK_PROOFS)
01285 CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
01286
01287
01288 Proof pf;
01289
01290
01291 const Expr& x = e[0];
01292 const Expr& y = e[1];
01293
01294
01295 if (withProof())
01296 pf = newPf("eqToIneq", e);
01297
01298
01299 return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
01300 }
01301
01302
01303 Theorem ArithTheoremProducerOld::flipInequality(const Expr& e)
01304 {
01305 Proof pf;
01306 if(CHECK_PROOFS) {
01307 CHECK_SOUND(isGT(e) || isGE(e),
01308 "ArithTheoremProducerOld::flipInequality: wrong kind: " +
01309 e.toString());
01310 }
01311
01312 int kind = isGE(e) ? LE : LT;
01313 Expr ret = Expr(kind, e[1], e[0]);
01314 if(withProof()) pf = newPf("flip_inequality", e,ret);
01315 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01316 }
01317
01318
01319
01320
01321
01322
01323 Theorem ArithTheoremProducerOld::negatedInequality(const Expr& e)
01324 {
01325 const Expr& ineq = e[0];
01326 if(CHECK_PROOFS) {
01327 CHECK_SOUND(e.isNot(),
01328 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01329 e.toString());
01330 CHECK_SOUND(isIneq(ineq),
01331 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01332 (ineq).toString());
01333 }
01334 Proof pf;
01335 if(withProof()) pf = newPf("negated_inequality", e);
01336
01337 int kind;
01338
01339
01340
01341
01342 kind =
01343 isLT(ineq) ? GE :
01344 isLE(ineq) ? GT :
01345 isGT(ineq) ? LE :
01346 LT;
01347 return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
01348 }
01349
01350
01351
01352 Theorem ArithTheoremProducerOld::realShadow(const Theorem& alphaLTt,
01353 const Theorem& tLTbeta)
01354 {
01355 const Expr& expr1 = alphaLTt.getExpr();
01356 const Expr& expr2 = tLTbeta.getExpr();
01357 if(CHECK_PROOFS) {
01358 CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
01359 (isLE(expr2) || isLT(expr2)),
01360 "ArithTheoremProducerOld::realShadow: Wrong Kind: " +
01361 alphaLTt.toString() + tLTbeta.toString());
01362
01363 CHECK_SOUND(expr1[1] == expr2[0],
01364 "ArithTheoremProducerOld::realShadow:"
01365 " t must be same for both inputs: " +
01366 expr1[1].toString() + " , " + expr2[0].toString());
01367 }
01368 Assumptions a(alphaLTt, tLTbeta);
01369 int firstKind = expr1.getKind();
01370 int secondKind = expr2.getKind();
01371 int kind = (firstKind == secondKind) ? firstKind : LT;
01372 Proof pf;
01373 if(withProof()) {
01374 vector<Proof> pfs;
01375 pfs.push_back(alphaLTt.getProof());
01376 pfs.push_back(tLTbeta.getProof());
01377 pf = newPf("real_shadow",expr1, expr2, pfs);
01378 }
01379 return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf);
01380 }
01381
01382
01383
01384
01385
01386
01387 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt,
01388 const Theorem& tLEalpha)
01389 {
01390 const Expr& expr1 = alphaLEt.getExpr();
01391 const Expr& expr2 = tLEalpha.getExpr();
01392 if(CHECK_PROOFS) {
01393 CHECK_SOUND(isLE(expr1) && isLE(expr2),
01394 "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " +
01395 alphaLEt.toString() + tLEalpha.toString());
01396
01397 CHECK_SOUND(expr1[1] == expr2[0],
01398 "ArithTheoremProducerOld::realShadowLTLE:"
01399 " t must be same for both inputs: " +
01400 alphaLEt.toString() + " , " + tLEalpha.toString());
01401
01402 CHECK_SOUND(expr1[0] == expr2[1],
01403 "ArithTheoremProducerOld::realShadowLTLE:"
01404 " alpha must be same for both inputs: " +
01405 alphaLEt.toString() + " , " + tLEalpha.toString());
01406 }
01407 Assumptions a(alphaLEt, tLEalpha);
01408 Proof pf;
01409 if(withProof()) {
01410 vector<Proof> pfs;
01411 pfs.push_back(alphaLEt.getProof());
01412 pfs.push_back(tLEalpha.getProof());
01413 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
01414 }
01415 return newRWTheorem(expr1[0], expr1[1], a, pf);
01416 }
01417
01418 Theorem
01419 ArithTheoremProducerOld::finiteInterval(const Theorem& aLEt,
01420 const Theorem& tLEac,
01421 const Theorem& isInta,
01422 const Theorem& isIntt) {
01423 const Expr& e1 = aLEt.getExpr();
01424 const Expr& e2 = tLEac.getExpr();
01425 if(CHECK_PROOFS) {
01426 CHECK_SOUND(isLE(e1) && isLE(e2),
01427 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01428 +e1.toString()+"\n e2 = "+e2.toString());
01429
01430 CHECK_SOUND(e1[1] == e2[0],
01431 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01432 +e1.toString()+"\n e2 = "+e2.toString());
01433
01434 CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
01435 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01436 +e1.toString()+"\n e2 = "+e2.toString());
01437
01438 CHECK_SOUND(e1[0] == e2[1][0],
01439 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01440 +e1.toString()+"\n e2 = "+e2.toString());
01441
01442 CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
01443 && e2[1][1].getRational() >= 1,
01444 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01445 +e1.toString()+"\n e2 = "+e2.toString());
01446
01447 const Expr& isIntaExpr = isInta.getExpr();
01448 const Expr& isInttExpr = isIntt.getExpr();
01449 CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
01450 "Wrong integrality constraint:\n e1 = "
01451 +e1.toString()+"\n isInta = "+isIntaExpr.toString());
01452 CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
01453 "Wrong integrality constraint:\n e1 = "
01454 +e1.toString()+"\n isIntt = "+isInttExpr.toString());
01455 }
01456 vector<Theorem> thms;
01457 thms.push_back(aLEt);
01458 thms.push_back(tLEac);
01459 thms.push_back(isInta);
01460 thms.push_back(isIntt);
01461 Assumptions a(thms);
01462 Proof pf;
01463 if(withProof()) {
01464 vector<Expr> es;
01465 vector<Proof> pfs;
01466 es.push_back(e1);
01467 es.push_back(e2);
01468 es.push_back(isInta.getExpr());
01469 es.push_back(isIntt.getExpr());
01470 pfs.push_back(aLEt.getProof());
01471 pfs.push_back(tLEac.getProof());
01472 pfs.push_back(isInta.getProof());
01473 pfs.push_back(isIntt.getProof());
01474 pf = newPf("finite_interval", es, pfs);
01475 }
01476
01477 Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
01478 return newTheorem(g, a, pf);
01479 }
01480
01481
01482
01483 Theorem ArithTheoremProducerOld::darkGrayShadow2ab(const Theorem& betaLEbx,
01484 const Theorem& axLEalpha,
01485 const Theorem& isIntAlpha,
01486 const Theorem& isIntBeta,
01487 const Theorem& isIntx) {
01488 const Expr& expr1 = betaLEbx.getExpr();
01489 const Expr& expr2 = axLEalpha.getExpr();
01490 const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01491 const Expr& isIntBetaExpr = isIntBeta.getExpr();
01492 const Expr& isIntxExpr = isIntx.getExpr();
01493
01494 if(CHECK_PROOFS) {
01495 CHECK_SOUND(isLE(expr1) && isLE(expr2),
01496 "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " +
01497 betaLEbx.toString() + axLEalpha.toString());
01498 }
01499
01500 const Expr& beta = expr1[0];
01501 const Expr& bx = expr1[1];
01502 const Expr& ax = expr2[0];
01503 const Expr& alpha = expr2[1];
01504 Rational a = isMult(ax)? ax[0].getRational() : 1;
01505 Rational b = isMult(bx)? bx[0].getRational() : 1;
01506 const Expr& x = isMult(ax)? ax[1] : ax;
01507
01508 if(CHECK_PROOFS) {
01509
01510 CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01511 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01512 "wrong integrality constraint:\n alpha = "
01513 +alpha.toString()+"\n isIntAlpha = "
01514 +isIntAlphaExpr.toString());
01515 CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01516 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01517 "wrong integrality constraint:\n beta = "
01518 +beta.toString()+"\n isIntBeta = "
01519 +isIntBetaExpr.toString());
01520 CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01521 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01522 "wrong integrality constraint:\n x = "
01523 +x.toString()+"\n isIntx = "
01524 +isIntxExpr.toString());
01525
01526 CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01527 "ArithTheoremProducerOld::darkGrayShadow2ab:\n ax<=alpha: " +
01528 axLEalpha.toString());
01529 CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01530 "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01531 +betaLEbx.toString()
01532 +"\n ax<=alpha: "+ axLEalpha.toString());
01533 CHECK_SOUND(1 <= a && a <= b && 2 <= b,
01534 "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01535 +betaLEbx.toString()
01536 +"\n ax<=alpha: "+ axLEalpha.toString());
01537 }
01538 vector<Theorem> thms;
01539 thms.push_back(betaLEbx);
01540 thms.push_back(axLEalpha);
01541 thms.push_back(isIntAlpha);
01542 thms.push_back(isIntBeta);
01543 thms.push_back(isIntx);
01544 Assumptions A(thms);
01545 Proof pf;
01546 if(withProof()) {
01547 vector<Proof> pfs;
01548 pfs.push_back(betaLEbx.getProof());
01549 pfs.push_back(axLEalpha.getProof());
01550 pfs.push_back(isIntAlpha.getProof());
01551 pfs.push_back(isIntBeta.getProof());
01552 pfs.push_back(isIntx.getProof());
01553
01554 pf = newPf("dark_grayshadow_2ab", expr1, expr2, pfs);
01555 }
01556
01557 Expr bAlpha = multExpr(rat(b), alpha);
01558 Expr aBeta = multExpr(rat(a), beta);
01559 Expr t = minusExpr(bAlpha, aBeta);
01560 Expr d = darkShadow(rat(a*b-1), t);
01561 Expr g = grayShadow(ax, alpha, -a+1, 0);
01562 return newTheorem((d || g) && (!d || !g), A, pf);
01563 }
01564
01565
01566 Theorem ArithTheoremProducerOld::darkGrayShadow2ba(const Theorem& betaLEbx,
01567 const Theorem& axLEalpha,
01568 const Theorem& isIntAlpha,
01569 const Theorem& isIntBeta,
01570 const Theorem& isIntx) {
01571 const Expr& expr1 = betaLEbx.getExpr();
01572 const Expr& expr2 = axLEalpha.getExpr();
01573 const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01574 const Expr& isIntBetaExpr = isIntBeta.getExpr();
01575 const Expr& isIntxExpr = isIntx.getExpr();
01576
01577 if(CHECK_PROOFS) {
01578 CHECK_SOUND(isLE(expr1) && isLE(expr2),
01579 "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " +
01580 betaLEbx.toString() + axLEalpha.toString());
01581 }
01582
01583 const Expr& beta = expr1[0];
01584 const Expr& bx = expr1[1];
01585 const Expr& ax = expr2[0];
01586 const Expr& alpha = expr2[1];
01587 Rational a = isMult(ax)? ax[0].getRational() : 1;
01588 Rational b = isMult(bx)? bx[0].getRational() : 1;
01589 const Expr& x = isMult(ax)? ax[1] : ax;
01590
01591 if(CHECK_PROOFS) {
01592
01593 CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01594 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01595 "wrong integrality constraint:\n alpha = "
01596 +alpha.toString()+"\n isIntAlpha = "
01597 +isIntAlphaExpr.toString());
01598 CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01599 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01600 "wrong integrality constraint:\n beta = "
01601 +beta.toString()+"\n isIntBeta = "
01602 +isIntBetaExpr.toString());
01603 CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01604 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01605 "wrong integrality constraint:\n x = "
01606 +x.toString()+"\n isIntx = "
01607 +isIntxExpr.toString());
01608
01609 CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01610 "ArithTheoremProducerOld::darkGrayShadow2ba:\n ax<=alpha: " +
01611 axLEalpha.toString());
01612 CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01613 "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01614 +betaLEbx.toString()
01615 +"\n ax<=alpha: "+ axLEalpha.toString());
01616 CHECK_SOUND(1 <= b && b <= a && 2 <= a,
01617 "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01618 +betaLEbx.toString()
01619 +"\n ax<=alpha: "+ axLEalpha.toString());
01620 }
01621 vector<Theorem> thms;
01622 thms.push_back(betaLEbx);
01623 thms.push_back(axLEalpha);
01624 thms.push_back(isIntAlpha);
01625 thms.push_back(isIntBeta);
01626 thms.push_back(isIntx);
01627 Assumptions A(thms);
01628 Proof pf;
01629 if(withProof()) {
01630 vector<Proof> pfs;
01631 pfs.push_back(betaLEbx.getProof());
01632 pfs.push_back(axLEalpha.getProof());
01633 pfs.push_back(isIntAlpha.getProof());
01634 pfs.push_back(isIntBeta.getProof());
01635 pfs.push_back(isIntx.getProof());
01636
01637 pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
01638 axLEalpha.getExpr(), pfs);
01639 }
01640
01641 Expr bAlpha = multExpr(rat(b), alpha);
01642 Expr aBeta = multExpr(rat(a), beta);
01643 Expr t = minusExpr(bAlpha, aBeta);
01644 Expr d = darkShadow(rat(a*b-1), t);
01645 Expr g = grayShadow(bx, beta, 0, b-1);
01646 return newTheorem((d || g) && (!d || !g), A, pf);
01647 }
01648
01649
01650
01651 Theorem ArithTheoremProducerOld::expandDarkShadow(const Theorem& darkShadow) {
01652 const Expr& theShadow = darkShadow.getExpr();
01653 if(CHECK_PROOFS){
01654 CHECK_SOUND(isDarkShadow(theShadow),
01655 "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " +
01656 theShadow.toString());
01657 }
01658 Proof pf;
01659 if(withProof())
01660 pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
01661 return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
01662 }
01663
01664
01665
01666 Theorem ArithTheoremProducerOld::expandGrayShadow0(const Theorem& grayShadow) {
01667 const Expr& theShadow = grayShadow.getExpr();
01668 if(CHECK_PROOFS) {
01669 CHECK_SOUND(isGrayShadow(theShadow),
01670 "ArithTheoremProducerOld::expandGrayShadowConst0:"
01671 " not GRAY_SHADOW: " +
01672 theShadow.toString());
01673 CHECK_SOUND(theShadow[2] == theShadow[3],
01674 "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " +
01675 theShadow.toString());
01676 }
01677 Proof pf;
01678 if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
01679 grayShadow.getProof());
01680 const Expr& v = theShadow[0];
01681 const Expr& e = theShadow[1];
01682 return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
01683 }
01684
01685
01686
01687
01688
01689
01690
01691 Theorem ArithTheoremProducerOld::splitGrayShadow(const Theorem& gThm) {
01692 const Expr& theShadow = gThm.getExpr();
01693 if(CHECK_PROOFS) {
01694 CHECK_SOUND(isGrayShadow(theShadow),
01695 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
01696 theShadow.toString());
01697 }
01698
01699 const Rational& c1 = theShadow[2].getRational();
01700 const Rational& c2 = theShadow[3].getRational();
01701
01702 if(CHECK_PROOFS) {
01703 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01704 "ArithTheoremProducerOld::expandGrayShadow: " +
01705 theShadow.toString());
01706 }
01707
01708 const Expr& v = theShadow[0];
01709 const Expr& e = theShadow[1];
01710
01711 Proof pf;
01712 if(withProof())
01713 pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
01714 Rational c(floor((c1+c2) / 2));
01715 Expr g1(grayShadow(v, e, c1, c));
01716 Expr g2(grayShadow(v, e, c+1, c2));
01717 return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
01718 }
01719
01720
01721 Theorem ArithTheoremProducerOld::expandGrayShadow(const Theorem& gThm) {
01722 const Expr& theShadow = gThm.getExpr();
01723 if(CHECK_PROOFS) {
01724 CHECK_SOUND(isGrayShadow(theShadow),
01725 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
01726 theShadow.toString());
01727 }
01728
01729 const Rational& c1 = theShadow[2].getRational();
01730 const Rational& c2 = theShadow[3].getRational();
01731
01732 if(CHECK_PROOFS) {
01733 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01734 "ArithTheoremProducerOld::expandGrayShadow: " +
01735 theShadow.toString());
01736 }
01737
01738 const Expr& v = theShadow[0];
01739 const Expr& e = theShadow[1];
01740
01741 Proof pf;
01742 if(withProof())
01743 pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
01744 Expr ineq1(leExpr(e+rat(c1), v));
01745 Expr ineq2(leExpr(v, e+rat(c2)));
01746 return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
01747 }
01748
01749
01750
01751 Theorem
01752 ArithTheoremProducerOld::expandGrayShadowConst(const Theorem& gThm) {
01753 const Expr& theShadow = gThm.getExpr();
01754 const Expr& ax = theShadow[0];
01755 const Expr& cExpr = theShadow[1];
01756 const Expr& bExpr = theShadow[2];
01757
01758 if(CHECK_PROOFS) {
01759 CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
01760 "ArithTheoremProducerOld::expandGrayShadowConst: "
01761 "'a' in a*x is not a const: " +theShadow.toString());
01762 }
01763
01764 Rational a = isMult(ax)? ax[0].getRational() : 1;
01765
01766 if(CHECK_PROOFS) {
01767 CHECK_SOUND(isGrayShadow(theShadow),
01768 "ArithTheoremProducerOld::expandGrayShadowConst: "
01769 "not a GRAY_SHADOW: " +theShadow.toString());
01770 CHECK_SOUND(a.isInteger() && a >= 1,
01771 "ArithTheoremProducerOld::expandGrayShadowConst: "
01772 "'a' is not integer: " +theShadow.toString());
01773 CHECK_SOUND(cExpr.isRational(),
01774 "ArithTheoremProducerOld::expandGrayShadowConst: "
01775 "'c' is not rational" +theShadow.toString());
01776 CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
01777 "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: "
01778 +theShadow.toString());
01779 }
01780
01781 const Rational& b = bExpr.getRational();
01782 const Rational& c = cExpr.getRational();
01783 Rational j = constRHSGrayShadow(c,b,a);
01784
01785 Rational signB = (b>0)? 1 : -1;
01786
01787 Rational bAbs = abs(b);
01788
01789 const Assumptions& assump(gThm.getAssumptionsRef());
01790 Proof pf;
01791 Theorem conc;
01792
01793 if(bAbs < j) {
01794 if(withProof())
01795 pf = newPf("expand_gray_shadow_const_0", theShadow,
01796 gThm.getProof());
01797 conc = newTheorem(d_em->falseExpr(), assump, pf);
01798 } else if(bAbs < a+j) {
01799 if(withProof())
01800 pf = newPf("expand_gray_shadow_const_1", theShadow,
01801 gThm.getProof());
01802 conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
01803 } else {
01804 if(withProof())
01805 pf = newPf("expand_gray_shadow_const", theShadow,
01806 gThm.getProof());
01807 Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
01808 conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
01809 assump, pf);
01810 }
01811
01812 return conc;
01813 }
01814
01815
01816 Theorem
01817 ArithTheoremProducerOld::grayShadowConst(const Theorem& gThm) {
01818 const Expr& g = gThm.getExpr();
01819 bool checkProofs(CHECK_PROOFS);
01820 if(checkProofs) {
01821 CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducerOld::grayShadowConst("
01822 +g.toString()+")");
01823 }
01824
01825 const Expr& ax = g[0];
01826 const Expr& e = g[1];
01827 const Rational& c1 = g[2].getRational();
01828 const Rational& c2 = g[3].getRational();
01829 Expr aExpr, x;
01830 d_theoryArith->separateMonomial(ax, aExpr, x);
01831
01832 if(checkProofs) {
01833 CHECK_SOUND(e.isRational() && e.getRational().isInteger(),
01834 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01835 CHECK_SOUND(aExpr.isRational(),
01836 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01837 }
01838
01839 const Rational& a = aExpr.getRational();
01840 const Rational& c = e.getRational();
01841
01842 if(checkProofs) {
01843 CHECK_SOUND(a.isInteger() && a >= 2,
01844 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01845 }
01846
01847 Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
01848 Expr newG((newC1 > newC2)? d_em->falseExpr()
01849 : grayShadow(x, rat(0), newC1, newC2));
01850 Proof pf;
01851 if(withProof())
01852 pf = newPf("gray_shadow_const", g, gThm.getProof());
01853 return newTheorem(newG, gThm.getAssumptionsRef(), pf);
01854 }
01855
01856
01857 Rational ArithTheoremProducerOld::constRHSGrayShadow(const Rational& c,
01858 const Rational& b,
01859 const Rational& a) {
01860 DebugAssert(c.isInteger() &&
01861 b.isInteger() &&
01862 a.isInteger() &&
01863 b != 0,
01864 "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints");
01865 if (b > 0)
01866 return mod(c+b, a);
01867 else
01868 return mod(a-(c+b), a);
01869 }
01870
01871
01872
01873
01874
01875 Theorem ArithTheoremProducerOld::lessThanToLE(const Theorem& less,
01876 const Theorem& isIntLHS,
01877 const Theorem& isIntRHS,
01878 bool changeRight) {
01879 const Expr& ineq = less.getExpr();
01880 const Expr& isIntLHSexpr = isIntLHS.getExpr();
01881 const Expr& isIntRHSexpr = isIntRHS.getExpr();
01882
01883 if(CHECK_PROOFS) {
01884 CHECK_SOUND(isLT(ineq),
01885 "ArithTheoremProducerOld::LTtoLE: ineq must be <");
01886
01887 CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
01888 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
01889 " ineq = "+ineq.toString()+"\n isIntLHS = "
01890 +isIntLHSexpr.toString());
01891 CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
01892 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
01893 " ineq = "+ineq.toString()+"\n isIntRHS = "
01894 +isIntRHSexpr.toString());
01895 }
01896 vector<Theorem> thms;
01897 thms.push_back(less);
01898 thms.push_back(isIntLHS);
01899 thms.push_back(isIntRHS);
01900 Assumptions a(thms);
01901 Proof pf;
01902 if(withProof()) {
01903 vector<Proof> pfs;
01904 pfs.push_back(less.getProof());
01905 pfs.push_back(isIntLHS.getProof());
01906 pfs.push_back(isIntRHS.getProof());
01907 pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
01908 ineq, pfs);
01909 }
01910 Expr le = changeRight?
01911 leExpr(ineq[0], ineq[1] + rat(-1))
01912 : leExpr(ineq[0] + rat(1), ineq[1]);
01913 return newRWTheorem(ineq, le, a, pf);
01914 }
01915
01916
01917
01918
01919
01920
01921
01922
01923
01924
01925 Theorem
01926 ArithTheoremProducerOld::intVarEqnConst(const Expr& eqn,
01927 const Theorem& isIntx) {
01928 const Expr& left(eqn[0]);
01929 const Expr& right(eqn[1]);
01930 const Expr& isIntxexpr(isIntx.getExpr());
01931
01932 if(CHECK_PROOFS) {
01933 CHECK_SOUND((isMult(right) && right[0].isRational())
01934 || (right.arity() == 2 && isPlus(right)
01935 && right[0].isRational()
01936 && ((!isMult(right[1]) || right[1][0].isRational()))),
01937 "ArithTheoremProducerOld::intVarEqnConst: "
01938 "rhs has a wrong format: " + right.toString());
01939 CHECK_SOUND(left.isRational() && 0 == left.getRational(),
01940 "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " +
01941 left.toString());
01942 }
01943
01944 Expr x(right);
01945 Rational a(1), c(0);
01946 if(isMult(right)) {
01947 Expr aExpr;
01948 d_theoryArith->separateMonomial(right, aExpr, x);
01949 a = aExpr.getRational();
01950 } else {
01951 c = right[0].getRational();
01952 Expr aExpr;
01953 d_theoryArith->separateMonomial(right[1], aExpr, x);
01954 a = aExpr.getRational();
01955 }
01956 if(CHECK_PROOFS) {
01957 CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
01958 "ArithTheoremProducerOld:intVarEqnConst: "
01959 "bad integrality constraint:\n right = " +
01960 right.toString()+"\n isIntx = "+isIntxexpr.toString());
01961 CHECK_SOUND(a!=0, "ArithTheoremProducerOld:intVarEqnConst: eqn = "
01962 +eqn.toString());
01963 }
01964 const Assumptions& assump(isIntx.getAssumptionsRef());
01965 Proof pf;
01966 if(withProof())
01967 pf = newPf("int_const_eq", eqn, isIntx.getProof());
01968
01969
01970 Rational r(-c/a);
01971
01972 if(r.isInteger())
01973 return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
01974 else
01975 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
01976 }
01977
01978
01979 Expr
01980 ArithTheoremProducerOld::create_t(const Expr& eqn) {
01981 const Expr& lhs = eqn[0];
01982 DebugAssert(isMult(lhs),
01983 CLASS_NAME "create_t : lhs must be a MULT"
01984 + lhs.toString());
01985 const Expr& x = lhs[1];
01986 Rational m = lhs[0].getRational()+1;
01987 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t: m = "+m.toString());
01988 vector<Expr> kids;
01989 if(isPlus(eqn[1]))
01990 sumModM(kids, eqn[1], m, m);
01991 else
01992 kids.push_back(monomialModM(eqn[1], m, m));
01993
01994 kids.push_back(multExpr(rat(1/m), x));
01995 return plusExpr(kids);
01996 }
01997
01998 Expr
01999 ArithTheoremProducerOld::create_t2(const Expr& lhs, const Expr& rhs,
02000 const Expr& sigma) {
02001 Rational m = lhs[0].getRational()+1;
02002 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t2: m = "+m.toString());
02003 vector<Expr> kids;
02004 if(isPlus(rhs))
02005 sumModM(kids, rhs, m, -1);
02006 else {
02007 kids.push_back(rat(0));
02008 Expr monom = monomialModM(rhs, m, -1);
02009 if(!monom.isRational())
02010 kids.push_back(monom);
02011 else
02012 DebugAssert(monom.getRational() == 0, "");
02013 }
02014 kids.push_back(rat(m)*sigma);
02015 return plusExpr(kids);
02016 }
02017
02018 Expr
02019 ArithTheoremProducerOld::create_t3(const Expr& lhs, const Expr& rhs,
02020 const Expr& sigma) {
02021 const Rational& a = lhs[0].getRational();
02022 Rational m = a+1;
02023 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t3: m = "+m.toString());
02024 vector<Expr> kids;
02025 if(isPlus(rhs))
02026 sumMulF(kids, rhs, m, 1);
02027 else {
02028 kids.push_back(rat(0));
02029 Expr monom = monomialMulF(rhs, m, 1);
02030 if(!monom.isRational())
02031 kids.push_back(monom);
02032 else
02033 DebugAssert(monom.getRational() == 0, "");
02034 }
02035 kids.push_back(rat(-a)*sigma);
02036 return plusExpr(kids);
02037 }
02038
02039 Rational
02040 ArithTheoremProducerOld::modEq(const Rational& i, const Rational& m) {
02041 DebugAssert(m > 0, "ArithTheoremProducerOld::modEq: m = "+m.toString());
02042 Rational half(1,2);
02043 Rational res((i - m*(floor((i/m) + half))));
02044 TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
02045 return res;
02046 }
02047
02048 Rational
02049 ArithTheoremProducerOld::f(const Rational& i, const Rational& m) {
02050 DebugAssert(m > 0, "ArithTheoremProducerOld::f: m = "+m.toString());
02051 Rational half(1,2);
02052 return (floor(i/m + half)+modEq(i,m));
02053 }
02054
02055 void
02056 ArithTheoremProducerOld::sumModM(vector<Expr>& summands, const Expr& sum,
02057 const Rational& m, const Rational& divisor) {
02058 DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumModM: divisor = "
02059 +divisor.toString());
02060 Expr::iterator i = sum.begin();
02061 DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02062 Rational C = i->getRational();
02063 C = modEq(C,m)/divisor;
02064 summands.push_back(rat(C));
02065 i++;
02066 for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02067 Expr monom = monomialModM(*i, m, divisor);
02068 if(!monom.isRational())
02069 summands.push_back(monom);
02070 else
02071 DebugAssert(monom.getRational() == 0, "");
02072 }
02073 }
02074
02075 Expr
02076 ArithTheoremProducerOld::monomialModM(const Expr& i,
02077 const Rational& m, const Rational& divisor)
02078 {
02079 DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialModM: divisor = "
02080 +divisor.toString());
02081 Expr res;
02082 if(isMult(i)) {
02083 Rational ai = i[0].getRational();
02084 ai = modEq(ai,m)/divisor;
02085 if(0 == ai) res = rat(0);
02086 else if(1 == ai && i.arity() == 2) res = i[1];
02087 else {
02088 vector<Expr> kids = i.getKids();
02089 kids[0] = rat(ai);
02090 res = multExpr(kids);
02091 }
02092 } else {
02093 Rational ai = modEq(1,m)/divisor;
02094 if(1 == ai) res = i;
02095 else res = rat(ai)*i;
02096 }
02097 DebugAssert(!res.isNull(), "ArithTheoremProducerOld::monomialModM()");
02098 TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
02099 +", div="+divisor.toString()+") = ", res, "");
02100 return res;
02101 }
02102
02103 void
02104 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands, const Expr& sum,
02105 const Rational& m, const Rational& divisor) {
02106 DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumMulF: divisor = "
02107 +divisor.toString());
02108 Expr::iterator i = sum.begin();
02109 DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02110 Rational C = i->getRational();
02111 C = f(C,m)/divisor;
02112 summands.push_back(rat(C));
02113 i++;
02114 for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02115 Expr monom = monomialMulF(*i, m, divisor);
02116 if(!monom.isRational())
02117 summands.push_back(monom);
02118 else
02119 DebugAssert(monom.getRational() == 0, "");
02120 }
02121 }
02122
02123 Expr
02124 ArithTheoremProducerOld::monomialMulF(const Expr& i,
02125 const Rational& m, const Rational& divisor)
02126 {
02127 DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialMulF: divisor = "
02128 +divisor.toString());
02129 Rational ai = isMult(i) ? (i)[0].getRational() : 1;
02130 Expr xi = isMult(i) ? (i)[1] : (i);
02131 ai = f(ai,m)/divisor;
02132 if(0 == ai) return rat(0);
02133 if(1 == ai) return xi;
02134 return multExpr(rat(ai), xi);
02135 }
02136
02137
02138
02139
02140 Expr
02141 ArithTheoremProducerOld::substitute(const Expr& term, ExprMap<Expr>& eMap)
02142 {
02143 ExprMap<Expr>::iterator i, iend = eMap.end();
02144
02145 i = eMap.find(term);
02146 if(iend != i)
02147 return (*i).second;
02148
02149 if (isMult(term)) {
02150
02151 i = eMap.find(term[1]);
02152 if(iend != i)
02153 return term[0]*(*i).second;
02154 else
02155 return term;
02156 }
02157
02158 if(isPlus(term)) {
02159 vector<Expr> output;
02160 for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
02161 output.push_back(substitute(*j, eMap));
02162 return plusExpr(output);
02163 }
02164 return term;
02165 }
02166
02167 bool ArithTheoremProducerOld::greaterthan(const Expr & l, const Expr & r)
02168 {
02169
02170 if (l==r) return false;
02171
02172 switch(l.getKind()) {
02173 case RATIONAL_EXPR:
02174 DebugAssert(!r.isRational(), "");
02175 return true;
02176 break;
02177 case POW:
02178 switch (r.getKind()) {
02179 case RATIONAL_EXPR:
02180
02181
02182 return false;
02183 break;
02184 case POW:
02185
02186
02187 return
02188 ((r[1] < l[1]) ||
02189 ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
02190 break;
02191
02192 case MULT:
02193 DebugAssert(r.arity() > 1, "");
02194 DebugAssert((r.arity() > 2) || (r[1] != l), "");
02195 if (r[1] == l) return false;
02196 return greaterthan(l, r[1]);
02197 break;
02198 case PLUS:
02199 DebugAssert(false, "");
02200 return true;
02201 break;
02202 default:
02203
02204 return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
02205 break;
02206 }
02207 break;
02208 case MULT:
02209 DebugAssert(l.arity() > 1, "");
02210 switch (r.getKind()) {
02211 case RATIONAL_EXPR:
02212 return false;
02213 break;
02214 case POW:
02215 DebugAssert(l.arity() > 1, "");
02216 DebugAssert((l.arity() > 2) || (l[1] != r), "");
02217
02218
02219 return ((l[1] == r) || greaterthan(l[1], r));
02220 break;
02221 case MULT:
02222 {
02223
02224 DebugAssert(r.arity() > 1, "");
02225 Expr::iterator i = l.begin();
02226 Expr::iterator j = r.begin();
02227 ++i;
02228 ++j;
02229 for (; i != l.end() && j != r.end(); ++i, ++j) {
02230 if (*i == *j)
02231 continue;
02232 return greaterthan(*i,*j);
02233 }
02234 DebugAssert(i != l.end() || j != r.end(), "");
02235 if (i == l.end()) {
02236
02237 return false;
02238 }
02239 else
02240 {
02241
02242 return true;
02243 }
02244 }
02245 break;
02246 case PLUS:
02247 DebugAssert(false, "");
02248 return true;
02249 break;
02250 default:
02251
02252 DebugAssert((l.arity() > 2) || (l[1] != r), "");
02253 return ((l[1] == r) || greaterthan(l[1], r));
02254 break;
02255 }
02256 break;
02257 case PLUS:
02258 DebugAssert(false, "");
02259 return true;
02260 break;
02261 default:
02262
02263 switch (r.getKind()) {
02264 case RATIONAL_EXPR:
02265 return false;
02266 break;
02267 case POW:
02268 return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
02269 break;
02270 case MULT:
02271 DebugAssert(r.arity() > 1, "");
02272 DebugAssert((r.arity() > 2) || (r[1] != l), "");
02273 if (l == r[1]) return false;
02274 return greaterthan(l,r[1]);
02275 break;
02276 case PLUS:
02277 DebugAssert(false, "");
02278 return true;
02279 break;
02280 default:
02281
02282 return (r < l);
02283 break;
02284 }
02285 break;
02286 }
02287 }
02288
02289
02290 Theorem
02291 ArithTheoremProducerOld::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
02292 const vector<Theorem>& isIntVars) {
02293 TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
02294 Proof pf;
02295
02296 if(CHECK_PROOFS)
02297 CHECK_SOUND(eqn.isRewrite(),
02298 "ArithTheoremProducerOld::eqElimInt: input must be an equation" +
02299 eqn.toString());
02300
02301 const Expr& lhs = eqn.getLHS();
02302 const Expr& rhs = eqn.getRHS();
02303 Expr a, x;
02304 d_theoryArith->separateMonomial(lhs, a, x);
02305
02306 if(CHECK_PROOFS) {
02307
02308 const Expr& isIntxe = isIntx.getExpr();
02309 CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
02310 "ArithTheoremProducerOld::eqElimInt\n eqn = "
02311 +eqn.getExpr().toString()
02312 +"\n isIntx = "+isIntxe.toString());
02313 CHECK_SOUND(isRational(a) && a.getRational().isInteger()
02314 && a.getRational() >= 2,
02315 "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.toString());
02316
02317
02318 CHECK_SOUND(!isDivide(rhs),
02319 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString());
02320
02321 if(!isPlus(rhs)) {
02322 Expr c, v;
02323 d_theoryArith->separateMonomial(rhs, c, v);
02324 CHECK_SOUND(isIntVars.size() == 1
02325 && isIntPred(isIntVars[0].getExpr())
02326 && isIntVars[0].getExpr()[0] == v
02327 && isRational(c) && c.getRational().isInteger(),
02328 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString()
02329 +"isIntVars.size = "+int2string(isIntVars.size()));
02330 } else {
02331 CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
02332 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02333
02334 CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
02335 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02336
02337 for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
02338 Expr c, v;
02339 d_theoryArith->separateMonomial(rhs[i+1], c, v);
02340 const Expr& isInt(isIntVars[i].getExpr());
02341 CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
02342 && isRational(c) && c.getRational().isInteger(),
02343 "ArithTheoremProducerOld::eqElimInt:\n rhs["+int2string(i+1)
02344 +"] = "+rhs[i+1].toString()
02345 +"\n isInt = "+isInt.toString());
02346 }
02347 }
02348 }
02349
02350
02351 static int varCount(0);
02352 Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
02353 newVar.setType(intType());
02354 Expr t2 = create_t2(lhs, rhs, newVar);
02355 Expr t3 = create_t3(lhs, rhs, newVar);
02356 vector<Expr> vars;
02357 vars.push_back(newVar);
02358 Expr res = d_em->newClosureExpr(EXISTS, vars,
02359 x.eqExpr(t2) && rat(0).eqExpr(t3));
02360
02361 vector<Theorem> thms(isIntVars);
02362 thms.push_back(isIntx);
02363 thms.push_back(eqn);
02364 Assumptions assump(thms);
02365
02366 if(withProof()) {
02367 vector<Proof> pfs;
02368 pfs.push_back(eqn.getProof());
02369 pfs.push_back(isIntx.getProof());
02370 vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
02371 for(; i!=iend; ++i)
02372 pfs.push_back(i->getProof());
02373 pf = newPf("eq_elim_int", eqn.getExpr(), pfs);
02374 }
02375
02376 Theorem thm(newTheorem(res, assump, pf));
02377 TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
02378 return thm;
02379 }
02380
02381
02382 Theorem
02383 ArithTheoremProducerOld::isIntConst(const Expr& e) {
02384 Proof pf;
02385
02386 if(CHECK_PROOFS) {
02387 CHECK_SOUND(isIntPred(e) && e[0].isRational(),
02388 "ArithTheoremProducerOld::isIntConst(e = "
02389 +e.toString()+")");
02390 }
02391 if(withProof())
02392 pf = newPf("is_int_const", e);
02393 bool isInt = e[0].getRational().isInteger();
02394 return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
02395 }
02396
02397
02398 Theorem
02399 ArithTheoremProducerOld::equalLeaves1(const Theorem& thm)
02400 {
02401 Proof pf;
02402 const Expr& e = thm.getRHS();
02403
02404 if (CHECK_PROOFS) {
02405 CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02406 e[1].getRational() == Rational(0) &&
02407 e[0].getKind() == PLUS &&
02408 e[0].arity() == 3 &&
02409 e[0][0].getKind() == RATIONAL_EXPR &&
02410 e[0][0].getRational() == Rational(0) &&
02411 e[0][1].getKind() == MULT &&
02412 e[0][1].arity() == 2 &&
02413 e[0][1][0].getKind() == RATIONAL_EXPR &&
02414 e[0][1][0].getRational() == Rational(-1),
02415 "equalLeaves1");
02416 }
02417 if (withProof())
02418 {
02419 vector<Proof> pfs;
02420 pfs.push_back(thm.getProof());
02421 pf = newPf("equalLeaves1", e, pfs);
02422 }
02423 return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
02424 }
02425
02426
02427 Theorem
02428 ArithTheoremProducerOld::equalLeaves2(const Theorem& thm)
02429 {
02430 Proof pf;
02431 const Expr& e = thm.getRHS();
02432
02433 if (CHECK_PROOFS) {
02434 CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02435 e[0].getRational() == Rational(0) &&
02436 e[1].getKind() == PLUS &&
02437 e[1].arity() == 3 &&
02438 e[1][0].getKind() == RATIONAL_EXPR &&
02439 e[1][0].getRational() == Rational(0) &&
02440 e[1][1].getKind() == MULT &&
02441 e[1][1].arity() == 2 &&
02442 e[1][1][0].getKind() == RATIONAL_EXPR &&
02443 e[1][1][0].getRational() == Rational(-1),
02444 "equalLeaves2");
02445 }
02446 if (withProof())
02447 {
02448 vector<Proof> pfs;
02449 pfs.push_back(thm.getProof());
02450 pf = newPf("equalLeaves2", e, pfs);
02451 }
02452 return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
02453 }
02454
02455
02456 Theorem
02457 ArithTheoremProducerOld::equalLeaves3(const Theorem& thm)
02458 {
02459 Proof pf;
02460 const Expr& e = thm.getRHS();
02461
02462 if (CHECK_PROOFS) {
02463 CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02464 e[1].getRational() == Rational(0) &&
02465 e[0].getKind() == PLUS &&
02466 e[0].arity() == 3 &&
02467 e[0][0].getKind() == RATIONAL_EXPR &&
02468 e[0][0].getRational() == Rational(0) &&
02469 e[0][2].getKind() == MULT &&
02470 e[0][2].arity() == 2 &&
02471 e[0][2][0].getKind() == RATIONAL_EXPR &&
02472 e[0][2][0].getRational() == Rational(-1),
02473 "equalLeaves3");
02474 }
02475 if (withProof())
02476 {
02477 vector<Proof> pfs;
02478 pfs.push_back(thm.getProof());
02479 pf = newPf("equalLeaves3", e, pfs);
02480 }
02481 return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
02482 }
02483
02484
02485 Theorem
02486 ArithTheoremProducerOld::equalLeaves4(const Theorem& thm)
02487 {
02488 Proof pf;
02489 const Expr& e = thm.getRHS();
02490
02491 if (CHECK_PROOFS) {
02492 CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02493 e[0].getRational() == Rational(0) &&
02494 e[1].getKind() == PLUS &&
02495 e[1].arity() == 3 &&
02496 e[1][0].getKind() == RATIONAL_EXPR &&
02497 e[1][0].getRational() == Rational(0) &&
02498 e[1][2].getKind() == MULT &&
02499 e[1][2].arity() == 2 &&
02500 e[1][2][0].getKind() == RATIONAL_EXPR &&
02501 e[1][2][0].getRational() == Rational(-1),
02502 "equalLeaves4");
02503 }
02504 if (withProof())
02505 {
02506 vector<Proof> pfs;
02507 pfs.push_back(thm.getProof());
02508 pf = newPf("equalLeaves4", e, pfs);
02509 }
02510 return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
02511 }
02512
02513 Theorem
02514 ArithTheoremProducerOld::diseqToIneq(const Theorem& diseq) {
02515 Proof pf;
02516
02517 const Expr& e = diseq.getExpr();
02518
02519 if(CHECK_PROOFS) {
02520 CHECK_SOUND(e.isNot() && e[0].isEq(),
02521 "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n"
02522 " e = "+e.toString());
02523 }
02524
02525 const Expr& x = e[0][0];
02526 const Expr& y = e[0][1];
02527
02528 if(withProof())
02529 pf = newPf(e, diseq.getProof());
02530 return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
02531 }
02532
02533 Theorem ArithTheoremProducerOld::dummyTheorem(const Expr& e) {
02534 Proof pf;
02535 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
02536 }
02537
02538 Theorem ArithTheoremProducerOld::oneElimination(const Expr& e) {
02539
02540
02541 if (CHECK_PROOFS)
02542 CHECK_SOUND(isMult(e) &&
02543 e.arity() == 2 &&
02544 e[0].isRational() &&
02545 e[0].getRational() == 1,
02546 "oneElimination: input must be a multiplication by one" + e.toString());
02547
02548
02549 Proof pf;
02550
02551
02552 if (withProof())
02553 pf = newPf("oneElimination", e);
02554
02555
02556 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
02557 }
02558
02559 Theorem ArithTheoremProducerOld::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
02560
02561
02562 const Expr& lowerBoundExpr = lowerBound.getExpr();
02563 const Expr& upperBoundExpr = upperBound.getExpr();
02564
02565
02566 if (CHECK_PROOFS) {
02567 CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
02568 CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
02569 CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
02570 CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
02571 CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
02572
02573
02574 Rational lowerBoundR = lowerBoundExpr[0].getRational();
02575 Rational upperBoundR = upperBoundExpr[0].getRational();
02576
02577 if (isLE(lowerBoundExpr) && isGE(upperBoundExpr))
02578 CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
02579 else
02580 CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
02581 }
02582
02583
02584 Proof pf;
02585
02586 if (withProof())
02587 pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
02588
02589
02590 Assumptions assumptions;
02591 assumptions.add(lowerBound);
02592 assumptions.add(upperBound);
02593
02594
02595 return newTheorem(d_em->falseExpr(), assumptions, pf);
02596 }
02597
02598 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) {
02599
02600
02601 const Expr& expr1 = thm1.getExpr();
02602 const Expr& expr2 = thm2.getExpr();
02603
02604
02605 if (CHECK_PROOFS) {
02606
02607 CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
02608 CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
02609
02610 if (isLE(expr1) || isLT(expr1))
02611 CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
02612 if (isGE(expr1) || isGT(expr1))
02613 CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
02614 }
02615
02616
02617 Assumptions a(thm1, thm2);
02618
02619
02620 int kind1 = expr1.getKind();
02621 int kind2 = expr2.getKind();
02622
02623
02624 int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
02625
02626
02627 Proof pf;
02628 if(withProof()) {
02629 vector<Proof> pfs;
02630 pfs.push_back(thm1.getProof());
02631 pfs.push_back(thm2.getProof());
02632 pf = newPf("addInequalities", expr1, expr2, pfs);
02633 }
02634
02635
02636 Expr leftSide = plusExpr(expr1[0], expr2[0]);
02637 Expr rightSide = plusExpr(expr1[1], expr2[1]);
02638
02639
02640 return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
02641 }
02642
02643 Theorem ArithTheoremProducerOld::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
02644
02645
02646 if (CHECK_PROOFS) {
02647
02648
02649 CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
02650 CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
02651
02652
02653 if (isLE(expr1) || isLT(expr1))
02654 CHECK_SOUND(isLE(expr2) || isLT(expr2), "implyWeakerInequality: expr2 should be <(=) also " + expr2.toString());
02655 if (isGE(expr1) || isGT(expr1))
02656 CHECK_SOUND(isGE(expr2) || isGT(expr2), "implyWeakerInequality: expr2 should be >(=) also" + expr2.toString());
02657
02658
02659 CHECK_SOUND(expr1[0].isRational(), "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
02660 CHECK_SOUND(expr2[0].isRational(), "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
02661
02662
02663 CHECK_SOUND(expr1[1] == expr2[1], "implyWeakerInequality: the expression must be the same" + expr1.toString() + " and " + expr2.toString());
02664
02665 Rational expr1rat = expr1[0].getRational();
02666 Rational expr2rat = expr2[0].getRational();
02667
02668
02669
02670 if (isLE(expr1) || isLT(expr2))
02671 CHECK_SOUND(expr2rat < expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02672 else
02673 CHECK_SOUND(expr2rat <= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02674 if (isGE(expr1) || isGT(expr2))
02675 CHECK_SOUND(expr2rat > expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02676 else
02677 CHECK_SOUND(expr2rat >= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02678
02679 }
02680
02681
02682 Proof pf;
02683 if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
02684
02685
02686 return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
02687 }
02688
02689 Theorem ArithTheoremProducerOld::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
02690
02691
02692 if (CHECK_PROOFS) {
02693 CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: lowerBound should be an inequality " + expr1.toString());
02694 CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: upperBound should be be an inequality " + expr2.toString());
02695 CHECK_SOUND(expr1[0].isRational(), "implyNegatedInequality: lowerBound left side should be a rational " + expr1.toString());
02696 CHECK_SOUND(expr2[0].isRational(), "implyNegatedInequality: upperBound left side should be a rational " + expr2.toString());
02697 CHECK_SOUND(expr1[1] == expr2[1], "implyNegatedInequality: bounds not on the same term " + expr1.toString() + ", " + expr2.toString());
02698
02699
02700 Rational lowerBoundR = expr1[0].getRational();
02701 Rational upperBoundR = expr2[0].getRational();
02702
02703 if (isLE(expr1) && isGE(expr2))
02704 CHECK_SOUND(upperBoundR < lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02705 if (isLT(expr1) || isGT(expr2))
02706 CHECK_SOUND(upperBoundR <= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02707 if (isGE(expr1) && isLE(expr2))
02708 CHECK_SOUND(upperBoundR > lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02709 if (isGT(expr1) || isLT(expr2))
02710 CHECK_SOUND(upperBoundR >= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02711 }
02712
02713
02714 Proof pf;
02715 if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2);
02716
02717
02718 return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf);
02719 }
02720
02721 Theorem ArithTheoremProducerOld::trustedRewrite(const Expr& expr1, const Expr& expr2) {
02722
02723
02724 Proof pf;
02725
02726
02727 if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
02728
02729
02730 return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
02731
02732 }
02733
02734 Theorem ArithTheoremProducerOld::integerSplit(const Expr& intVar, const Rational& intPoint) {
02735
02736
02737 if (CHECK_PROOFS) {
02738 CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
02739 }
02740
02741
02742 const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
02743
02744
02745 Proof pf;
02746 if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
02747
02748
02749 return newTheorem(split, Assumptions::emptyAssump(), pf);
02750 }
02751
02752
02753 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
02754
02755
02756
02757 if (CHECK_PROOFS) {
02758
02759 CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
02760 CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
02761 CHECK_SOUND(constr[0].isRational(), "rafineStrictInteger: right side of the constraint muts be a rational");
02762 }
02763
02764
02765 Rational bound = constr[0].getRational();
02766
02767
02768 int kind = constr.getKind();
02769
02770
02771 switch (kind) {
02772 case LT:
02773 kind = LE;
02774 if (bound.isInteger()) bound ++;
02775 else bound = ceil(bound);
02776 break;
02777 case LE:
02778 kind = LE;
02779 if (!bound.isInteger()) bound = ceil(bound);
02780 break;
02781 case GT:
02782 kind = GE;
02783 if (bound.isInteger()) bound --;
02784 else bound = floor(bound);
02785 break;
02786 case GE:
02787 kind = GE;
02788 if (!bound.isInteger()) bound = floor(bound);
02789 break;
02790 }
02791
02792
02793 Expr newConstr(kind, rat(bound), constr[1]);
02794
02795
02796 const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
02797
02798
02799 Proof pf;
02800 if (withProof()) pf = newPf("rafineStrictInteger", constr, isIntConstrThm.getProof());
02801
02802
02803 return newRWTheorem(constr, newConstr, assump, pf);
02804 }