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