CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file arith_theorem_producer.cpp 00004 * 00005 * Author: Vijay Ganesh, Sergey Berezin 00006 * 00007 * Created: Dec 13 02:09:04 GMT 2002 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 // CLASS: ArithProofRules 00021 // 00022 // AUTHOR: Sergey Berezin, 12/11/2002 00023 // AUTHOR: Vijay Ganesh, 05/30/2003 00024 // 00025 // Description: TRUSTED implementation of arithmetic proof rules. 00026 // 00027 /////////////////////////////////////////////////////////////////////////////// 00028 00029 // This code is trusted 00030 #define _CVC3_TRUSTED_ 00031 00032 #include "arith_theorem_producer_old.h" 00033 #include "theory_core.h" 00034 #include "theory_arith_old.h" 00035 #include <algorithm> 00036 00037 using namespace std; 00038 using namespace CVC3; 00039 00040 //////////////////////////////////////////////////////////////////// 00041 // TheoryArith: trusted method for creating ArithTheoremProducerOld 00042 //////////////////////////////////////////////////////////////////// 00043 00044 ArithProofRules* TheoryArithOld::createProofRulesOld() { 00045 return new ArithTheoremProducerOld(theoryCore()->getTM(), this); 00046 } 00047 00048 //////////////////////////////////////////////////////////////////// 00049 // Canonization rules 00050 //////////////////////////////////////////////////////////////////// 00051 00052 00053 #define CLASS_NAME "ArithTheoremProducerOld" 00054 00055 00056 // Rule for variables: e == 1 * e 00057 Theorem ArithTheoremProducerOld::varToMult(const Expr& e) { 00058 Proof pf; 00059 if(withProof()) pf = newPf("var_to_mult", e); 00060 return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf); 00061 } 00062 00063 00064 // Rule for unary minus: -e == (-1) * e 00065 Theorem ArithTheoremProducerOld::uMinusToMult(const Expr& e) { 00066 Proof pf; 00067 if(withProof()) pf = newPf("uminus_to_mult", e); 00068 return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf); 00069 } 00070 00071 00072 // ==> x - y = x + (-1) * y 00073 Theorem ArithTheoremProducerOld::minusToPlus(const Expr& x, const Expr& y) 00074 { 00075 Proof pf; 00076 if(withProof()) pf = newPf("minus_to_plus", x, y); 00077 return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf); 00078 } 00079 00080 00081 // Rule for unary minus: -e == e/(-1) 00082 // This is to reduce the number of almost identical rules for uminus and div 00083 Theorem ArithTheoremProducerOld::canonUMinusToDivide(const Expr& e) { 00084 Proof pf; 00085 if(withProof()) pf = newPf("canon_uminus", e); 00086 return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf); 00087 } 00088 00089 // Rules for division by constant 00090 00091 // (c)/(d) ==> (c/d). When d==0, c/0 = 0 (our total extension). 00092 Theorem ArithTheoremProducerOld::canonDivideConst(const Expr& c, 00093 const Expr& d) { 00094 // Make sure c and d are a const 00095 if(CHECK_PROOFS) { 00096 CHECK_SOUND(isRational(c), 00097 CLASS_NAME "::canonDivideConst:\n c not a constant: " 00098 + c.toString()); 00099 CHECK_SOUND(isRational(d), 00100 CLASS_NAME "::canonDivideConst:\n d not a constant: " 00101 + d.toString()); 00102 } 00103 Proof pf; 00104 if(withProof()) 00105 pf = newPf("canon_divide_const", c, d, d_hole); 00106 const Rational& dr = d.getRational(); 00107 return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf); 00108 } 00109 00110 // (c * x)/d ==> (c/d) * x, takes (c*x) and d 00111 Theorem ArithTheoremProducerOld::canonDivideMult(const Expr& cx, 00112 const Expr& d) { 00113 // Check the format of c*x 00114 if(CHECK_PROOFS) { 00115 CHECK_SOUND(isMult(cx) && isRational(cx[0]), 00116 CLASS_NAME "::canonDivideMult:\n " 00117 "Not a (c * x) expression: " 00118 + cx.toString()); 00119 CHECK_SOUND(isRational(d), 00120 CLASS_NAME "::canonDivideMult:\n " 00121 "d is not a constant: " + d.toString()); 00122 } 00123 const Rational& dr = d.getRational(); 00124 Rational cdr(dr==0? 0 : (cx[0].getRational()/dr)); 00125 Expr cd(rat(cdr)); 00126 Proof pf; 00127 if(withProof()) 00128 pf = newPf("canon_divide_mult", cx[0], cx[1], d); 00129 // (c/d) may be == 1, so we also need to canonize 1*x to x 00130 if(cdr == 1) 00131 return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf); 00132 else if(cdr == 0) // c/0 == 0 case 00133 return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf); 00134 else 00135 return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf); 00136 } 00137 00138 // (+ t1 ... tn)/d ==> (+ (t1/d) ... (tn/d)) 00139 Theorem ArithTheoremProducerOld::canonDividePlus(const Expr& sum, const Expr& d) { 00140 if(CHECK_PROOFS) { 00141 CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]), 00142 CLASS_NAME "::canonUMinusPlus:\n " 00143 "Expr is not a canonical sum: " 00144 + sum.toString()); 00145 CHECK_SOUND(isRational(d), 00146 CLASS_NAME "::canonUMinusPlus:\n " 00147 "d is not a const: " + d.toString()); 00148 } 00149 // First, propagate '/d' down to the args 00150 Proof pf; 00151 if(withProof()) 00152 pf = newPf("canon_divide_plus", rat(sum.arity()), 00153 sum.begin(), sum.end()); 00154 vector<Expr> newKids; 00155 for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i) 00156 newKids.push_back((*i)/d); 00157 // (+ t1 ... tn)/d == (+ (t1/d) ... (tn/d)) 00158 return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf); 00159 } 00160 00161 // x/(d) ==> (1/d) * x, unless d == 1 00162 Theorem ArithTheoremProducerOld::canonDivideVar(const Expr& e, const Expr& d) { 00163 if(CHECK_PROOFS) { 00164 CHECK_SOUND(isRational(d), 00165 CLASS_NAME "::canonDivideVar:\n " 00166 "d is not a const: " + d.toString()); 00167 } 00168 Proof pf; 00169 00170 if(withProof()) 00171 pf = newPf("canon_divide_var", e); 00172 00173 const Rational& dr = d.getRational(); 00174 if(dr == 1) 00175 return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf); 00176 if(dr == 0) // e/0 == 0 (total extension of division) 00177 return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf); 00178 else 00179 return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf); 00180 } 00181 00182 00183 // Multiplication 00184 // (MULT expr1 expr2 expr3 ...) 00185 // Each expr is in canonical form, i.e. it can be a 00186 // 1) Rational constant 00187 // 2) Arithmetic Leaf (var or term from another theory) 00188 // 3) (POW rational leaf) 00189 // where rational cannot be 0 or 1 00190 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3) 00191 // If rational == 1 then there should be at least two mterms 00192 // 5) (PLUS rational sterm_1 ...) where each sterm is of 00193 // type (2) or (3) or (4) 00194 // if rational == 0 then there should be at least two sterms 00195 00196 00197 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids) 00198 { 00199 DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), ""); 00200 if (mulKids.size() == 1) { 00201 return mulKids[0]; 00202 } 00203 if ((mulKids[0] == rat(1)) && mulKids.size() == 2) { 00204 return mulKids[1]; 00205 } 00206 else 00207 return multExpr(mulKids); 00208 } 00209 00210 Expr ArithTheoremProducerOld::canonMultConstMult(const Expr & c, 00211 const Expr & e) 00212 { 00213 // c is a rational 00214 // e is (MULT rat mterm'_1 ....) 00215 // assume that e2 is already in canonic form 00216 DebugAssert(c.isRational() && e.getKind() == MULT, ""); 00217 std::vector<Expr> mulKids; 00218 DebugAssert ((e.arity() > 1) && (e[0].isRational()), 00219 "ArithTheoremProducerOld::canonMultConstMult: " 00220 "a canonized MULT expression must have arity " 00221 "greater than 1: and first child must be " 00222 "rational " + e.toString()); 00223 Expr::iterator i = e.begin(); 00224 mulKids.push_back(rat(c.getRational() * (*i).getRational())); 00225 ++i; 00226 for(; i != e.end(); ++i) { 00227 mulKids.push_back(*i); 00228 } 00229 return simplifiedMultExpr(mulKids); 00230 } 00231 00232 Expr ArithTheoremProducerOld::canonMultConstPlus(const Expr & e1, 00233 const Expr & e2) 00234 { 00235 DebugAssert(e1.isRational() && e2.getKind() == PLUS && 00236 e2.arity() > 0, ""); 00237 // e1 is a rational 00238 // e2 is of the form (PLUS rational sterm1 sterm2 ...) 00239 // assume that e2 is already in canonic form 00240 std::vector<Theorem> thmPlusVector; 00241 Expr::iterator i = e2.begin(); 00242 for(; i!= e2.end(); ++i) { 00243 thmPlusVector.push_back(canonMultMtermMterm(e1*(*i))); 00244 } 00245 00246 Theorem thmPlus1 = 00247 d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector); 00248 return thmPlus1.getRHS(); 00249 } 00250 00251 Expr ArithTheoremProducerOld::canonMultPowPow(const Expr & e1, 00252 const Expr & e2) 00253 { 00254 DebugAssert(e1.getKind() == POW && e2.getKind() == POW, ""); 00255 // (POW r1 leaf1) * (POW r2 leaf2) 00256 Expr leaf1 = e1[1]; 00257 Expr leaf2 = e2[1]; 00258 Expr can_expr; 00259 if (leaf1 == leaf2) { 00260 Rational rsum = e1[0].getRational() + e2[0].getRational(); 00261 if (rsum == 0) { 00262 return rat(1); 00263 } 00264 else if (rsum == 1) { 00265 return leaf1; 00266 } 00267 else 00268 { 00269 return powExpr(rat(rsum), leaf1); 00270 } 00271 } 00272 else 00273 { 00274 std::vector<Expr> mulKids; 00275 mulKids.push_back(rat(1)); 00276 // the leafs should be put in decreasing order 00277 if (leaf1 < leaf2) { 00278 mulKids.push_back(e2); 00279 mulKids.push_back(e1); 00280 } 00281 else 00282 { 00283 mulKids.push_back(e1); 00284 mulKids.push_back(e2); 00285 } 00286 // FIXME: don't really need to simplify, just wrap up a MULT? 00287 return simplifiedMultExpr(mulKids); 00288 } 00289 } 00290 00291 Expr ArithTheoremProducerOld::canonMultPowLeaf(const Expr & e1, 00292 const Expr & e2) 00293 { 00294 DebugAssert(e1.getKind() == POW, ""); 00295 // (POW r1 leaf1) * leaf2 00296 Expr leaf1 = e1[1]; 00297 Expr leaf2 = e2; 00298 Expr can_expr; 00299 if (leaf1 == leaf2) { 00300 Rational rsum = e1[0].getRational() + 1; 00301 if (rsum == 0) { 00302 return rat(1); 00303 } 00304 else if (rsum == 1) { 00305 return leaf1; 00306 } 00307 else 00308 { 00309 return powExpr(rat(rsum), leaf1); 00310 } 00311 } 00312 else 00313 { 00314 std::vector<Expr> mulKids; 00315 mulKids.push_back(rat(1)); 00316 // the leafs should be put in decreasing order 00317 if (leaf1 < leaf2) { 00318 mulKids.push_back(e2); 00319 mulKids.push_back(e1); 00320 } 00321 else 00322 { 00323 mulKids.push_back(e1); 00324 mulKids.push_back(e2); 00325 } 00326 return simplifiedMultExpr(mulKids); 00327 } 00328 } 00329 00330 Expr ArithTheoremProducerOld::canonMultLeafLeaf(const Expr & e1, 00331 const Expr & e2) 00332 { 00333 // leaf1 * leaf2 00334 Expr leaf1 = e1; 00335 Expr leaf2 = e2; 00336 Expr can_expr; 00337 if (leaf1 == leaf2) { 00338 return powExpr(rat(2), leaf1); 00339 } 00340 else 00341 { 00342 std::vector<Expr> mulKids; 00343 mulKids.push_back(rat(1)); 00344 // the leafs should be put in decreasing order 00345 if (leaf1 < leaf2) { 00346 mulKids.push_back(e2); 00347 mulKids.push_back(e1); 00348 } 00349 else 00350 { 00351 mulKids.push_back(e1); 00352 mulKids.push_back(e2); 00353 } 00354 return simplifiedMultExpr(mulKids); 00355 } 00356 } 00357 00358 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(const Expr & e1, 00359 const Expr & e2) 00360 { 00361 DebugAssert(e2.getKind() == MULT, ""); 00362 // Leaf * (MULT rat1 mterm1 ...) 00363 // (POW r1 leaf1) * (MULT rat1 mterm1 ...) where 00364 // each mterm is a leaf or (POW r leaf). Furthermore the leafs 00365 // in the mterms are in descending order 00366 Expr leaf1 = e1.getKind() == POW ? e1[1] : e1; 00367 std::vector<Expr> mulKids; 00368 DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more"); 00369 Expr::iterator i = e2.begin(); 00370 // push the rational 00371 mulKids.push_back(*i); 00372 ++i; 00373 // Now i points to the first mterm 00374 for(; i != e2.end(); ++i) { 00375 Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i); 00376 if (leaf1 == leaf2) { 00377 Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1; 00378 Rational r2 = 00379 ((*i).getKind() == POW ? (*i)[0].getRational() : 1); 00380 // if r1 + r2 == 0 then it is the case of x^n * x^{-n} 00381 // So, nothing needs to be added 00382 if (r1 + r2 != 0) { 00383 if (r1 + r2 == 1) { 00384 mulKids.push_back(leaf1); 00385 } 00386 else 00387 { 00388 mulKids.push_back(powExpr(rat(r1 + r2), leaf1)); 00389 } 00390 } 00391 break; 00392 } 00393 // This ensures that the leaves in the mterms are also arranged 00394 // in decreasing order 00395 // Note that this will need to be changed if we want the order to 00396 // be increasing order. 00397 else if (leaf2 < leaf1) { 00398 mulKids.push_back(e1); 00399 mulKids.push_back(*i); 00400 break; 00401 } 00402 else // leaf1 < leaf2 00403 mulKids.push_back(*i); 00404 } 00405 if (i == e2.end()) { 00406 mulKids.push_back(e1); 00407 } 00408 else 00409 { 00410 // e1 and *i have already been added 00411 for (++i; i != e2.end(); ++i) { 00412 mulKids.push_back(*i); 00413 } 00414 } 00415 return simplifiedMultExpr(mulKids); 00416 } 00417 00418 // Local class for ordering monomials; note, that it flips the 00419 // ordering given by greaterthan(), to sort in ascending order. 00420 class MonomialLess { 00421 public: 00422 bool operator()(const Expr& e1, const Expr& e2) const { 00423 return ArithTheoremProducerOld::greaterthan(e1,e2); 00424 } 00425 }; 00426 00427 typedef map<Expr,Rational,MonomialLess> MonomMap; 00428 00429 Expr 00430 ArithTheoremProducerOld::canonCombineLikeTerms(const std::vector<Expr> & sumExprs) 00431 { 00432 Rational constant = 0; 00433 MonomMap sumHashMap; 00434 vector<Expr> sumKids; 00435 00436 // Add each distinct mterm (not including the rational) into 00437 // an appropriate hash map entry 00438 std::vector<Expr>::const_iterator i = sumExprs.begin(); 00439 for (; i != sumExprs.end(); ++i) { 00440 Expr mul = *i; 00441 if (mul.isRational()) { 00442 constant = constant + mul.getRational(); 00443 } 00444 else { 00445 switch (mul.getKind()) { 00446 case MULT: { 00447 std::vector<Expr> mulKids; 00448 DebugAssert(mul.arity() > 1 && mul[0].isRational(),""); 00449 mulKids.push_back(rat(1)); 00450 Expr::iterator j = mul.begin(); 00451 ++j; 00452 for (; j!= mul.end(); ++j) { 00453 mulKids.push_back(*j); 00454 } 00455 00456 // make sure that tempExpr is also in canonic form 00457 Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1]; 00458 MonomMap::iterator i=sumHashMap.find(tempExpr); 00459 if (i == sumHashMap.end()) { 00460 sumHashMap[tempExpr] = mul[0].getRational(); 00461 } 00462 else { 00463 (*i).second += mul[0].getRational(); 00464 } 00465 } 00466 break; 00467 default: { 00468 MonomMap::iterator i=sumHashMap.find(mul); 00469 // covers the case of POW, leaf 00470 if (i == sumHashMap.end()) { 00471 sumHashMap[mul] = 1; 00472 } 00473 else { 00474 (*i).second += 1; 00475 } 00476 break; 00477 } 00478 } 00479 } 00480 } 00481 // Now transfer to sumKids 00482 sumKids.push_back(rat(constant)); 00483 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end(); 00484 for(; j != jend; ++j) { 00485 if ((*j).second != 0) 00486 sumKids.push_back 00487 (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS()); 00488 } 00489 00490 /* 00491 for (unsigned k = 0; k < sumKids.size(); ++k) 00492 { 00493 cout << "sumKids[" << k << "] = " << sumKids[k].toString() << endl; 00494 } 00495 */ 00496 00497 // The ordering in map guarantees the correct order; no need to sort 00498 00499 // std::sort(sumKids.begin(), sumKids.end(), greaterthan); 00500 00501 if ((constant == 0) && (sumKids.size() == 2)) { 00502 return sumKids[1]; 00503 } 00504 else if (sumKids.size() == 1) { 00505 return sumKids[0]; 00506 } 00507 else 00508 return plusExpr(sumKids); 00509 } 00510 00511 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(const Expr & e1, 00512 const Expr & e2) 00513 { 00514 DebugAssert(e2.getKind() == PLUS, ""); 00515 // Leaf * (PLUS rational sterm1 ...) 00516 // or 00517 // (POW n1 x1) * (PLUS rational sterm1 ...) 00518 // or 00519 // (MULT r1 m1 m2 ...) * (PLUS rational sterm1 ...) 00520 // assume that e1 and e2 are themselves canonized 00521 std::vector<Expr> sumExprs; 00522 // Multiply each term in turn. 00523 Expr::iterator i = e2.begin(); 00524 for (; i != e2.end(); ++i) { 00525 sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS()); 00526 } 00527 return canonCombineLikeTerms(sumExprs); 00528 } 00529 00530 Expr ArithTheoremProducerOld::canonMultPlusPlus(const Expr & e1, 00531 const Expr & e2) 00532 { 00533 DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, ""); 00534 // (PLUS r1 .... ) * (PLUS r1' ...) 00535 // assume that e1 and e2 are themselves canonized 00536 00537 std::vector<Expr> sumExprs; 00538 // Multiply each term in turn. 00539 Expr::iterator i = e1.begin(); 00540 for (; i != e1.end(); ++i) { 00541 Expr::iterator j = e2.begin(); 00542 for (; j != e2.end(); ++j) { 00543 sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS()); 00544 } 00545 } 00546 return canonCombineLikeTerms(sumExprs); 00547 } 00548 00549 00550 00551 // The following produces a Theorem which is the result of multiplication 00552 // of two canonized mterms. e = e1*e2 00553 Theorem 00554 ArithTheoremProducerOld::canonMultMtermMterm(const Expr& e) 00555 { 00556 if(CHECK_PROOFS) { 00557 CHECK_SOUND(isMult(e) && e.arity() == 2, 00558 "canonMultMtermMterm: e = "+e.toString()); 00559 } 00560 Proof pf; 00561 Expr rhs; 00562 const Expr& e1 = e[0]; 00563 const Expr& e2 = e[1]; 00564 string cmmm = "canon_mult_mterm_mterm"; 00565 00566 if (e1.isRational()) { 00567 // e1 is a Rational 00568 const Rational& c = e1.getRational(); 00569 if (c == 0) 00570 return canonMultZero(e2); 00571 else if (c == 1) 00572 return canonMultOne(e2); 00573 else { 00574 switch (e2.getKind()) { 00575 case RATIONAL_EXPR : 00576 // rat * rat 00577 return canonMultConstConst(e1,e2); 00578 break; 00579 // TODO case of leaf 00580 case POW: 00581 // rat * (POW rat leaf) 00582 // nothing to simplify 00583 return d_theoryArith->reflexivityRule (e); 00584 00585 break; 00586 case MULT: 00587 rhs = canonMultConstMult(e1,e2); 00588 if(withProof()) pf = newPf(cmmm,e,rhs); 00589 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00590 break; 00591 case PLUS: 00592 rhs = canonMultConstPlus(e1,e2); 00593 if(withProof()) pf = newPf(cmmm,e,rhs); 00594 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00595 break; 00596 default: 00597 // TODO: I am going to assume that this is just a leaf 00598 // i.e., a variable or term from another theory 00599 return d_theoryArith->reflexivityRule(e); 00600 break; 00601 } 00602 } 00603 } 00604 else if (e1.getKind() == POW) { 00605 switch (e2.getKind()) { 00606 case RATIONAL_EXPR: 00607 // switch the order of the two arguments 00608 return canonMultMtermMterm(e2 * e1); 00609 break; 00610 case POW: 00611 rhs = canonMultPowPow(e1,e2); 00612 if(withProof()) pf = newPf(cmmm,e,rhs); 00613 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf); 00614 break; 00615 case MULT: 00616 rhs = canonMultLeafOrPowMult(e1,e2); 00617 if(withProof()) pf = newPf(cmmm,e,rhs); 00618 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00619 break; 00620 case PLUS: 00621 rhs = canonMultLeafOrPowOrMultPlus(e1,e2); 00622 if(withProof()) pf = newPf(cmmm,e,rhs); 00623 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00624 break; 00625 default: 00626 rhs = canonMultPowLeaf(e1,e2); 00627 if(withProof()) pf = newPf(cmmm,e,rhs); 00628 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf); 00629 break; 00630 } 00631 } 00632 else if (e1.getKind() == MULT) { 00633 switch (e2.getKind()) { 00634 case RATIONAL_EXPR: 00635 case POW: 00636 // switch the order of the two arguments 00637 return canonMultMtermMterm(e2 * e1); 00638 break; 00639 case MULT: 00640 { 00641 // (Mult r m1 m2 ...) (Mult r' m1' m2' ...) 00642 Expr result = e2; 00643 Expr::iterator i = e1.begin(); 00644 for (; i != e1.end(); ++i) { 00645 result = canonMultMtermMterm((*i) * result).getRHS(); 00646 } 00647 if(withProof()) pf = newPf(cmmm,e,result); 00648 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf); 00649 } 00650 break; 00651 case PLUS: 00652 rhs = canonMultLeafOrPowOrMultPlus(e1,e2); 00653 if(withProof()) pf = newPf(cmmm,e,rhs); 00654 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf); 00655 break; 00656 default: 00657 // leaf 00658 // switch the order of the two arguments 00659 return canonMultMtermMterm(e2 * e1); 00660 break; 00661 } 00662 } 00663 else if (e1.getKind() == PLUS) { 00664 switch (e2.getKind()) { 00665 case RATIONAL_EXPR: 00666 case POW: 00667 case MULT: 00668 // switch the order of the two arguments 00669 return canonMultMtermMterm(e2 * e1); 00670 break; 00671 case PLUS: 00672 rhs = canonMultPlusPlus(e1,e2); 00673 if(withProof()) pf = newPf(cmmm,e,rhs); 00674 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00675 break; 00676 default: 00677 // leaf 00678 // switch the order of the two arguments 00679 return canonMultMtermMterm(e2 * e1); 00680 break; 00681 } 00682 } 00683 else { 00684 // leaf 00685 switch (e2.getKind()) { 00686 case RATIONAL_EXPR: 00687 // switch the order of the two arguments 00688 return canonMultMtermMterm(e2 * e1); 00689 break; 00690 case POW: 00691 rhs = canonMultPowLeaf(e2,e1); 00692 if(withProof()) pf = newPf(cmmm,e,rhs); 00693 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00694 break; 00695 case MULT: 00696 rhs = canonMultLeafOrPowMult(e1,e2);; 00697 if(withProof()) pf = newPf(cmmm,e,rhs); 00698 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00699 break; 00700 case PLUS: 00701 rhs = canonMultLeafOrPowOrMultPlus(e1,e2); 00702 if(withProof()) pf = newPf(cmmm,e,rhs); 00703 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00704 break; 00705 default: 00706 // leaf * leaf 00707 rhs = canonMultLeafLeaf(e1,e2); 00708 if(withProof()) pf = newPf(cmmm,e,rhs); 00709 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00710 break; 00711 } 00712 } 00713 FatalAssert(false, "Unreachable"); 00714 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf); 00715 } 00716 00717 // (PLUS expr1 expr2 ...) where each expr is itself in canonic form 00718 Theorem 00719 ArithTheoremProducerOld::canonPlus(const Expr& e) 00720 { 00721 Proof pf; 00722 00723 if (withProof()) { 00724 pf = newPf("canon_plus", e); 00725 } 00726 DebugAssert(e.getKind() == PLUS, ""); 00727 00728 // First flatten the PLUS 00729 00730 std::vector<Expr> sumKids; 00731 Expr::iterator i = e.begin(); 00732 for(; i != e.end(); ++i) { 00733 if ((*i).getKind() != PLUS) { 00734 sumKids.push_back(*i); 00735 } 00736 else 00737 { 00738 Expr::iterator j = (*i).begin(); 00739 for(; j != (*i).end(); ++j) 00740 sumKids.push_back(*j); 00741 } 00742 } 00743 Expr val = canonCombineLikeTerms(sumKids); 00744 if (withProof()) { 00745 pf = newPf("canon_plus", e, val); 00746 } 00747 return newRWTheorem(e, val, Assumptions::emptyAssump(), pf); 00748 } 00749 00750 // (MULT expr1 expr2 ...) where each expr is itself in canonic form 00751 Theorem 00752 ArithTheoremProducerOld::canonMult(const Expr& e) 00753 { 00754 Proof pf; 00755 TRACE("arith canon", "canonMult(", e.toString(), ")"); 00756 DebugAssert(e.getKind() == MULT && e.arity() > 1, ""); 00757 Expr::iterator i = e.begin(); 00758 Expr result = *i; 00759 ++i; 00760 for (; i != e.end(); ++i) { 00761 result = canonMultMtermMterm(result * (*i)).getRHS(); 00762 } 00763 if (withProof()) { 00764 pf = newPf("canon_mult", e,result); 00765 } 00766 00767 // If multiplicative sign split is on do it 00768 if (d_theoryArith->nonlinearSignSplit()) { 00769 00770 // Add the sign splits 00771 Expr positive = d_em->trueExpr(); 00772 Expr negative = d_em->falseExpr(); 00773 vector<Expr> zero; 00774 00775 // we do the case split if it's not trivial 00776 int count_non_trivial = 0; 00777 int count_constants = 0; 00778 00779 // a1*a2*...*an is positive if there is an even number of negative ones 00780 // a1*a2*...*an is negative if there is an odd number of negative ones 00781 for (i = e.begin(); i != e.end(); ++i) { 00782 Expr current = (*i); 00783 00784 if (isPlus(current)) count_non_trivial ++; 00785 if (current.isRational()) count_constants ++; 00786 if (isPow(current) && current[0].getRational() < 0) { 00787 // Bail on negative powers, it's normalization 00788 count_non_trivial = 0; 00789 break; 00790 } 00791 00792 zero.push_back(current.eqExpr(rat(0))); 00793 positive = Expr(XOR, positive, ltExpr(current, rat(0))); 00794 negative = Expr(XOR, negative, ltExpr(current, rat(0))); 00795 } 00796 00797 if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) { 00798 // Any of the factors is zero 00799 Expr zero_lemma = orExpr(zero).iffExpr(result.eqExpr(rat(0))); 00800 Expr positive_lemma = positive.impExpr(geExpr(result, rat(0))); 00801 Expr negative_lemma = negative.impExpr(leExpr(result, rat(0))); 00802 Expr lemma = positive_lemma.andExpr(negative_lemma.andExpr(zero_lemma)); 00803 00804 Proof split_pf; 00805 if (withProof()) split_pf = newPf("multiplicative_sign_split", e, lemma); 00806 Theorem case_split_thm = newTheorem(lemma, Assumptions::emptyAssump(), split_pf); 00807 00808 TRACE("arith nonlinear", "adding sign split: ", lemma, ""); 00809 00810 d_theoryArith->addMultiplicativeSignSplit(case_split_thm); 00811 } 00812 } 00813 00814 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf); 00815 } 00816 00817 00818 Theorem 00819 ArithTheoremProducerOld::canonInvertConst(const Expr& e) 00820 { 00821 if(CHECK_PROOFS) 00822 CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString()); 00823 00824 Proof pf; 00825 00826 if (withProof()) { 00827 pf = newPf("canon_invert_const", e); 00828 } 00829 const Rational& er = e.getRational(); 00830 return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf); 00831 } 00832 00833 00834 Theorem 00835 ArithTheoremProducerOld::canonInvertLeaf(const Expr& e) 00836 { 00837 Proof pf; 00838 00839 if (withProof()) { 00840 pf = newPf("canon_invert_leaf", e); 00841 } 00842 return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf); 00843 } 00844 00845 00846 Theorem 00847 ArithTheoremProducerOld::canonInvertPow(const Expr& e) 00848 { 00849 DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString()); 00850 00851 Proof pf; 00852 00853 if (withProof()) { 00854 pf = newPf("canon_invert_pow", e); 00855 } 00856 if (e[0].getRational() == -1) 00857 return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf); 00858 else 00859 return newRWTheorem((rat(1)/e), 00860 powExpr(rat(-e[0].getRational()), e[1]), 00861 Assumptions::emptyAssump(), 00862 pf); 00863 } 00864 00865 Theorem 00866 ArithTheoremProducerOld::canonInvertMult(const Expr& e) 00867 { 00868 DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString()); 00869 00870 Proof pf; 00871 00872 if (withProof()) { 00873 pf = newPf("canon_invert_mult", e); 00874 } 00875 00876 DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString()); 00877 Expr result = canonInvert(e[0]).getRHS(); 00878 for (int i = 1; i < e.arity(); ++i) { 00879 result = 00880 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS(); 00881 } 00882 return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf); 00883 } 00884 00885 00886 // Given an expression e in Canonic form generate 1/e in canonic form 00887 // This function assumes that e is not a PLUS expression 00888 Theorem 00889 ArithTheoremProducerOld::canonInvert(const Expr& e) 00890 { 00891 DebugAssert(e.getKind() != PLUS, 00892 "Cannot do inverse on a PLUS"+e.toString()); 00893 switch (e.getKind()) { 00894 case RATIONAL_EXPR: 00895 return canonInvertConst(e); 00896 break; 00897 case POW: 00898 return canonInvertPow(e); 00899 break; 00900 case MULT: 00901 return canonInvertMult(e); 00902 break; 00903 default: 00904 // leaf 00905 return canonInvertLeaf(e); 00906 break; 00907 } 00908 } 00909 00910 00911 Theorem ArithTheoremProducerOld::moveSumConstantRight(const Expr& e) { 00912 00913 // Check soundness of the rule if necessary 00914 if (CHECK_PROOFS) { 00915 CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString()); 00916 CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString()); 00917 CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString()); 00918 } 00919 00920 // The rational constant of the sum 00921 Rational r = 0; 00922 00923 // The right hand side of the expression 00924 Expr right = e[0]; 00925 00926 // The vector of sum terms 00927 vector<Expr> sumTerms; 00928 00929 // Get all the non rational children and 00930 if (!right.isRational()) 00931 for(Expr::iterator it = right.begin(); it != right.end(); it ++) { 00932 // If the term is rational then add the rational number to r 00933 if ((*it).isRational()) r = r + (*it).getRational(); 00934 // Otherwise just add the sumTerm to the sumTerms 00935 else sumTerms.push_back((*it)); 00936 } 00937 00938 // Setup the new expression 00939 Expr transformed; 00940 if (sumTerms.size() > 1) 00941 // If the number of summands is > 1 return the sum of them 00942 transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r)); 00943 else 00944 // Otherwise return the one summand as itself 00945 transformed = Expr(e.getKind(), sumTerms[0], rat(-r)); 00946 00947 00948 // If proof is needed set it up 00949 Proof pf; 00950 if (withProof()) pf = newPf("arithm_sum_constant_right", e); 00951 00952 // Retrun the theorem explaining the transformation 00953 return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf); 00954 } 00955 00956 Theorem 00957 ArithTheoremProducerOld::canonDivide(const Expr& e) 00958 { 00959 DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString()); 00960 Proof pf; 00961 00962 if (withProof()) { 00963 pf = newPf("canon_invert_divide", e); 00964 } 00965 00966 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf); 00967 00968 return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS())); 00969 } 00970 00971 00972 // Rules for multiplication 00973 // t*c ==> c*t, takes constant c and term t 00974 Theorem 00975 ArithTheoremProducerOld::canonMultTermConst(const Expr& c, const Expr& t) { 00976 Proof pf; 00977 if(CHECK_PROOFS) { 00978 CHECK_SOUND(isRational(c), 00979 CLASS_NAME "::canonMultTermConst:\n " 00980 "c is not a constant: " + c.toString()); 00981 } 00982 if(withProof()) pf = newPf("canon_mult_term_const", c, t); 00983 return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf); 00984 } 00985 00986 // Rules for multiplication 00987 // t1*t2 ==> Error, takes t1 and t2 where both are non-constants 00988 Theorem 00989 ArithTheoremProducerOld::canonMultTerm1Term2(const Expr& t1, const Expr& t2) { 00990 // Proof pf; 00991 // if(withProof()) pf = newPf("canon_mult_term1_term2", t1, t2); 00992 if(CHECK_PROOFS) { 00993 CHECK_SOUND(false, "Fatal Error: We don't support multiplication" 00994 "of two non constant terms at this time " 00995 + t1.toString() + " and " + t2.toString()); 00996 } 00997 return Theorem(); 00998 } 00999 01000 // Rules for multiplication 01001 // 0*x = 0, takes x 01002 Theorem ArithTheoremProducerOld::canonMultZero(const Expr& e) { 01003 Proof pf; 01004 if(withProof()) pf = newPf("canon_mult_zero", e); 01005 return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf); 01006 } 01007 01008 // Rules for multiplication 01009 // 1*x ==> x, takes x 01010 Theorem ArithTheoremProducerOld::canonMultOne(const Expr& e) { 01011 Proof pf; 01012 if(withProof()) pf = newPf("canon_mult_one", e); 01013 return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf); 01014 } 01015 01016 // Rules for multiplication 01017 // c1*c2 ==> c', takes constant c1*c2 01018 Theorem 01019 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) { 01020 Proof pf; 01021 if(CHECK_PROOFS) { 01022 CHECK_SOUND(isRational(c1), 01023 CLASS_NAME "::canonMultConstConst:\n " 01024 "c1 is not a constant: " + c1.toString()); 01025 CHECK_SOUND(isRational(c2), 01026 CLASS_NAME "::canonMultConstConst:\n " 01027 "c2 is not a constant: " + c2.toString()); 01028 } 01029 if(withProof()) pf = newPf("canon_mult_const_const", c1, c2); 01030 return 01031 newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf); 01032 } 01033 01034 // Rules for multiplication 01035 // c1*(c2*t) ==> c'*t, takes c1 and c2 and t 01036 Theorem 01037 ArithTheoremProducerOld::canonMultConstTerm(const Expr& c1, 01038 const Expr& c2,const Expr& t) { 01039 Proof pf; 01040 if(CHECK_PROOFS) { 01041 CHECK_SOUND(isRational(c1), 01042 CLASS_NAME "::canonMultConstTerm:\n " 01043 "c1 is not a constant: " + c1.toString()); 01044 CHECK_SOUND(isRational(c2), 01045 CLASS_NAME "::canonMultConstTerm:\n " 01046 "c2 is not a constant: " + c2.toString()); 01047 } 01048 01049 if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t); 01050 return 01051 newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf); 01052 } 01053 01054 // Rules for multiplication 01055 // c1*(+ c2 v1 ...) ==> (+ c1c2 c1v1 ...), takes c1 and the sum 01056 Theorem 01057 ArithTheoremProducerOld::canonMultConstSum(const Expr& c1, const Expr& sum) { 01058 Proof pf; 01059 std::vector<Expr> sumKids; 01060 01061 if(CHECK_PROOFS) { 01062 CHECK_SOUND(isRational(c1), 01063 CLASS_NAME "::canonMultConstTerm:\n " 01064 "c1 is not a constant: " + c1.toString()); 01065 CHECK_SOUND(PLUS == sum.getKind(), 01066 CLASS_NAME "::canonMultConstTerm:\n " 01067 "the kind must be a PLUS: " + sum.toString()); 01068 } 01069 Expr::iterator i = sum.begin(); 01070 for(; i != sum.end(); ++i) 01071 sumKids.push_back(c1*(*i)); 01072 Expr ret = plusExpr(sumKids); 01073 if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret); 01074 return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf); 01075 } 01076 01077 01078 // c^n = c' (compute the constant power expression) 01079 Theorem 01080 ArithTheoremProducerOld::canonPowConst(const Expr& e) { 01081 if(CHECK_PROOFS) { 01082 CHECK_SOUND(e.getKind() == POW && e.arity() == 2 01083 && e[0].isRational() && e[1].isRational(), 01084 "ArithTheoremProducerOld::canonPowConst("+e.toString()+")"); 01085 } 01086 const Rational& p = e[0].getRational(); 01087 const Rational& base = e[1].getRational(); 01088 if(CHECK_PROOFS) { 01089 CHECK_SOUND(p.isInteger(), 01090 "ArithTheoremProducerOld::canonPowConst("+e.toString()+")"); 01091 } 01092 Expr res; 01093 if (base == 0 && p < 0) { 01094 res = rat(0); 01095 } 01096 else res = rat(pow(p, base)); 01097 Proof pf; 01098 if(withProof()) 01099 pf = newPf("canon_pow_const", e, res); 01100 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf); 01101 } 01102 01103 01104 // Rules for addition 01105 // flattens the input. accepts a PLUS expr 01106 Theorem 01107 ArithTheoremProducerOld::canonFlattenSum(const Expr& e) { 01108 Proof pf; 01109 std::vector<Expr> sumKids; 01110 if(CHECK_PROOFS) { 01111 CHECK_SOUND(PLUS == e.getKind(), 01112 CLASS_NAME "::canonFlattenSum:\n" 01113 "input must be a PLUS:" + e.toString()); 01114 } 01115 01116 Expr::iterator i = e.begin(); 01117 for(; i != e.end(); ++i){ 01118 if (PLUS != (*i).getKind()) 01119 sumKids.push_back(*i); 01120 else { 01121 Expr::iterator j = (*i).begin(); 01122 for(; j != (*i).end(); ++j) 01123 sumKids.push_back(*j); 01124 } 01125 } 01126 Expr ret = plusExpr(sumKids); 01127 if(withProof()) pf = newPf("canon_flatten_sum", e,ret); 01128 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf); 01129 } 01130 01131 // Rules for addition 01132 // combine like terms. accepts a flattened PLUS expr 01133 Theorem 01134 ArithTheoremProducerOld::canonComboLikeTerms(const Expr& e) { 01135 Proof pf; 01136 std::vector<Expr> sumKids; 01137 ExprMap<Rational> sumHashMap; 01138 Rational constant = 0; 01139 01140 if(CHECK_PROOFS) { 01141 Expr::iterator k = e.begin(); 01142 for(; k != e.end(); ++k) 01143 CHECK_SOUND(!isPlus(*k), 01144 CLASS_NAME "::canonComboLikeTerms:\n" 01145 "input must be a flattened PLUS:" + k->toString()); 01146 } 01147 Expr::iterator i = e.begin(); 01148 for(; i != e.end(); ++i){ 01149 if(i->isRational()) 01150 constant = constant + i->getRational(); 01151 else { 01152 if (!isMult(*i)) { 01153 if(0 == sumHashMap.count((*i))) 01154 sumHashMap[*i] = 1; 01155 else 01156 sumHashMap[*i] += 1; 01157 } 01158 else { 01159 if(0 == sumHashMap.count((*i)[1])) 01160 sumHashMap[(*i)[1]] = (*i)[0].getRational(); 01161 else 01162 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational(); 01163 } 01164 } 01165 } 01166 01167 sumKids.push_back(rat(constant)); 01168 ExprMap<Rational>::iterator j = sumHashMap.begin(); 01169 for(; j != sumHashMap.end(); ++j) { 01170 if(0 == (*j).second) 01171 ;//do nothing 01172 else if (1 == (*j).second) 01173 sumKids.push_back((*j).first); 01174 else 01175 sumKids.push_back(rat((*j).second) * (*j).first); 01176 } 01177 01178 //constant is same as sumKids[0]. 01179 //corner cases: "0 + monomial" and "constant"(no monomials) 01180 01181 Expr ret; 01182 if(2 == sumKids.size() && 0 == constant) ret = sumKids[1]; 01183 else if (1 == sumKids.size()) ret = sumKids[0]; 01184 else ret = plusExpr(sumKids); 01185 01186 if(withProof()) pf = newPf("canon_combo_like_terms",e,ret); 01187 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf); 01188 } 01189 01190 01191 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ... 01192 Theorem ArithTheoremProducerOld::multEqZero(const Expr& expr) 01193 { 01194 Proof pf; 01195 vector<Expr> kids; 01196 01197 int side = expr[0].isRational() ? 1 : 0; 01198 01199 vector<Expr> non_zero; 01200 01201 Expr::iterator i = expr[side].begin(), iend = expr[side].end(); 01202 for (; i != iend; ++i) { 01203 Expr x = *i; 01204 // If a rational it can't be 0, so it is false, i.e. just skip it 01205 if (x.isRational()) { 01206 CHECK_SOUND(x.getRational() != 0, "multEqZero: once of the constants is 0"); 01207 } else { 01208 Expr leaf = x; 01209 if (isPow(x)) { 01210 // We assume that 1 / 0 = 0 for simplicity and totality. 01211 // Divisions by zero that affect the result can be identified by enabling TCCs. 01212 // if (x[0].getRational() < 0) { 01213 // non_zero.push_back(x[1].eqExpr(rat(0)).notExpr()); 01214 // continue; 01215 // } 01216 // else 01217 leaf = x[1]; 01218 } 01219 if (leaf >= rat(0)) 01220 kids.push_back(leaf.eqExpr(rat(0))); 01221 else 01222 kids.push_back(rat(0).eqExpr(leaf)); 01223 } 01224 } 01225 Expr newExpr; 01226 if (kids.size() == 1) newExpr = kids[0]; 01227 else newExpr = Expr(OR, kids); 01228 if (withProof()) { 01229 pf = newPf("multEqZero", expr); 01230 } 01231 // if (non_zero.size() == 0) 01232 return newRWTheorem(expr, newExpr, Assumptions::emptyAssump(), pf); 01233 // else return newRWTheorem(expr, Expr(OR, kids).andExpr(Expr(AND, non_zero)), Assumptions::emptyAssump(), pf); 01234 } 01235 01236 01237 // 0 = (^ c x) <=> false if c <=0 01238 // <=> 0 = x if c > 0 01239 Theorem ArithTheoremProducerOld::powEqZero(const Expr& expr) 01240 { 01241 if (CHECK_PROOFS) { 01242 CHECK_SOUND(expr.isEq() && expr[0].isRational() && 01243 expr[0].getRational() == 0 && 01244 isPow(expr[1]) && expr[1].arity() == 2 && 01245 expr[1][0].isRational(), 01246 "powEqZero invariant violated"+expr.toString()); 01247 } 01248 Proof pf; 01249 if (withProof()) { 01250 pf = newPf("powEqZero", expr); 01251 } 01252 Rational r = expr[1][0].getRational(); 01253 Expr res; 01254 if (r <= 0) { 01255 res = d_em->falseExpr(); 01256 } 01257 else { 01258 res = rat(0).eqExpr(expr[1][1]); 01259 } 01260 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf); 01261 } 01262 01263 01264 // x^n - y^n = 0 <=> x = y (if n is odd) 01265 // x^n - y^n = 0 <=> x = y OR x = -y (if n is even) 01266 Theorem ArithTheoremProducerOld::elimPower(const Expr& expr) 01267 { 01268 Expr power1, power2; 01269 bool ok = d_theoryArith->isPowersEquality(expr, power1, power2); 01270 if (CHECK_PROOFS) 01271 CHECK_SOUND(ok, "elimPower invariant violated"+expr.toString()); 01272 Proof pf; 01273 if (withProof()) 01274 pf = newPf("elimPower", expr); 01275 Rational r = power1[0].getRational(); 01276 Expr res = power1[1].eqExpr(power2[1]); 01277 if (r % 2 == 0) 01278 res = res.orExpr(power1[1].eqExpr(-power2[1])); 01279 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf); 01280 } 01281 01282 01283 // x^n = c <=> x = root (if n is odd and root^n = c) 01284 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c) 01285 Theorem ArithTheoremProducerOld::elimPowerConst(const Expr& expr, const Rational& root) 01286 { 01287 if (CHECK_PROOFS) 01288 CHECK_SOUND(expr.isEq(), "elimPowerConst invariant violated" + expr.toString()); 01289 Rational constant; 01290 Expr power; 01291 bool ok = d_theoryArith->isPowerEquality(expr, constant, power); 01292 if (CHECK_PROOFS) { 01293 CHECK_SOUND(ok, "elimPowerConst invariant violated" + expr.toString()); 01294 CHECK_SOUND(pow(power[0].getRational(), root) == constant, "elimPowerConst invariant violated" + expr.toString()); 01295 } 01296 01297 Proof pf; 01298 if (withProof()) 01299 pf = newPf("elimPowerConst", expr, rat(root)); 01300 Rational r = power[0].getRational(); 01301 Expr res = power[1].eqExpr(rat(root)); 01302 if (r % 2 == 0) 01303 res = res.orExpr(power[1].eqExpr(rat(-root))); 01304 01305 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf); 01306 } 01307 01308 01309 // x^n = c <=> false (if n is even and c is negative) 01310 Theorem ArithTheoremProducerOld::evenPowerEqNegConst(const Expr& expr) 01311 { 01312 if (CHECK_PROOFS) 01313 CHECK_SOUND(expr.isEq(), "evenPowerEqNegConst, expecting equality, got " + expr.toString()); 01314 Rational constant; 01315 Expr power; 01316 bool ok = d_theoryArith->isPowerEquality(expr, constant, power); 01317 if (CHECK_PROOFS) { 01318 CHECK_SOUND(ok, "evenPowerEqNegConst invariant violated" + expr.toString()); 01319 CHECK_SOUND(constant < 0, "evenPowerEqNegConst invariant violated" + expr.toString()); 01320 CHECK_SOUND(power[0].getRational().isInteger() && power[0].getRational() % 2 == 0, "evenPowerEqNegConst invariant violated" + expr.toString()); 01321 } 01322 Proof pf; 01323 if (withProof()) 01324 pf = newPf("evenPowerEqNegConst", expr); 01325 return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf); 01326 } 01327 01328 01329 // x^n = c <=> ` (if x is an integer and c is not a perfect n power) 01330 Theorem ArithTheoremProducerOld::intEqIrrational(const Expr& expr, const Theorem& isIntx) 01331 { 01332 if (CHECK_PROOFS) 01333 CHECK_SOUND(expr.isEq(), "intEqIrrational invariant violated" + expr.toString()); 01334 Rational constant; 01335 Expr power; 01336 bool ok = d_theoryArith->isPowerEquality(expr, constant, power); 01337 if (CHECK_PROOFS) { 01338 CHECK_SOUND(ok, "intEqIrrational invariant violated" + expr.toString()); 01339 CHECK_SOUND(constant != 0, "intEqIrrational invariant violated" + expr.toString()); 01340 CHECK_SOUND(power[0].getRational() > 0, "intEqIrrational invariant violated" + expr.toString()); 01341 CHECK_SOUND(ratRoot(constant, power[0].getRational().getUnsigned()) == 0, "intEqIrrational invariant violated" + expr.toString()); 01342 CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0], "intEqIrrational invariant violated" + isIntx.getExpr()[0].toString()); 01343 } 01344 01345 const Assumptions& assump(isIntx.getAssumptionsRef()); 01346 Proof pf; 01347 if (withProof()) 01348 pf = newPf("int_eq_irr", expr, isIntx.getProof()); 01349 return newRWTheorem(expr, d_em->falseExpr(), assump, pf); 01350 } 01351 01352 01353 // e[0] kind e[1] <==> true when e[0] kind e[1], 01354 // false when e[0] !kind e[1], for constants only 01355 Theorem ArithTheoremProducerOld::constPredicate(const Expr& e) { 01356 if(CHECK_PROOFS) { 01357 CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]), 01358 CLASS_NAME "::constPredicate:\n " 01359 "non-const parameters: " + e.toString()); 01360 } 01361 Proof pf; 01362 bool result(false); 01363 int kind = e.getKind(); 01364 Rational r1 = e[0].getRational(), r2 = e[1].getRational(); 01365 switch(kind) { 01366 case EQ: 01367 result = (r1 == r2)?true : false; 01368 break; 01369 case LT: 01370 result = (r1 < r2)?true : false; 01371 break; 01372 case LE: 01373 result = (r1 <= r2)?true : false; 01374 break; 01375 case GT: 01376 result = (r1 > r2)?true : false; 01377 break; 01378 case GE: 01379 result = (r1 >= r2)?true : false; 01380 break; 01381 default: 01382 if(CHECK_PROOFS) { 01383 CHECK_SOUND(false, 01384 "ArithTheoremProducerOld::constPredicate: wrong kind"); 01385 } 01386 break; 01387 } 01388 Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr(); 01389 if(withProof()) pf = newPf("const_predicate", e,ret); 01390 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf); 01391 } 01392 01393 // e[0] kind e[1] <==> 0 kind e[1] - e[0] 01394 Theorem ArithTheoremProducerOld::rightMinusLeft(const Expr& e) 01395 { 01396 Proof pf; 01397 int kind = e.getKind(); 01398 if(CHECK_PROOFS) { 01399 CHECK_SOUND((EQ==kind) || 01400 (LT==kind) || 01401 (LE==kind) || 01402 (GE==kind) || 01403 (GT==kind), 01404 "ArithTheoremProducerOld::rightMinusLeft: wrong kind"); 01405 } 01406 if(withProof()) pf = newPf("right_minus_left",e); 01407 return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf); 01408 } 01409 01410 01411 // e[0] kind e[1] <==> 0 kind e[1] - e[0] 01412 Theorem ArithTheoremProducerOld::leftMinusRight(const Expr& e) 01413 { 01414 Proof pf; 01415 int kind = e.getKind(); 01416 if(CHECK_PROOFS) { 01417 CHECK_SOUND((EQ==kind) || 01418 (LT==kind) || 01419 (LE==kind) || 01420 (GE==kind) || 01421 (GT==kind), 01422 "ArithTheoremProducerOld::rightMinusLeft: wrong kind"); 01423 } 01424 if(withProof()) pf = newPf("left_minus_right",e); 01425 return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf); 01426 } 01427 01428 01429 // x kind y <==> x + z kind y + z 01430 Theorem ArithTheoremProducerOld::plusPredicate(const Expr& x, 01431 const Expr& y, 01432 const Expr& z, int kind) { 01433 if(CHECK_PROOFS) { 01434 CHECK_SOUND((EQ==kind) || 01435 (LT==kind) || 01436 (LE==kind) || 01437 (GE==kind) || 01438 (GT==kind), 01439 "ArithTheoremProducerOld::plusPredicate: wrong kind"); 01440 } 01441 Proof pf; 01442 Expr left = Expr(kind, x, y); 01443 Expr right = Expr(kind, x + z, y + z); 01444 if(withProof()) pf = newPf("plus_predicate",left,right); 01445 return newRWTheorem(left, right, Assumptions::emptyAssump(), pf); 01446 } 01447 01448 // x = y <==> x * z = y * z 01449 Theorem ArithTheoremProducerOld::multEqn(const Expr& x, 01450 const Expr& y, 01451 const Expr& z) { 01452 Proof pf; 01453 if(CHECK_PROOFS) 01454 CHECK_SOUND(z.isRational() && z.getRational() != 0, 01455 "ArithTheoremProducerOld::multEqn(): multiplying equation by 0"); 01456 if(withProof()) pf = newPf("mult_eqn", x, y, z); 01457 return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf); 01458 } 01459 01460 01461 // x = y <==> z=0 OR x * 1/z = y * 1/z 01462 Theorem ArithTheoremProducerOld::divideEqnNonConst(const Expr& x, 01463 const Expr& y, 01464 const Expr& z) { 01465 Proof pf; 01466 if(withProof()) pf = newPf("mult_eqn_nonconst", x, y, z); 01467 return newRWTheorem(x.eqExpr(y), (z.eqExpr(rat(0))).orExpr((x / z).eqExpr(y / z)), 01468 Assumptions::emptyAssump(), pf); 01469 } 01470 01471 01472 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z 01473 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z 01474 Theorem ArithTheoremProducerOld::multIneqn(const Expr& e, const Expr& z) 01475 { 01476 int kind = e.getKind(); 01477 01478 if(CHECK_PROOFS) { 01479 CHECK_SOUND((LT==kind) || 01480 (LE==kind) || 01481 (GE==kind) || 01482 (GT==kind), 01483 "ArithTheoremProducerOld::multIneqn: wrong kind"); 01484 CHECK_SOUND(z.isRational() && z.getRational() != 0, 01485 "ArithTheoremProducerOld::multIneqn: " 01486 "z must be non-zero rational: " + z.toString()); 01487 } 01488 Op op(e.getOp()); 01489 Proof pf; 01490 01491 Expr ret; 01492 if(0 < z.getRational()) 01493 ret = Expr(op, e[0]*z, e[1]*z); 01494 else 01495 ret = Expr(op, e[1]*z, e[0]*z); 01496 if(withProof()) pf = newPf("mult_ineqn", e, ret); 01497 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf); 01498 } 01499 01500 01501 // 01502 // If expr: 01503 // If b > 0 then (0 <= a + bx) <==> (0 <= floor(a/b) + x) 01504 // b < 0 then (0 <= a + bx) <==> (0 >= ceil(a/b) + x) 01505 // b > 0 then (0 >= a + bx) <==> (0 >= ceil(a/b) + x) 01506 // b < 0 then (0 >= a + bx) <==> (0 <= floor(a/b) + x) 01507 // 01508 Theorem ArithTheoremProducerOld::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) 01509 { 01510 // Get the inequality parts 01511 Expr lhs = ineq[0]; 01512 Expr rhs = ineq[1]; 01513 01514 // Get the kind of the inequality 01515 int kind = ineq.getKind(); 01516 01517 01518 if(CHECK_PROOFS) { 01519 // isIntRHS should be an int proof of rhs 01520 const Expr& isIntRHSExpr = isIntRHS.getExpr(); 01521 CHECK_SOUND(isIntPred(isIntRHSExpr) && isIntRHSExpr[0] == rhs, "ArithTheoremProducerOld::multSimpleIneqnInt: not an integer proof of rhs"); 01522 01523 // It's an inequality 01524 CHECK_SOUND((LT == kind) || (LE==kind) || (GE==kind) || (GT==kind), "ArithTheoremProducerOld::multSimpleIneqnInt: wrong kind"); 01525 01526 // Left-hand side is 0 01527 CHECK_SOUND(lhs.isRational() && lhs.getRational() == 0, "ArithTheoremProducerOld::multSimpleIneqnInt: left-hand side must be 0"); 01528 01529 // Tight hand side is a sum (a + b*x) where a and b are integers, x is a var 01530 CHECK_SOUND(isPlus(rhs), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side must be a plus"); 01531 CHECK_SOUND(rhs.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus"); 01532 01533 Expr a = rhs[0]; // Should be an integer 01534 Expr bx = rhs[1]; // Should be an integer multiplied by a variable 01535 01536 // a is an integer 01537 CHECK_SOUND(a.isRational() && a.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of a constant"); 01538 01539 // bx should be a multiplication of an intgere and a variable 01540 CHECK_SOUND(isMult(bx) && bx.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication"); 01541 Expr b = bx[0]; 01542 Expr x = bx[1]; 01543 01544 // b should be an integer 01545 CHECK_SOUND(b.isRational() && b.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant"); 01546 // x should be a variable 01547 CHECK_SOUND(x.isVar(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant and a leaf"); 01548 01549 // GCD(a, b) should be 1 01550 //CHECK_SOUND(gcd(a.getRational(), b.getRational()) == 1, "ArithTheoremProducerOld::multSimpleIneqnInt: inequation not normalized!!!"); 01551 } 01552 01553 Proof pf; 01554 if(withProof()) { 01555 vector<Proof> pfs; 01556 pfs.push_back(isIntRHS.getProof()); 01557 pf = newPf("simpleineqint", ineq, pf); 01558 } 01559 01560 Rational a = rhs[0].getRational(); 01561 Rational b = rhs[1][0].getRational(); 01562 Expr x = rhs[1][1]; 01563 01564 Rational new_const; 01565 Expr ret; 01566 switch (kind) { 01567 case LT: 01568 if (b > 0) { 01569 new_const = floor(a/b); 01570 if (new_const != 0) 01571 ret = Expr(kind, rat(0), rat(new_const) + x); 01572 else 01573 ret = Expr(kind, rat(0), x); 01574 } 01575 else { 01576 new_const = ceil(a/b); 01577 //ret = geExpr(rat(0), rat(new_const) + x); 01578 if (new_const != 0) 01579 ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x); 01580 else 01581 ret = Expr(kind, rat(0), rat(-1)*x); 01582 } 01583 break; 01584 break; 01585 case LE: 01586 if (b > 0) { 01587 new_const = floor(a/b); 01588 if (new_const != 0) 01589 ret = Expr(kind, rat(0), rat(new_const) + x); 01590 else 01591 ret = Expr(kind, rat(0), x); 01592 } 01593 else { 01594 new_const = ceil(a/b); 01595 //ret = geExpr(rat(0), rat(new_const) + x); 01596 if (new_const != 0) 01597 ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x); 01598 else 01599 ret = Expr(kind, rat(0), rat(-1)*x); 01600 } 01601 break; 01602 case GE: 01603 case GT: 01604 // Setup the result kind 01605 if (kind == GT) kind = LT; 01606 else kind = LE; 01607 01608 if (b > 0) { 01609 new_const = ceil(a/b); 01610 //ret = geExpr(rat(0), rat(new_const) + x); 01611 if (new_const != 0) 01612 ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x); 01613 else 01614 ret = Expr(kind, rat(0), rat(-1)*x); 01615 } 01616 else { 01617 new_const = floor(a/b); 01618 if (new_const != 0) 01619 ret = Expr(kind, rat(0), rat(new_const) + x); 01620 else 01621 ret = Expr(kind, rat(0), x); 01622 } 01623 break; 01624 } 01625 01626 // Return the new theorem 01627 return newRWTheorem(ineq, ret, Assumptions::emptyAssump(), pf); 01628 } 01629 01630 01631 Theorem ArithTheoremProducerOld::eqToIneq(const Expr& e) { 01632 01633 // Check soundness of the rule if necessary 01634 if (CHECK_PROOFS) 01635 CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString()); 01636 01637 // The proof object we will use 01638 Proof pf; 01639 01640 // The parts of the equality x = y 01641 const Expr& x = e[0]; 01642 const Expr& y = e[1]; 01643 01644 // Setup the proof if needed 01645 if (withProof()) 01646 pf = newPf("eqToIneq", e); 01647 01648 // Retrun the theorem explaining the transformation 01649 return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf); 01650 } 01651 01652 // "op1 GE|GT op2" <==> op2 LE|LT op1 01653 Theorem ArithTheoremProducerOld::flipInequality(const Expr& e) 01654 { 01655 Proof pf; 01656 if(CHECK_PROOFS) { 01657 CHECK_SOUND(isGT(e) || isGE(e), 01658 "ArithTheoremProducerOld::flipInequality: wrong kind: " + 01659 e.toString()); 01660 } 01661 01662 int kind = isGE(e) ? LE : LT; 01663 Expr ret = Expr(kind, e[1], e[0]); 01664 if(withProof()) pf = newPf("flip_inequality", e,ret); 01665 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf); 01666 } 01667 01668 01669 // NOT (op1 LT op2) <==> (op1 GE op2) 01670 // NOT (op1 LE op2) <==> (op1 GT op2) 01671 // NOT (op1 GT op2) <==> (op1 LE op2) 01672 // NOT (op1 GE op2) <==> (op1 LT op2) 01673 Theorem ArithTheoremProducerOld::negatedInequality(const Expr& e) 01674 { 01675 const Expr& ineq = e[0]; 01676 if(CHECK_PROOFS) { 01677 CHECK_SOUND(e.isNot(), 01678 "ArithTheoremProducerOld::negatedInequality: wrong kind: " + 01679 e.toString()); 01680 CHECK_SOUND(isIneq(ineq), 01681 "ArithTheoremProducerOld::negatedInequality: wrong kind: " + 01682 (ineq).toString()); 01683 } 01684 Proof pf; 01685 if(withProof()) pf = newPf("negated_inequality", e); 01686 01687 int kind; 01688 // NOT (op1 LT op2) <==> (op1 GE op2) 01689 // NOT (op1 LE op2) <==> (op1 GT op2) 01690 // NOT (op1 GT op2) <==> (op1 LE op2) 01691 // NOT (op1 GE op2) <==> (op1 LT op2) 01692 kind = 01693 isLT(ineq) ? GE : 01694 isLE(ineq) ? GT : 01695 isGT(ineq) ? LE : 01696 LT; 01697 return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf); 01698 } 01699 01700 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta" 01701 //and returns "|- alpha LT|LE beta" 01702 Theorem ArithTheoremProducerOld::realShadow(const Theorem& alphaLTt, 01703 const Theorem& tLTbeta) 01704 { 01705 const Expr& expr1 = alphaLTt.getExpr(); 01706 const Expr& expr2 = tLTbeta.getExpr(); 01707 if(CHECK_PROOFS) { 01708 CHECK_SOUND((isLE(expr1) || isLT(expr1)) && 01709 (isLE(expr2) || isLT(expr2)), 01710 "ArithTheoremProducerOld::realShadow: Wrong Kind: " + 01711 alphaLTt.toString() + tLTbeta.toString()); 01712 01713 CHECK_SOUND(expr1[1] == expr2[0], 01714 "ArithTheoremProducerOld::realShadow:" 01715 " t must be same for both inputs: " + 01716 expr1[1].toString() + " , " + expr2[0].toString()); 01717 } 01718 Assumptions a(alphaLTt, tLTbeta); 01719 int firstKind = expr1.getKind(); 01720 int secondKind = expr2.getKind(); 01721 int kind = (firstKind == secondKind) ? firstKind : LT; 01722 Proof pf; 01723 if(withProof()) { 01724 vector<Proof> pfs; 01725 pfs.push_back(alphaLTt.getProof()); 01726 pfs.push_back(tLTbeta.getProof()); 01727 pf = newPf("real_shadow",expr1, expr2, pfs); 01728 } 01729 return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf); 01730 } 01731 01732 //! alpha <= t <= alpha ==> t = alpha 01733 01734 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha" 01735 and returns "|- t = alpha" 01736 */ 01737 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt, 01738 const Theorem& tLEalpha) 01739 { 01740 const Expr& expr1 = alphaLEt.getExpr(); 01741 const Expr& expr2 = tLEalpha.getExpr(); 01742 if(CHECK_PROOFS) { 01743 CHECK_SOUND(isLE(expr1) && isLE(expr2), 01744 "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " + 01745 alphaLEt.toString() + tLEalpha.toString()); 01746 01747 CHECK_SOUND(expr1[1] == expr2[0], 01748 "ArithTheoremProducerOld::realShadowLTLE:" 01749 " t must be same for both inputs: " + 01750 alphaLEt.toString() + " , " + tLEalpha.toString()); 01751 01752 CHECK_SOUND(expr1[0] == expr2[1], 01753 "ArithTheoremProducerOld::realShadowLTLE:" 01754 " alpha must be same for both inputs: " + 01755 alphaLEt.toString() + " , " + tLEalpha.toString()); 01756 } 01757 Assumptions a(alphaLEt, tLEalpha); 01758 Proof pf; 01759 if(withProof()) { 01760 vector<Proof> pfs; 01761 pfs.push_back(alphaLEt.getProof()); 01762 pfs.push_back(tLEalpha.getProof()); 01763 pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs); 01764 } 01765 return newRWTheorem(expr1[0], expr1[1], a, pf); 01766 } 01767 01768 Theorem 01769 ArithTheoremProducerOld::finiteInterval(const Theorem& aLEt, 01770 const Theorem& tLEac, 01771 const Theorem& isInta, 01772 const Theorem& isIntt) { 01773 const Expr& e1 = aLEt.getExpr(); 01774 const Expr& e2 = tLEac.getExpr(); 01775 if(CHECK_PROOFS) { 01776 CHECK_SOUND(isLE(e1) && isLE(e2), 01777 "ArithTheoremProducerOld::finiteInterval:\n e1 = " 01778 +e1.toString()+"\n e2 = "+e2.toString()); 01779 // term 't' is the same in both inequalities 01780 CHECK_SOUND(e1[1] == e2[0], 01781 "ArithTheoremProducerOld::finiteInterval:\n e1 = " 01782 +e1.toString()+"\n e2 = "+e2.toString()); 01783 // RHS in e2 is (a+c) 01784 CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2, 01785 "ArithTheoremProducerOld::finiteInterval:\n e1 = " 01786 +e1.toString()+"\n e2 = "+e2.toString()); 01787 // term 'a' in LHS of e1 and RHS of e2 is the same 01788 CHECK_SOUND(e1[0] == e2[1][0], 01789 "ArithTheoremProducerOld::finiteInterval:\n e1 = " 01790 +e1.toString()+"\n e2 = "+e2.toString()); 01791 // 'c' in the RHS of e2 is a positive integer constant 01792 CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger() 01793 && e2[1][1].getRational() >= 1, 01794 "ArithTheoremProducerOld::finiteInterval:\n e1 = " 01795 +e1.toString()+"\n e2 = "+e2.toString()); 01796 // Integrality constraints 01797 const Expr& isIntaExpr = isInta.getExpr(); 01798 const Expr& isInttExpr = isIntt.getExpr(); 01799 CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0], 01800 "Wrong integrality constraint:\n e1 = " 01801 +e1.toString()+"\n isInta = "+isIntaExpr.toString()); 01802 CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1], 01803 "Wrong integrality constraint:\n e1 = " 01804 +e1.toString()+"\n isIntt = "+isInttExpr.toString()); 01805 } 01806 vector<Theorem> thms; 01807 thms.push_back(aLEt); 01808 thms.push_back(tLEac); 01809 thms.push_back(isInta); 01810 thms.push_back(isIntt); 01811 Assumptions a(thms); 01812 Proof pf; 01813 if(withProof()) { 01814 vector<Expr> es; 01815 vector<Proof> pfs; 01816 es.push_back(e1); 01817 es.push_back(e2); 01818 es.push_back(isInta.getExpr()); 01819 es.push_back(isIntt.getExpr()); 01820 pfs.push_back(aLEt.getProof()); 01821 pfs.push_back(tLEac.getProof()); 01822 pfs.push_back(isInta.getProof()); 01823 pfs.push_back(isIntt.getProof()); 01824 pf = newPf("finite_interval", es, pfs); 01825 } 01826 // Construct GRAY_SHADOW(t, a, 0, c) 01827 Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational())); 01828 return newTheorem(g, a, pf); 01829 } 01830 01831 01832 // Dark & Gray shadows when a <= b 01833 Theorem ArithTheoremProducerOld::darkGrayShadow2ab(const Theorem& betaLEbx, 01834 const Theorem& axLEalpha, 01835 const Theorem& isIntAlpha, 01836 const Theorem& isIntBeta, 01837 const Theorem& isIntx) { 01838 const Expr& expr1 = betaLEbx.getExpr(); 01839 const Expr& expr2 = axLEalpha.getExpr(); 01840 const Expr& isIntAlphaExpr = isIntAlpha.getExpr(); 01841 const Expr& isIntBetaExpr = isIntBeta.getExpr(); 01842 const Expr& isIntxExpr = isIntx.getExpr(); 01843 01844 if(CHECK_PROOFS) { 01845 CHECK_SOUND(isLE(expr1) && isLE(expr2), 01846 "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " + 01847 betaLEbx.toString() + axLEalpha.toString()); 01848 } 01849 01850 const Expr& beta = expr1[0]; 01851 const Expr& bx = expr1[1]; 01852 const Expr& ax = expr2[0]; 01853 const Expr& alpha = expr2[1]; 01854 Expr a_expr, b_expr, x; 01855 d_theoryArith->separateMonomial(ax, a_expr, x); 01856 d_theoryArith->separateMonomial(bx, b_expr, x); 01857 Rational a = a_expr.getRational(); 01858 Rational b = b_expr.getRational(); 01859 01860 if(CHECK_PROOFS) { 01861 // Integrality constraints 01862 CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha, 01863 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01864 "wrong integrality constraint:\n alpha = " 01865 +alpha.toString()+"\n isIntAlpha = " 01866 +isIntAlphaExpr.toString()); 01867 CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta, 01868 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01869 "wrong integrality constraint:\n beta = " 01870 +beta.toString()+"\n isIntBeta = " 01871 +isIntBetaExpr.toString()); 01872 CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x, 01873 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01874 "wrong integrality constraint:\n x = " 01875 +x.toString()+"\n isIntx = " 01876 +isIntxExpr.toString()); 01877 // NOT FOR NONLINEAR: Expressions ax and bx should match on x 01878 // CHECK_SOUND(!isMult(ax) || ax.arity() == 2, 01879 // "ArithTheoremProducerOld::darkGrayShadow2ab:\n ax<=alpha: " + 01880 // axLEalpha.toString()); 01881 // CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x), 01882 // "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: " 01883 // +betaLEbx.toString() 01884 // +"\n ax<=alpha: "+ axLEalpha.toString()); 01885 CHECK_SOUND(1 <= a && a <= b && 2 <= b, 01886 "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: " 01887 +betaLEbx.toString() 01888 +"\n ax<=alpha: "+ axLEalpha.toString()); 01889 } 01890 vector<Theorem> thms; 01891 thms.push_back(betaLEbx); 01892 thms.push_back(axLEalpha); 01893 thms.push_back(isIntAlpha); 01894 thms.push_back(isIntBeta); 01895 thms.push_back(isIntx); 01896 Assumptions A(thms); 01897 01898 Expr bAlpha = multExpr(rat(b), alpha); 01899 Expr aBeta = multExpr(rat(a), beta); 01900 Expr t = minusExpr(bAlpha, aBeta); 01901 Expr d = geExpr(t, rat(a*b-1)); 01902 Expr g = grayShadow(ax, alpha, -a+1, 0); 01903 01904 Proof pf; 01905 if(withProof()) { 01906 vector<Expr> exprs; 01907 exprs.push_back(expr1); 01908 exprs.push_back(expr2); 01909 exprs.push_back(d); 01910 exprs.push_back(g); 01911 01912 vector<Proof> pfs; 01913 pfs.push_back(betaLEbx.getProof()); 01914 pfs.push_back(axLEalpha.getProof()); 01915 pfs.push_back(isIntAlpha.getProof()); 01916 pfs.push_back(isIntBeta.getProof()); 01917 pfs.push_back(isIntx.getProof()); 01918 01919 pf = newPf("dark_grayshadow_2ab", exprs, pfs); 01920 } 01921 01922 return newTheorem((d || g), A, pf); 01923 } 01924 01925 // Dark & Gray shadows when b <= a 01926 Theorem ArithTheoremProducerOld::darkGrayShadow2ba(const Theorem& betaLEbx, 01927 const Theorem& axLEalpha, 01928 const Theorem& isIntAlpha, 01929 const Theorem& isIntBeta, 01930 const Theorem& isIntx) { 01931 const Expr& expr1 = betaLEbx.getExpr(); 01932 const Expr& expr2 = axLEalpha.getExpr(); 01933 const Expr& isIntAlphaExpr = isIntAlpha.getExpr(); 01934 const Expr& isIntBetaExpr = isIntBeta.getExpr(); 01935 const Expr& isIntxExpr = isIntx.getExpr(); 01936 01937 if(CHECK_PROOFS) { 01938 CHECK_SOUND(isLE(expr1) && isLE(expr2), 01939 "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " + 01940 betaLEbx.toString() + axLEalpha.toString()); 01941 } 01942 01943 const Expr& beta = expr1[0]; 01944 const Expr& bx = expr1[1]; 01945 const Expr& ax = expr2[0]; 01946 const Expr& alpha = expr2[1]; 01947 01948 Expr a_expr, b_expr, x; 01949 d_theoryArith->separateMonomial(ax, a_expr, x); 01950 d_theoryArith->separateMonomial(bx, b_expr, x); 01951 Rational a = a_expr.getRational(); 01952 Rational b = b_expr.getRational(); 01953 01954 if(CHECK_PROOFS) { 01955 // Integrality constraints 01956 CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha, 01957 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01958 "wrong integrality constraint:\n alpha = " 01959 +alpha.toString()+"\n isIntAlpha = " 01960 +isIntAlphaExpr.toString()); 01961 CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta, 01962 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01963 "wrong integrality constraint:\n beta = " 01964 +beta.toString()+"\n isIntBeta = " 01965 +isIntBetaExpr.toString()); 01966 CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x, 01967 "ArithTheoremProducerOld::darkGrayShadow2ab:\n " 01968 "wrong integrality constraint:\n x = " 01969 +x.toString()+"\n isIntx = " 01970 +isIntxExpr.toString()); 01971 // NOT FOR NONLINEAR: Expressions ax and bx should match on x 01972 // CHECK_SOUND(!isMult(ax) || ax.arity() == 2, 01973 // "ArithTheoremProducerOld::darkGrayShadow2ba:\n ax<=alpha: " + 01974 // axLEalpha.toString()); 01975 // CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x), 01976 // "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: " 01977 // +betaLEbx.toString() 01978 // +"\n ax<=alpha: "+ axLEalpha.toString()); 01979 CHECK_SOUND(1 <= b && b <= a && 2 <= a, 01980 "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: " 01981 +betaLEbx.toString() 01982 +"\n ax<=alpha: "+ axLEalpha.toString()); 01983 } 01984 vector<Theorem> thms; 01985 thms.push_back(betaLEbx); 01986 thms.push_back(axLEalpha); 01987 thms.push_back(isIntAlpha); 01988 thms.push_back(isIntBeta); 01989 thms.push_back(isIntx); 01990 Assumptions A(thms); 01991 Proof pf; 01992 if(withProof()) { 01993 vector<Proof> pfs; 01994 pfs.push_back(betaLEbx.getProof()); 01995 pfs.push_back(axLEalpha.getProof()); 01996 pfs.push_back(isIntAlpha.getProof()); 01997 pfs.push_back(isIntBeta.getProof()); 01998 pfs.push_back(isIntx.getProof()); 01999 02000 pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(), 02001 axLEalpha.getExpr(), pfs); 02002 } 02003 02004 Expr bAlpha = multExpr(rat(b), alpha); 02005 Expr aBeta = multExpr(rat(a), beta); 02006 Expr t = minusExpr(bAlpha, aBeta); 02007 Expr d = geExpr(t, rat(a*b-1)); 02008 Expr g = grayShadow(bx, beta, 0, b-1); 02009 return newTheorem((d || g), A, pf); 02010 } 02011 02012 /*! takes a dark shadow and expands it into an inequality. 02013 */ 02014 Theorem ArithTheoremProducerOld::expandDarkShadow(const Theorem& darkShadow) { 02015 const Expr& theShadow = darkShadow.getExpr(); 02016 if(CHECK_PROOFS){ 02017 CHECK_SOUND(isDarkShadow(theShadow), 02018 "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " + 02019 theShadow.toString()); 02020 } 02021 Proof pf; 02022 if(withProof()) 02023 pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof()); 02024 return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf); 02025 } 02026 02027 02028 // takes a grayShadow (c1==c2) and expands it into an equality 02029 Theorem ArithTheoremProducerOld::expandGrayShadow0(const Theorem& grayShadow) { 02030 const Expr& theShadow = grayShadow.getExpr(); 02031 if(CHECK_PROOFS) { 02032 CHECK_SOUND(isGrayShadow(theShadow), 02033 "ArithTheoremProducerOld::expandGrayShadowConst0:" 02034 " not GRAY_SHADOW: " + 02035 theShadow.toString()); 02036 CHECK_SOUND(theShadow[2] == theShadow[3], 02037 "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " + 02038 theShadow.toString()); 02039 } 02040 Proof pf; 02041 if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow, 02042 grayShadow.getProof()); 02043 const Expr& v = theShadow[0]; 02044 const Expr& e = theShadow[1]; 02045 return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf); 02046 } 02047 02048 02049 // G ==> (G1 or G2) and (!G1 or !G2), 02050 // where G = G(x, e, c1, c2), 02051 // G1 = G(x,e,c1,c) 02052 // G2 = G(x,e,c+1,c2), 02053 // and c = floor((c1+c2)/2) 02054 Theorem ArithTheoremProducerOld::splitGrayShadow(const Theorem& gThm) { 02055 const Expr& theShadow = gThm.getExpr(); 02056 if(CHECK_PROOFS) { 02057 CHECK_SOUND(isGrayShadow(theShadow), 02058 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" + 02059 theShadow.toString()); 02060 } 02061 02062 const Rational& c1 = theShadow[2].getRational(); 02063 const Rational& c2 = theShadow[3].getRational(); 02064 02065 if(CHECK_PROOFS) { 02066 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2, 02067 "ArithTheoremProducerOld::expandGrayShadow: " + 02068 theShadow.toString()); 02069 } 02070 02071 const Expr& v = theShadow[0]; 02072 const Expr& e = theShadow[1]; 02073 02074 Proof pf; 02075 Rational c(floor((c1+c2) / 2)); 02076 Expr g1(grayShadow(v, e, c1, c)); 02077 Expr g2(grayShadow(v, e, c+1, c2)); 02078 02079 if(withProof()){ 02080 vector<Expr> exprs; 02081 exprs.push_back(theShadow); 02082 exprs.push_back(g1); 02083 exprs.push_back(g2); 02084 pf = newPf("split_gray_shadow", exprs, gThm.getProof()); 02085 } 02086 02087 return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf); 02088 } 02089 02090 02091 Theorem ArithTheoremProducerOld::expandGrayShadow(const Theorem& gThm) { 02092 const Expr& theShadow = gThm.getExpr(); 02093 if(CHECK_PROOFS) { 02094 CHECK_SOUND(isGrayShadow(theShadow), 02095 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" + 02096 theShadow.toString()); 02097 } 02098 02099 const Rational& c1 = theShadow[2].getRational(); 02100 const Rational& c2 = theShadow[3].getRational(); 02101 02102 if(CHECK_PROOFS) { 02103 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2, 02104 "ArithTheoremProducerOld::expandGrayShadow: " + 02105 theShadow.toString()); 02106 } 02107 02108 const Expr& v = theShadow[0]; 02109 const Expr& e = theShadow[1]; 02110 02111 Proof pf; 02112 if(withProof()) 02113 pf = newPf("expand_gray_shadow", theShadow, gThm.getProof()); 02114 Expr ineq1(leExpr(e+rat(c1), v)); 02115 Expr ineq2(leExpr(v, e+rat(c2))); 02116 return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf); 02117 } 02118 02119 02120 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant 02121 Theorem 02122 ArithTheoremProducerOld::expandGrayShadowConst(const Theorem& gThm) { 02123 const Expr& theShadow = gThm.getExpr(); 02124 const Expr& ax = theShadow[0]; 02125 const Expr& cExpr = theShadow[1]; 02126 const Expr& bExpr = theShadow[2]; 02127 02128 if(CHECK_PROOFS) { 02129 CHECK_SOUND(!isMult(ax) || ax[0].isRational(), 02130 "ArithTheoremProducerOld::expandGrayShadowConst: " 02131 "'a' in a*x is not a const: " +theShadow.toString()); 02132 } 02133 02134 Rational a = isMult(ax)? ax[0].getRational() : 1; 02135 02136 if(CHECK_PROOFS) { 02137 CHECK_SOUND(isGrayShadow(theShadow), 02138 "ArithTheoremProducerOld::expandGrayShadowConst: " 02139 "not a GRAY_SHADOW: " +theShadow.toString()); 02140 CHECK_SOUND(a.isInteger() && a >= 1, 02141 "ArithTheoremProducerOld::expandGrayShadowConst: " 02142 "'a' is not integer: " +theShadow.toString()); 02143 CHECK_SOUND(cExpr.isRational(), 02144 "ArithTheoremProducerOld::expandGrayShadowConst: " 02145 "'c' is not rational" +theShadow.toString()); 02146 CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(), 02147 "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: " 02148 +theShadow.toString()); 02149 } 02150 02151 const Rational& b = bExpr.getRational(); 02152 const Rational& c = cExpr.getRational(); 02153 Rational j = constRHSGrayShadow(c,b,a); 02154 // Compute sign(b)*j(c,b,a) 02155 Rational signB = (b>0)? 1 : -1; 02156 // |b| (absolute value of b) 02157 Rational bAbs = abs(b); 02158 02159 const Assumptions& assump(gThm.getAssumptionsRef()); 02160 Proof pf; 02161 Theorem conc; // Conclusion of the rule 02162 02163 if(bAbs < j) { 02164 if(withProof()) 02165 pf = newPf("expand_gray_shadow_const_0", theShadow, 02166 gThm.getProof()); 02167 conc = newTheorem(d_em->falseExpr(), assump, pf); 02168 } else if(bAbs < a+j) { 02169 if(withProof()) 02170 pf = newPf("expand_gray_shadow_const_1", theShadow, 02171 gThm.getProof()); 02172 conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf); 02173 } else { 02174 if(withProof()) 02175 pf = newPf("expand_gray_shadow_const", theShadow, 02176 gThm.getProof()); 02177 Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j)))); 02178 conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow), 02179 assump, pf); 02180 } 02181 02182 return conc; 02183 } 02184 02185 02186 Theorem 02187 ArithTheoremProducerOld::grayShadowConst(const Theorem& gThm) { 02188 const Expr& g = gThm.getExpr(); 02189 bool checkProofs(CHECK_PROOFS); 02190 if(checkProofs) { 02191 CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducerOld::grayShadowConst(" 02192 +g.toString()+")"); 02193 } 02194 02195 const Expr& ax = g[0]; 02196 const Expr& e = g[1]; 02197 const Rational& c1 = g[2].getRational(); 02198 const Rational& c2 = g[3].getRational(); 02199 Expr aExpr, x; 02200 d_theoryArith->separateMonomial(ax, aExpr, x); 02201 02202 if(checkProofs) { 02203 CHECK_SOUND(e.isRational() && e.getRational().isInteger(), 02204 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")"); 02205 CHECK_SOUND(aExpr.isRational(), 02206 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")"); 02207 } 02208 02209 const Rational& a = aExpr.getRational(); 02210 const Rational& c = e.getRational(); 02211 02212 if(checkProofs) { 02213 CHECK_SOUND(a.isInteger() && a >= 2, 02214 "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")"); 02215 } 02216 02217 Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a); 02218 Expr newG((newC1 > newC2)? d_em->falseExpr() 02219 : grayShadow(x, rat(0), newC1, newC2)); 02220 Proof pf; 02221 if(withProof()) 02222 pf = newPf("gray_shadow_const", g, newG, gThm.getProof()); 02223 return newTheorem(newG, gThm.getAssumptionsRef(), pf); 02224 } 02225 02226 02227 Rational ArithTheoremProducerOld::constRHSGrayShadow(const Rational& c, 02228 const Rational& b, 02229 const Rational& a) { 02230 DebugAssert(c.isInteger() && 02231 b.isInteger() && 02232 a.isInteger() && 02233 b != 0, 02234 "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints"); 02235 if (b > 0) 02236 return mod(c+b, a); 02237 else 02238 return mod(a-(c+b), a); 02239 } 02240 02241 /*! Takes a Theorem(\\alpha < \\beta) and returns 02242 * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1) 02243 * where \\alpha and \\beta are integer expressions 02244 */ 02245 Theorem ArithTheoremProducerOld::lessThanToLE(const Theorem& less, 02246 const Theorem& isIntLHS, 02247 const Theorem& isIntRHS, 02248 bool changeRight) { 02249 const Expr& ineq = less.getExpr(); 02250 const Expr& isIntLHSexpr = isIntLHS.getExpr(); 02251 const Expr& isIntRHSexpr = isIntRHS.getExpr(); 02252 02253 if(CHECK_PROOFS) { 02254 CHECK_SOUND(isLT(ineq), 02255 "ArithTheoremProducerOld::LTtoLE: ineq must be <"); 02256 // Integrality check 02257 CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0], 02258 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n" 02259 " ineq = "+ineq.toString()+"\n isIntLHS = " 02260 +isIntLHSexpr.toString()); 02261 CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1], 02262 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n" 02263 " ineq = "+ineq.toString()+"\n isIntRHS = " 02264 +isIntRHSexpr.toString()); 02265 } 02266 vector<Theorem> thms; 02267 thms.push_back(less); 02268 thms.push_back(isIntLHS); 02269 thms.push_back(isIntRHS); 02270 Assumptions a(thms); 02271 Proof pf; 02272 Expr le = changeRight? 02273 leExpr(ineq[0], ineq[1] + rat(-1)) 02274 : leExpr(ineq[0] + rat(1), ineq[1]); 02275 if(withProof()) { 02276 vector<Proof> pfs; 02277 pfs.push_back(less.getProof()); 02278 pfs.push_back(isIntLHS.getProof()); 02279 pfs.push_back(isIntRHS.getProof()); 02280 pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs", 02281 ineq,le, pfs); 02282 } 02283 02284 return newRWTheorem(ineq, le, a, pf); 02285 } 02286 02287 02288 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x 02289 * \param isIntx is a proof of IS_INTEGER(x) 02290 * 02291 * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else 02292 * return the theorem 0 = c + a.x <==> false. 02293 * 02294 * It also handles the special case of 0 = a.x <==> x = 0 02295 */ 02296 Theorem 02297 ArithTheoremProducerOld::intVarEqnConst(const Expr& eqn, 02298 const Theorem& isIntx) { 02299 const Expr& left(eqn[0]); 02300 const Expr& right(eqn[1]); 02301 const Expr& isIntxexpr(isIntx.getExpr()); 02302 02303 if(CHECK_PROOFS) { 02304 CHECK_SOUND((isMult(right) && right[0].isRational()) 02305 || (right.arity() == 2 && isPlus(right) 02306 && right[0].isRational() 02307 && ((!isMult(right[1]) || right[1][0].isRational()))), 02308 "ArithTheoremProducerOld::intVarEqnConst: " 02309 "rhs has a wrong format: " + right.toString()); 02310 CHECK_SOUND(left.isRational() && 0 == left.getRational(), 02311 "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " + 02312 left.toString()); 02313 } 02314 // Integrality constraint 02315 Expr x(right); 02316 Rational a(1), c(0); 02317 if(isMult(right)) { 02318 Expr aExpr; 02319 d_theoryArith->separateMonomial(right, aExpr, x); 02320 a = aExpr.getRational(); 02321 } else { // right is a PLUS 02322 c = right[0].getRational(); 02323 Expr aExpr; 02324 d_theoryArith->separateMonomial(right[1], aExpr, x); 02325 a = aExpr.getRational(); 02326 } 02327 if(CHECK_PROOFS) { 02328 CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x, 02329 "ArithTheoremProducerOld:intVarEqnConst: " 02330 "bad integrality constraint:\n right = " + 02331 right.toString()+"\n isIntx = "+isIntxexpr.toString()); 02332 CHECK_SOUND(a!=0, "ArithTheoremProducerOld:intVarEqnConst: eqn = " 02333 +eqn.toString()); 02334 } 02335 const Assumptions& assump(isIntx.getAssumptionsRef()); 02336 02337 /* 02338 Proof pf; 02339 if(withProof()) 02340 pf = newPf("int_const_eq", eqn, isIntx.getProof()); 02341 02342 // Solve for x: x = r = -c/a 02343 Rational r(-c/a); 02344 02345 if(r.isInteger()){ 02346 return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf); 02347 else 02348 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf); 02349 */ 02350 02351 Proof pf; 02352 // Solve for x: x = r = -c/a 02353 Rational r(-c/a); 02354 02355 if(r.isInteger()){ 02356 if(withProof()) 02357 pf = newPf("int_const_eq", eqn, x.eqExpr(rat(r)),isIntx.getProof()); 02358 return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf); 02359 } 02360 else{ 02361 if(withProof()) 02362 pf = newPf("int_const_eq", eqn, d_em->falseExpr(),isIntx.getProof()); 02363 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf); 02364 } 02365 } 02366 02367 02368 Expr 02369 ArithTheoremProducerOld::create_t(const Expr& eqn) { 02370 const Expr& lhs = eqn[0]; 02371 DebugAssert(isMult(lhs), 02372 CLASS_NAME "create_t : lhs must be a MULT" 02373 + lhs.toString()); 02374 const Expr& x = lhs[1]; 02375 Rational m = lhs[0].getRational()+1; 02376 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t: m = "+m.toString()); 02377 vector<Expr> kids; 02378 if(isPlus(eqn[1])) 02379 sumModM(kids, eqn[1], m, m); 02380 else 02381 kids.push_back(monomialModM(eqn[1], m, m)); 02382 02383 kids.push_back(multExpr(rat(1/m), x)); 02384 return plusExpr(kids); 02385 } 02386 02387 Expr 02388 ArithTheoremProducerOld::create_t2(const Expr& lhs, const Expr& rhs, 02389 const Expr& sigma) { 02390 Rational m = lhs[0].getRational()+1; 02391 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t2: m = "+m.toString()); 02392 vector<Expr> kids; 02393 if(isPlus(rhs)) 02394 sumModM(kids, rhs, m, -1); 02395 else { 02396 kids.push_back(rat(0)); // For canonical form 02397 Expr monom = monomialModM(rhs, m, -1); 02398 if(!monom.isRational()) 02399 kids.push_back(monom); 02400 else 02401 DebugAssert(monom.getRational() == 0, ""); 02402 } 02403 kids.push_back(rat(m)*sigma); 02404 return plusExpr(kids); 02405 } 02406 02407 Expr 02408 ArithTheoremProducerOld::create_t3(const Expr& lhs, const Expr& rhs, 02409 const Expr& sigma) { 02410 const Rational& a = lhs[0].getRational(); 02411 Rational m = a+1; 02412 DebugAssert(m > 0, "ArithTheoremProducerOld::create_t3: m = "+m.toString()); 02413 vector<Expr> kids; 02414 if(isPlus(rhs)) 02415 sumMulF(kids, rhs, m, 1); 02416 else { 02417 kids.push_back(rat(0)); // For canonical form 02418 Expr monom = monomialMulF(rhs, m, 1); 02419 if(!monom.isRational()) 02420 kids.push_back(monom); 02421 else 02422 DebugAssert(monom.getRational() == 0, ""); 02423 } 02424 kids.push_back(rat(-a)*sigma); 02425 return plusExpr(kids); 02426 } 02427 02428 Rational 02429 ArithTheoremProducerOld::modEq(const Rational& i, const Rational& m) { 02430 DebugAssert(m > 0, "ArithTheoremProducerOld::modEq: m = "+m.toString()); 02431 Rational half(1,2); 02432 Rational res((i - m*(floor((i/m) + half)))); 02433 TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, ""); 02434 return res; 02435 } 02436 02437 Rational 02438 ArithTheoremProducerOld::f(const Rational& i, const Rational& m) { 02439 DebugAssert(m > 0, "ArithTheoremProducerOld::f: m = "+m.toString()); 02440 Rational half(1,2); 02441 return (floor(i/m + half)+modEq(i,m)); 02442 } 02443 02444 void 02445 ArithTheoremProducerOld::sumModM(vector<Expr>& summands, const Expr& sum, 02446 const Rational& m, const Rational& divisor) { 02447 DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumModM: divisor = " 02448 +divisor.toString()); 02449 Expr::iterator i = sum.begin(); 02450 DebugAssert(i != sum.end(), CLASS_NAME "::sumModM"); 02451 Rational C = i->getRational(); 02452 C = modEq(C,m)/divisor; 02453 summands.push_back(rat(C)); 02454 i++; 02455 for(Expr::iterator iend=sum.end(); i!=iend; ++i) { 02456 Expr monom = monomialModM(*i, m, divisor); 02457 if(!monom.isRational()) 02458 summands.push_back(monom); 02459 else 02460 DebugAssert(monom.getRational() == 0, ""); 02461 } 02462 } 02463 02464 Expr 02465 ArithTheoremProducerOld::monomialModM(const Expr& i, 02466 const Rational& m, const Rational& divisor) 02467 { 02468 DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialModM: divisor = " 02469 +divisor.toString()); 02470 Expr res; 02471 if(isMult(i)) { 02472 Rational ai = i[0].getRational(); 02473 ai = modEq(ai,m)/divisor; 02474 if(0 == ai) res = rat(0); 02475 else if(1 == ai && i.arity() == 2) res = i[1]; 02476 else { 02477 vector<Expr> kids = i.getKids(); 02478 kids[0] = rat(ai); 02479 res = multExpr(kids); 02480 } 02481 } else { // It's a single variable 02482 Rational ai = modEq(1,m)/divisor; 02483 if(1 == ai) res = i; 02484 else res = rat(ai)*i; 02485 } 02486 DebugAssert(!res.isNull(), "ArithTheoremProducerOld::monomialModM()"); 02487 TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString() 02488 +", div="+divisor.toString()+") = ", res, ""); 02489 return res; 02490 } 02491 02492 void 02493 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands, const Expr& sum, 02494 const Rational& m, const Rational& divisor) { 02495 DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumMulF: divisor = " 02496 +divisor.toString()); 02497 Expr::iterator i = sum.begin(); 02498 DebugAssert(i != sum.end(), CLASS_NAME "::sumModM"); 02499 Rational C = i->getRational(); 02500 C = f(C,m)/divisor; 02501 summands.push_back(rat(C)); 02502 i++; 02503 for(Expr::iterator iend=sum.end(); i!=iend; ++i) { 02504 Expr monom = monomialMulF(*i, m, divisor); 02505 if(!monom.isRational()) 02506 summands.push_back(monom); 02507 else 02508 DebugAssert(monom.getRational() == 0, ""); 02509 } 02510 } 02511 02512 Expr 02513 ArithTheoremProducerOld::monomialMulF(const Expr& i, 02514 const Rational& m, const Rational& divisor) 02515 { 02516 DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialMulF: divisor = " 02517 +divisor.toString()); 02518 Rational ai = isMult(i) ? (i)[0].getRational() : 1; 02519 Expr xi = isMult(i) ? (i)[1] : (i); 02520 ai = f(ai,m)/divisor; 02521 if(0 == ai) return rat(0); 02522 if(1 == ai) return xi; 02523 return multExpr(rat(ai), xi); 02524 } 02525 02526 // This recursive function accepts a term, t, and a 'map' of 02527 // substitutions [x1/t1, x2/t2,...,xn/tn]. it returns a t' which is 02528 // basically t[x1/t1,x2/t2...xn/tn] 02529 Expr 02530 ArithTheoremProducerOld::substitute(const Expr& term, ExprMap<Expr>& eMap) 02531 { 02532 ExprMap<Expr>::iterator i, iend = eMap.end(); 02533 02534 i = eMap.find(term); 02535 if(iend != i) 02536 return (*i).second; 02537 02538 if (isMult(term)) { 02539 //in this case term is of the form c.x 02540 i = eMap.find(term[1]); 02541 if(iend != i) 02542 return term[0]*(*i).second; 02543 else 02544 return term; 02545 } 02546 02547 if(isPlus(term)) { 02548 vector<Expr> output; 02549 for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j) 02550 output.push_back(substitute(*j, eMap)); 02551 return plusExpr(output); 02552 } 02553 return term; 02554 } 02555 02556 bool ArithTheoremProducerOld::greaterthan(const Expr & l, const Expr & r) 02557 { 02558 // DebugAssert(l != r, ""); 02559 if (l==r) return false; 02560 02561 switch(l.getKind()) { 02562 case RATIONAL_EXPR: 02563 DebugAssert(!r.isRational(), ""); 02564 return true; 02565 break; 02566 case POW: 02567 switch (r.getKind()) { 02568 case RATIONAL_EXPR: 02569 // TODO: 02570 // alternately I could return (not greaterthan(r,l)) 02571 return false; 02572 break; 02573 case POW: 02574 // x^n > y^n if x > y 02575 // x^n1 > x^n2 if n1 > n2 02576 return 02577 ((r[1] < l[1]) || 02578 ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational()))); 02579 break; 02580 02581 case MULT: 02582 DebugAssert(r.arity() > 1, ""); 02583 DebugAssert((r.arity() > 2) || (r[1] != l), ""); 02584 if (r[1] == l) return false; 02585 return greaterthan(l, r[1]); 02586 break; 02587 case PLUS: 02588 DebugAssert(false, ""); 02589 return true; 02590 break; 02591 default: 02592 // leaf 02593 return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1)); 02594 break; 02595 } 02596 break; 02597 case MULT: 02598 DebugAssert(l.arity() > 1, ""); 02599 switch (r.getKind()) { 02600 case RATIONAL_EXPR: 02601 return false; 02602 break; 02603 case POW: 02604 DebugAssert(l.arity() > 1, ""); 02605 DebugAssert((l.arity() > 2) || (l[1] != r), ""); 02606 // TODO: 02607 // alternately return (not greaterthan(r,l) 02608 return ((l[1] == r) || greaterthan(l[1], r)); 02609 break; 02610 case MULT: 02611 { 02612 02613 DebugAssert(r.arity() > 1, ""); 02614 Expr::iterator i = l.begin(); 02615 Expr::iterator j = r.begin(); 02616 ++i; 02617 ++j; 02618 for (; i != l.end() && j != r.end(); ++i, ++j) { 02619 if (*i == *j) 02620 continue; 02621 return greaterthan(*i,*j); 02622 } 02623 DebugAssert(i != l.end() || j != r.end(), ""); 02624 if (i == l.end()) { 02625 // r is bigger 02626 return false; 02627 } 02628 else 02629 { 02630 // l is bigger 02631 return true; 02632 } 02633 } 02634 break; 02635 case PLUS: 02636 DebugAssert(false, ""); 02637 return true; 02638 break; 02639 default: 02640 // leaf 02641 DebugAssert((l.arity() > 2) || (l[1] != r), ""); 02642 return ((l[1] == r) || greaterthan(l[1], r)); 02643 break; 02644 } 02645 break; 02646 case PLUS: 02647 DebugAssert(false, ""); 02648 return true; 02649 break; 02650 default: 02651 // leaf 02652 switch (r.getKind()) { 02653 case RATIONAL_EXPR: 02654 return false; 02655 break; 02656 case POW: 02657 return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1))); 02658 break; 02659 case MULT: 02660 DebugAssert(r.arity() > 1, ""); 02661 DebugAssert((r.arity() > 2) || (r[1] != l), ""); 02662 if (l == r[1]) return false; 02663 return greaterthan(l,r[1]); 02664 break; 02665 case PLUS: 02666 DebugAssert(false, ""); 02667 return true; 02668 break; 02669 default: 02670 // leaf 02671 return (r < l); 02672 break; 02673 } 02674 break; 02675 } 02676 } 02677 02678 02679 /*! IS_INTEGER(x) |= EXISTS (y : INT) y = x 02680 * where x is not already known to be an integer. 02681 */ 02682 Theorem ArithTheoremProducerOld::IsIntegerElim(const Theorem& isIntx) 02683 { 02684 Expr expr = isIntx.getExpr(); 02685 if (CHECK_PROOFS) { 02686 CHECK_SOUND(expr.getKind() == IS_INTEGER, 02687 "Expected IS_INTEGER predicate"); 02688 } 02689 expr = expr[0]; 02690 DebugAssert(!d_theoryArith->isInteger(expr), "Expected non-integer"); 02691 02692 Assumptions a(isIntx); 02693 Proof pf; 02694 02695 if (withProof()) 02696 { 02697 pf = newPf("isIntElim", isIntx.getProof()); 02698 } 02699 02700 Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType()); 02701 Expr res = d_em->newClosureExpr(EXISTS, newVar, newVar.eqExpr(expr)); 02702 02703 return newTheorem(res, a, pf); 02704 } 02705 02706 02707 Theorem 02708 ArithTheoremProducerOld::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx, 02709 const vector<Theorem>& isIntVars) { 02710 TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {"); 02711 Proof pf; 02712 02713 if(CHECK_PROOFS) 02714 CHECK_SOUND(eqn.isRewrite(), 02715 "ArithTheoremProducerOld::eqElimInt: input must be an equation" + 02716 eqn.toString()); 02717 02718 const Expr& lhs = eqn.getLHS(); 02719 const Expr& rhs = eqn.getRHS(); 02720 Expr a, x; 02721 d_theoryArith->separateMonomial(lhs, a, x); 02722 02723 if(CHECK_PROOFS) { 02724 // Checking LHS 02725 const Expr& isIntxe = isIntx.getExpr(); 02726 CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x, 02727 "ArithTheoremProducerOld::eqElimInt\n eqn = " 02728 +eqn.getExpr().toString() 02729 +"\n isIntx = "+isIntxe.toString()); 02730 CHECK_SOUND(isRational(a) && a.getRational().isInteger() 02731 && a.getRational() >= 2, 02732 "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.toString()); 02733 // Checking RHS 02734 // It cannot be a division (we don't handle it) 02735 CHECK_SOUND(!isDivide(rhs), 02736 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString()); 02737 // If it's a single monomial, then it's the only "variable" 02738 if(!isPlus(rhs)) { 02739 Expr c, v; 02740 d_theoryArith->separateMonomial(rhs, c, v); 02741 CHECK_SOUND(isIntVars.size() == 1 02742 && isIntPred(isIntVars[0].getExpr()) 02743 && isIntVars[0].getExpr()[0] == v 02744 && isRational(c) && c.getRational().isInteger(), 02745 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString() 02746 +"isIntVars.size = "+int2string(isIntVars.size())); 02747 } else { // RHS is a plus 02748 CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(), 02749 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString()); 02750 // Check the free constant 02751 CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(), 02752 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString()); 02753 // Check the vars 02754 for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) { 02755 Expr c, v; 02756 d_theoryArith->separateMonomial(rhs[i+1], c, v); 02757 const Expr& isInt(isIntVars[i].getExpr()); 02758 CHECK_SOUND(isIntPred(isInt) && isInt[0] == v 02759 && isRational(c) && c.getRational().isInteger(), 02760 "ArithTheoremProducerOld::eqElimInt:\n rhs["+int2string(i+1) 02761 +"] = "+rhs[i+1].toString() 02762 +"\n isInt = "+isInt.toString()); 02763 } 02764 } 02765 } 02766 02767 // Creating a fresh bound variable 02768 static int varCount(0); 02769 Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++)); 02770 newVar.setType(intType()); 02771 Expr t2 = create_t2(lhs, rhs, newVar); 02772 Expr t3 = create_t3(lhs, rhs, newVar); 02773 vector<Expr> vars; 02774 vars.push_back(newVar); 02775 Expr res = d_em->newClosureExpr(EXISTS, vars, 02776 x.eqExpr(t2) && rat(0).eqExpr(t3)); 02777 02778 vector<Theorem> thms(isIntVars); 02779 thms.push_back(isIntx); 02780 thms.push_back(eqn); 02781 Assumptions assump(thms); 02782 02783 if(withProof()) { 02784 vector<Proof> pfs; 02785 pfs.push_back(eqn.getProof()); 02786 pfs.push_back(isIntx.getProof()); 02787 vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end(); 02788 for(; i!=iend; ++i) 02789 pfs.push_back(i->getProof()); 02790 pf = newPf("eq_elim_int", eqn.getExpr(), res, pfs); 02791 } 02792 02793 Theorem thm(newTheorem(res, assump, pf)); 02794 TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }"); 02795 return thm; 02796 } 02797 02798 02799 Theorem 02800 ArithTheoremProducerOld::isIntConst(const Expr& e) { 02801 Proof pf; 02802 02803 if(CHECK_PROOFS) { 02804 CHECK_SOUND(isIntPred(e) && e[0].isRational(), 02805 "ArithTheoremProducerOld::isIntConst(e = " 02806 +e.toString()+")"); 02807 } 02808 if(withProof()) 02809 pf = newPf("is_int_const", e); 02810 bool isInt = e[0].getRational().isInteger(); 02811 return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf); 02812 } 02813 02814 02815 Theorem 02816 ArithTheoremProducerOld::equalLeaves1(const Theorem& thm) 02817 { 02818 Proof pf; 02819 const Expr& e = thm.getRHS(); 02820 02821 if (CHECK_PROOFS) { 02822 CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR && 02823 e[1].getRational() == Rational(0) && 02824 e[0].getKind() == PLUS && 02825 e[0].arity() == 3 && 02826 e[0][0].getKind() == RATIONAL_EXPR && 02827 e[0][0].getRational() == Rational(0) && 02828 e[0][1].getKind() == MULT && 02829 e[0][1].arity() == 2 && 02830 e[0][1][0].getKind() == RATIONAL_EXPR && 02831 e[0][1][0].getRational() == Rational(-1), 02832 "equalLeaves1"); 02833 } 02834 if (withProof()) 02835 { 02836 vector<Proof> pfs; 02837 pfs.push_back(thm.getProof()); 02838 pf = newPf("equalLeaves1", e, pfs); 02839 } 02840 return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf); 02841 } 02842 02843 02844 Theorem 02845 ArithTheoremProducerOld::equalLeaves2(const Theorem& thm) 02846 { 02847 Proof pf; 02848 const Expr& e = thm.getRHS(); 02849 02850 if (CHECK_PROOFS) { 02851 CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR && 02852 e[0].getRational() == Rational(0) && 02853 e[1].getKind() == PLUS && 02854 e[1].arity() == 3 && 02855 e[1][0].getKind() == RATIONAL_EXPR && 02856 e[1][0].getRational() == Rational(0) && 02857 e[1][1].getKind() == MULT && 02858 e[1][1].arity() == 2 && 02859 e[1][1][0].getKind() == RATIONAL_EXPR && 02860 e[1][1][0].getRational() == Rational(-1), 02861 "equalLeaves2"); 02862 } 02863 if (withProof()) 02864 { 02865 vector<Proof> pfs; 02866 pfs.push_back(thm.getProof()); 02867 pf = newPf("equalLeaves2", e, pfs); 02868 } 02869 return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf); 02870 } 02871 02872 02873 Theorem 02874 ArithTheoremProducerOld::equalLeaves3(const Theorem& thm) 02875 { 02876 Proof pf; 02877 const Expr& e = thm.getRHS(); 02878 02879 if (CHECK_PROOFS) { 02880 CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR && 02881 e[1].getRational() == Rational(0) && 02882 e[0].getKind() == PLUS && 02883 e[0].arity() == 3 && 02884 e[0][0].getKind() == RATIONAL_EXPR && 02885 e[0][0].getRational() == Rational(0) && 02886 e[0][2].getKind() == MULT && 02887 e[0][2].arity() == 2 && 02888 e[0][2][0].getKind() == RATIONAL_EXPR && 02889 e[0][2][0].getRational() == Rational(-1), 02890 "equalLeaves3"); 02891 } 02892 if (withProof()) 02893 { 02894 vector<Proof> pfs; 02895 pfs.push_back(thm.getProof()); 02896 pf = newPf("equalLeaves3", e, pfs); 02897 } 02898 return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf); 02899 } 02900 02901 02902 Theorem 02903 ArithTheoremProducerOld::equalLeaves4(const Theorem& thm) 02904 { 02905 Proof pf; 02906 const Expr& e = thm.getRHS(); 02907 02908 if (CHECK_PROOFS) { 02909 CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR && 02910 e[0].getRational() == Rational(0) && 02911 e[1].getKind() == PLUS && 02912 e[1].arity() == 3 && 02913 e[1][0].getKind() == RATIONAL_EXPR && 02914 e[1][0].getRational() == Rational(0) && 02915 e[1][2].getKind() == MULT && 02916 e[1][2].arity() == 2 && 02917 e[1][2][0].getKind() == RATIONAL_EXPR && 02918 e[1][2][0].getRational() == Rational(-1), 02919 "equalLeaves4"); 02920 } 02921 if (withProof()) 02922 { 02923 vector<Proof> pfs; 02924 pfs.push_back(thm.getProof()); 02925 pf = newPf("equalLeaves4", e, pfs); 02926 } 02927 return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf); 02928 } 02929 02930 Theorem 02931 ArithTheoremProducerOld::diseqToIneq(const Theorem& diseq) { 02932 Proof pf; 02933 02934 const Expr& e = diseq.getExpr(); 02935 02936 if(CHECK_PROOFS) { 02937 CHECK_SOUND(e.isNot() && e[0].isEq(), 02938 "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n" 02939 " e = "+e.toString()); 02940 } 02941 02942 const Expr& x = e[0][0]; 02943 const Expr& y = e[0][1]; 02944 02945 if(withProof()) 02946 pf = newPf(e, diseq.getProof()); 02947 return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf); 02948 } 02949 02950 Theorem ArithTheoremProducerOld::dummyTheorem(const Expr& e) { 02951 Proof pf; 02952 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf); 02953 } 02954 02955 Theorem ArithTheoremProducerOld::oneElimination(const Expr& e) { 02956 02957 // Check soundness 02958 if (CHECK_PROOFS) 02959 CHECK_SOUND(isMult(e) && 02960 e.arity() == 2 && 02961 e[0].isRational() && 02962 e[0].getRational() == 1, 02963 "oneElimination: input must be a multiplication by one" + e.toString()); 02964 02965 // The proof object that we will us 02966 Proof pf; 02967 02968 // Setup the proof if needed 02969 if (withProof()) 02970 pf = newPf("oneElimination", e); 02971 02972 // Return the rewrite theorem that explains the phenomenon 02973 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf); 02974 } 02975 02976 Theorem ArithTheoremProducerOld::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) { 02977 02978 // Get the expressions 02979 const Expr& lowerBoundExpr = lowerBound.getExpr(); 02980 const Expr& upperBoundExpr = upperBound.getExpr(); 02981 02982 // Check soundness 02983 if (CHECK_PROOFS) { 02984 CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString()); 02985 CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString()); 02986 CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString()); 02987 CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString()); 02988 CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString()); 02989 02990 // Get the bounds 02991 Rational lowerBoundR = lowerBoundExpr[0].getRational(); 02992 Rational upperBoundR = upperBoundExpr[0].getRational(); 02993 02994 if (isLE(lowerBoundExpr) && isGE(upperBoundExpr)) { 02995 CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable"); 02996 } else { 02997 CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable"); 02998 } 02999 } 03000 03001 // The proof object that we will use 03002 Proof pf; 03003 // Setup the proof if needed 03004 if (withProof()) 03005 pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr); 03006 03007 // Put the bounds expressions in the assumptions 03008 Assumptions assumptions; 03009 assumptions.add(lowerBound); 03010 assumptions.add(upperBound); 03011 03012 // Return the theorem 03013 return newTheorem(d_em->falseExpr(), assumptions, pf); 03014 } 03015 03016 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) { 03017 03018 // Get the expressions of the theorem 03019 const Expr& expr1 = thm1.getExpr(); 03020 const Expr& expr2 = thm2.getExpr(); 03021 03022 // Check soundness 03023 if (CHECK_PROOFS) { 03024 03025 CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString()); 03026 CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString()); 03027 03028 if (isLE(expr1) || isLT(expr1)) 03029 CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString()); 03030 if (isGE(expr1) || isGT(expr1)) 03031 CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString()); 03032 } 03033 03034 // Create the assumptions 03035 Assumptions a(thm1, thm2); 03036 03037 // Get the kinds of the inequalitites 03038 int kind1 = expr1.getKind(); 03039 int kind2 = expr2.getKind(); 03040 03041 // Set-up the resulting inequality 03042 int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT; 03043 03044 // Create the proof object 03045 Proof pf; 03046 if(withProof()) { 03047 vector<Proof> pfs; 03048 pfs.push_back(thm1.getProof()); 03049 pfs.push_back(thm2.getProof()); 03050 pf = newPf("addInequalities", expr1, expr2, pfs); 03051 } 03052 03053 // Create the new expressions 03054 Expr leftSide = plusExpr(expr1[0], expr2[0]); 03055 Expr rightSide = plusExpr(expr1[1], expr2[1]); 03056 03057 // Return the theorem 03058 return newTheorem(Expr(kind, leftSide, rightSide), a, pf); 03059 } 03060 03061 // 03062 // 0 <= c1 + t 03063 // ==> 0 <= c2 + t 03064 // if c2 > c1 03065 Theorem ArithTheoremProducerOld::implyWeakerInequality(const Expr& expr1, const Expr& expr2) { 03066 03067 // Check soundness 03068 if (CHECK_PROOFS) { 03069 03070 // Both must be inequalitites 03071 CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString()); 03072 CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString()); 03073 03074 // Left sides must be zero 03075 CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString()); 03076 CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString()); 03077 03078 // Get the expr1 monomials and constant 0 <= c1 + t1 03079 Rational c1 = 0; 03080 vector<Expr> t1_children; 03081 if (isPlus(expr1[1])) { 03082 int start_i = 0; 03083 if (expr1[1][0].isRational()) { 03084 start_i = 1; 03085 c1 = expr1[1][0].getRational(); 03086 } 03087 int end_i = expr1[1].arity(); 03088 for(int i = start_i; i < end_i; i ++) { 03089 const Expr& term = expr1[1][i]; 03090 t1_children.push_back(term); 03091 } 03092 } else 03093 t1_children.push_back(expr1[1]); 03094 Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]); 03095 03096 // Get the expr1 monomials and constant 0 <= c1 + t1 03097 Rational c2 = 0; 03098 vector<Expr> t2_children; 03099 if (isPlus(expr2[1])) { 03100 int start_i = 0; 03101 if (expr2[1][0].isRational()) { 03102 start_i = 1; 03103 c2 = expr2[1][0].getRational(); 03104 } 03105 int end_i = expr2[1].arity(); 03106 for(int i = start_i; i < end_i; i ++) { 03107 const Expr& term = expr2[1][i]; 03108 t2_children.push_back(term); 03109 } 03110 } else 03111 t2_children.push_back(expr2[1]); 03112 Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]); 03113 03114 CHECK_SOUND(t2 == t1, "implyWeakerInequality: terms different " + t1.toString() + " vs " + t2.toString()); 03115 CHECK_SOUND(c2 > c1 || (c2 == c1 && !(expr1.getKind() == LE && expr2.getKind() == LT)), "implyWeakerInequality: c2 is not bigger than c1" + expr1.toString() + " --> " + expr2.toString()); 03116 } 03117 // Create the proof object 03118 Proof pf; 03119 if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2); 03120 03121 // Return the theorem 03122 return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf); 03123 } 03124 03125 // Takes 03126 // Expr1: 0 <= c1 + t1 03127 // Expr2: 0 <= c2 + t2 (t2 is -t1) 03128 // if c1 + c2 < 0 then Expr1 => !Expr2 03129 // 03130 03131 Theorem ArithTheoremProducerOld::implyNegatedInequality(const Expr& expr1, const Expr& expr2) { 03132 03133 // Check soundness 03134 // Check soundness 03135 if (CHECK_PROOFS) { 03136 03137 // Both must be inequalitites 03138 CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: expr1 should be an inequality" + expr1.toString()); 03139 CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: expr1 should be an inequality" + expr2.toString()); 03140 03141 // Left sides must be zero 03142 CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyNegatedInequality: expr1 should have a rational on the left side" + expr1.toString()); 03143 CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyNegatedInequality: expr2 should have a rational on the left side" + expr2.toString()); 03144 03145 // Get the expr1 monomials and constant 0 <= c1 + t1 03146 Rational c1 = 0; 03147 vector<Expr> t1_children; 03148 if (isPlus(expr1[1])) { 03149 int start_i = 0; 03150 if (expr1[1][0].isRational()) { 03151 start_i = 1; 03152 c1 = expr1[1][0].getRational(); 03153 } 03154 int end_i = expr1[1].arity(); 03155 for(int i = start_i; i < end_i; i ++) { 03156 const Expr& term = expr1[1][i]; 03157 t1_children.push_back(term); 03158 } 03159 } else 03160 t1_children.push_back(expr1[1]); 03161 Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]); 03162 03163 // Get the expr1 monomials and constant 0 <= c1 + t1 03164 Rational c2 = 0; 03165 vector<Expr> t2_children; 03166 if (isPlus(expr2[1])) { 03167 int start_i = 0; 03168 if (expr2[1][0].isRational()) { 03169 start_i = 1; 03170 c2 = expr2[1][0].getRational(); 03171 } 03172 int end_i = expr2[1].arity(); 03173 for(int i = start_i; i < end_i; i ++) { 03174 const Expr& term = expr2[1][i]; 03175 t2_children.push_back(term); 03176 } 03177 } else 03178 t2_children.push_back(expr2[1]); 03179 Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]); 03180 03181 // t1 shoud be -t2 03182 if (isPlus(t1) && isPlus(t2)) { 03183 CHECK_SOUND(t1.arity() == t2.arity(), "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString()); 03184 for (int i = 0; i < t1.arity(); i++) { 03185 Expr term_t1 = t1[i]; 03186 Expr term_t2 = t2[i]; 03187 Rational t1_c = (isMult(term_t1) ? term_t1[0].getRational() : 1); 03188 term_t1 = (isMult(term_t1) ? term_t1[1] : term_t1); 03189 Rational t2_c = (isMult(term_t2) ? term_t2[0].getRational() : 1); 03190 term_t2 = (isMult(term_t2) ? term_t2[1] : term_t2); 03191 CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString()); 03192 CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString()); 03193 } 03194 } else { 03195 Rational t1_c = (isMult(t1) ? t1[0].getRational() : 1); 03196 Expr term_t1 = (isMult(t1) ? t1[1] : t1); 03197 Rational t2_c = (isMult(t2) ? t2[0].getRational() : 1); 03198 Expr term_t2 = (isMult(t2) ? t2[1] : t2); 03199 CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString()); 03200 CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString()); 03201 } 03202 03203 int kind1 = expr1.getKind(); 03204 int kind2 = expr2.getKind(); 03205 bool bothStrict = kind1 == LT && kind2 == LT; 03206 CHECK_SOUND(c1 + c2 < 0 || (c1 + c2 == 0 && bothStrict), "implyNegatedInequality: sum of constants not negative!"); 03207 } 03208 03209 // The proof object that we will use 03210 Proof pf; 03211 if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2, expr2.negate()); 03212 03213 // Return the theorem 03214 return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf); 03215 } 03216 03217 Theorem ArithTheoremProducerOld::trustedRewrite(const Expr& expr1, const Expr& expr2) { 03218 03219 // The proof object that we will us 03220 Proof pf; 03221 03222 // Setup the proof if needed 03223 if (withProof()) pf = newPf("trustedRewrite", expr1, expr2); 03224 03225 // Return the rewrite theorem that explains the phenomenon 03226 return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf); 03227 03228 } 03229 03230 Theorem ArithTheoremProducerOld::integerSplit(const Expr& intVar, const Rational& intPoint) { 03231 03232 // Check soundness 03233 if (CHECK_PROOFS) { 03234 CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString()); 03235 } 03236 03237 // Create the expression 03238 const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1)))); 03239 03240 // The proof object that we will use 03241 Proof pf; 03242 if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint)); 03243 03244 // Return the theorem 03245 return newTheorem(split, Assumptions::emptyAssump(), pf); 03246 } 03247 03248 // 03249 // Changed from the new arithmetic, takes 03250 // 0 op c + t, where t is an integer expression but c is a rational 03251 // or 0 op x, where x is a leaf 03252 // 03253 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) { 03254 03255 // Check soundness 03256 if (CHECK_PROOFS) { 03257 // Right side of the constraint should correspond to the proved integer expression 03258 CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString()); 03259 CHECK_SOUND(constr[0].isRational() && constr[0].getRational() == 0, "rafineStrictInteger: left hand side must be 0"); 03260 CHECK_SOUND(d_theoryArith->isLeaf(constr[1]) || constr[1][0].isRational(), "rafineStrictInteger: right side of the constraint must be a leaf or a sum, with the first one a rational"); 03261 03262 // We have to check that the non-constant children of inequality correspond to the integrality theorem's children 03263 Expr intSum = isIntConstrThm.getExpr()[0]; 03264 Expr ineqSum = constr[1]; 03265 if (isPlus(intSum)) { 03266 int i, j; 03267 for (i = 0, j = 1; i < intSum.arity() && j < ineqSum.arity(); i ++, j ++) 03268 if (!(intSum[i] == ineqSum[j])) break; 03269 CHECK_SOUND(i == intSum.arity() && j == ineqSum.arity(), "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side"); 03270 } else 03271 CHECK_SOUND(intSum == ineqSum || intSum == ineqSum[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + ineqSum[1].getString()); 03272 } 03273 03274 // Get the contraint bound 03275 Rational c = (isPlus(constr[1]) ? constr[1][0].getRational() : 0); 03276 03277 // Get the kind of the constraint 03278 int kind = constr.getKind(); 03279 03280 // If the bound is strict, make it non-strict 03281 switch (kind) { 03282 case LT: 03283 kind = LE; 03284 if (c.isInteger()) c --; // 0 < 3 + x --> 0 <= 2 + x 03285 else c = floor(c); // 0 < 3.4 + x --> 0 <= 3 + x 03286 break; 03287 case LE: 03288 kind = LE; 03289 if (!c.isInteger()) c = floor(c); // 0 <= 3.5 + x --> 0 <= 3 + x 03290 break; 03291 case GT: 03292 kind = GE; 03293 if (c.isInteger()) c ++; // 0 > 3 + x --> 0 >= 4 + x 03294 else c = ceil(c); // 0 > 3.4 + x --> 0 >= 4 + x 03295 break; 03296 case GE: 03297 kind = GE; 03298 if (!c.isInteger()) c = ceil(c); // 0 >= 3.4 + x --> 4 >= x 03299 break; 03300 } 03301 03302 // The new constraint 03303 vector<Expr> newChildren; 03304 if (isPlus(constr[1])) { 03305 for (int i = 0; i < constr[1].arity(); i ++) 03306 if (constr[1][i].isRational()) newChildren.push_back(rat(c)); 03307 else newChildren.push_back(constr[1][i]); 03308 } else { 03309 if (c != 0) newChildren.push_back(rat(c)); 03310 newChildren.push_back(constr[1]); 03311 } 03312 Expr newSum = newChildren.size() > 1 ? plusExpr(newChildren) : newChildren[0]; 03313 Expr newConstr(kind, rat(0), newSum); 03314 03315 // Pick up the assumptions from the integer proof 03316 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); 03317 03318 // Construct the proof object if necessary 03319 Proof pf; 03320 if (withProof()) 03321 pf = newPf("rafineStrictInteger", constr,newConstr, isIntConstrThm.getProof()); 03322 03323 // Return the rewrite theorem that explains the phenomenon 03324 return newRWTheorem(constr, newConstr, assump, pf); 03325 } 03326 03327 03328 // Given: 03329 // 0 = c + t 03330 // where t is integer and c is not 03331 // deduce bot 03332 Theorem ArithTheoremProducerOld::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) { 03333 03334 // Check soundness 03335 if (CHECK_PROOFS) { 03336 // Right side of the constraint should correspond to the proved integer expression 03337 CHECK_SOUND(constr.getKind() == EQ, "intEqualityRationalConstant: expected a constraint got : " + constr.toString()); 03338 bool sum_on_rhs = (constr[0].isRational() && constr[0].getRational() == 0); 03339 bool sum_on_lhs = (constr[1].isRational() && constr[1].getRational() == 0); 03340 CHECK_SOUND((sum_on_rhs && !sum_on_lhs) ||(!sum_on_rhs && sum_on_lhs), 03341 "intEqualityRationalConstant: left or right hand side must be 0"); 03342 CHECK_SOUND((sum_on_rhs && constr[1][0].isRational() && !constr[1][0].getRational().isInteger()) || 03343 (sum_on_lhs && constr[0][0].isRational() && !constr[0][0].getRational().isInteger()), 03344 "intEqualityRationalConstant: left or right side of the constraint must be a sum, with the first one a rational (non integer)"); 03345 03346 // We have to check that the non-constant children of inequality correspond to the integrality theorem's children 03347 Expr intSum = isIntConstrThm.getExpr()[0]; 03348 Expr eqSum = (sum_on_lhs ? constr[0] : constr[1]); 03349 if (isPlus(intSum)) { 03350 int i, j; 03351 for (i = 0, j = 1; i < intSum.arity() && j < eqSum.arity(); i ++, j ++) 03352 if (!(intSum[i] == eqSum[j])) break; 03353 CHECK_SOUND(i == intSum.arity() && j == eqSum.arity(), "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side"); 03354 } else 03355 CHECK_SOUND(intSum == eqSum[1], "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + eqSum[1].getString()); 03356 } 03357 03358 const Assumptions& assump(isIntConstrThm.getAssumptionsRef()); 03359 03360 // Construct the proof object if necessary 03361 Proof pf; 03362 if (withProof()) 03363 pf = newPf("intEqualityRationalConstant", constr, isIntConstrThm.getProof()); 03364 03365 // Return the rewrite theorem that explains the phenomenon 03366 return newRWTheorem(constr, d_em->falseExpr(), assump, pf); 03367 } 03368 03369 Theorem ArithTheoremProducerOld::cycleConflict(const vector<Theorem>& inequalitites) { 03370 Proof pf; 03371 if(withProof()) { 03372 vector<Expr> es; 03373 vector<Proof> pfs; 03374 for(unsigned i = 0; i < inequalitites.size(); i++) { 03375 es.push_back(inequalitites[i].getExpr()); 03376 pfs.push_back(inequalitites[i].getProof()); 03377 } 03378 pf = newPf("cycleConflict", es, pfs); 03379 } 03380 03381 Assumptions a; 03382 for(unsigned i = 0; i < inequalitites.size(); i ++) 03383 a.add(inequalitites[i]); 03384 03385 return newTheorem(d_em->falseExpr(), a, pf); 03386 } 03387 03388 Theorem ArithTheoremProducerOld::implyEqualities(const std::vector<Theorem>& inequalities) { 03389 Assumptions a; 03390 vector<Expr> conjuncts; 03391 for(unsigned i = 0; i < inequalities.size(); i ++) { 03392 a.add(inequalities[i]); 03393 Expr inequality = inequalities[i].getExpr(); 03394 Expr equality = inequality[0].eqExpr(inequality[1]); 03395 conjuncts.push_back(equality); 03396 } 03397 03398 Proof pf; 03399 if(withProof()) { 03400 vector<Expr> es; 03401 vector<Proof> pfs; 03402 for(unsigned i = 0; i < inequalities.size(); i++) { 03403 es.push_back(inequalities[i].getExpr()); 03404 pfs.push_back(inequalities[i].getProof()); 03405 } 03406 pf = newPf("implyEqualities", Expr(RAW_LIST,conjuncts),Expr(RAW_LIST,es), pfs); 03407 } 03408 03409 return newTheorem(andExpr(conjuncts), a, pf); 03410 } 03411 03412 /*! Takes a Theorem(\\alpha < \\beta) and returns 03413 * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1) 03414 * where \\alpha and \\beta are integer expressions 03415 */ 03416 Theorem ArithTheoremProducerOld::lessThanToLERewrite(const Expr& ineq, 03417 const Theorem& isIntLHS, 03418 const Theorem& isIntRHS, 03419 bool changeRight) { 03420 03421 const Expr& isIntLHSexpr = isIntLHS.getExpr(); 03422 const Expr& isIntRHSexpr = isIntRHS.getExpr(); 03423 03424 if(CHECK_PROOFS) { 03425 CHECK_SOUND(isLT(ineq), "ArithTheoremProducerOld::LTtoLE: ineq must be <"); 03426 // Integrality check 03427 CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0], 03428 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n" 03429 " ineq = "+ineq.toString()+"\n isIntLHS = " 03430 +isIntLHSexpr.toString()); 03431 CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1], 03432 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n" 03433 " ineq = "+ineq.toString()+"\n isIntRHS = " 03434 +isIntRHSexpr.toString()); 03435 } 03436 03437 vector<Theorem> thms; 03438 thms.push_back(isIntLHS); 03439 thms.push_back(isIntRHS); 03440 Assumptions a(thms); 03441 Proof pf; 03442 Expr le = changeRight? leExpr(ineq[0], ineq[1] + rat(-1)) : leExpr(ineq[0] + rat(1), ineq[1]); 03443 if(withProof()) { 03444 vector<Proof> pfs; 03445 pfs.push_back(isIntLHS.getProof()); 03446 pfs.push_back(isIntRHS.getProof()); 03447 pf = newPf(changeRight? "lessThan_To_LE_rhs_rwr" : "lessThan_To_LE_lhs_rwr", ineq, le, pfs); 03448 } 03449 03450 return newRWTheorem(ineq, le, a, pf); 03451 } 03452 03453 // G ==> (G1 or G2) and (!G1 or !G2), 03454 // where G = G(x, e, c1, c2), 03455 // V x = e + i, for i in c1 .. c2 03456 Theorem ArithTheoremProducerOld::splitGrayShadowSmall(const Theorem& gThm) { 03457 const Expr& theShadow = gThm.getExpr(); 03458 if(CHECK_PROOFS) { 03459 CHECK_SOUND(isGrayShadow(theShadow), 03460 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" + 03461 theShadow.toString()); 03462 } 03463 03464 const Rational& c1 = theShadow[2].getRational(); 03465 const Rational& c2 = theShadow[3].getRational(); 03466 03467 if(CHECK_PROOFS) { 03468 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2, 03469 "ArithTheoremProducerOld::expandGrayShadow: " + 03470 theShadow.toString()); 03471 } 03472 03473 const Expr& v = theShadow[0]; 03474 const Expr& e = theShadow[1]; 03475 03476 vector<Expr> disjuncts; 03477 for (int i = c1.getInt(); i <= c2.getInt(); i ++) { 03478 Expr disjunct = v.eqExpr(e + rat(i)); 03479 disjuncts.push_back(disjunct); 03480 } 03481 Expr bigOr = orExpr(disjuncts); 03482 03483 Proof pf; 03484 if(withProof()){ 03485 vector<Expr> exprs; 03486 exprs.push_back(theShadow); 03487 exprs.push_back(bigOr); 03488 pf = newPf("split_gray_shadow", exprs, gThm.getProof()); 03489 } 03490 03491 return newTheorem(bigOr, gThm.getAssumptionsRef(), pf); 03492 } 03493 03494 Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) { 03495 Proof pf; 03496 03497 if(withProof()) { 03498 vector<Expr> es; 03499 vector<Proof> pfs; 03500 for(unsigned i = 0; i < antecedentThms.size(); i++) { 03501 es.push_back(antecedentThms[i].getExpr()); 03502 pfs.push_back(antecedentThms[i].getProof()); 03503 } 03504 pf = newPf("implyWeakerInequalityDiffLogic", implied, Expr(RAW_LIST,es), pfs); 03505 } 03506 03507 Assumptions a; 03508 for(unsigned i = 0; i < antecedentThms.size(); i ++) { 03509 a.add(antecedentThms[i]); 03510 } 03511 03512 return newTheorem(implied, a, pf); 03513 03514 } 03515 03516 Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) { 03517 Proof pf; 03518 03519 if(withProof()) { 03520 vector<Expr> es; 03521 vector<Proof> pfs; 03522 for(unsigned i = 0; i < antecedentThms.size(); i++) { 03523 es.push_back(antecedentThms[i].getExpr()); 03524 pfs.push_back(antecedentThms[i].getProof()); 03525 } 03526 pf = newPf("implyNegatedInequalityDiffLogic",implied.notExpr(), Expr(RAW_LIST, es), pfs); 03527 } 03528 03529 Assumptions a; 03530 for(unsigned i = 0; i < antecedentThms.size(); i ++) { 03531 a.add(antecedentThms[i]); 03532 } 03533 03534 return newTheorem(implied.notExpr(), a, pf); 03535 03536 } 03537 03538 03539 Theorem ArithTheoremProducerOld::expandGrayShadowRewrite(const Expr& theShadow) { 03540 03541 if(CHECK_PROOFS) { 03542 CHECK_SOUND(isGrayShadow(theShadow), 03543 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" + 03544 theShadow.toString()); 03545 } 03546 03547 const Rational& c1 = theShadow[2].getRational(); 03548 const Rational& c2 = theShadow[3].getRational(); 03549 03550 if(CHECK_PROOFS) { 03551 CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2, 03552 "ArithTheoremProducerOld::expandGrayShadow: " + 03553 theShadow.toString()); 03554 } 03555 03556 const Expr& v = theShadow[0]; 03557 const Expr& e = theShadow[1]; 03558 03559 Proof pf; 03560 if(withProof()) 03561 pf = newPf("expand_gray_shadow", theShadow); 03562 Expr ineq1(leExpr(e+rat(c1), v)); 03563 Expr ineq2(leExpr(v, e+rat(c2))); 03564 return newRWTheorem(theShadow, ineq1 && ineq2, Assumptions::emptyAssump(), pf); 03565 } 03566 03567 Theorem ArithTheoremProducerOld::compactNonLinearTerm(const Expr& nonLinear) { 03568 03569 // The set of common leaves 03570 multiset<Expr> commonLeaves; 03571 bool first = true; 03572 03573 // Go through the terms and intersect the leaf sets 03574 for (int i = 0; i < nonLinear.arity(); i ++) { 03575 if (!nonLinear[i].isRational()) { 03576 // Get the current monomial 03577 Expr monomial = nonLinear[i]; 03578 03579 // A set to keep the variables 03580 multiset<Expr> currentLeaves; 03581 03582 // Get the set of leaves in this term 03583 if (isMult(monomial)) { 03584 for (int j = 0; j < monomial.arity(); j ++) 03585 if (!monomial[j].isRational()) { 03586 if (isPow(monomial[j])) { 03587 for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++) 03588 currentLeaves.insert(monomial[j][1]); 03589 } else 03590 currentLeaves.insert(monomial[j]); 03591 } 03592 } else if (isPow(monomial)) { 03593 for (int p = 0; p < monomial[0].getRational().getInt(); p ++) 03594 currentLeaves.insert(monomial[1]); 03595 } else 03596 currentLeaves.insert(monomial); 03597 03598 // And intersect them 03599 if (first) { 03600 commonLeaves.swap(currentLeaves); 03601 first = false; 03602 } else { 03603 multiset<Expr> intersectLeaves; 03604 set_intersection(currentLeaves.begin(), currentLeaves.end(), 03605 commonLeaves.begin(), commonLeaves.end(), 03606 insert_iterator< multiset<Expr> > 03607 (intersectLeaves, intersectLeaves.begin())); 03608 intersectLeaves.swap(commonLeaves); 03609 } 03610 } 03611 } 03612 03613 Expr result; 03614 if (commonLeaves.size() > 0) { 03615 03616 // The constant to add in the beginnings 03617 Expr constant = rat(0); 03618 03619 // The sum of of the rest when we pullout the common factors 03620 vector<Expr> sumChildren; 03621 03622 // Go through them again and construct the sum of the rest 03623 for (int i = 0; i < nonLinear.arity(); i ++) { 03624 if (!nonLinear[i].isRational()) { 03625 // Get the current monomial 03626 Expr monomial = nonLinear[i]; 03627 03628 // A set to keep the variables 03629 multiset<Expr> currentChildren; 03630 03631 // Get the set of childrent of this multiplication 03632 if (isMult(monomial)) { 03633 for (int j = 0; j < monomial.arity(); j ++) 03634 if (isPow(monomial[j])) { 03635 for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++) 03636 currentChildren.insert(monomial[j][1]); 03637 } else 03638 currentChildren.insert(monomial[j]); 03639 } else if (isPow(monomial)) { 03640 for (int p = 0; p < monomial[0].getRational().getInt(); p ++) 03641 currentChildren.insert(monomial[1]); 03642 } else 03643 currentChildren.insert(monomial); 03644 03645 // Take the difference and construct a multiplication 03646 multiset<Expr> diffChildren; 03647 set_difference(currentChildren.begin(), currentChildren.end(), 03648 commonLeaves.begin(), commonLeaves.end(), 03649 insert_iterator< multiset<Expr> > 03650 (diffChildren, diffChildren.begin())); 03651 03652 // Go create another sumChildren element 03653 if (diffChildren.size() == 1) { 03654 sumChildren.push_back(*diffChildren.begin()); 03655 } else if (diffChildren.size() == 0) { 03656 sumChildren.push_back(rat(1)); 03657 } else { 03658 multiset<Expr>::iterator it = diffChildren.begin(); 03659 multiset<Expr>::iterator it_end = diffChildren.end(); 03660 vector<Expr> multChildren; 03661 while (it != it_end) { 03662 multChildren.push_back(*it); 03663 it ++; 03664 } 03665 sumChildren.push_back(multExpr(multChildren)); 03666 } 03667 } else 03668 constant = nonLinear[i]; 03669 } 03670 03671 // The children of the final multiplication 03672 vector<Expr> multChildren; 03673 multChildren.push_back(plusExpr(sumChildren)); 03674 multiset<Expr>::iterator it = commonLeaves.begin(); 03675 multiset<Expr>::iterator it_end = commonLeaves.end(); 03676 for (; it != it_end; it ++) 03677 multChildren.push_back(*it); 03678 result = plusExpr(constant, multExpr(multChildren)); 03679 } else { 03680 // We have no common leaves to take out 03681 result = nonLinear; 03682 } 03683 03684 Proof pf; 03685 if(withProof()) 03686 pf = newPf("compactNonlinear", nonLinear, result); 03687 03688 return newRWTheorem(nonLinear, result, Assumptions::emptyAssump(), pf); 03689 } 03690 03691 // 03692 // -c <= x1*x2*...*xn 03693 // if c = 0 then "only even number of x_i's can be negative" or one of them is zero 03694 // x1 = 0 or x2 = 0 or ... or xn = 0 03695 // or (x1 03696 // else "only only even number of x_i's can be negative" and none of them is zero" 03697 Theorem ArithTheoremProducerOld::nonLinearIneqSignSplit(const Theorem& ineqThm) { 03698 03699 // Get the inequality 03700 Expr ineq = ineqThm.getExpr(); 03701 Expr rhs = ineq[1]; 03702 03703 // Get the constant 03704 Rational c = (isMult(rhs) ? 0 : rhs[0].getRational()); 03705 if(CHECK_PROOFS) { 03706 CHECK_SOUND(c <= 0, "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString()); 03707 CHECK_SOUND(isMult(rhs) || (isPlus(rhs) && rhs.arity() == 2), "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString()); 03708 } 03709 03710 Expr signXor = d_em->trueExpr(); 03711 Expr mult = (isMult(rhs) ? rhs : rhs[1]); 03712 for (int i = 0; i < mult.arity(); i ++) { 03713 Expr term = mult[i]; 03714 if (isPow(term) && term[0].getRational() < 0) 03715 term = Expr(POW, -term[0], term[1]); 03716 signXor = Expr(XOR, signXor, ltExpr(term, rat(0))); 03717 } 03718 03719 if (c == 0 && ineq.getKind() == LE) { 03720 Expr zeroOr = d_em->falseExpr(); 03721 for (int i = 0; i < mult.arity(); i ++) { 03722 Expr term = mult[i]; 03723 zeroOr = zeroOr.orExpr(term.eqExpr(rat(0))); 03724 } 03725 signXor = zeroOr.orExpr(signXor); 03726 } 03727 03728 Proof pf; 03729 if(withProof()) { 03730 vector<Expr> exprs; 03731 exprs.push_back(ineq); 03732 exprs.push_back(signXor); 03733 pf = newPf("nonLinearIneqSignSplit", exprs, ineqThm.getProof()); 03734 } 03735 03736 Assumptions assumptions; 03737 assumptions.add(ineqThm); 03738 03739 return newTheorem(signXor, assumptions, pf); 03740 } 03741 03742 Theorem ArithTheoremProducerOld::implyDiffLogicBothBounds(const Expr& x, 03743 std::vector<Theorem>& c1_le_x, Rational c1, 03744 std::vector<Theorem>& x_le_c2, Rational c2) 03745 { 03746 Proof pf; 03747 03748 if(withProof()) { 03749 vector<Expr> es; 03750 vector<Proof> pfs; 03751 for(unsigned i = 0; i < c1_le_x.size(); i++) { 03752 es.push_back(c1_le_x[i].getExpr()); 03753 pfs.push_back(c1_le_x[i].getProof()); 03754 } 03755 for(unsigned i = 0; i < x_le_c2.size(); i++) { 03756 es.push_back(x_le_c2[i].getExpr()); 03757 pfs.push_back(x_le_c2[i].getProof()); 03758 } 03759 pf = newPf("implyDiffLogicBothBounds", es, pfs); 03760 } 03761 03762 Assumptions a; 03763 for(unsigned i = 0; i < x_le_c2.size(); i ++) { 03764 a.add(c1_le_x[i]); 03765 } 03766 for(unsigned i = 0; i < x_le_c2.size(); i ++) { 03767 a.add(c1_le_x[i]); 03768 } 03769 03770 Expr implied = grayShadow(x, rat(0), c1, c2); 03771 03772 return newTheorem(implied, a, pf); 03773 } 03774 03775 Theorem ArithTheoremProducerOld::addInequalities(const vector<Theorem>& thms) { 03776 03777 // Check soundness 03778 if (CHECK_PROOFS) { 03779 for (unsigned i = 0; i < thms.size(); i ++) { 03780 Expr expr = thms[i].getExpr(); 03781 CHECK_SOUND(isIneq(expr), "addInequalities: expecting an inequality for, got " + expr.toString()); 03782 CHECK_SOUND(isLE(expr) || isLT(expr), "addInequalities: expr should be <(=) " + expr.toString()); 03783 } 03784 } 03785 03786 // Create the assumptions 03787 Assumptions a; 03788 for (unsigned i = 0; i < thms.size(); i ++) 03789 a.add(thms[i]); 03790 03791 // Get the kinds of the inequalitites 03792 int kind = LE; 03793 for (unsigned i = 0; i < thms.size(); i ++) 03794 if (thms[i].getExpr().getKind() == LT) kind = LT; 03795 03796 // Create the proof object 03797 Proof pf; 03798 if(withProof()) { 03799 vector<Proof> pfs; 03800 vector<Expr> exps; 03801 for (unsigned i = 0; i < thms.size(); i ++) { 03802 pfs.push_back(thms[i].getProof()); 03803 exps.push_back(thms[i].getExpr()); 03804 } 03805 pf = newPf("addInequalities", exps, pfs); 03806 } 03807 03808 // Create the new expressions 03809 vector<Expr> summandsLeft; 03810 vector<Expr> summandsRight; 03811 for (unsigned i = 0; i < thms.size(); i ++) { 03812 summandsLeft.push_back(thms[i].getExpr()[0]); 03813 summandsRight.push_back(thms[i].getExpr()[1]); 03814 } 03815 Expr leftSide = plusExpr(summandsLeft); 03816 Expr rightSide = plusExpr(summandsRight); 03817 03818 // Return the theorem 03819 return newTheorem(Expr(kind, leftSide, rightSide), a, pf); 03820 } 03821 03822 // x^1 <-> x 03823 Theorem ArithTheoremProducerOld::powerOfOne(const Expr& e) { 03824 03825 if(CHECK_PROOFS) { 03826 CHECK_SOUND(isPow(e), "ArithTheoremProducerOld::powerOfOne: not a power expression" + e.toString()); 03827 CHECK_SOUND(e[0].isRational() && e[0].getRational() == 1, "ArithTheoremProducerOld::powerOfOne: not a power of 1" + e.toString()); 03828 } 03829 03830 Proof pf; 03831 if(withProof()) 03832 pf = newPf("power_of_one", e); 03833 03834 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf); 03835 } 03836 03837 03838 void ArithTheoremProducerOld::getLeaves(const Expr& e, set<Rational>& s, ExprHashMap<bool>& cache) 03839 { 03840 if (e.isRational()) { 03841 s.insert(e.getRational()); 03842 return; 03843 } 03844 03845 if (e.isAtomic() && d_theoryArith->isLeaf(e)) { 03846 return; 03847 } 03848 03849 ExprHashMap<bool>::iterator it = cache.find(e); 03850 if (it != cache.end()) return; 03851 03852 cache[e] = true; 03853 03854 DebugAssert(e.arity() > 0, "Expected non-zero arity"); 03855 int k = 0; 03856 03857 if (e.isITE()) { 03858 k = 1; 03859 } 03860 03861 for (; k < e.arity(); ++k) { 03862 getLeaves(e[k], s, cache); 03863 } 03864 } 03865 03866 03867 Theorem ArithTheoremProducerOld::rewriteLeavesConst(const Expr& e) 03868 { 03869 DebugAssert(e.isPropAtom() && d_theoryArith->leavesAreNumConst(e), 03870 "invariant violated"); 03871 DebugAssert(e.getKind() == EQ || e.getKind() == LT || e.getKind() == LE || e.getKind() == GT || e.getKind() == GE, 03872 "Unexpected kind"); 03873 set<Rational> lhs, rhs; 03874 ExprHashMap<bool> cache; 03875 getLeaves(e[0], lhs, cache); 03876 03877 cache.clear(); 03878 getLeaves(e[1], rhs, cache); 03879 03880 Expr res; 03881 switch (e.getKind()) { 03882 case EQ: { 03883 set<Rational> common; 03884 set_intersection(lhs.begin(), lhs.end(), rhs.begin(), rhs.end(), 03885 inserter(common, common.begin())); 03886 if (common.empty()) { 03887 res = d_em->falseExpr(); 03888 } 03889 break; 03890 } 03891 case LT: { 03892 set<Rational>::iterator it; 03893 it = lhs.end(); 03894 --it; 03895 if ((*it) < (*(rhs.begin()))) { 03896 res = d_em->trueExpr(); 03897 } else { 03898 it = rhs.end(); 03899 --it; 03900 if ((*it) <= (*(lhs.begin()))) { 03901 res = d_em->falseExpr(); 03902 } 03903 } 03904 break; 03905 } 03906 case LE: { 03907 set<Rational>::iterator it; 03908 it = lhs.end(); 03909 --it; 03910 if ((*it) <= (*(rhs.begin()))) { 03911 res = d_em->trueExpr(); 03912 } 03913 else { 03914 it = rhs.end(); 03915 --it; 03916 if ((*it) < (*(lhs.begin()))) { 03917 res = d_em->falseExpr(); 03918 break; 03919 } 03920 } 03921 break; 03922 } 03923 case GT: { 03924 set<Rational>::iterator it; 03925 it = lhs.end(); 03926 --it; 03927 if ((*it) > (*(rhs.begin()))) { 03928 res = d_em->trueExpr(); 03929 } else { 03930 it = rhs.end(); 03931 --it; 03932 if ((*it) >= (*(lhs.begin()))) { 03933 res = d_em->falseExpr(); 03934 } 03935 } 03936 break; 03937 } 03938 case GE: { 03939 set<Rational>::iterator it; 03940 it = lhs.end(); 03941 --it; 03942 if ((*it) >= (*(rhs.begin()))) { 03943 res = d_em->trueExpr(); 03944 } 03945 else { 03946 it = rhs.end(); 03947 --it; 03948 if ((*it) > (*(lhs.begin()))) { 03949 res = d_em->falseExpr(); 03950 break; 03951 } 03952 } 03953 break; 03954 } 03955 default: 03956 break; 03957 } 03958 if (res.isNull()) return d_theoryArith->reflexivityRule(e); 03959 else { 03960 Proof pf; 03961 if(withProof()) 03962 pf = newPf("rewrite_leaves_const", e); 03963 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf); 03964 } 03965 }