CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_arith_old.cpp 00004 * 00005 * Author: Clark Barrett, Vijay Ganesh. 00006 * 00007 * Created: Fri Jan 17 18:39:18 2003 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 00021 00022 #include "theory_arith_old.h" 00023 #include "arith_proof_rules.h" 00024 //#include "arith_expr.h" 00025 #include "arith_exception.h" 00026 #include "typecheck_exception.h" 00027 #include "eval_exception.h" 00028 #include "parser_exception.h" 00029 #include "smtlib_exception.h" 00030 #include "theory_core.h" 00031 #include "command_line_flags.h" 00032 //TODO: remove this dependency 00033 #include "../theory_core/core_proof_rules.h" 00034 00035 00036 using namespace std; 00037 using namespace CVC3; 00038 00039 00040 /////////////////////////////////////////////////////////////////////////////// 00041 // TheoryArithOld::FreeConst Methods // 00042 /////////////////////////////////////////////////////////////////////////////// 00043 00044 namespace CVC3 { 00045 00046 ostream& operator<<(ostream& os, const TheoryArithOld::FreeConst& fc) { 00047 os << "FreeConst(r=" << fc.getConst() << ", " 00048 << (fc.strict()? "strict" : "non-strict") << ")"; 00049 return os; 00050 } 00051 00052 /////////////////////////////////////////////////////////////////////////////// 00053 // TheoryArithOld::Ineq Methods // 00054 /////////////////////////////////////////////////////////////////////////////// 00055 00056 ostream& operator<<(ostream& os, const TheoryArithOld::Ineq& ineq) { 00057 os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on " 00058 << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = " 00059 << ineq.getConst() << ")"; 00060 return os; 00061 } 00062 } // End of namespace CVC3 00063 00064 00065 /////////////////////////////////////////////////////////////////////////////// 00066 // TheoryArithOld Private Methods // 00067 /////////////////////////////////////////////////////////////////////////////// 00068 00069 00070 Theorem TheoryArithOld::isIntegerThm(const Expr& e) { 00071 // Quick checks 00072 Type t = e.getType(); 00073 if (isReal(t)) return Theorem(); 00074 if (isInt(t)) return typePred(e); 00075 00076 // Try harder 00077 return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e)); 00078 } 00079 00080 00081 Theorem TheoryArithOld::isIntegerDerive(const Expr& isIntE, const Theorem& thm) { 00082 const Expr& e = thm.getExpr(); 00083 // We found it! 00084 if(e == isIntE) return thm; 00085 00086 Theorem res; 00087 // If the theorem is an AND, look inside each child 00088 if(e.isAnd()) { 00089 int i, iend=e.arity(); 00090 for(i=0; i<iend; ++i) { 00091 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i)); 00092 if(!res.isNull()) return res; 00093 } 00094 } 00095 return res; 00096 } 00097 00098 const Rational& TheoryArithOld::freeConstIneq(const Expr& ineq, bool varOnRHS) { 00099 DebugAssert(isIneq(ineq), "TheoryArithOld::freeConstIneq("+ineq.toString()+")"); 00100 const Expr& e = varOnRHS? ineq[0] : ineq[1]; 00101 00102 switch(e.getKind()) { 00103 case PLUS: 00104 return e[0].getRational(); 00105 case RATIONAL_EXPR: 00106 return e.getRational(); 00107 default: { // MULT, DIV, or Variable 00108 static Rational zero(0); 00109 return zero; 00110 } 00111 } 00112 } 00113 00114 00115 const TheoryArithOld::FreeConst& 00116 TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS, 00117 bool& subsumed) { 00118 TRACE("arith ineq", "TheoryArithOld::updateSubsumptionDB(", ineq, 00119 ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")"); 00120 DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArithOld::updateSubsumptionDB(" 00121 +ineq.toString()+")"); 00122 // Indexing expression: same as ineq only without the free const 00123 Expr index; 00124 const Expr& t = varOnRHS? ineq[0] : ineq[1]; 00125 bool strict(isLT(ineq)); 00126 Rational c(0); 00127 if(isPlus(t)) { 00128 DebugAssert(t.arity() >= 2, "TheoryArithOld::updateSubsumptionDB(" 00129 +ineq.toString()+")"); 00130 c = t[0].getRational(); // Extract the free const in ineq 00131 Expr newT; 00132 if(t.arity() == 2) { 00133 newT = t[1]; 00134 } else { 00135 vector<Expr> kids; 00136 Expr::iterator i=t.begin(), iend=t.end(); 00137 kids.push_back(rat(0)); 00138 for(++i; i!=iend; ++i) kids.push_back(*i); 00139 DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size()) 00140 +", ineq = "+ineq.toString()); 00141 newT = plusExpr(kids); 00142 } 00143 if(varOnRHS) 00144 index = leExpr(rat(0), canonSimplify(ineq[1] - newT).getRHS()); 00145 else 00146 index = leExpr(canonSimplify(ineq[0]-newT).getRHS(), rat(0)); 00147 } else if(isRational(t)) { 00148 c = t.getRational(); 00149 if(varOnRHS) 00150 index = leExpr(rat(0), ineq[1]); 00151 else 00152 index = leExpr(ineq[0], rat(0)); 00153 } else if(isLT(ineq)) 00154 index = leExpr(ineq[0], ineq[1]); 00155 else 00156 index = ineq; 00157 // Now update the database, check for subsumption, and extract the constant 00158 CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index), 00159 iend=d_freeConstDB.end(); 00160 if(i == iend) { 00161 subsumed = false; 00162 // Create a new entry 00163 CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index]; 00164 obj = FreeConst(c,strict); 00165 TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, ""); 00166 return obj.get(); 00167 } else { 00168 CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index]; 00169 const FreeConst& fc = obj.get(); 00170 if(varOnRHS) { 00171 subsumed = (c < fc.getConst() || 00172 (c == fc.getConst() && (!strict || fc.strict()))); 00173 } else { 00174 subsumed = (c > fc.getConst() || 00175 (c == fc.getConst() && (strict || !fc.strict()))); 00176 } 00177 if(!subsumed) { 00178 obj = FreeConst(c,strict); 00179 TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, ""); 00180 } 00181 return obj.get(); 00182 } 00183 } 00184 00185 00186 bool TheoryArithOld::kidsCanonical(const Expr& e) { 00187 if(isLeaf(e)) return true; 00188 bool res(true); 00189 for(int i=0; res && i<e.arity(); ++i) { 00190 Expr simp(canon(e[i]).getRHS()); 00191 res = (e[i] == simp); 00192 IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i] 00193 << "\nsimplified = " << simp << endl;) 00194 } 00195 return res; 00196 } 00197 00198 00199 /////////////////////////////////////////////////////////////////////////////// 00200 // // 00201 // Function: TheoryArithOld::canon // 00202 // Author: Clark Barrett, Vijay Ganesh. // 00203 // Created: Sat Feb 8 14:46:32 2003 // 00204 // Description: Compute a canonical form for expression e and return a // 00205 // theorem that e is equal to its canonical form. // 00206 // Note that canonical form for arith expressions is one of the following: // 00207 // 1. rational constant // 00208 // 2. arithmetic leaf // 00209 // (i.e. variable or term from some other theory) // 00210 // 3. (MULT rat leaf) // 00211 // where rat is a non-zero rational constant, leaf is an arithmetic leaf // 00212 // 4. (PLUS const term_0 term_1 ... term_n) // 00213 // where each term_i is either a leaf or (MULT rat leaf) // 00214 // and each leaf in term_i must be strictly greater than the leaf in // 00215 // term_{i+1}. // 00216 // // 00217 /////////////////////////////////////////////////////////////////////////////// 00218 Theorem TheoryArithOld::canon(const Expr& e) 00219 { 00220 TRACE("arith canon","canon(",e,") {"); 00221 DebugAssert(kidsCanonical(e), "TheoryArithOld::canon("+e.toString()+")"); 00222 Theorem result; 00223 switch (e.getKind()) { 00224 case UMINUS: { 00225 Theorem thm = d_rules->uMinusToMult(e[0]); 00226 Expr e2 = thm.getRHS(); 00227 result = transitivityRule(thm, canon(e2)); 00228 } 00229 break; 00230 case PLUS: /* { 00231 Theorem plusThm, plusThm1; 00232 plusThm = d_rules->canonFlattenSum(e); 00233 plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS()); 00234 result = transitivityRule(plusThm,plusThm1); 00235 } 00236 */ 00237 result = d_rules->canonPlus(e); 00238 break; 00239 case MINUS: { 00240 DebugAssert(e.arity() == 2,""); 00241 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]); 00242 // this produces e0 + (-1)*e1; we have to canonize it in 2 steps 00243 Expr sum(minus_eq_sum.getRHS()); 00244 Theorem thm(canon(sum[1])); 00245 if(thm.getLHS() == thm.getRHS()) 00246 result = canonThm(minus_eq_sum); 00247 // The sum changed; do the work 00248 else { 00249 vector<unsigned> changed; 00250 vector<Theorem> thms; 00251 changed.push_back(1); 00252 thms.push_back(thm); 00253 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms)); 00254 result = transitivityRule(minus_eq_sum, sum_eq_canon); 00255 } 00256 break; 00257 } 00258 00259 case MULT: 00260 result = d_rules->canonMult(e); 00261 break; 00262 /* 00263 case MULT: { 00264 Theorem thmMult, thmMult1; 00265 Expr exprMult; 00266 Expr e0 = e[0]; 00267 Expr e1 = e[1]; 00268 if(e0.isRational()) { 00269 if(rat(0) == e0) 00270 result = d_rules->canonMultZero(e1); 00271 else if (rat(1) == e0) 00272 result = d_rules->canonMultOne(e1); 00273 else 00274 switch(e1.getKind()) { 00275 case RATIONAL_EXPR : 00276 result = d_rules->canonMultConstConst(e0,e1); 00277 break; 00278 case MULT: 00279 DebugAssert(e1[0].isRational(), 00280 "theory_arith::canon:\n " 00281 "canon:MULT:MULT child is not canonical: " 00282 + e1[0].toString()); 00283 00284 thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]); 00285 result = transitivityRule(thmMult,canon(thmMult.getRHS())); 00286 break; 00287 case PLUS:{ 00288 Theorem thmPlus, thmPlus1; 00289 Expr ePlus; 00290 std::vector<Theorem> thmPlusVector; 00291 thmPlus = d_rules->canonMultConstSum(e0,e1); 00292 ePlus = thmPlus.getRHS(); 00293 Expr::iterator i = ePlus.begin(); 00294 for(;i != ePlus.end();++i) 00295 thmPlusVector.push_back(canon(*i)); 00296 thmPlus1 = substitutivityRule(PLUS, thmPlusVector); 00297 result = transitivityRule(thmPlus, thmPlus1); 00298 break; 00299 } 00300 default: 00301 result = reflexivityRule(e); 00302 break; 00303 } 00304 } 00305 else { 00306 if(e1.isRational()){ 00307 00308 // canonMultTermConst just reverses the order of the const and the 00309 // term. Then canon is called again. 00310 Theorem t1 = d_rules->canonMultTermConst(e1,e0); 00311 result = transitivityRule(t1,canon(t1.getRHS())); 00312 } 00313 else 00314 00315 // This is where the assertion for non-linear multiplication is 00316 // produced. 00317 result = d_rules->canonMultTerm1Term2(e0,e1); 00318 } 00319 break; 00320 } 00321 00322 */ 00323 case DIVIDE:{ 00324 /* 00325 case DIVIDE:{ 00326 if (e[1].isRational()) { 00327 if (e[1].getRational() == 0) 00328 throw ArithException("Divide by 0 error in "+e.toString()); 00329 Theorem thm = d_rules->canonDivideVar(e[0], e[1]); 00330 Expr e2 = thm.getRHS(); 00331 result = transitivityRule(thm, canon(e2)); 00332 } 00333 else 00334 { 00335 // TODO: to be handled 00336 throw ArithException("Divide by a non-const not handled in "+e.toString()); 00337 } 00338 break; 00339 } 00340 */ 00341 00342 // Division by 0 is OK (total extension, protected by TCCs) 00343 // if (e[1].isRational() && e[1].getRational() == 0) 00344 // throw ArithException("Divide by 0 error in "+e.toString()); 00345 if (e[1].getKind() == PLUS) 00346 throw ArithException("Divide by a PLUS expression not handled in"+e.toString()); 00347 result = d_rules->canonDivide(e); 00348 break; 00349 } 00350 case POW: 00351 if(e[1].isRational()) 00352 result = d_rules->canonPowConst(e); 00353 else { 00354 // x ^ 1 --> x 00355 if (e[0].isRational() && e[0].getRational() == 1) { 00356 result = d_rules->powerOfOne(e); 00357 } else 00358 result = reflexivityRule(e); 00359 } 00360 break; 00361 default: 00362 result = reflexivityRule(e); 00363 break; 00364 } 00365 TRACE("arith canon","canon => ",result," }"); 00366 return result; 00367 } 00368 00369 00370 Theorem 00371 TheoryArithOld::canonSimplify(const Expr& e) { 00372 TRACE("arith simplify", "canonSimplify(", e, ") {"); 00373 DebugAssert(kidsCanonical(e), 00374 "TheoryArithOld::canonSimplify("+e.toString()+")"); 00375 DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified"); 00376 Expr tmp(e); 00377 Theorem thm = canon(e); 00378 if(thm.getRHS().hasFind()) 00379 thm = transitivityRule(thm, find(thm.getRHS())); 00380 // We shouldn't rely on simplification in this function anymore 00381 DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()), 00382 "canonSimplify("+e.toString()+")\n" 00383 +"canon(e) = "+thm.getRHS().toString() 00384 +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString()); 00385 // if(tmp != thm.getRHS()) 00386 // thm = transitivityRule(thm, simplifyThm(thm.getRHS())); 00387 // while(tmp != thm.getRHS()) { 00388 // tmp = thm.getRHS(); 00389 // thm = canon(thm); 00390 // if(tmp != thm.getRHS()) 00391 // thm = transitivityRule(thm, simplifyThm(thm.getRHS())); 00392 // } 00393 TRACE("arith", "canonSimplify =>", thm, " }"); 00394 return thm; 00395 } 00396 00397 /*! accepts a theorem, canonizes it, applies iffMP and substituvity to 00398 * derive the canonized thm 00399 */ 00400 Theorem 00401 TheoryArithOld::canonPred(const Theorem& thm) { 00402 vector<Theorem> thms; 00403 DebugAssert(thm.getExpr().arity() == 2, 00404 "TheoryArithOld::canonPred: bad theorem: "+thm.toString()); 00405 Expr e(thm.getExpr()); 00406 thms.push_back(canonSimplify(e[0])); 00407 thms.push_back(canonSimplify(e[1])); 00408 Theorem result = iffMP(thm, substitutivityRule(e.getOp(), thms)); 00409 00410 return result; 00411 } 00412 00413 /*! accepts an equivalence theorem, canonizes it, applies iffMP and 00414 * substituvity to derive the canonized thm 00415 */ 00416 Theorem 00417 TheoryArithOld::canonPredEquiv(const Theorem& thm) { 00418 vector<Theorem> thms; 00419 DebugAssert(thm.getRHS().arity() == 2, 00420 "TheoryArithOld::canonPredEquiv: bad theorem: "+thm.toString()); 00421 Expr e(thm.getRHS()); 00422 thms.push_back(canonSimplify(e[0])); 00423 thms.push_back(canonSimplify(e[1])); 00424 Theorem result = transitivityRule(thm, substitutivityRule(e.getOp(), thms)); 00425 00426 return result; 00427 } 00428 00429 /*! accepts an equivalence theorem whose RHS is a conjunction, 00430 * canonizes it, applies iffMP and substituvity to derive the 00431 * canonized thm 00432 */ 00433 Theorem 00434 TheoryArithOld::canonConjunctionEquiv(const Theorem& thm) { 00435 vector<Theorem> thms; 00436 return thm; 00437 } 00438 00439 /*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem) 00440 * -# translate e to the form e' = 0 00441 * -# if (e'.isRational()) then {if e' != 0 return false else true} 00442 * -# a for loop checks if all the variables are integers. 00443 * - if not isolate a suitable real variable and call processRealEq(). 00444 * - if all variables are integers then isolate suitable variable 00445 * and call processIntEq(). 00446 */ 00447 Theorem TheoryArithOld::doSolve(const Theorem& thm) 00448 { 00449 const Expr& e = thm.getExpr(); 00450 if (e.isTrue() || e.isFalse()) return thm; 00451 TRACE("arith eq","doSolve(",e,") {"); 00452 DebugAssert(thm.isRewrite(), "thm = "+thm.toString()); 00453 Theorem eqnThm; 00454 vector<Theorem> thms; 00455 // Move LHS to the RHS, if necessary 00456 if(e[0].isRational() && e[0].getRational() == 0) 00457 eqnThm = thm; 00458 else { 00459 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e)); 00460 eqnThm = canonPred(eqnThm); 00461 } 00462 // eqnThm is of the form 0 = e' 00463 // 'right' is of the form e' 00464 Expr right = eqnThm.getRHS(); 00465 // Check for trivial equation 00466 if (right.isRational()) { 00467 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr())); 00468 TRACE("arith eq","doSolve => ",result," }"); 00469 return result; 00470 } 00471 00472 //normalize 00473 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr())); 00474 TRACE("arith eq","doSolve => ",eqnThm.getExpr()," }"); 00475 right = eqnThm.getRHS(); 00476 00477 //eqn is of the form 0 = e' and is normalized where 'right' denotes e' 00478 //FIXME: change processRealEq to accept equations as well instead of theorems 00479 00480 try { 00481 if (isMult(right)) { 00482 DebugAssert(right.arity() > 1, "Expected arity > 1"); 00483 if (right[0].isRational()) { 00484 Rational r = right[0].getRational(); 00485 if (r == 0) return getCommonRules()->trueTheorem(); 00486 else if (r == 1) { 00487 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); 00488 return getCommonRules()->trueTheorem(); 00489 } 00490 Theorem res = iffMP(eqnThm, 00491 d_rules->multEqn(eqnThm.getLHS(), 00492 right, rat(1/r))); 00493 res = canonPred(res); 00494 return doSolve(res); 00495 } 00496 else { 00497 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); 00498 return getCommonRules()->trueTheorem(); 00499 } 00500 } 00501 else if (isPow(right)) { 00502 DebugAssert(right.arity() == 2, "Expected arity 2"); 00503 if (right[0].isRational()) { 00504 return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr()))); 00505 } 00506 throw ArithException("Can't solve exponential eqn: "+eqnThm.toString()); 00507 } 00508 else { 00509 if(!isInteger(right)) { 00510 return processRealEq(eqnThm); 00511 } 00512 else { 00513 return processIntEq(eqnThm); 00514 } 00515 } 00516 } catch(ArithException& e) { 00517 FatalAssert(false, "We should never get here!!! : " + e.toString()); 00518 00519 // // Nonlinear bail out 00520 // Theorem res; 00521 // if (isPlus(right)) { 00522 // // Solve for something 00523 // // Try to simulate groebner basis by picking the highest term 00524 // Expr isolated = right[1]; 00525 // int isolated_degree = termDegree(isolated); 00526 // for (int i = 2; i < right.arity(); i ++) { 00527 // int degree = termDegree(right[i]); 00528 // if (degree > isolated_degree) { 00529 // isolated = right[i]; 00530 // isolated_degree = degree; 00531 // } 00532 // } 00533 // Rational coeff; 00534 // if (isMult(isolated) && isolated[0].isRational()) { 00535 // coeff = isolated[0].getRational(); 00536 // DebugAssert(coeff != 0, "Expected nonzero coeff"); 00537 // isolated = canon(isolated / rat(coeff)).getRHS(); 00538 // } else coeff = 1; 00539 // res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff))); 00540 // res = canonPred(res); 00541 // res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(), isolated, EQ)); 00542 // res = canonPred(res); 00543 // TRACE("arith nonlinear", "solved for: ", res.getExpr(), ""); 00544 // } else 00545 // res = symmetryRule(eqnThm); // Flip to e' = 0 00546 // TRACE("arith eq", "doSolve: failed to solve an equation: ", e, ""); 00547 // IF_DEBUG(debugger.counter("FAILED to solve equalities")++;) 00548 // setIncomplete("Non-linear arithmetic equalities"); 00549 // 00550 // // Since we are forgetting about this equation, setup for updates 00551 // TRACE("arith nonlinear", "adding setup to ", eqnThm.getExpr(), ""); 00552 // setupRec(eqnThm.getExpr()); 00553 // return getCommonRules()->trueTheorem(); 00554 } 00555 FatalAssert(false, ""); 00556 return Theorem(); 00557 } 00558 00559 /*! pick a monomial for the input equation. This function is used only 00560 * if the equation is an integer equation. Choose the monomial with 00561 * the smallest absolute value of coefficient. 00562 */ 00563 bool TheoryArithOld::pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin) 00564 { 00565 DebugAssert(isPlus(right) && right.arity() > 1, 00566 "TheoryArithOld::pickIntEqMonomial right is wrong :-): " + 00567 right.toString()); 00568 DebugAssert(right[0].isRational(), 00569 "TheoryArithOld::pickIntEqMonomial. right[0] must be const" + 00570 right.toString()); 00571 // DebugAssert(isInteger(right), 00572 // "TheoryArithOld::pickIntEqMonomial: right is of type int: " + 00573 // right.toString()); 00574 //right is of the form "C + a1x1 + ... + anxn". min is initialized 00575 //to a1 00576 Expr::iterator istart = right.begin(), iend = right.end(); 00577 istart++; 00578 Expr::iterator i = istart, j; 00579 bool found = false; 00580 nonlin = false; 00581 Rational min, coeff; 00582 Expr leaf; 00583 for(; i != iend; ++i) { 00584 if (isLeaf(*i)) { 00585 leaf = *i; 00586 coeff = 1; 00587 } 00588 else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) { 00589 leaf = (*i)[1]; 00590 coeff = abs((*i)[0].getRational()); 00591 } 00592 else { 00593 nonlin = true; 00594 continue; 00595 } 00596 for (j = istart; j != iend; ++j) { 00597 if (j != i && isLeafIn(leaf, *j)) break; 00598 } 00599 if (j == iend) { 00600 if (!found || min > coeff) { 00601 min = coeff; 00602 isolated = *i; 00603 found = true; 00604 } 00605 } 00606 } 00607 return found; 00608 } 00609 00610 /*! input is 0=e' Theorem and some of the vars in e' are of 00611 * type REAL. isolate one of them and send back to framework. output 00612 * is "var = e''" Theorem. 00613 */ 00614 Theorem 00615 TheoryArithOld::processRealEq(const Theorem& eqn) 00616 { 00617 DebugAssert(eqn.getLHS().isRational() && 00618 eqn.getLHS().getRational() == 0, 00619 "processRealEq invariant violated"); 00620 Expr right = eqn.getRHS(); 00621 // Find variable to isolate and store it in left. Pick the largest 00622 // (according to the total ordering) variable. FIXME: change from 00623 // total ordering to the ordering we devised for inequalities. 00624 00625 // TODO: I have to pick a variable that appears as a variable in the 00626 // term but does not appear as a variable anywhere else. The variable 00627 // must appear as a single leaf and not in a MULT expression with some 00628 // other variables and nor in a POW expression. 00629 00630 bool found = false; 00631 Expr left; 00632 00633 if (isPlus(right)) { 00634 DebugAssert(right[0].isRational(), "Expected first term to be rational"); 00635 for(int i = 1, iend = right.arity(); i < iend; ++i) { 00636 Expr c = right[i]; 00637 DebugAssert(!isRational(c), "Expected non-rational"); 00638 if(!isInteger(c)) { 00639 if (isLeaf(c) || 00640 ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) { 00641 Expr leaf = isLeaf(c) ? c : c[1]; 00642 int j; 00643 for (j = 1; j < iend; ++j) { 00644 if (j!= i 00645 && isLeafIn(leaf, right[j]) 00646 ) { 00647 break; 00648 } 00649 } 00650 if (j == iend) { 00651 left = c; 00652 found = true; 00653 break; 00654 } 00655 } 00656 } 00657 } 00658 } 00659 else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) || 00660 isLeaf(right)) { 00661 left = right; 00662 found = true; 00663 } 00664 00665 if (!found) { 00666 // The only way we can not get an isolated in the reals is if all of them 00667 // are non-linear. In this case we might have some integers to solve for 00668 // so we try that. The integer solver shouldn't be able to solve for the 00669 // reals, as they are not solvable and we should be safe. One of such 00670 // examples is if some constant ITE got skolemized and we have an equation 00671 // like SKOLEM = x^2 (bug79), in which case we should solve for the SKOLEM 00672 // where skolem is an INT variable. 00673 if (isNonlinearEq(eqn.getExpr())) 00674 return processIntEq(eqn); 00675 else throw 00676 ArithException("Can't find a leaf for solve in "+eqn.toString()); 00677 } 00678 00679 Rational r = -1; 00680 if (isMult(left)) { 00681 DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs"); 00682 DebugAssert(left[0].getRational() != 0, "left = "+left.toString()); 00683 r = -1/left[0].getRational(); 00684 left = left[1]; 00685 } 00686 00687 DebugAssert(isReal(getBaseType(left)) && !isInteger(left), 00688 "TheoryArithOld::ProcessRealEq: left is integer:\n left = " 00689 +left.toString()); 00690 // Normalize equation so that coefficient of the monomial 00691 // corresponding to "left" in eqn[1] is -1 00692 Theorem result(iffMP(eqn, 00693 d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r)))); 00694 result = canonPred(result); 00695 00696 // Isolate left 00697 result = iffMP(result, d_rules->plusPredicate(result.getLHS(), 00698 result.getRHS(), left, EQ)); 00699 result = canonPred(result); 00700 TRACE("arith","processRealEq => ",result," }"); 00701 return result; 00702 } 00703 00704 00705 void TheoryArithOld::getFactors(const Expr& e, set<Expr>& factors) 00706 { 00707 switch (e.getKind()) { 00708 case RATIONAL_EXPR: break; 00709 case MULT: { 00710 Expr::iterator i = e.begin(), iend = e.end(); 00711 for (; i != iend; ++i) { 00712 getFactors(*i, factors); 00713 } 00714 break; 00715 } 00716 case POW: { 00717 DebugAssert(e.arity() == 2, "invariant violated"); 00718 if (!isIntegerConst(e[0]) || e[0].getRational() <= 0) { 00719 throw ArithException("not positive integer exponent in "+e.toString()); 00720 } 00721 if (isLeaf(e[1])) factors.insert(e[1]); 00722 break; 00723 } 00724 default: { 00725 DebugAssert(isLeaf(e), "expected leaf"); 00726 DebugAssert(factors.find(e) == factors.end(), "expected new entry"); 00727 factors.insert(e); 00728 break; 00729 } 00730 } 00731 } 00732 00733 00734 /*! 00735 * \param eqn is a single equation 0 = e 00736 * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t 00737 */ 00738 Theorem 00739 TheoryArithOld::processSimpleIntEq(const Theorem& eqn) 00740 { 00741 TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {"); 00742 DebugAssert(eqn.isRewrite(), 00743 "TheoryArithOld::processSimpleIntEq: eqn must be equality" + 00744 eqn.getExpr().toString()); 00745 00746 Expr right = eqn.getRHS(); 00747 00748 DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(), 00749 "TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" + 00750 eqn.getExpr().toString()); 00751 00752 DebugAssert(!isMult(right) && !isPow(right), "should have been handled above"); 00753 if (isPlus(right)) { 00754 if (2 == right.arity() && 00755 (isLeaf(right[1]) || 00756 (isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) { 00757 //we take care of special cases like 0 = c + a.x, 0 = c + x, 00758 Expr c,x; 00759 separateMonomial(right[1], c, x); 00760 Theorem isIntx(isIntegerThm(x)); 00761 DebugAssert(!isIntx.isNull(), "right = "+right.toString() 00762 +"\n x = "+x.toString()); 00763 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx))); 00764 TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }"); 00765 return res; 00766 } 00767 // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x 00768 Expr isolated; 00769 bool nonlin; 00770 if (pickIntEqMonomial(right, isolated, nonlin)) { 00771 TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, ""); 00772 00773 // First, we compute the 'sign factor' with which to multiply the 00774 // eqn. if the coeff of isolated is positive (i.e. 'isolated' is 00775 // of the form x or a.x where a>0 ) then r must be -1 and if coeff 00776 // of 'isolated' is negative, r=1. 00777 Rational r = isMult(isolated) ? 00778 ((isolated[0].getRational() > 0) ? -1 : 1) : -1; 00779 Theorem result; 00780 if (-1 == r) { 00781 // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is 00782 // positive. modify eqn (0=e') to the equation (0=canon(-1*e')) 00783 result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r))); 00784 result = canonPred(result); 00785 Expr e = result.getRHS(); 00786 00787 // Isolate the 'isolated' 00788 result = iffMP(result, 00789 d_rules->plusPredicate(result.getLHS(),result.getRHS(), 00790 isolated, EQ)); 00791 } else { 00792 //r is 1 and hence isolated is -a.x. Make 'isolated' positive. 00793 const Rational& minusa = isolated[0].getRational(); 00794 Rational a = -1*minusa; 00795 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1]; 00796 00797 // Isolate the 'isolated' 00798 result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(), 00799 right,isolated,EQ)); 00800 } 00801 // Canonize the result 00802 result = canonPred(result); 00803 00804 //if isolated is 'x' or 1*x, then return result else continue processing. 00805 if(!isMult(isolated) || isolated[0].getRational() == 1) { 00806 TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }"); 00807 return result; 00808 } else if (!nonlin) { 00809 DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2, 00810 "TheoryArithOld::processSimpleIntEq: isolated must be mult " 00811 "with coeff >= 2.\n isolated = " + isolated.toString()); 00812 00813 // Compute IS_INTEGER() for lhs and rhs 00814 Expr lhs = result.getLHS(); 00815 Expr rhs = result.getRHS(); 00816 Expr a, x; 00817 separateMonomial(lhs, a, x); 00818 Theorem isIntLHS = isIntegerThm(x); 00819 vector<Theorem> isIntRHS; 00820 if(!isPlus(rhs)) { // rhs is a MULT 00821 Expr c, v; 00822 separateMonomial(rhs, c, v); 00823 isIntRHS.push_back(isIntegerThm(v)); 00824 DebugAssert(!isIntRHS.back().isNull(), ""); 00825 } else { // rhs is a PLUS 00826 DebugAssert(isPlus(rhs), "rhs = "+rhs.toString()); 00827 DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString()); 00828 Expr::iterator i=rhs.begin(), iend=rhs.end(); 00829 ++i; // Skip the free constant 00830 for(; i!=iend; ++i) { 00831 Expr c, v; 00832 separateMonomial(*i, c, v); 00833 isIntRHS.push_back(isIntegerThm(v)); 00834 DebugAssert(!isIntRHS.back().isNull(), ""); 00835 } 00836 } 00837 // Derive (EXISTS (x:INT): x = t2 AND 0 = t3) 00838 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS); 00839 // Skolemize the quantifier 00840 result = getCommonRules()->skolemize(result); 00841 // Canonize t2 and t3 generated by this rule 00842 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2, 00843 "processSimpleIntEq: result = "+result.getExpr().toString()); 00844 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0)); 00845 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1)); 00846 Theorem newRes = getCommonRules()->andIntro(thm1, thm2); 00847 if(newRes.getExpr() != result.getExpr()) result = newRes; 00848 00849 TRACE("arith eq", "processSimpleIntEq => ", result, " }"); 00850 return result; 00851 } 00852 } 00853 throw 00854 ArithException("Can't find a leaf for solve in "+eqn.toString()); 00855 } else { 00856 // eqn is 0 = x. Flip it and return 00857 Theorem result = symmetryRule(eqn); 00858 TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }"); 00859 return result; 00860 } 00861 } 00862 00863 /*! input is 0=e' Theorem and all of the vars in e' are of 00864 * type INT. isolate one of them and send back to framework. output 00865 * is "var = e''" Theorem and some associated equations in 00866 * solved form. 00867 */ 00868 Theorem 00869 TheoryArithOld::processIntEq(const Theorem& eqn) 00870 { 00871 TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {"); 00872 // Equations in the solved form. 00873 std::vector<Theorem> solvedAndNewEqs; 00874 Theorem newEq(eqn), result; 00875 bool done(false); 00876 do { 00877 result = processSimpleIntEq(newEq); 00878 // 'result' is of the from (x1=t1) AND 0=t' 00879 if(result.isRewrite()) { 00880 solvedAndNewEqs.push_back(result); 00881 done = true; 00882 } 00883 else if (result.getExpr().isBoolConst()) { 00884 done = true; 00885 } 00886 else { 00887 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2, 00888 "TheoryArithOld::processIntEq("+eqn.getExpr().toString() 00889 +")\n result = "+result.getExpr().toString()); 00890 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0)); 00891 newEq = getCommonRules()->andElim(result, 1); 00892 } 00893 } while(!done); 00894 Theorem res; 00895 if (result.getExpr().isFalse()) res = result; 00896 else if (solvedAndNewEqs.size() > 0) 00897 res = solvedForm(solvedAndNewEqs); 00898 else res = result; 00899 TRACE("arith eq", "processIntEq => ", res.getExpr(), " }"); 00900 return res; 00901 } 00902 00903 /*! 00904 * Takes a vector of equations and for every equation x_i=t_i 00905 * substitutes t_j for x_j in t_i for all j>i. This turns the system 00906 * of equations into a solved form. 00907 * 00908 * Assumption: variables x_j may appear in the RHS terms t_i ONLY for 00909 * i<j, but not for i>=j. 00910 */ 00911 Theorem 00912 TheoryArithOld::solvedForm(const vector<Theorem>& solvedEqs) 00913 { 00914 DebugAssert(solvedEqs.size() > 0, "TheoryArithOld::solvedForm()"); 00915 00916 // Trace code 00917 TRACE_MSG("arith eq", "TheoryArithOld::solvedForm:solvedEqs(\n ["); 00918 IF_DEBUG(if(debugger.trace("arith eq")) { 00919 for(vector<Theorem>::const_iterator j = solvedEqs.begin(), 00920 jend=solvedEqs.end(); j!=jend;++j) 00921 TRACE("arith eq", "", j->getExpr(), ",\n "); 00922 }) 00923 TRACE_MSG("arith eq", " ]) {"); 00924 // End of Trace code 00925 00926 vector<Theorem>::const_reverse_iterator 00927 i = solvedEqs.rbegin(), 00928 iend = solvedEqs.rend(); 00929 // Substitution map: a variable 'x' is mapped to a Theorem x=t. 00930 // This map accumulates the resulting solved form. 00931 ExprMap<Theorem> subst; 00932 for(; i!=iend; ++i) { 00933 if(i->isRewrite()) { 00934 Theorem thm = substAndCanonize(*i, subst); 00935 TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ", 00936 thm.getExpr(), ""); 00937 subst[i->getLHS()] = thm; 00938 } 00939 else { 00940 // This is the FALSE case: just return the contradiction 00941 DebugAssert(i->getExpr().isFalse(), 00942 "TheoryArithOld::solvedForm: an element of solvedEqs must " 00943 "be either EQ or FALSE: "+i->toString()); 00944 return *i; 00945 } 00946 } 00947 // Now we've collected the solved form in 'subst'. Wrap it up into 00948 // a conjunction and return. 00949 vector<Theorem> thms; 00950 for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end(); 00951 i!=iend; ++i) 00952 thms.push_back(i->second); 00953 00954 if (thms.size() > 1) return getCommonRules()->andIntro(thms); 00955 else return thms.back(); 00956 } 00957 00958 00959 /*! 00960 * ASSUMPTION: 't' is a fully canonized arithmetic term, and every 00961 * element of subst is a fully canonized equation of the form x=e, 00962 * indexed by the LHS variable. 00963 */ 00964 00965 Theorem 00966 TheoryArithOld::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst) 00967 { 00968 TRACE("arith eq", "substAndCanonize(", t, ") {"); 00969 // Quick and dirty check: return immediately if subst is empty 00970 if(subst.empty()) { 00971 Theorem res(reflexivityRule(t)); 00972 TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }"); 00973 return res; 00974 } 00975 // Check if we can substitute 't' directly 00976 ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end(); 00977 if(i!=iend) { 00978 TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }"); 00979 return i->second; 00980 } 00981 // The base case: t is an i-leaf 00982 if(isLeaf(t)) { 00983 Theorem res(reflexivityRule(t)); 00984 TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }"); 00985 return res; 00986 } 00987 // 't' is an arithmetic term; recurse into the children 00988 vector<Theorem> thms; 00989 vector<unsigned> changed; 00990 for(unsigned j=0, jend=t.arity(); j!=jend; ++j) { 00991 Theorem thm = substAndCanonize(t[j], subst); 00992 if(thm.getRHS() != t[j]) { 00993 thm = canonThm(thm); 00994 thms.push_back(thm); 00995 changed.push_back(j); 00996 } 00997 } 00998 // Do the actual substitution and canonize the result 00999 Theorem res; 01000 if(thms.size() > 0) { 01001 res = substitutivityRule(t, changed, thms); 01002 res = canonThm(res); 01003 } 01004 else 01005 res = reflexivityRule(t); 01006 TRACE("arith eq", "substAndCanonize => ", res, " }"); 01007 return res; 01008 } 01009 01010 01011 /*! 01012 * ASSUMPTION: 't' is a fully canonized equation of the form x = t, 01013 * and so is every element of subst, indexed by the LHS variable. 01014 */ 01015 01016 Theorem 01017 TheoryArithOld::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst) 01018 { 01019 // Quick and dirty check: return immediately if subst is empty 01020 if(subst.empty()) return eq; 01021 01022 DebugAssert(eq.isRewrite(), "TheoryArithOld::substAndCanonize: t = " 01023 +eq.getExpr().toString()); 01024 const Expr& t = eq.getRHS(); 01025 // Do the actual substitution in the term t 01026 Theorem thm = substAndCanonize(t, subst); 01027 // Substitution had no result: return the original equation 01028 if(thm.getRHS() == t) return eq; 01029 // Otherwise substitute the result into the equation 01030 vector<Theorem> thms; 01031 vector<unsigned> changed; 01032 thms.push_back(thm); 01033 changed.push_back(1); 01034 return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms)); 01035 } 01036 01037 void TheoryArithOld::processBuffer() 01038 { 01039 // Process the inequalities in the buffer 01040 bool varOnRHS; 01041 01042 // If we are in difference logic only, just return 01043 if (diffLogicOnly) return; 01044 01045 while (!inconsistent() && (d_bufferIdx_0 < d_buffer_0.size() || d_bufferIdx_1 < d_buffer_1.size() || d_bufferIdx_2 < d_buffer_2.size() || d_bufferIdx_3 < d_buffer_3.size())) { 01046 01047 // Get the unprojected inequality 01048 Theorem ineqThm; 01049 if (d_bufferIdx_0 < d_buffer_0.size()) { 01050 ineqThm = d_buffer_0[d_bufferIdx_0]; 01051 d_bufferIdx_0 = d_bufferIdx_0 + 1; 01052 } else if (d_bufferIdx_1 < d_buffer_1.size()) { 01053 ineqThm = d_buffer_1[d_bufferIdx_1]; 01054 d_bufferIdx_1 = d_bufferIdx_1 + 1; 01055 } else if (d_bufferIdx_2 < d_buffer_2.size()) { 01056 ineqThm = d_buffer_2[d_bufferIdx_2]; 01057 d_bufferIdx_2 = d_bufferIdx_2 + 1; 01058 } else { 01059 ineqThm = d_buffer_3[d_bufferIdx_3]; 01060 d_bufferIdx_3 = d_bufferIdx_3 + 1; 01061 } 01062 01063 // // Skip this inequality if it is stale 01064 // if(isStale(ineqThm.getExpr())) { 01065 // TRACE("arith buffer", "processBuffer(", ineqThm.getExpr(), ")... skipping stale"); 01066 // continue; 01067 // } 01068 // Dejan: project the finds, not the originals (if not projected already) 01069 const Expr& inequality = ineqThm.getExpr(); 01070 Theorem inequalityFindThm = inequalityToFind(ineqThm, true); 01071 Expr inequalityFind = inequalityFindThm.getExpr(); 01072 // if (inequality != inequalityFind) 01073 // enqueueFact(inequalityFindThm); 01074 01075 TRACE("arith buffer", "processing: ", inequality, ""); 01076 TRACE("arith buffer", "with find : ", inequalityFind, ""); 01077 01078 if (!isIneq(inequalityFind)) { 01079 TRACE("arith buffer", "find not an inequality... ", "", "skipping"); 01080 continue; 01081 } 01082 01083 if (alreadyProjected.find(inequalityFind) != alreadyProjected.end()) { 01084 TRACE("arith buffer", "already projected ... ", "", "skipping"); 01085 continue; 01086 } 01087 01088 01089 // We put the dummy for now, isolate variable will set it properly (or the find's one) 01090 // This one is just if the find is different. If the find is different 01091 // We will not check it again in update, so we're fine 01092 Expr dummy; 01093 alreadyProjected[inequality] = dummy; 01094 if (inequality != inequalityFind) { 01095 01096 alreadyProjected[inequalityFind] = dummy; 01097 01098 Expr rhs = inequalityFind[1]; 01099 01100 // Collect the statistics about variables 01101 if(isPlus(rhs)) { 01102 for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) { 01103 Expr monomial = *i; 01104 updateStats(monomial); 01105 } 01106 } else // It's a monomial 01107 updateStats(rhs); 01108 } 01109 01110 // See if this one is subsumed by a stronger inequality 01111 // c1 <= t1, t2 <= c2 01112 Rational c1, c2; 01113 Expr t1, t2; 01114 // Every term in the buffer has to have a lower bound set!!! 01115 // Except for the ones that changed the find 01116 extractTermsFromInequality(inequalityFind, c1, t1, c2, t2); 01117 if (termLowerBound.find(t1) != termLowerBound.end() && c1 != termLowerBound[t1]) { 01118 TRACE("arith ineq", "skipping because stronger bounds asserted ", inequalityFind.toString(), ":" + t1.toString()); 01119 DebugAssert(termLowerBoundThm.find(t1) != termLowerBoundThm.end(), "No lower bound on asserted atom!!! " + t1.toString()); 01120 Theorem strongerBound = termLowerBoundThm[t1]; 01121 //enqueueFact(d_rules->implyWeakerInequality(strongerBound.getExpr(), inequalityFindThm.getExpr())); 01122 continue; 01123 } 01124 01125 Theorem thm1 = isolateVariable(inequalityFindThm, varOnRHS); 01126 const Expr& ineq = thm1.getExpr(); 01127 if (ineq.isFalse()) 01128 setInconsistent(thm1); 01129 else 01130 if(!ineq.isTrue()) { 01131 01132 // Check that the variable is indeed isolated correctly 01133 DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]), "TheoryArithOld::processBuffer(): bad result from isolateVariable:\nineq = "+ineq.toString()); 01134 // and project the inequality 01135 projectInequalities(thm1, varOnRHS); 01136 } 01137 } 01138 } 01139 01140 01141 void TheoryArithOld::updateStats(const Rational& c, const Expr& v) 01142 { 01143 TRACE("arith stats", "updateStats("+c.toString()+", ", v, ")"); 01144 01145 // we can get numbers as checking for variables is not possible (nonlinear stuff) 01146 if (v.isRational()) return; 01147 01148 if (v.getType() != d_realType) { 01149 // Dejan: update the max coefficient of the variable 01150 if (c < 0) { 01151 // Goes to the left side 01152 ExprMap<Rational>::iterator maxFind = maxCoefficientLeft.find(v); 01153 if (maxFind == maxCoefficientLeft.end()) { 01154 maxCoefficientLeft[v] = - c; 01155 TRACE("arith stats", "max left", "", ""); 01156 } 01157 else 01158 if ((*maxFind).second < -c) { 01159 TRACE("arith stats", "max left", "", ""); 01160 maxCoefficientLeft[v] = -c; 01161 } 01162 } else { 01163 // Stays on the right side 01164 ExprMap<Rational>::iterator maxFind = maxCoefficientRight.find(v); 01165 if (maxFind == maxCoefficientRight.end()) { 01166 maxCoefficientRight[v] = c; 01167 TRACE("arith stats", "max right", "", ""); 01168 } 01169 else 01170 if((*maxFind).second < c) { 01171 TRACE("arith stats", "max right", "", ""); 01172 maxCoefficientRight[v] = c; 01173 } 01174 } 01175 } 01176 01177 if(c > 0) { 01178 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1; 01179 else d_countRight[v] = 1; 01180 } 01181 else 01182 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1; 01183 else d_countLeft[v] = 1; 01184 } 01185 01186 01187 void TheoryArithOld::updateStats(const Expr& monomial) 01188 { 01189 Expr c, m; 01190 separateMonomial(monomial, c, m); 01191 updateStats(c.getRational(), m); 01192 } 01193 01194 int TheoryArithOld::extractTermsFromInequality(const Expr& inequality, 01195 Rational& c1, Expr& t1, 01196 Rational& c2, Expr& t2) { 01197 01198 TRACE("arith extract", "extract(", inequality.toString(), ")"); 01199 01200 DebugAssert(isIneq(inequality), "extractTermsFromInequality: expexting an inequality got: " + inequality.getString() + ")"); 01201 01202 Expr rhs = inequality[1]; 01203 01204 c1 = 0; 01205 01206 // Extract the non-constant term (both sides) 01207 vector<Expr> positive_children, negative_children; 01208 if (isPlus(rhs)) { 01209 int start_i = 0; 01210 if (rhs[0].isRational()) { 01211 start_i = 1; 01212 c1 = -rhs[0].getRational(); 01213 } 01214 int end_i = rhs.arity(); 01215 for(int i = start_i; i < end_i; i ++) { 01216 const Expr& term = rhs[i]; 01217 positive_children.push_back(term); 01218 negative_children.push_back(canon(multExpr(rat(-1),term)).getRHS()); 01219 } 01220 } else { 01221 positive_children.push_back(rhs); 01222 negative_children.push_back(canon(multExpr(rat(-1), rhs)).getRHS()); 01223 } 01224 01225 int num_vars = positive_children.size(); 01226 01227 // c1 <= t1 01228 t1 = (num_vars > 1 ? canon(plusExpr(positive_children)).getRHS() : positive_children[0]); 01229 01230 // c2 is the upper bound on t2 : t2 <= c2 01231 c2 = -c1; 01232 t2 = (num_vars > 1 ? canon(plusExpr(negative_children)).getRHS() : negative_children[0]); 01233 01234 TRACE("arith extract", "extract: ", c1.toString() + " <= ", t1.toString()); 01235 01236 return num_vars; 01237 } 01238 01239 bool TheoryArithOld::addToBuffer(const Theorem& thm, bool priority) { 01240 01241 TRACE("arith buffer", "addToBuffer(", thm.getExpr().toString(), ")"); 01242 01243 Expr ineq = thm.getExpr(); 01244 const Expr& rhs = thm.getExpr()[1]; 01245 01246 bool nonLinear = false; 01247 Rational nonLinearConstant = 0; 01248 Expr compactNonLinear; 01249 Theorem compactNonLinearThm; 01250 01251 // Collect the statistics about variables and check for non-linearity 01252 if(isPlus(rhs)) { 01253 for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) { 01254 Expr monomial = *i; 01255 updateStats(monomial); 01256 // check for non-linear 01257 if (isMult(monomial)) { 01258 if ((monomial[0].isRational() && monomial.arity() >= 3) || 01259 (!monomial[0].isRational() && monomial.arity() >= 2) || 01260 (monomial.arity() == 2 && isPow(monomial[1]))) 01261 nonLinear = true; 01262 } 01263 } 01264 if (nonLinear) { 01265 compactNonLinearThm = d_rules->compactNonLinearTerm(rhs); 01266 compactNonLinear = compactNonLinearThm.getRHS(); 01267 } 01268 } 01269 else // It's a monomial 01270 { 01271 updateStats(rhs); 01272 if (isMult(rhs)) 01273 if ((rhs[0].isRational() && rhs.arity() >= 3) 01274 || (!rhs[0].isRational() && rhs.arity() >= 2) 01275 || (rhs.arity() == 2 && isPow(rhs[1]))) { 01276 nonLinear = true; 01277 compactNonLinear = rhs; 01278 compactNonLinearThm = reflexivityRule(compactNonLinear); 01279 } 01280 } 01281 01282 if (bufferedInequalities.find(ineq) != bufferedInequalities.end()) { 01283 TRACE("arith buffer", "addToBuffer()", "", "... already in db"); 01284 if (formulaAtoms.find(ineq) != formulaAtoms.end()) { 01285 TRACE("arith buffer", "it's a formula atom, enqueuing.", "", ""); 01286 enqueueFact(thm); 01287 } 01288 return false; 01289 } 01290 01291 if (nonLinear && (isMult(rhs) || compactNonLinear != rhs)) { 01292 TRACE("arith nonlinear", "compact version of ", rhs, " is " + compactNonLinear.toString()); 01293 // Replace the rhs with the compacted nonlinear term 01294 Theorem thm1 = (compactNonLinear != rhs ? 01295 iffMP(thm, substitutivityRule(ineq, 1, compactNonLinearThm)) : thm); 01296 // Now, try to deduce the signednes of multipliers 01297 Rational c = (isMult(rhs) ? 0 : compactNonLinear[0].getRational()); 01298 // We can deduct the signs if the constant is not bigger than 0 01299 if (c <= 0) { 01300 thm1 = d_rules->nonLinearIneqSignSplit(thm1); 01301 TRACE("arith nonlinear", "spliting on signs : ", thm1.getExpr(), ""); 01302 enqueueFact(thm1); 01303 } 01304 } 01305 01306 // Get c1, c2, t1, t2 such that c1 <= t1 and t2 <= c2 01307 Expr t1, t2; 01308 Rational c1, c2; 01309 int num_vars = extractTermsFromInequality(ineq, c1, t1, c2, t2); 01310 01311 // If 2 variable, do add to difference logic (allways, just in case) 01312 bool factIsDiffLogic = false; 01313 if (num_vars <= 2) { 01314 01315 TRACE("arith diff", t2, " < ", c2); 01316 // c1 <= t1, check if difference logic 01317 // t1 of the form 0 + ax + by 01318 Expr ax = (num_vars == 2 ? t2[1] : t2); 01319 Expr a_expr, x; 01320 separateMonomial(ax, a_expr, x); 01321 Rational a = a_expr.getRational(); 01322 Expr by = (num_vars == 2 ? t2[2] : (a < 0 ? zero : rat(-1)*zero)); 01323 Expr b_expr, y; 01324 separateMonomial(by, b_expr, y); 01325 Rational b = b_expr.getRational(); 01326 01327 // Check for non-linear 01328 if (!isLeaf(x) || !isLeaf(y)) 01329 setIncomplete("Non-linear arithmetic inequalities"); 01330 01331 if (a == 1 && b == -1) { 01332 diffLogicGraph.addEdge(x, y, c2, thm); 01333 factIsDiffLogic = true; 01334 } 01335 else if (a == -1 && b == 1) { 01336 diffLogicGraph.addEdge(y, x, c2, thm); 01337 factIsDiffLogic = true; 01338 } 01339 // Not difference logic, put it in the 3 or more vars buffer 01340 else { 01341 diffLogicOnly = false; 01342 TRACE("arith diff", "not diff logic", thm.getExpr().toString(), ""); 01343 } 01344 01345 if (diffLogicGraph.isUnsat()) { 01346 TRACE("diff unsat", "UNSAT", " : ", diffLogicGraph.getUnsatTheorem()); 01347 setInconsistent(diffLogicGraph.getUnsatTheorem()); 01348 return false; 01349 } 01350 } else { 01351 diffLogicOnly = false; 01352 TRACE("arith diff", "not diff logic", thm.getExpr().toString(), ""); 01353 } 01354 01355 // For now we treat all the bound as LE, weaker 01356 CDMap<Expr, Rational>::iterator find_lower = termLowerBound.find(t1); 01357 if (find_lower != termLowerBound.end()) { 01358 // found bound c <= t1 01359 Rational found_c = (*find_lower).second; 01360 // If found c is bigger than the new one, we are done 01361 if (c1 <= found_c && !(found_c == c1 && ineq.getKind() == LT)) { 01362 TRACE("arith buffer", "addToBuffer()", "", "... lower_bound subsumed"); 01363 // Removed assert. Can happen that an atom is not asserted yet, and get's implied as 01364 // a formula atom and then asserted here. it's fine 01365 //DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + ""); 01366 return false; 01367 } else { 01368 Theorem oldLowerBound = termLowerBoundThm[t1]; 01369 Expr oldIneq = oldLowerBound.getExpr(); 01370 if (formulaAtoms.find(oldIneq) != formulaAtoms.end()) 01371 enqueueFact(getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, oldIneq))); 01372 termLowerBound[t1] = c1; 01373 termLowerBoundThm[t1] = thm; 01374 } 01375 } else { 01376 termLowerBound[t1] = c1; 01377 termLowerBoundThm[t1] = thm; 01378 } 01379 01380 CDMap<Expr, Rational>::iterator find_upper = termUpperBound.find(t2); 01381 if (find_upper != termUpperBound.end()) { 01382 // found bound t2 <= c 01383 Rational found_c = (*find_upper).second; 01384 // If found c is smaller than the new one, we are done 01385 if (found_c <= c2 && !(found_c == c2 && ineq.getKind() == LT)) { 01386 TRACE("arith buffer", "addToBuffer()", "", "... upper_bound subsumed"); 01387 //DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + ""); 01388 return false; 01389 } else { 01390 termUpperBound[t2] = c2; 01391 termUpperBoundThm[t2] = thm; 01392 } 01393 } else { 01394 termUpperBound[t2] = c2; 01395 termUpperBoundThm[t2] = thm; 01396 } 01397 01398 // See if the bounds on the term can infer conflict or equality 01399 if (termUpperBound.find(t1) != termUpperBound.end() && 01400 termLowerBound.find(t1) != termLowerBound.end() && 01401 termUpperBound[t1] <= termLowerBound[t1]) { 01402 Theorem thm1 = termUpperBoundThm[t1]; 01403 Theorem thm2 = termLowerBoundThm[t1]; 01404 TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString()); 01405 enqueueFact(d_rules->addInequalities(thm1, thm2)); 01406 } else 01407 if (termUpperBound.find(t2) != termUpperBound.end() && 01408 termLowerBound.find(t2) != termLowerBound.end() && 01409 termUpperBound[t2] <= termLowerBound[t2]) { 01410 Theorem thm1 = termUpperBoundThm[t2]; 01411 Theorem thm2 = termLowerBoundThm[t2]; 01412 TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString()); 01413 enqueueFact(d_rules->addInequalities(thm1, thm2)); 01414 } 01415 01416 if (true) { 01417 // See if we can propagate anything to the formula atoms 01418 // c1 <= t1 ===> c <= t1 for c < c1 01419 AtomsMap::iterator find = formulaAtomLowerBound.find(t1); 01420 AtomsMap::iterator find_end = formulaAtomLowerBound.end(); 01421 if (find != find_end) { 01422 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin(); 01423 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end(); 01424 while (bounds != bounds_end) { 01425 TRACE("arith atoms", "trying propagation", ineq, (*bounds).second); 01426 const Expr& implied = (*bounds).second; 01427 // Try to do some theory propagation 01428 if ((*bounds).first < c1 || (!(ineq.getKind() == LE && implied.getKind() == LT) && (*bounds).first == c1)) { 01429 // c1 <= t1 => c <= t1 (for c <= c1) 01430 // c1 < t1 => c <= t1 (for c <= c1) 01431 // c1 <= t1 => c < t1 (for c < c1) 01432 Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, implied)); 01433 enqueueFact(impliedThm); 01434 } 01435 bounds ++; 01436 } 01437 } 01438 01439 // 01440 // c1 <= t1 ==> !(t1 <= c) for c < c1 01441 // ==> !(-c <= t2) 01442 // i.e. all coefficient in in the implied are opposite of t1 01443 find = formulaAtomUpperBound.find(t1); 01444 find_end = formulaAtomUpperBound.end(); 01445 if (find != find_end) { 01446 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin(); 01447 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end(); 01448 while (bounds != bounds_end) { 01449 TRACE("arith atoms", "trying propagation", ineq, (*bounds).second); 01450 const Expr& implied = (*bounds).second; 01451 // Try to do some theory propagation 01452 if ((*bounds).first < c1) { 01453 Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyNegatedInequality(ineq, implied)); 01454 enqueueFact(impliedThm); 01455 } 01456 bounds ++; 01457 } 01458 } 01459 } 01460 01461 // Register this as a resource 01462 theoryCore()->getResource(); 01463 01464 // If out of resources, bail out 01465 if (theoryCore()->outOfResources()) return false; 01466 01467 // Checking because we could have projected it as a find of some other 01468 // equation 01469 if (alreadyProjected.find(ineq) == alreadyProjected.end()) { 01470 // We buffer it if it's not marked for not buffering 01471 if (dontBuffer.find(ineq) == dontBuffer.end()) { 01472 // We give priority to the one that can produce a conflict 01473 if (priority) 01474 d_buffer_0.push_back(thm); 01475 else { 01476 // Push it into the buffer (one var) 01477 if (num_vars == 1) d_buffer_1.push_back(thm); 01478 else if (num_vars == 2) d_buffer_2.push_back(thm); 01479 else d_buffer_3.push_back(thm); 01480 } 01481 01482 if (factIsDiffLogic) diff_logic_size = diff_logic_size + 1; 01483 } 01484 } 01485 01486 // Remember that it's in the buffer 01487 bufferedInequalities[ineq] = thm; 01488 01489 // Since we care about this atom, lets set it up 01490 if (!ineq.hasFind()) 01491 theoryCore()->setupTerm(ineq, this, thm); 01492 01493 return true; 01494 } 01495 01496 01497 Theorem TheoryArithOld::isolateVariable(const Theorem& inputThm, 01498 bool& isolatedVarOnRHS) 01499 { 01500 Theorem result(inputThm); 01501 const Expr& e = inputThm.getExpr(); 01502 TRACE("arith","isolateVariable(",e,") {"); 01503 TRACE("arith ineq", "isolateVariable(", e, ") {"); 01504 //we assume all the children of e are canonized 01505 DebugAssert(isLT(e)||isLE(e), 01506 "TheoryArithOld::isolateVariable: " + e.toString() + 01507 " wrong kind"); 01508 int kind = e.getKind(); 01509 DebugAssert(e[0].isRational() && e[0].getRational() == 0, 01510 "TheoryArithOld::isolateVariable: theorem must be of " 01511 "the form 0 < rhs: " + inputThm.toString()); 01512 01513 const Expr& zero = e[0]; 01514 Expr right = e[1]; 01515 // Check for trivial in-equation. 01516 if (right.isRational()) { 01517 result = iffMP(result, d_rules->constPredicate(e)); 01518 TRACE("arith ineq","isolateVariable => ",result.getExpr()," }"); 01519 TRACE("arith","isolateVariable => ",result," }"); 01520 return result; 01521 } 01522 01523 // Normalization of inequality to make coefficients integer and 01524 // relatively prime. 01525 01526 Expr factor(computeNormalFactor(right, false)); 01527 TRACE("arith", "isolateVariable: factor = ", factor, ""); 01528 DebugAssert(factor.getRational() > 0, 01529 "isolateVariable: factor="+factor.toString()); 01530 // Now multiply the inequality by the factor, unless it is 1 01531 if(factor.getRational() != 1) { 01532 result = iffMP(result, d_rules->multIneqn(e, factor)); 01533 // And canonize the result 01534 result = canonPred(result); 01535 result = rafineInequalityToInteger(result); 01536 right = result.getExpr()[1]; 01537 } 01538 01539 // Find monomial to isolate and store it in isolatedMonomial 01540 Expr isolatedMonomial = right; 01541 01542 if (isPlus(right)) 01543 isolatedMonomial = pickMonomial(right); 01544 01545 TRACE("arith ineq", "isolatedMonomial => ",isolatedMonomial,""); 01546 01547 // Set the correct isolated monomial 01548 // Now, if something gets updated, but this monomial is not changed, we don't 01549 // Have to rebuffer it as the projection will still be accurate when updated 01550 alreadyProjected[e] = isolatedMonomial; 01551 01552 Rational r = -1; 01553 isolatedVarOnRHS = true; 01554 if (isMult(isolatedMonomial)) { 01555 r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1; 01556 isolatedVarOnRHS = 01557 ((isolatedMonomial[0].getRational()) >= 0)? true : false; 01558 } 01559 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS(); 01560 TRACE("arith ineq", "-(isolatedMonomial) => ",isolatedMonomial,""); 01561 // Isolate isolatedMonomial on to the LHS 01562 result = iffMP(result, d_rules->plusPredicate(zero, right, 01563 isolatedMonomial, kind)); 01564 // Canonize the resulting inequality 01565 TRACE("arith ineq", "resutl => ",result,""); 01566 result = canonPred(result); 01567 if(1 != r) { 01568 result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r))); 01569 result = canonPred(result); 01570 } 01571 TRACE("arith ineq","isolateVariable => ",result.getExpr()," }"); 01572 TRACE("arith","isolateVariable => ",result," }"); 01573 return result; 01574 } 01575 01576 Expr 01577 TheoryArithOld::computeNormalFactor(const Expr& right, bool normalizeConstants) { 01578 // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is 01579 // of the form c1/d1*x1 + ... + cn/dn*xn 01580 Rational factor; 01581 if(isPlus(right)) { 01582 vector<Rational> nums, denoms; 01583 for(int i=0, iend=right.arity(); i<iend; ++i) { 01584 switch(right[i].getKind()) { 01585 case RATIONAL_EXPR: 01586 if (normalizeConstants) { 01587 Rational c(abs(right[i].getRational())); 01588 nums.push_back(c.getNumerator()); 01589 denoms.push_back(c.getDenominator()); 01590 break; 01591 } 01592 break; 01593 case MULT: { 01594 Rational c(abs(right[i][0].getRational())); 01595 nums.push_back(c.getNumerator()); 01596 denoms.push_back(c.getDenominator()); 01597 break; 01598 } 01599 default: // it's a variable 01600 nums.push_back(1); 01601 denoms.push_back(1); 01602 break; 01603 } 01604 } 01605 Rational gcd_nums = gcd(nums); 01606 // x/0 == 0 in our model, as a total extension of arithmetic. The 01607 // particular value of x/0 is irrelevant, since the DP is guarded 01608 // by the top-level TCCs, and it is safe to return any value in 01609 // cases when terms are undefined. 01610 factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums); 01611 } else if(isMult(right)) { 01612 const Rational& r = right[0].getRational(); 01613 factor = (r==0)? 0 : (1/abs(r)); 01614 } 01615 else 01616 factor = 1; 01617 return rat(factor); 01618 } 01619 01620 01621 bool TheoryArithOld::lessThanVar(const Expr& isolatedMonomial, const Expr& var2) 01622 { 01623 DebugAssert(!isRational(var2) && !isRational(isolatedMonomial), 01624 "TheoryArithOld::findMaxVar: isolatedMonomial cannot be rational" + 01625 isolatedMonomial.toString()); 01626 Expr c, var0, var1; 01627 separateMonomial(isolatedMonomial, c, var0); 01628 separateMonomial(var2, c, var1); 01629 return var0 < var1; 01630 } 01631 01632 /*! "Stale" means it contains non-simplified subexpressions. For 01633 * terms, it checks the expression's find pointer; for formulas it 01634 * checks the children recursively (no caching!). So, apply it with 01635 * caution, and only to simple atomic formulas (like inequality). 01636 */ 01637 bool TheoryArithOld::isStale(const Expr& e) { 01638 if(e.isTerm()) 01639 return e != find(e).getRHS(); 01640 // It's better be a simple predicate (like inequality); we check the 01641 // kids recursively 01642 bool stale=false; 01643 for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i) 01644 stale = isStale(*i); 01645 return stale; 01646 } 01647 01648 01649 bool TheoryArithOld::isStale(const TheoryArithOld::Ineq& ineq) { 01650 TRACE("arith stale", "isStale(", ineq, ") {"); 01651 const Expr& ineqExpr = ineq.ineq().getExpr(); 01652 const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS()); 01653 bool strict(isLT(ineqExpr)); 01654 const FreeConst& fc = ineq.getConst(); 01655 01656 bool subsumed; 01657 01658 if (ineqExpr.hasFind() && find(ineqExpr[1]).getRHS() != ineqExpr[1]) 01659 return true; 01660 01661 if(ineq.varOnRHS()) { 01662 subsumed = (c < fc.getConst() || 01663 (c == fc.getConst() && !strict && fc.strict())); 01664 } else { 01665 subsumed = (c > fc.getConst() || 01666 (c == fc.getConst() && strict && !fc.strict())); 01667 } 01668 01669 bool res; 01670 if(subsumed) { 01671 res = true; 01672 TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }"); 01673 } 01674 else { 01675 res = isStale(ineqExpr); 01676 TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }"); 01677 } 01678 return res; 01679 } 01680 01681 01682 void TheoryArithOld::separateMonomial(const Expr& e, Expr& c, Expr& var) { 01683 TRACE("separateMonomial", "separateMonomial(", e, ")"); 01684 DebugAssert(!isPlus(e), 01685 "TheoryArithOld::separateMonomial(e = "+e.toString()+")"); 01686 if(isMult(e)) { 01687 DebugAssert(e.arity() >= 2, 01688 "TheoryArithOld::separateMonomial(e = "+e.toString()+")"); 01689 c = e[0]; 01690 if(e.arity() == 2) var = e[1]; 01691 else { 01692 vector<Expr> kids = e.getKids(); 01693 kids[0] = rat(1); 01694 var = multExpr(kids); 01695 } 01696 } else { 01697 c = rat(1); 01698 var = e; 01699 } 01700 DebugAssert(c.isRational(), "TheoryArithOld::separateMonomial(e = " 01701 +e.toString()+", c = "+c.toString()+")"); 01702 DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1), 01703 "TheoryArithOld::separateMonomial(e = " 01704 +e.toString()+", var = "+var.toString()+")"); 01705 } 01706 01707 01708 void TheoryArithOld::projectInequalities(const Theorem& theInequality, 01709 bool isolatedVarOnRHS) 01710 { 01711 01712 TRACE("arith project", "projectInequalities(", theInequality.getExpr(), 01713 ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false") 01714 +") {"); 01715 DebugAssert(isLE(theInequality.getExpr()) || 01716 isLT(theInequality.getExpr()), 01717 "TheoryArithOld::projectIsolatedVar: "\ 01718 "theInequality is of the wrong form: " + 01719 theInequality.toString()); 01720 01721 //TODO: DebugAssert to check if the isolatedMonomial is of the right 01722 //form and the whether we are indeed getting inequalities. 01723 Theorem theIneqThm(theInequality); 01724 Expr theIneq = theIneqThm.getExpr(); 01725 01726 // If the inequality is strict and integer, change it to non-strict 01727 if(isLT(theIneq)) { 01728 Theorem isIntLHS(isIntegerThm(theIneq[0])); 01729 Theorem isIntRHS(isIntegerThm(theIneq[1])); 01730 if ((!isIntLHS.isNull() && !isIntRHS.isNull())) { 01731 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, !isolatedVarOnRHS); 01732 theIneqThm = canonPred(iffMP(theIneqThm, thm)); 01733 theIneq = theIneqThm.getExpr(); 01734 } 01735 } 01736 01737 Expr isolatedMonomial = isolatedVarOnRHS ? theIneq[1] : theIneq[0]; 01738 01739 Expr monomialVar, a; 01740 separateMonomial(isolatedMonomial, a, monomialVar); 01741 01742 bool subsumed; 01743 const FreeConst& bestConst = updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed); 01744 01745 if(subsumed) { 01746 IF_DEBUG(debugger.counter("subsumed inequalities")++;) 01747 TRACE("arith ineq", "subsumed inequality: ", theIneq, ""); 01748 } else { 01749 // If the isolated variable is actually a non-linear term, we are 01750 // incomplete 01751 if(isMult(monomialVar) || isPow(monomialVar)) 01752 setIncomplete("Non-linear arithmetic inequalities"); 01753 01754 // First, we need to make sure the isolated inequality is 01755 // setup properly. 01756 // setupRec(theIneq[0]); 01757 // setupRec(theIneq[1]); 01758 theoryCore()->setupTerm(theIneq[0], this, theIneqThm); 01759 theoryCore()->setupTerm(theIneq[1], this, theIneqThm); 01760 // Add the inequality into the appropriate DB. 01761 ExprMap<CDList<Ineq> *>& db1 = isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB; 01762 ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar); 01763 if(it1 == db1.end()) { 01764 CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext()); 01765 list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); 01766 db1[monomialVar] = list; 01767 } 01768 else 01769 ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); 01770 01771 ExprMap<CDList<Ineq> *>& db2 = isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB; 01772 ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar); 01773 if(it == db2.end()) { 01774 TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }"); 01775 return; 01776 } 01777 01778 CDList<Ineq>& listOfDBIneqs = *((*it).second); 01779 Theorem betaLTt, tLTalpha, thm; 01780 for(int i = listOfDBIneqs.size() - 1; !inconsistent() && i >= 0; --i) { 01781 const Ineq& ineqEntry = listOfDBIneqs[i]; 01782 const Theorem& ineqThm = ineqEntry.ineq(); //inequalityToFind(ineqEntry.ineq(), isolatedVarOnRHS); 01783 01784 // ineqExntry might be stale 01785 01786 if(!isStale(ineqEntry)) { 01787 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; 01788 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm; 01789 01790 thm = normalizeProjectIneqs(betaLTt, tLTalpha); 01791 if (thm.isNull()) continue; 01792 01793 IF_DEBUG(debugger.counter("real shadows")++;) 01794 01795 // Check for TRUE and FALSE theorems 01796 Expr e(thm.getExpr()); 01797 01798 if(e.isFalse()) { 01799 setInconsistent(thm); 01800 TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }"); 01801 return; 01802 } 01803 else { 01804 if(!e.isTrue() && !e.isEq()) { 01805 // setup the term so that it comes out in updates 01806 addToBuffer(thm, false); 01807 } 01808 else if(e.isEq()) 01809 enqueueFact(thm); 01810 } 01811 } else { 01812 IF_DEBUG(debugger.counter("stale inequalities")++;) 01813 } 01814 } 01815 } 01816 01817 TRACE_MSG("arith ineq", "projectInequalities => }"); 01818 } 01819 01820 Theorem TheoryArithOld::normalizeProjectIneqs(const Theorem& ineqThm1, 01821 const Theorem& ineqThm2) 01822 { 01823 //ineq1 is of the form beta < b.x or beta < x [ or with <= ] 01824 //ineq2 is of the form a.x < alpha or x < alpha. 01825 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2; 01826 Expr ineq1 = betaLTt.getExpr(); 01827 Expr ineq2 = tLTalpha.getExpr(); 01828 Expr c,x; 01829 separateMonomial(ineq2[0], c, x); 01830 Theorem isIntx(isIntegerThm(x)); 01831 Theorem isIntBeta(isIntegerThm(ineq1[0])); 01832 Theorem isIntAlpha(isIntegerThm(ineq2[1])); 01833 bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull()); 01834 01835 TRACE("arith ineq", "normalizeProjectIneqs(", ineq1, 01836 ", "+ineq2.toString()+") {"); 01837 DebugAssert((isLE(ineq1) || isLT(ineq1)) && 01838 (isLE(ineq2) || isLT(ineq2)), 01839 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " + 01840 ineq1.toString() + ineq2.toString()); 01841 DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]), 01842 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " + 01843 ineq1.toString() + ineq2.toString()); 01844 01845 //compute the factors to multiply the two inequalities with 01846 //so that they get the form beta < t and t < alpha. 01847 Rational factor1 = 1, factor2 = 1; 01848 Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1; 01849 Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1; 01850 if(b != a) { 01851 factor1 = a; 01852 factor2 = b; 01853 } 01854 01855 //if the ineqs are of type int then apply one of the gray 01856 //dark shadow rules. 01857 // FIXME: intResult should also be checked for immediate 01858 // optimizations, as those below for 'result'. Also, if intResult 01859 // is a single inequality, we may want to handle it similarly to the 01860 // 'result' rather than enqueuing directly. 01861 if(isInt && (a >= 2 || b >= 2)) { 01862 Theorem intResult; 01863 if(a <= b) 01864 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha, 01865 isIntAlpha, isIntBeta, isIntx); 01866 else 01867 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha, 01868 isIntAlpha, isIntBeta, isIntx); 01869 enqueueFact(intResult); 01870 // Fetch dark and gray shadows 01871 const Expr& DorG = intResult.getExpr(); 01872 DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString()); 01873 const Expr& G = DorG[1]; 01874 DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString()); 01875 // Set the higher splitter priority for dark shadow 01876 // Expr tmp = simplifyExpr(D); 01877 // if (!tmp.isBoolConst()) 01878 // addSplitter(tmp, 5); 01879 // Also set a higher priority to the NEGATION of GRAY_SHADOW 01880 Expr tmp = simplifyExpr(!G); 01881 if (!tmp.isBoolConst()) 01882 addSplitter(tmp, 1); 01883 IF_DEBUG(debugger.counter("dark+gray shadows")++;) 01884 01885 // Dejan: Let's forget about the real shadow, we are doing integers 01886 // /return intResult; 01887 } 01888 01889 //actually normalize the inequalities 01890 if(1 != factor1) { 01891 Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1))); 01892 betaLTt = canonPred(thm2); 01893 ineq1 = betaLTt.getExpr(); 01894 } 01895 if(1 != factor2) { 01896 Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2))); 01897 tLTalpha = canonPred(thm2); 01898 ineq2 = tLTalpha.getExpr(); 01899 } 01900 01901 //IF_DEBUG(debugger.counter("real shadows")++;) 01902 01903 Expr beta(ineq1[0]); 01904 Expr alpha(ineq2[1]); 01905 // In case of alpha <= t <= alpha, we generate t = alpha 01906 if(isLE(ineq1) && isLE(ineq2) && alpha == beta) { 01907 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha); 01908 TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }"); 01909 return result; 01910 } 01911 01912 // Check if this inequality is a finite interval 01913 // if(isInt) 01914 // processFiniteInterval(betaLTt, tLTalpha); 01915 01916 // // Only do the real shadow if a and b = 1 01917 // if (isInt && a > 1 && b > 1) 01918 // return Theorem(); 01919 01920 //project the normalized inequalities. 01921 01922 Theorem result = d_rules->realShadow(betaLTt, tLTalpha); 01923 01924 // FIXME: Clark's changes. Is 'rewrite' more or less efficient? 01925 // result = iffMP(result, rewrite(result.getExpr())); 01926 // TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }"); 01927 01928 // Now, transform the result into 0 < rhs and see if rhs is a const 01929 Expr e(result.getExpr()); 01930 // int kind = e.getKind(); 01931 if(!(e[0].isRational() && e[0].getRational() == 0)) 01932 result = iffMP(result, d_rules->rightMinusLeft(e)); 01933 result = canonPred(result); 01934 01935 //result is "0 kind e'". where e' is equal to canon(e[1]-e[0]) 01936 Expr right = result.getExpr()[1]; 01937 // Check for trivial inequality 01938 if (right.isRational()) 01939 result = iffMP(result, d_rules->constPredicate(result.getExpr())); 01940 else 01941 result = normalize(result); 01942 TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }"); 01943 return result; 01944 } 01945 01946 Rational TheoryArithOld::currentMaxCoefficient(Expr var) 01947 { 01948 // We prefer real variables 01949 if (var.getType() == d_realType) return -100; 01950 01951 // Find the biggest left side coefficient 01952 ExprMap<Rational>::iterator findMaxLeft = maxCoefficientLeft.find(var); 01953 Rational leftMax = -1; 01954 if (findMaxLeft != maxCoefficientLeft.end()) 01955 leftMax = (*findMaxLeft).second; 01956 01957 // 01958 ExprMap<Rational>::iterator findMaxRight = maxCoefficientRight.find(var); 01959 Rational rightMax = -1; 01960 if (findMaxRight != maxCoefficientRight.end()) 01961 rightMax = (*findMaxRight).second; 01962 01963 // What is the max coefficient 01964 // If one is undefined, dont take it. My first thought was to project away unbounded 01965 // ones, but it happens that you get another constraint on it later and the hell breaks 01966 // loose if they have big coefficients. 01967 Rational returnValue; 01968 if (leftMax == -1) returnValue = rightMax; 01969 else if (rightMax == -1) returnValue = leftMax; 01970 else if (leftMax < rightMax) returnValue = rightMax; 01971 else returnValue = leftMax; 01972 01973 TRACE("arith stats", "max coeff of ", var.toString(), ": " + returnValue.toString() + "(left=" + leftMax.toString() + ",right=" + rightMax.toString()); 01974 01975 return returnValue; 01976 } 01977 01978 void TheoryArithOld::fixCurrentMaxCoefficient(Expr var, Rational max) { 01979 fixedMaxCoefficient[var] = max; 01980 } 01981 01982 void TheoryArithOld::selectSmallestByCoefficient(const vector<Expr>& input, vector<Expr>& output) { 01983 01984 // Clear the output vector 01985 output.clear(); 01986 01987 // Get the first variable, and set it as best 01988 Expr best_variable = input[0]; 01989 Rational best_coefficient = currentMaxCoefficient(best_variable); 01990 output.push_back(best_variable); 01991 01992 for(unsigned int i = 1; i < input.size(); i ++) { 01993 01994 // Get the current variable 01995 Expr current_variable = input[i]; 01996 // Get the current variable's max coefficient 01997 Rational current_coefficient = currentMaxCoefficient(current_variable); 01998 01999 // If strictly better than the current best, remember it 02000 if ((current_coefficient < best_coefficient)) { 02001 best_variable = current_variable; 02002 best_coefficient = current_coefficient; 02003 output.clear(); 02004 } 02005 02006 // If equal to the current best, push it to the stack (in 10% range) 02007 if (current_coefficient == best_coefficient) 02008 output.push_back(current_variable); 02009 } 02010 02011 // Fix the selected best coefficient 02012 //fixCurrentMaxCoefficient(best_variable, best_coefficient); 02013 } 02014 02015 Expr TheoryArithOld::pickMonomial(const Expr& right) 02016 { 02017 DebugAssert(isPlus(right), "TheoryArithOld::pickMonomial: Wrong Kind: " + 02018 right.toString()); 02019 if(theoryCore()->getFlags()["var-order"].getBool()) { 02020 Expr::iterator i = right.begin(); 02021 Expr isolatedMonomial = right[1]; 02022 //PLUS always has at least two elements and the first element is 02023 //always a constant. hence ++i in the initialization of the for 02024 //loop. 02025 for(++i; i != right.end(); ++i) 02026 if(lessThanVar(isolatedMonomial,*i)) 02027 isolatedMonomial = *i; 02028 return isolatedMonomial; 02029 } 02030 02031 ExprMap<Expr> var2monomial; 02032 vector<Expr> vars; 02033 Expr::iterator i = right.begin(), iend = right.end(); 02034 for(;i != iend; ++i) { 02035 if(i->isRational()) 02036 continue; 02037 Expr c, var; 02038 separateMonomial(*i, c, var); 02039 var2monomial[var] = *i; 02040 vars.push_back(var); 02041 } 02042 02043 vector<Expr> largest; 02044 d_graph.selectLargest(vars, largest); 02045 DebugAssert(0 < largest.size(), 02046 "TheoryArithOld::pickMonomial: selectLargest: failed!!!!"); 02047 02048 // DEJAN: Rafine the largest by coefficient values 02049 vector<Expr> largest_small_coeff; 02050 selectSmallestByCoefficient(largest, largest_small_coeff); 02051 DebugAssert(0 < largest_small_coeff.size(), "TheoryArithOld::pickMonomial: selectLargestByCOefficient: failed!!!!"); 02052 02053 size_t pickedVar = 0; 02054 // Pick the variable which will generate the fewest number of 02055 // projections 02056 02057 size_t size = largest_small_coeff.size(); 02058 int minProjections = -1; 02059 if (size > 1) 02060 for(size_t k=0; k< size; ++k) { 02061 const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]); 02062 // Grab the counters for the variable 02063 int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0; 02064 int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0; 02065 int n(nRight*nLeft); 02066 TRACE("arith ineq", "pickMonomial: var=", var, 02067 ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft)); 02068 if(minProjections < 0 || minProjections > n) { 02069 minProjections = n; 02070 pickedVar = k; 02071 } 02072 TRACE("arith ineq", "Number of projections for "+var.toString()+" = ", n, ""); 02073 } 02074 02075 02076 const Expr& largestVar = largest_small_coeff[pickedVar]; 02077 // FIXME: TODO: update the counters (subtract counts for the vars 02078 // other than largestVar 02079 02080 // Update the graph (all edges to the largest in the graph, not just the small coefficients). 02081 for(size_t k = 0; k < vars.size(); ++k) { 02082 if(vars[k] != largestVar) 02083 d_graph.addEdge(largestVar, vars[k]); 02084 } 02085 02086 TRACE("arith buffer", "picked var : ", var2monomial[largestVar].toString(), ""); 02087 02088 return var2monomial[largestVar]; 02089 } 02090 02091 void TheoryArithOld::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2) 02092 { 02093 TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")"); 02094 DebugAssert(e1 != e2, "TheoryArithOld::VarOrderGraph::addEdge(" 02095 +e1.toString()+", "+e2.toString()+")"); 02096 d_edges[e1].push_back(e2); 02097 } 02098 02099 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not 02100 //comparable) 02101 bool TheoryArithOld::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2) 02102 { 02103 d_cache.clear(); 02104 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2 02105 return dfs(e1,e2); 02106 } 02107 02108 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2 02109 bool TheoryArithOld::VarOrderGraph::dfs(const Expr& e1, const Expr& e2) 02110 { 02111 if(e1 == e2) 02112 return true; 02113 if(d_cache.count(e2) > 0) 02114 return false; 02115 if(d_edges.count(e2) == 0) 02116 return false; 02117 d_cache[e2] = true; 02118 vector<Expr>& e2Edges = d_edges[e2]; 02119 vector<Expr>::iterator i = e2Edges.begin(); 02120 vector<Expr>::iterator iend = e2Edges.end(); 02121 //if dfs finds e1 then i != iend else i is equal to iend 02122 for(; i != iend && !dfs(e1,*i); ++i); 02123 return (i != iend); 02124 } 02125 02126 void TheoryArithOld::VarOrderGraph::dfs(const Expr& v, vector<Expr>& output_list) 02127 { 02128 TRACE("arith shared", "dfs(", v.toString(), ")"); 02129 02130 // If visited already we are done 02131 if (d_cache.count(v) > 0) return; 02132 02133 // Dfs further 02134 if(d_edges.count(v) != 0) { 02135 // We have edges, so lets dfs it further 02136 vector<Expr>& vEdges = d_edges[v]; 02137 vector<Expr>::iterator e = vEdges.begin(); 02138 vector<Expr>::iterator e_end = vEdges.end(); 02139 while (e != e_end) { 02140 dfs(*e, output_list); 02141 e ++; 02142 } 02143 } 02144 02145 // Mark as visited and add to the output list 02146 d_cache[v] = true; 02147 output_list.push_back(v); 02148 } 02149 02150 void TheoryArithOld::VarOrderGraph::getVerticesTopological(vector<Expr>& output_list) 02151 { 02152 // Clear the cache 02153 d_cache.clear(); 02154 output_list.clear(); 02155 02156 // Go through all the vertices and run a dfs from them 02157 ExprMap< vector<Expr> >::iterator v_it = d_edges.begin(); 02158 ExprMap< vector<Expr> >::iterator v_it_end = d_edges.end(); 02159 while (v_it != v_it_end) 02160 { 02161 // Run dfs from this vertex 02162 dfs(v_it->first, output_list); 02163 // Go to the next one 02164 v_it ++; 02165 } 02166 } 02167 02168 void TheoryArithOld::VarOrderGraph::selectSmallest(vector<Expr>& v1, 02169 vector<Expr>& v2) 02170 { 02171 int v1Size = v1.size(); 02172 vector<bool> v3(v1Size); 02173 for(int j=0; j < v1Size; ++j) 02174 v3[j] = false; 02175 02176 for(int j=0; j < v1Size; ++j) { 02177 if(v3[j]) continue; 02178 for(int i =0; i < v1Size; ++i) { 02179 if((i == j) || v3[i]) 02180 continue; 02181 if(lessThan(v1[i],v1[j])) { 02182 v3[j] = true; 02183 break; 02184 } 02185 } 02186 } 02187 vector<Expr> new_v1; 02188 02189 for(int j = 0; j < v1Size; ++j) 02190 if(!v3[j]) v2.push_back(v1[j]); 02191 else new_v1.push_back(v1[j]); 02192 v1 = new_v1; 02193 } 02194 02195 02196 void TheoryArithOld::VarOrderGraph::selectLargest(const vector<Expr>& v1, 02197 vector<Expr>& v2) 02198 { 02199 int v1Size = v1.size(); 02200 vector<bool> v3(v1Size); 02201 for(int j=0; j < v1Size; ++j) 02202 v3[j] = false; 02203 02204 for(int j=0; j < v1Size; ++j) { 02205 if(v3[j]) continue; 02206 for(int i =0; i < v1Size; ++i) { 02207 if((i == j) || v3[i]) 02208 continue; 02209 if(lessThan(v1[j],v1[i])) { 02210 v3[j] = true; 02211 break; 02212 } 02213 } 02214 } 02215 02216 for(int j = 0; j < v1Size; ++j) 02217 if(!v3[j]) v2.push_back(v1[j]); 02218 } 02219 02220 /////////////////////////////////////////////////////////////////////////////// 02221 // TheoryArithOld Public Methods // 02222 /////////////////////////////////////////////////////////////////////////////// 02223 02224 02225 TheoryArithOld::TheoryArithOld(TheoryCore* core) 02226 : TheoryArith(core, "ArithmeticOld"), 02227 d_diseq(core->getCM()->getCurrentContext()), 02228 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0), 02229 diseqSplitAlready(core->getCM()->getCurrentContext()), 02230 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0), 02231 d_freeConstDB(core->getCM()->getCurrentContext()), 02232 d_buffer_0(core->getCM()->getCurrentContext()), 02233 d_buffer_1(core->getCM()->getCurrentContext()), 02234 d_buffer_2(core->getCM()->getCurrentContext()), 02235 d_buffer_3(core->getCM()->getCurrentContext()), 02236 // Initialize index to 0 at scope 0 02237 d_bufferIdx_0(core->getCM()->getCurrentContext(), 0, 0), 02238 d_bufferIdx_1(core->getCM()->getCurrentContext(), 0, 0), 02239 d_bufferIdx_2(core->getCM()->getCurrentContext(), 0, 0), 02240 d_bufferIdx_3(core->getCM()->getCurrentContext(), 0, 0), 02241 diff_logic_size(core->getCM()->getCurrentContext(), 0, 0), 02242 d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())), 02243 d_splitSign(&(core->getFlags()["nonlinear-sign-split"].getBool())), 02244 d_grayShadowThres(&(core->getFlags()["grayshadow-threshold"].getInt())), 02245 d_countRight(core->getCM()->getCurrentContext()), 02246 d_countLeft(core->getCM()->getCurrentContext()), 02247 d_sharedTerms(core->getCM()->getCurrentContext()), 02248 d_sharedTermsList(core->getCM()->getCurrentContext()), 02249 d_sharedVars(core->getCM()->getCurrentContext()), 02250 bufferedInequalities(core->getCM()->getCurrentContext()), 02251 termLowerBound(core->getCM()->getCurrentContext()), 02252 termLowerBoundThm(core->getCM()->getCurrentContext()), 02253 termUpperBound(core->getCM()->getCurrentContext()), 02254 termUpperBoundThm(core->getCM()->getCurrentContext()), 02255 alreadyProjected(core->getCM()->getCurrentContext()), 02256 dontBuffer(core->getCM()->getCurrentContext()), 02257 diffLogicOnly(core->getCM()->getCurrentContext(), true, 0), 02258 diffLogicGraph(0, core, 0, core->getCM()->getCurrentContext()), 02259 shared_index_1(core->getCM()->getCurrentContext(), 0, 0), 02260 shared_index_2(core->getCM()->getCurrentContext(), 0, 0), 02261 termUpperBounded(core->getCM()->getCurrentContext()), 02262 termLowerBounded(core->getCM()->getCurrentContext()), 02263 termConstrainedBelow(core->getCM()->getCurrentContext()), 02264 termConstrainedAbove(core->getCM()->getCurrentContext()) 02265 { 02266 IF_DEBUG(d_diseq.setName("CDList[TheoryArithOld::d_diseq]");) 02267 IF_DEBUG(d_buffer_0.setName("CDList[TheoryArithOld::d_buffer_0]");) 02268 IF_DEBUG(d_buffer_1.setName("CDList[TheoryArithOld::d_buffer_1]");) 02269 IF_DEBUG(d_buffer_2.setName("CDList[TheoryArithOld::d_buffer_2]");) 02270 IF_DEBUG(d_buffer_3.setName("CDList[TheoryArithOld::d_buffer_3]");) 02271 IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_0]");) 02272 IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_1]");) 02273 IF_DEBUG(d_bufferIdx_2.setName("CDList[TheoryArithOld::d_bufferIdx_2]");) 02274 IF_DEBUG(d_bufferIdx_3.setName("CDList[TheoryArithOld::d_bufferIdx_3]");) 02275 02276 getEM()->newKind(REAL, "_REAL", true); 02277 getEM()->newKind(INT, "_INT", true); 02278 getEM()->newKind(SUBRANGE, "_SUBRANGE", true); 02279 02280 getEM()->newKind(UMINUS, "_UMINUS"); 02281 getEM()->newKind(PLUS, "_PLUS"); 02282 getEM()->newKind(MINUS, "_MINUS"); 02283 getEM()->newKind(MULT, "_MULT"); 02284 getEM()->newKind(DIVIDE, "_DIVIDE"); 02285 getEM()->newKind(POW, "_POW"); 02286 getEM()->newKind(INTDIV, "_INTDIV"); 02287 getEM()->newKind(MOD, "_MOD"); 02288 getEM()->newKind(LT, "_LT"); 02289 getEM()->newKind(LE, "_LE"); 02290 getEM()->newKind(GT, "_GT"); 02291 getEM()->newKind(GE, "_GE"); 02292 getEM()->newKind(IS_INTEGER, "_IS_INTEGER"); 02293 getEM()->newKind(NEGINF, "_NEGINF"); 02294 getEM()->newKind(POSINF, "_POSINF"); 02295 getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW"); 02296 getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW"); 02297 02298 getEM()->newKind(REAL_CONST, "_REAL_CONST"); 02299 02300 d_kinds.push_back(REAL); 02301 d_kinds.push_back(INT); 02302 d_kinds.push_back(SUBRANGE); 02303 d_kinds.push_back(IS_INTEGER); 02304 d_kinds.push_back(UMINUS); 02305 d_kinds.push_back(PLUS); 02306 d_kinds.push_back(MINUS); 02307 d_kinds.push_back(MULT); 02308 d_kinds.push_back(DIVIDE); 02309 d_kinds.push_back(POW); 02310 d_kinds.push_back(INTDIV); 02311 d_kinds.push_back(MOD); 02312 d_kinds.push_back(LT); 02313 d_kinds.push_back(LE); 02314 d_kinds.push_back(GT); 02315 d_kinds.push_back(GE); 02316 d_kinds.push_back(RATIONAL_EXPR); 02317 d_kinds.push_back(NEGINF); 02318 d_kinds.push_back(POSINF); 02319 d_kinds.push_back(DARK_SHADOW); 02320 d_kinds.push_back(GRAY_SHADOW); 02321 d_kinds.push_back(REAL_CONST); 02322 02323 registerTheory(this, d_kinds, true); 02324 02325 d_rules = createProofRulesOld(); 02326 diffLogicGraph.setRules(d_rules); 02327 diffLogicGraph.setArith(this); 02328 02329 d_realType = Type(getEM()->newLeafExpr(REAL)); 02330 d_intType = Type(getEM()->newLeafExpr(INT)); 02331 02332 // Make the zero variable 02333 Theorem thm_exists_zero = getCommonRules()->varIntroSkolem(rat(0)); 02334 zero = thm_exists_zero.getExpr()[1]; 02335 } 02336 02337 02338 // Destructor: delete the proof rules class if it's present 02339 TheoryArithOld::~TheoryArithOld() { 02340 if(d_rules != NULL) delete d_rules; 02341 // Clear the inequality databases 02342 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(), 02343 iend=d_inequalitiesRightDB.end(); i!=iend; ++i) { 02344 delete (i->second); 02345 free(i->second); 02346 } 02347 for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(), 02348 iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) { 02349 delete (i->second); 02350 free (i->second); 02351 } 02352 unregisterTheory(this, d_kinds, true); 02353 } 02354 02355 void TheoryArithOld::collectVars(const Expr& e, vector<Expr>& vars, 02356 set<Expr>& cache) { 02357 // Check the cache first 02358 if(cache.count(e) > 0) return; 02359 // Not processed yet. Cache the expression and proceed 02360 cache.insert(e); 02361 if(isLeaf(e)) vars.push_back(e); 02362 else 02363 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 02364 collectVars(*i, vars, cache); 02365 } 02366 02367 void 02368 TheoryArithOld::processFiniteInterval 02369 (const Theorem& alphaLEax, 02370 const Theorem& bxLEbeta) { 02371 const Expr& ineq1(alphaLEax.getExpr()); 02372 const Expr& ineq2(bxLEbeta.getExpr()); 02373 DebugAssert(isLE(ineq1), "TheoryArithOld::processFiniteInterval: ineq1 = " 02374 +ineq1.toString()); 02375 DebugAssert(isLE(ineq2), "TheoryArithOld::processFiniteInterval: ineq2 = " 02376 +ineq2.toString()); 02377 // If the inequalities are not integer, just return (nothing to do) 02378 if(!isInteger(ineq1[0]) 02379 || !isInteger(ineq1[1]) 02380 || !isInteger(ineq2[0]) 02381 || !isInteger(ineq2[1])) 02382 return; 02383 02384 const Expr& ax = ineq1[1]; 02385 const Expr& bx = ineq2[0]; 02386 DebugAssert(!isPlus(ax) && !isRational(ax), 02387 "TheoryArithOld::processFiniteInterval:\n ax = "+ax.toString()); 02388 DebugAssert(!isPlus(bx) && !isRational(bx), 02389 "TheoryArithOld::processFiniteInterval:\n bx = "+bx.toString()); 02390 Expr a = isMult(ax)? ax[0] : rat(1); 02391 Expr b = isMult(bx)? bx[0] : rat(1); 02392 02393 Theorem thm1(alphaLEax), thm2(bxLEbeta); 02394 // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary 02395 if(a != b) { 02396 thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b))); 02397 thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a))); 02398 } 02399 // Check that a*beta - b*alpha == c > 0 02400 const Expr& alphaLEt = thm1.getExpr(); 02401 const Expr& alpha = alphaLEt[0]; 02402 const Expr& t = alphaLEt[1]; 02403 const Expr& beta = thm2.getExpr()[1]; 02404 Expr c = canon(beta - alpha).getRHS(); 02405 02406 if(c.isRational() && c.getRational() >= 1) { 02407 // This is a finite interval. First, derive t <= alpha + c: 02408 // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c 02409 // Then substitute that in thm2 02410 Theorem bEQac = symmetryRule(canon(alpha + c)); 02411 // Substitute beta == alpha+c for the second child of thm2 02412 vector<unsigned> changed; 02413 vector<Theorem> thms; 02414 changed.push_back(1); 02415 thms.push_back(bEQac); 02416 Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms); 02417 tLEac = iffMP(thm2, tLEac); 02418 // Derive and enqueue the finite interval constraint 02419 Theorem isInta(isIntegerThm(alpha)); 02420 Theorem isIntt(isIntegerThm(t)); 02421 if (d_sharedTerms.find(thm1.getExpr()[1]) != d_sharedTerms.end()) 02422 enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt)); 02423 } 02424 } 02425 02426 02427 void 02428 TheoryArithOld::processFiniteIntervals(const Expr& x) { 02429 // If x is not integer, do not bother 02430 if(!isInteger(x)) return; 02431 // Process every pair of the opposing inequalities for 'x' 02432 ExprMap<CDList<Ineq> *>::iterator iLeft, iRight; 02433 iLeft = d_inequalitiesLeftDB.find(x); 02434 if(iLeft == d_inequalitiesLeftDB.end()) return; 02435 iRight = d_inequalitiesRightDB.find(x); 02436 if(iRight == d_inequalitiesRightDB.end()) return; 02437 // There are some opposing inequalities; get the lists 02438 CDList<Ineq>& ineqsLeft = *(iLeft->second); 02439 CDList<Ineq>& ineqsRight = *(iRight->second); 02440 // Get the sizes of the lists 02441 size_t sizeLeft = ineqsLeft.size(); 02442 size_t sizeRight = ineqsRight.size(); 02443 // Process all the pairs of the opposing inequalities 02444 for(size_t l=0; l<sizeLeft; ++l) 02445 for(size_t r=0; r<sizeRight; ++r) 02446 processFiniteInterval(ineqsRight[r], ineqsLeft[l]); 02447 } 02448 02449 /*! This function recursively decends expression tree <strong>without 02450 * caching</strong> until it hits a node that is already setup. Be 02451 * careful on what expressions you are calling it. 02452 */ 02453 void 02454 TheoryArithOld::setupRec(const Expr& e) { 02455 if(e.hasFind()) return; 02456 // First, set up the kids recursively 02457 for (int k = 0; k < e.arity(); ++k) { 02458 setupRec(e[k]); 02459 } 02460 // Create a find pointer for e 02461 e.setFind(reflexivityRule(e)); 02462 e.setEqNext(reflexivityRule(e)); 02463 // And call our own setup() 02464 setup(e); 02465 } 02466 02467 02468 void TheoryArithOld::addSharedTerm(const Expr& e) { 02469 if (d_sharedTerms.find(e) == d_sharedTerms.end()) { 02470 d_sharedTerms[e] = true; 02471 d_sharedTermsList.push_back(e); 02472 02473 // if (!isIntegerThm(e).isNull()) { 02474 // int i, size = d_sharedTermsList.size(); 02475 // for (i = 0; i < size - 1; i ++) { 02476 // Expr e2 = d_sharedTermsList[i]; 02477 // if (!isIntegerThm(e2).isNull()) 02478 // if (!find(e).getRHS().isRational() || !find(e2).getRHS().isRational()) 02479 // addSplitter(e.eqExpr(e2)); 02480 // } 02481 // } 02482 } 02483 } 02484 02485 02486 void TheoryArithOld::assertFact(const Theorem& e) 02487 { 02488 TRACE("arith assert", "assertFact(", e.getExpr().toString(), ")"); 02489 02490 // Pick up any multiplicative case splits and enqueue them 02491 for (unsigned i = 0; i < multiplicativeSignSplits.size(); i ++) 02492 enqueueFact(multiplicativeSignSplits[i]); 02493 multiplicativeSignSplits.clear(); 02494 02495 const Expr& expr = e.getExpr(); 02496 if (expr.isNot() && expr[0].isEq()) { 02497 IF_DEBUG(debugger.counter("[arith] received disequalities")++;) 02498 02499 // Expr eq = expr[0]; 02500 // 02501 // // We want to expand on difference logic disequalities as soon as possible 02502 // bool diff_logic = false; 02503 // if (eq[1].isRational() && eq[1].getRational() == 0) { 02504 // if (!isPlus(eq[0])) { 02505 // if (isLeaf(eq[0])) diff_logic = true; 02506 // } 02507 // else { 02508 // int arity = eq[0].arity(); 02509 // if (arity <= 2) { 02510 // if (eq[0][0].isRational()) 02511 // diff_logic = true; 02512 // else { 02513 // Expr ax = eq[0][0], a, x; 02514 // Expr by = eq[0][1], b, y; 02515 // separateMonomial(ax, a, x); 02516 // separateMonomial(by, b, y); 02517 // if (isLeaf(x) && isLeaf(y)) 02518 // if ((a.getRational() == 1 && b.getRational() == -1) || 02519 // (a.getRational() == -1 && b.getRational() == 1)) 02520 // diff_logic = true; 02521 // } 02522 // } 02523 // if (arity == 3 && eq[0][0].isRational()) { 02524 // Expr ax = eq[0][1], a, x; 02525 // Expr by = eq[0][2], b, y; 02526 // separateMonomial(ax, a, x); 02527 // separateMonomial(by, b, y); 02528 // if (isLeaf(x) && isLeaf(y)) 02529 // if ((a.getRational() == 1 && b.getRational() == -1) || 02530 // (a.getRational() == -1 && b.getRational() == 1)) 02531 // diff_logic = true; 02532 // } 02533 // } 02534 // } 02535 // 02536 // if (diff_logic) 02537 // enqueueFact(d_rules->diseqToIneq(e)); 02538 // else 02539 d_diseq.push_back(e); 02540 } 02541 else if (!expr.isEq()){ 02542 if (expr.isNot()) { 02543 // If expr[0] is asserted to *not* be an integer, we track it 02544 // so we will detect if it ever becomes equal to an integer. 02545 if (expr[0].getKind() == IS_INTEGER) { 02546 expr[0][0].addToNotify(this, expr[0]); 02547 } 02548 // This can only be negation of dark or gray shadows, or 02549 // disequalities, which we ignore. Negations of inequalities 02550 // are handled in rewrite, we don't even receive them here. 02551 02552 // if (isGrayShadow(expr[0])) { 02553 // TRACE("arith gray", "expanding ", expr.toString(), ""); 02554 // Theorem expand = d_rules->expandGrayShadowRewrite(expr[0]); 02555 // enqueueFact(iffMP(e, substitutivityRule(expr, 0, expand))); 02556 // } 02557 02558 } 02559 else if(isDarkShadow(expr)) { 02560 enqueueFact(d_rules->expandDarkShadow(e)); 02561 IF_DEBUG(debugger.counter("received DARK_SHADOW")++;) 02562 } 02563 else if(isGrayShadow(expr)) { 02564 IF_DEBUG(debugger.counter("received GRAY_SHADOW")++;) 02565 const Rational& c1 = expr[2].getRational(); 02566 const Rational& c2 = expr[3].getRational(); 02567 02568 // If gray shadow bigger than the treshold, we are done 02569 if (*d_grayShadowThres > -1 && (c2 - c1 > *d_grayShadowThres)) { 02570 setIncomplete("Some gray shadows ignored due to threshold"); 02571 return; 02572 } 02573 02574 const Expr& v = expr[0]; 02575 const Expr& ee = expr[1]; 02576 if(c1 == c2) 02577 enqueueFact(d_rules->expandGrayShadow0(e)); 02578 else { 02579 Theorem gThm(e); 02580 // Check if we can reduce the number of cases in G(ax,c,c1,c2) 02581 if(ee.isRational() && isMult(v) 02582 && v[0].isRational() && v[0].getRational() >= 2) { 02583 IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++;) 02584 gThm = d_rules->grayShadowConst(e); 02585 } 02586 // (Possibly) new gray shadow 02587 const Expr& g = gThm.getExpr(); 02588 if(g.isFalse()) 02589 setInconsistent(gThm); 02590 else if(g[2].getRational() == g[3].getRational()) 02591 enqueueFact(d_rules->expandGrayShadow0(gThm)); 02592 else if(g[3].getRational() - g[2].getRational() <= 5) { 02593 // Assert c1+e <= v <= c2+e 02594 enqueueFact(d_rules->expandGrayShadow(gThm)); 02595 // Split G into 2 cases x = l_bound and the other 02596 Theorem thm2 = d_rules->splitGrayShadowSmall(gThm); 02597 enqueueFact(thm2); 02598 } 02599 else { 02600 // Assert c1+e <= v <= c2+e 02601 enqueueFact(d_rules->expandGrayShadow(gThm)); 02602 // Split G into 2 cases (binary search b/w c1 and c2) 02603 Theorem thm2 = d_rules->splitGrayShadow(gThm); 02604 enqueueFact(thm2); 02605 // Fetch the two gray shadows 02606 // DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2, 02607 // "thm2 = "+thm2.getExpr().toString()); 02608 // const Expr& G1orG2 = thm2.getExpr()[0]; 02609 // DebugAssert(G1orG2.isOr() && G1orG2.arity()==2, 02610 // "G1orG2 = "+G1orG2.toString()); 02611 // const Expr& G1 = G1orG2[0]; 02612 // const Expr& G2 = G1orG2[1]; 02613 // DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString()); 02614 // DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString()); 02615 // // Split on the left disjunct first (keep the priority low) 02616 // Expr tmp = simplifyExpr(G1); 02617 // if (!tmp.isBoolConst()) 02618 // addSplitter(tmp, 1); 02619 // tmp = simplifyExpr(G2); 02620 // if (!tmp.isBoolConst()) 02621 // addSplitter(tmp, -1); 02622 } 02623 } 02624 } 02625 else { 02626 DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr), 02627 "expected LE or LT: "+expr.toString()); 02628 if(isLE(expr) || isLT(expr)) { 02629 IF_DEBUG(debugger.counter("recevied inequalities")++;) 02630 02631 // // Assert the equivalent negated inequality 02632 // Theorem thm; 02633 // if (isLE(expr)) thm = d_rules->negatedInequality(!gtExpr(expr[0],expr[1])); 02634 // else thm = d_rules->negatedInequality(!geExpr(expr[0],expr[1])); 02635 // thm = symmetryRule(thm); 02636 // Theorem thm2 = simplify(thm.getRHS()[0]); 02637 // DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite"); 02638 // thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2); 02639 // thm = transitivityRule(thm, thm2); 02640 // enqueueFact(iffMP(e, thm)); 02641 02642 // Buffer the inequality 02643 addToBuffer(e); 02644 02645 unsigned total_buf_size = d_buffer_0.size() + d_buffer_1.size() + d_buffer_2.size() + d_buffer_3.size(); 02646 unsigned processed = d_bufferIdx_0 + d_bufferIdx_1 + d_bufferIdx_2 + d_bufferIdx_3; 02647 TRACE("arith ineq", "buffer.size() = ", total_buf_size, 02648 ", index="+int2string(processed) 02649 +", threshold="+int2string(*d_bufferThres)); 02650 02651 if(!diffLogicOnly && *d_bufferThres >= 0 && (total_buf_size > *d_bufferThres + processed) && !d_inModelCreation) { 02652 processBuffer(); 02653 } 02654 } else { 02655 IF_DEBUG(debugger.counter("arith IS_INTEGER")++;) 02656 if (!isInteger(expr[0])) { 02657 enqueueFact(d_rules->IsIntegerElim(e)); 02658 } 02659 } 02660 } 02661 } 02662 else { 02663 IF_DEBUG(debugger.counter("[arith] received t1=t2")++;) 02664 02665 // const Expr lhs = e.getExpr()[0]; 02666 // const Expr rhs = e.getExpr()[1]; 02667 // 02668 // CDMap<Expr, Rational>::iterator l_bound_find = termLowerBound[lhs]; 02669 // if (l_bound_find != termLowerBound.end()) { 02670 // Rational lhs_bound = (*l_bound_find).second; 02671 // CDMap<Expr, Rational>::iterator l_bound_find_rhs = termLowerBound[rhs]; 02672 // if (l_bound_find_rhs != termLowerBound.end()) { 02673 // 02674 // } else { 02675 // // Add the new bound for the rhs 02676 // termLowerBound[rhs] = lhs_bound; 02677 // termLowerBoundThm = 02678 // } 02679 // 02680 // } 02681 02682 02683 } 02684 } 02685 02686 02687 void TheoryArithOld::checkSat(bool fullEffort) 02688 { 02689 // vector<Expr>::const_iterator e; 02690 // vector<Expr>::const_iterator eEnd; 02691 // TODO: convert back to use iterators 02692 TRACE("arith checksat", "checksat(fullEffort = ", fullEffort? "true, modelCreation = " : "false, modelCreation = ", (d_inModelCreation ? "true)" : "false)")); 02693 TRACE("arith ineq", "TheoryArithOld::checkSat(fullEffort=", 02694 fullEffort? "true" : "false", ")"); 02695 if (fullEffort) { 02696 02697 // Process the buffer if necessary 02698 if (!inconsistent()) 02699 processBuffer(); 02700 02701 // Expand the needded inequalitites 02702 int total_buffer_size = d_buffer_0.size() + d_buffer_1.size() + d_buffer_2.size() + d_buffer_3.size(); 02703 02704 int constrained_vars = 0; 02705 if (!inconsistent() && total_buffer_size > 0) 02706 constrained_vars = computeTermBounds(); 02707 02708 bool something_enqueued = false; 02709 02710 if (d_inModelCreation || (!inconsistent() && total_buffer_size > 0 && constrained_vars > 0)) { 02711 // If in model creation we might have to reconsider some of the dis-equalities 02712 if (d_inModelCreation) d_diseqIdx = 0; 02713 02714 // Now go and try to split 02715 for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) { 02716 TRACE("model", "[arith] refining diseq: ", d_diseq[d_diseqIdx].getExpr() , ""); 02717 02718 // Get the disequality theorem and the expression 02719 Theorem diseqThm = d_diseq[d_diseqIdx]; 02720 Expr diseq = diseqThm.getExpr(); 02721 02722 // If we split on this one already 02723 if (diseqSplitAlready.find(diseq) != diseqSplitAlready.end()) continue; 02724 02725 // Get the equality 02726 Expr eq = diseq[0]; 02727 02728 // Get the left-hand-side and the right-hands side 02729 Expr lhs = eq[0]; 02730 Expr rhs = eq[1]; 02731 DebugAssert(lhs.hasFind() && rhs.hasFind(), "Part of dis-equality has no find!"); 02732 lhs = find(lhs).getRHS(); 02733 rhs = find(rhs).getRHS(); 02734 02735 // If the value of the equality is already determined by instantiation, we just skip it 02736 // This can happen a lot as we infer equalities in difference logic 02737 if (lhs.isRational() && rhs.isRational()) { 02738 TRACE("arith diseq", "disequality already evaluated : ", diseq.toString(), ""); 02739 continue; 02740 } 02741 02742 // We can allow ourselfs not to care about specific values if we are 02743 // not in model creation 02744 if (!d_inModelCreation) { 02745 // If the left or the right hand side is unbounded, we don't care right now 02746 if (!isConstrained(lhs) || !isConstrained(rhs)) continue; 02747 if (getUpperBound(lhs) < getLowerBound(rhs)) continue; 02748 if (getUpperBound(rhs) < getLowerBound(lhs)) continue; 02749 } 02750 02751 TRACE("arith ineq", "[arith] refining diseq: ", d_diseq[d_diseqIdx].getExpr() , ""); 02752 02753 // We don't know the value of the disequlaity, split on it (for now) 02754 enqueueFact(d_rules->diseqToIneq(diseqThm)); 02755 something_enqueued = true; 02756 02757 // Mark it as split already 02758 diseqSplitAlready[diseq] = true; 02759 } 02760 } 02761 02762 // Split on shared term equalities 02763 if (!something_enqueued && !inconsistent() && total_buffer_size > 0 && constrained_vars > 0) { 02764 unsigned size = d_sharedTermsList.size(); 02765 02766 Expr t1, t2; 02767 Expr t1_find, t2_find; 02768 02769 TRACE("arith shared", "expanding on shared term equalities","",""); 02770 02771 TheoryArithOld::DifferenceLogicGraph::EpsRational t1_find_lowerBound; 02772 TheoryArithOld::DifferenceLogicGraph::EpsRational t1_find_upperBound; 02773 02774 // start from (0, 0) 02775 if (shared_index_1 < size) { 02776 t1 = d_sharedTermsList[shared_index_1]; 02777 DebugAssert(!t1.isNull(), "t1 is null!"); 02778 DebugAssert(t1.hasFind(), "t1 has no find"); 02779 t1_find = find(t1).getRHS(); 02780 t1_find_lowerBound = getLowerBound(t1_find); 02781 t1_find_upperBound = getUpperBound(t1_find); 02782 } 02783 while (!something_enqueued && !inconsistent() && shared_index_1 < size) { 02784 02785 // Take the next t2 02786 shared_index_2 = shared_index_2 + 1; 02787 02788 // If off limits, move on t1 02789 if (shared_index_2 >= shared_index_1 || t1_find != t1 || !isConstrained(t1_find)) { 02790 // Take the fist t2 02791 shared_index_2 = 0; 02792 t2 = d_sharedTermsList[0]; 02793 DebugAssert(!t2.isNull(), "t2 is null!"); 02794 02795 // Take the next t1 02796 shared_index_1 = shared_index_1 + 1; 02797 while (shared_index_1 < size) { 02798 t1 = d_sharedTermsList[shared_index_1]; 02799 DebugAssert(!t1.isNull(), "t1 is null!"); 02800 DebugAssert(t1.hasFind(), "t1 has no find"); 02801 t1_find = find(t1).getRHS(); 02802 if (t1_find != t1 || !isConstrained(t1_find)) { 02803 shared_index_1 = shared_index_1 + 1; 02804 continue; 02805 } else { 02806 t1_find_lowerBound = getLowerBound(t1_find); 02807 t1_find_upperBound = getUpperBound(t1_find); 02808 break; 02809 } 02810 } 02811 if (shared_index_1 >= size) break; 02812 } else { 02813 t2 = d_sharedTermsList[shared_index_2]; 02814 DebugAssert(!t2.isNull(), "t2 is null!"); 02815 } 02816 02817 TRACE("arith shared", "comparing : ", int2string(shared_index_1) + " with", int2string(shared_index_2)); 02818 02819 DebugAssert(t2.hasFind(), "t2 has no find"); 02820 t2_find = find(t2).getRHS(); 02821 if (t2_find != t2) continue; 02822 if (t2_find == t1_find) continue; 02823 if (t2_find.isRational() && t1_find.isRational()) continue; 02824 if (!isConstrained(t2_find)) continue; 02825 if (getUpperBound(t2_find) < t1_find_lowerBound) continue; 02826 if (t1_find_upperBound < getLowerBound(t2_find)) continue; 02827 02828 TRACE("arith shared", "comparing : ", int2string(shared_index_1) + " with ", int2string(shared_index_2) + " (of " + int2string(size) + ")"); 02829 TRACE("arith shared", "checking shared term eq for ", t1.toString() + " and ", t2.toString()); 02830 02831 // Construct the equality disjunct if both are integers 02832 if (!isIntegerThm(t1_find).isNull() && !isIntegerThm(t2_find).isNull()) { 02833 // The equality 02834 Expr eq = t2_find.eqExpr(t1_find); 02835 // Try to simplify it to trivial 02836 Theorem simplifyEq = canonSimp(eq); 02837 if (simplifyEq.getRHS().isBoolConst()) { 02838 // It must not be true, false is possible due to asserted disequalities 02839 // Only exception are non-linear equalities which might be asserted 02840 DebugAssert(simplifyEq.getRHS().isFalse() || isNonlinearEq(eq), "Simplification of the shared equality is true!!!" + eq.toString()); 02841 continue; 02842 } 02843 // Add it if not trivial 02844 addSplitter(eq, 0); 02845 // We've enqueued something interesting 02846 something_enqueued = true; 02847 TRACE("arith shared", "adding shared term eq for ", eq.toString(), ""); 02848 } 02849 } 02850 } 02851 02852 IF_DEBUG( 02853 { 02854 bool dejans_printouts = false; 02855 if (dejans_printouts) { 02856 cerr << "Disequalities after CheckSat" << endl; 02857 for (unsigned i = 0; i < d_diseq.size(); i ++) { 02858 Expr diseq = d_diseq[i].getExpr(); 02859 Expr d_find = find(diseq[0]).getRHS(); 02860 cerr << diseq.toString() << ":" << d_find.toString() << endl; 02861 } 02862 cerr << "Arith Buffer after CheckSat (0)" << endl; 02863 for (unsigned i = 0; i < d_buffer_0.size(); i ++) { 02864 Expr ineq = d_buffer_0[i].getExpr(); 02865 Expr rhs = find(ineq[1]).getRHS(); 02866 cerr << ineq.toString() << ":" << rhs.toString() << endl; 02867 } 02868 cerr << "Arith Buffer after CheckSat (1)" << endl; 02869 for (unsigned i = 0; i < d_buffer_1.size(); i ++) { 02870 Expr ineq = d_buffer_1[i].getExpr(); 02871 Expr rhs = find(ineq[1]).getRHS(); 02872 cerr << ineq.toString() << ":" << rhs.toString() << endl; 02873 } 02874 cerr << "Arith Buffer after CheckSat (2)" << endl; 02875 for (unsigned i = 0; i < d_buffer_2.size(); i ++) { 02876 Expr ineq = d_buffer_2[i].getExpr(); 02877 Expr rhs = find(ineq[1]).getRHS(); 02878 cerr << ineq.toString() << ":" << rhs.toString() << endl; 02879 } 02880 cerr << "Arith Buffer after CheckSat (3)" << endl; 02881 for (unsigned i = 0; i < d_buffer_3.size(); i ++) { 02882 Expr ineq = d_buffer_3[i].getExpr(); 02883 Expr rhs = find(ineq[1]).getRHS(); 02884 cerr << ineq.toString() << ":" << rhs.toString() << endl; 02885 } 02886 } 02887 } 02888 ) 02889 } 02890 } 02891 02892 02893 02894 void TheoryArithOld::refineCounterExample() 02895 { 02896 d_inModelCreation = true; 02897 TRACE("model", "refineCounterExample[TheoryArithOld] ", "", "{"); 02898 CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2, 02899 iend = d_sharedTerms.end(); 02900 // Add equalities over all pairs of shared terms as suggested 02901 // splitters. Notice, that we want to split on equality 02902 // (positively) first, to reduce the size of the model. 02903 for(; it!=iend; ++it) { 02904 // Copy by value: the elements in the pair from *it are NOT refs in CDMap 02905 Expr e1 = (*it).first; 02906 for(it2 = it, ++it2; it2!=iend; ++it2) { 02907 Expr e2 = (*it2).first; 02908 DebugAssert(isReal(getBaseType(e1)), 02909 "TheoryArithOld::refineCounterExample: e1 = "+e1.toString() 02910 +"\n type(e1) = "+e1.getType().toString()); 02911 if(findExpr(e1) != findExpr(e2)) { 02912 DebugAssert(isReal(getBaseType(e2)), 02913 "TheoryArithOld::refineCounterExample: e2 = "+e2.toString() 02914 +"\n type(e2) = "+e2.getType().toString()); 02915 Expr eq = simplifyExpr(e1.eqExpr(e2)); 02916 if (!eq.isBoolConst()) { 02917 addSplitter(eq); 02918 } 02919 } 02920 } 02921 } 02922 TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}"); 02923 } 02924 02925 02926 void 02927 TheoryArithOld::findRationalBound(const Expr& varSide, const Expr& ratSide, 02928 const Expr& var, 02929 Rational &r) 02930 { 02931 Expr c, x; 02932 separateMonomial(varSide, c, x); 02933 02934 if (!findExpr(ratSide).isRational() && isNonlinearEq(ratSide.eqExpr(rat(0)))) 02935 throw ArithException("Could not generate the model due to non-linear arithmetic"); 02936 02937 DebugAssert(findExpr(c).isRational(), 02938 "seperateMonomial failed"); 02939 DebugAssert(findExpr(ratSide).isRational(), 02940 "smallest variable in graph, should not have variables" 02941 " in inequalities: "); 02942 DebugAssert(x == var, "separateMonomial found different variable: " 02943 + var.toString()); 02944 r = findExpr(ratSide).getRational() / findExpr(c).getRational(); 02945 } 02946 02947 bool 02948 TheoryArithOld::findBounds(const Expr& e, Rational& lub, Rational& glb) 02949 { 02950 bool strictLB=false, strictUB=false; 02951 bool right = (d_inequalitiesRightDB.count(e) > 0 02952 && d_inequalitiesRightDB[e]->size() > 0); 02953 bool left = (d_inequalitiesLeftDB.count(e) > 0 02954 && d_inequalitiesLeftDB[e]->size() > 0); 02955 int numRight = 0, numLeft = 0; 02956 if(right) { //rationals less than e 02957 CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e]; 02958 for(unsigned int i=0; i<ratsLTe->size(); i++) { 02959 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!"); 02960 Expr ineq = (*ratsLTe)[i].ineq().getExpr(); 02961 Expr leftSide = ineq[0], rightSide = ineq[1]; 02962 Rational r; 02963 findRationalBound(rightSide, leftSide, e , r); 02964 if(numRight==0 || r>glb){ 02965 glb = r; 02966 strictLB = isLT(ineq); 02967 } 02968 numRight++; 02969 } 02970 TRACE("model", " =>Lower bound ", glb.toString(), ""); 02971 } 02972 if(left) { //rationals greater than e 02973 CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e]; 02974 for(unsigned int i=0; i<ratsGTe->size(); i++) { 02975 DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!"); 02976 Expr ineq = (*ratsGTe)[i].ineq().getExpr(); 02977 Expr leftSide = ineq[0], rightSide = ineq[1]; 02978 Rational r; 02979 findRationalBound(leftSide, rightSide, e, r); 02980 if(numLeft==0 || r<lub) { 02981 lub = r; 02982 strictUB = isLT(ineq); 02983 } 02984 numLeft++; 02985 } 02986 TRACE("model", " =>Upper bound ", lub.toString(), ""); 02987 } 02988 if(!left && !right) { 02989 lub = 0; 02990 glb = 0; 02991 } 02992 if(!left && right) {lub = glb +2;} 02993 if(!right && left) {glb = lub-2;} 02994 DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller " 02995 "than least upper bound"); 02996 return strictLB; 02997 } 02998 02999 void TheoryArithOld::assignVariables(std::vector<Expr>&v) 03000 { 03001 int count = 0; 03002 03003 if (diffLogicOnly) 03004 { 03005 // Compute the model 03006 diffLogicGraph.computeModel(); 03007 // Get values for the variables 03008 for (unsigned i = 0; i < v.size(); i ++) { 03009 Expr x = v[i]; 03010 assignValue(x, rat(diffLogicGraph.getValuation(x))); 03011 } 03012 // Done 03013 return; 03014 } 03015 03016 while (v.size() > 0) 03017 { 03018 std::vector<Expr> bottom; 03019 d_graph.selectSmallest(v, bottom); 03020 TRACE("model", "Finding variables to assign. Iteration # ", count, ""); 03021 for(unsigned int i = 0; i<bottom.size(); i++) 03022 { 03023 Expr e = bottom[i]; 03024 TRACE("model", "Found: ", e, ""); 03025 // Check if it is already a concrete constant 03026 if(e.isRational()) continue; 03027 03028 Rational lub, glb; 03029 bool strictLB; 03030 strictLB = findBounds(e, lub, glb); 03031 Rational mid; 03032 if(isInteger(e)) { 03033 if(strictLB && glb.isInteger()) 03034 mid = glb + 1; 03035 else 03036 mid = ceil(glb); 03037 } 03038 else 03039 mid = (lub + glb)/2; 03040 03041 TRACE("model", "Assigning mid = ", mid, " {"); 03042 assignValue(e, rat(mid)); 03043 TRACE("model", "Assigned find(e) = ", findExpr(e), " }"); 03044 if(inconsistent()) return; // Punt immediately if failed 03045 } 03046 count++; 03047 } 03048 } 03049 03050 void TheoryArithOld::computeModelBasic(const std::vector<Expr>& v) 03051 { 03052 d_inModelCreation = true; 03053 vector<Expr> reps; 03054 TRACE("model", "Arith=>computeModel ", "", "{"); 03055 for(unsigned int i=0; i <v.size(); ++i) { 03056 const Expr& e = v[i]; 03057 if(findExpr(e) == e) { 03058 TRACE("model", "arith variable:", e , ""); 03059 reps.push_back(e); 03060 } 03061 else { 03062 TRACE("model", "arith variable:", e , ""); 03063 TRACE("model", " ==> is defined by: ", findExpr(e) , ""); 03064 } 03065 } 03066 assignVariables(reps); 03067 TRACE("model", "Arith=>computeModel", "", "}"); 03068 d_inModelCreation = false; 03069 } 03070 03071 // For any arith expression 'e', if the subexpressions are assigned 03072 // concrete values, then find(e) must already be a concrete value. 03073 void TheoryArithOld::computeModel(const Expr& e, vector<Expr>& vars) { 03074 DebugAssert(findExpr(e).isRational(), "TheoryArithOld::computeModel(" 03075 +e.toString()+")\n e is not assigned concrete value.\n" 03076 +" find(e) = "+findExpr(e).toString()); 03077 assignValue(simplify(e)); 03078 vars.push_back(e); 03079 } 03080 03081 Theorem TheoryArithOld::checkIntegerEquality(const Theorem& thm) { 03082 03083 // Check if this is a rewrite theorem 03084 bool rewrite = thm.isRewrite(); 03085 03086 // If it's an integer theorem, then rafine it to integer domain 03087 Expr eq = (rewrite ? thm.getRHS() : thm.getExpr()); 03088 03089 TRACE("arith rafine", "TheoryArithOld::checkIntegerEquality(", eq, ")"); 03090 DebugAssert(eq.getKind() == EQ, "checkIntegerEquality: must be an equality"); 03091 03092 // Trivial equalities, we don't care 03093 if (!isPlus(eq[1]) && !isPlus(eq[0])) return thm; 03094 Expr old_sum = (isPlus(eq[1]) ? eq[1] : eq[0]); 03095 03096 // Get the sum part 03097 vector<Expr> children; 03098 bool const_is_integer = true; // Assuming only one constant is present (canon called before this) 03099 for (int i = 0; i < old_sum.arity(); i ++) 03100 if (!old_sum[i].isRational()) 03101 children.push_back(old_sum[i]); 03102 else 03103 const_is_integer = old_sum[i].getRational().isInteger(); 03104 03105 // If the constants are integers, we don't care 03106 if (const_is_integer) return thm; 03107 03108 Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]); 03109 // Check for integer of the remainder of the sum 03110 Theorem isIntegerEquality = isIntegerThm(sum); 03111 // If it is an integer, it's unsat 03112 if (!isIntegerEquality.isNull()) { 03113 Theorem false_thm = d_rules->intEqualityRationalConstant(isIntegerEquality, eq); 03114 if (rewrite) return transitivityRule(thm, false_thm); 03115 else return iffMP(thm, false_thm); 03116 } 03117 else return thm; 03118 } 03119 03120 03121 Theorem TheoryArithOld::rafineInequalityToInteger(const Theorem& thm) { 03122 03123 // Check if this is a rewrite theorem 03124 bool rewrite = thm.isRewrite(); 03125 03126 // If it's an integer theorem, then rafine it to integer domain 03127 Expr ineq = (rewrite ? thm.getRHS() : thm.getExpr()); 03128 03129 TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger(", ineq, ")"); 03130 DebugAssert(isIneq(ineq), "rafineInequalityToInteger: must be an inequality"); 03131 03132 // Trivial inequalities are rafined 03133 // if (!isPlus(ineq[1])) return thm; 03134 03135 // Get the sum part 03136 vector<Expr> children; 03137 if (isPlus(ineq[1])) { 03138 for (int i = 0; i < ineq[1].arity(); i ++) 03139 if (!ineq[1][i].isRational()) 03140 children.push_back(ineq[1][i]); 03141 } else children.push_back(ineq[1]); 03142 03143 Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]); 03144 // Check for integer of the remainder of the sum 03145 Theorem isIntegerInequality = isIntegerThm(sum); 03146 // If it is an integer, do rafine it 03147 if (!isIntegerInequality.isNull()) { 03148 Theorem rafine = d_rules->rafineStrictInteger(isIntegerInequality, ineq); 03149 TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger()", "=>", rafine.getRHS()); 03150 if (rewrite) return canonPredEquiv(transitivityRule(thm, rafine)); 03151 else return canonPred(iffMP(thm, rafine)); 03152 } 03153 else return thm; 03154 } 03155 03156 03157 03158 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it 03159 * and returns a theorem to that effect. assumes e is non-trivial 03160 * i.e. e is not '0=const' or 'const=0' or '0 <= const' etc. 03161 */ 03162 Theorem TheoryArithOld::normalize(const Expr& e) { 03163 //e is an eqn or ineqn. e is not a trivial eqn or ineqn 03164 //trivial means 0 = const or 0 <= const. 03165 TRACE("arith normalize", "normalize(", e, ") {"); 03166 DebugAssert(e.isEq() || isIneq(e), 03167 "normalize: input must be Eq or Ineq: " + e.toString()); 03168 DebugAssert(!isIneq(e) || (0 == e[0].getRational()), 03169 "normalize: if (e is ineq) then e[0] must be 0" + 03170 e.toString()); 03171 if(e.isEq()) { 03172 if(e[0].isRational()) { 03173 DebugAssert(0 == e[0].getRational(), 03174 "normalize: if e is Eq and e[0] is rat then e[0]==0"); 03175 } 03176 else { 03177 //if e[0] is not rational then e[1] must be rational. 03178 DebugAssert(e[1].isRational() && 0 == e[1].getRational(), 03179 "normalize: if e is Eq and e[1] is rat then e[1]==0\n" 03180 " e = "+e.toString()); 03181 } 03182 } 03183 03184 Expr factor; 03185 if(e[0].isRational()) 03186 factor = computeNormalFactor(e[1], false); 03187 else 03188 factor = computeNormalFactor(e[0], false); 03189 03190 TRACE("arith normalize", "normalize: factor = ", factor, ""); 03191 DebugAssert(factor.getRational() > 0, 03192 "normalize: factor="+ factor.toString()); 03193 03194 Theorem thm(reflexivityRule(e)); 03195 // Now multiply the equality by the factor, unless it is 1 03196 if(factor.getRational() != 1) { 03197 int kind = e.getKind(); 03198 switch(kind) { 03199 case EQ: 03200 //TODO: DEJAN FIX 03201 thm = d_rules->multEqn(e[0], e[1], factor); 03202 // And canonize the result 03203 thm = canonPredEquiv(thm); 03204 03205 // If this is an equation of the form 0 = c + sum, c is not integer, but sum is 03206 // then equation has no solutions 03207 thm = checkIntegerEquality(thm); 03208 03209 break; 03210 case LE: 03211 case LT: 03212 case GE: 03213 case GT: { 03214 thm = d_rules->multIneqn(e, factor); 03215 // And canonize the result 03216 thm = canonPredEquiv(thm); 03217 // Try to rafine to integer domain 03218 thm = rafineInequalityToInteger(thm); 03219 break; 03220 } 03221 03222 default: 03223 // MS .net doesn't accept "..." + int 03224 ostringstream ss; 03225 ss << "normalize: control should not reach here " << kind; 03226 DebugAssert(false, ss.str()); 03227 break; 03228 } 03229 } else 03230 if (e.getKind() == EQ) 03231 thm = checkIntegerEquality(thm); 03232 03233 TRACE("arith normalize", "normalize => ", thm, " }"); 03234 return(thm); 03235 } 03236 03237 03238 Theorem TheoryArithOld::normalize(const Theorem& eIffEqn) { 03239 if (eIffEqn.isRewrite()) return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS())); 03240 else return iffMP(eIffEqn, normalize(eIffEqn.getExpr())); 03241 } 03242 03243 03244 Theorem TheoryArithOld::rewrite(const Expr& e) 03245 { 03246 DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified"); 03247 TRACE("arith", "TheoryArithOld::rewrite(", e, ") {"); 03248 Theorem thm; 03249 if (!e.isTerm()) { 03250 if (!e.isAbsLiteral()) { 03251 if (e.isPropAtom() && leavesAreNumConst(e)) { 03252 if (e.getSize() < 200) { 03253 Expr eNew = e; 03254 thm = reflexivityRule(eNew); 03255 while (eNew.containsTermITE()) { 03256 thm = transitivityRule(thm, getCommonRules()->liftOneITE(eNew)); 03257 DebugAssert(!thm.isRefl(), "Expected non-reflexive"); 03258 thm = transitivityRule(thm, theoryCore()->getCoreRules()->rewriteIteCond(thm.getRHS())); 03259 thm = transitivityRule(thm, simplify(thm.getRHS())); 03260 eNew = thm.getRHS(); 03261 } 03262 } 03263 else { 03264 thm = d_rules->rewriteLeavesConst(e); 03265 if (thm.isRefl()) { 03266 e.setRewriteNormal(); 03267 } 03268 else { 03269 thm = transitivityRule(thm, simplify(thm.getRHS())); 03270 } 03271 } 03272 // if (!thm.getRHS().isBoolConst()) { 03273 // e.setRewriteNormal(); 03274 // thm = reflexivityRule(e); 03275 // } 03276 } 03277 else { 03278 e.setRewriteNormal(); 03279 thm = reflexivityRule(e); 03280 } 03281 TRACE("arith", "TheoryArithOld::rewrite[non-literal] => ", thm, " }"); 03282 return thm; 03283 } 03284 switch(e.getKind()) { 03285 case EQ: 03286 { 03287 // canonical form for an equality of two leaves 03288 // is just l == r instead of 0 + (-1 * l) + r = 0. 03289 if (isLeaf(e[0]) && isLeaf(e[1])) 03290 thm = reflexivityRule(e); 03291 else { // Otherwise, it is "lhs = 0" 03292 //first convert e to the form 0=e' 03293 if((e[0].isRational() && e[0].getRational() == 0) 03294 || (e[1].isRational() && e[1].getRational() == 0)) 03295 //already in 0=e' or e'=0 form 03296 thm = reflexivityRule(e); 03297 else { 03298 thm = d_rules->rightMinusLeft(e); 03299 thm = canonPredEquiv(thm); 03300 } 03301 // Check for trivial equation 03302 if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) { 03303 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS())); 03304 } else { 03305 //else equation is non-trivial 03306 thm = normalize(thm); 03307 // Normalization may yield non-simplified terms 03308 if (!thm.getRHS().isBoolConst()) 03309 thm = canonPredEquiv(thm); 03310 } 03311 } 03312 03313 // Equations must be oriented such that lhs >= rhs as Exprs; 03314 // this ordering is given by operator<(Expr,Expr). 03315 const Expr& eq = thm.getRHS(); 03316 if(eq.isEq() && eq[0] < eq[1]) 03317 thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq)); 03318 03319 // Check if the equation is nonlinear 03320 Expr nonlinearEq = thm.getRHS(); 03321 if (nonlinearEq.isEq() && isNonlinearEq(nonlinearEq)) { 03322 03323 TRACE("arith nonlinear", "nonlinear eq rewrite: ", nonlinearEq, ""); 03324 03325 Expr left = nonlinearEq[0]; 03326 Expr right = nonlinearEq[1]; 03327 03328 // Check for multiplicative equations, i.e. x*y = 0 03329 if (isNonlinearSumTerm(left) && right.isRational() && right.getRational() == 0) { 03330 Theorem eq_thm = d_rules->multEqZero(nonlinearEq); 03331 thm = transitivityRule(thm, eq_thm); 03332 thm = transitivityRule(thm, theoryCore()->simplify(thm.getRHS())); 03333 break; 03334 } 03335 03336 // Heuristics for a sum 03337 if (isPlus(left)) { 03338 03339 // Search for common factor 03340 if (left[0].getRational() == 0) { 03341 Expr::iterator i = left.begin(), iend = left.end(); 03342 ++ i; 03343 set<Expr> factors; 03344 set<Expr>::iterator is, isend; 03345 getFactors(*i, factors); 03346 for (++i; i != iend; ++i) { 03347 set<Expr> factors2; 03348 getFactors(*i, factors2); 03349 for (is = factors.begin(), isend = factors.end(); is != isend;) { 03350 if (factors2.find(*is) == factors2.end()) { 03351 factors.erase(is ++); 03352 } else 03353 ++ is; 03354 } 03355 if (factors.empty()) break; 03356 } 03357 if (!factors.empty()) { 03358 thm = transitivityRule(thm, d_rules->divideEqnNonConst(left, rat(0), *(factors.begin()))); 03359 // got (factor != 0) OR (left / factor = right / factor), need to simplify 03360 thm = transitivityRule(thm, simplify(thm.getRHS())); 03361 TRACE("arith nonlinear", "nonlinear eq rewrite (factoring): ", thm.getRHS(), ""); 03362 break; 03363 } 03364 } 03365 03366 // Look for equal powers (eq in the form of c + pow1 - pow2 = 0) 03367 Rational constant; 03368 Expr power1; 03369 Expr power2; 03370 if (isPowersEquality(nonlinearEq, power1, power2)) { 03371 // Eliminate the powers 03372 thm = transitivityRule(thm, d_rules->elimPower(nonlinearEq)); 03373 thm = transitivityRule(thm, simplify(thm.getRHS())); 03374 TRACE("arith nonlinear", "nonlinear eq rewrite (equal powers): ", thm.getRHS(), ""); 03375 break; 03376 } else 03377 // Look for one power equality (c - pow = 0); 03378 if (isPowerEquality(nonlinearEq, constant, power1)) { 03379 Rational pow1 = power1[0].getRational(); 03380 if (pow1 % 2 == 0 && constant < 0) { 03381 thm = transitivityRule(thm, d_rules->evenPowerEqNegConst(nonlinearEq)); 03382 TRACE("arith nonlinear", "nonlinear eq rewrite (even power = negative): ", thm.getRHS(), ""); 03383 break; 03384 } 03385 DebugAssert(constant != 0, "Expected nonzero const"); 03386 Rational root = ratRoot(constant, pow1.getUnsigned()); 03387 if (root != 0) { 03388 thm = transitivityRule(thm, d_rules->elimPowerConst(nonlinearEq, root)); 03389 thm = transitivityRule(thm, simplify(thm.getRHS())); 03390 TRACE("arith nonlinear", "nonlinear eq rewrite (rational root): ", thm.getRHS(), ""); 03391 break; 03392 } else { 03393 Theorem isIntPower(isIntegerThm(left)); 03394 if (!isIntPower.isNull()) { 03395 thm = transitivityRule(thm, d_rules->intEqIrrational(nonlinearEq, isIntPower)); 03396 TRACE("arith nonlinear", "nonlinear eq rewrite (irational root): ", thm.getRHS(), ""); 03397 break; 03398 } 03399 } 03400 } 03401 } 03402 03403 // Non-solvable nonlinear equations are rewritten as conjunction of inequalities 03404 if (!canPickEqMonomial(nonlinearEq[0])) { 03405 thm = transitivityRule(thm, d_rules->eqToIneq(nonlinearEq)); 03406 thm = transitivityRule(thm, simplify(thm.getRHS())); 03407 TRACE("arith nonlinear", "nonlinear eq rewrite (not solvable): ", thm.getRHS(), ""); 03408 break; 03409 } 03410 } 03411 } 03412 break; 03413 case GRAY_SHADOW: 03414 case DARK_SHADOW: 03415 thm = reflexivityRule(e); 03416 break; 03417 case IS_INTEGER: { 03418 Theorem res(isIntegerDerive(e, typePred(e[0]))); 03419 if(!res.isNull()) 03420 thm = getCommonRules()->iffTrue(res); 03421 else 03422 thm = reflexivityRule(e); 03423 break; 03424 } 03425 case NOT: 03426 if (!isIneq(e[0])) 03427 //in this case we have "NOT of DARK or GRAY_SHADOW." 03428 thm = reflexivityRule(e); 03429 else { 03430 //In this case we have the "NOT of ineq". get rid of NOT 03431 //and then treat like an ineq 03432 thm = d_rules->negatedInequality(e); 03433 DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()), 03434 "Expected GE or GT"); 03435 thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS())); 03436 thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS())); 03437 thm = canonPredEquiv(thm); 03438 03439 // If the inequality is strict and integer, change it to non-strict 03440 Expr theIneq = thm.getRHS(); 03441 if(isLT(theIneq)) { 03442 // Check if integer 03443 Theorem isIntLHS(isIntegerThm(theIneq[0])); 03444 Theorem isIntRHS(isIntegerThm(theIneq[1])); 03445 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull()); 03446 if (isInt) { 03447 thm = canonPredEquiv( 03448 transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true))); 03449 } 03450 } 03451 03452 // Check for trivial inequation 03453 if ((thm.getRHS())[1].isRational()) 03454 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS())); 03455 else { 03456 //else ineq is non-trivial 03457 thm = normalize(thm); 03458 // Normalization may yield non-simplified terms 03459 thm = canonPredEquiv(thm); 03460 } 03461 } 03462 break; 03463 case LT: 03464 case GT: 03465 case LE: 03466 case GE: { 03467 03468 if (isGE(e) || isGT(e)) { 03469 thm = d_rules->flipInequality(e); 03470 thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS())); 03471 } 03472 else 03473 thm = d_rules->rightMinusLeft(e); 03474 03475 thm = canonPredEquiv(thm); 03476 03477 // If the inequality is strict and integer, change it to non-strict 03478 Expr theIneq = thm.getRHS(); 03479 if(isLT(theIneq)) { 03480 // Check if integer 03481 Theorem isIntLHS(isIntegerThm(theIneq[0])); 03482 Theorem isIntRHS(isIntegerThm(theIneq[1])); 03483 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull()); 03484 if (isInt) { 03485 thm = canonPredEquiv( 03486 transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true))); 03487 } 03488 } 03489 03490 // Check for trivial inequation 03491 if ((thm.getRHS())[1].isRational()) 03492 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS())); 03493 else { // ineq is non-trivial 03494 thm = normalize(thm); 03495 thm = canonPredEquiv(thm); 03496 if (thm.getRHS()[1].isRational()) 03497 thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS())); 03498 } 03499 break; 03500 } 03501 default: 03502 DebugAssert(false, 03503 "Theory_Arith::rewrite: control should not reach here"); 03504 break; 03505 } 03506 } 03507 else { 03508 if (e.isAtomic()) 03509 thm = canon(e); 03510 else 03511 thm = reflexivityRule(e); 03512 } 03513 // TODO: this needs to be reviewed, esp for non-linear case 03514 // Arith canonization is idempotent 03515 if (theoryOf(thm.getRHS()) == this) 03516 thm.getRHS().setRewriteNormal(); 03517 TRACE("arith", "TheoryArithOld::rewrite => ", thm, " }"); 03518 return thm; 03519 } 03520 03521 03522 void TheoryArithOld::setup(const Expr& e) 03523 { 03524 if (!e.isTerm()) { 03525 if (e.isNot()) return; 03526 // if(e.getKind() == IS_INTEGER) { 03527 // e[0].addToNotify(this, e); 03528 // return; 03529 // } 03530 if (isIneq(e)) { 03531 DebugAssert((isLT(e)||isLE(e)) && 03532 e[0].isRational() && e[0].getRational() == 0, 03533 "TheoryArithOld::setup: expected 0 < rhs:" + e.toString()); 03534 e[1].addToNotify(this, e); 03535 } else { 03536 // if (e.isEq()) { 03537 // // Nonlinear solved equations 03538 // if (isNonlinearEq(e) && e[0].isRational() && e[0].getRational() == 0) 03539 // e[0].addToNotify(this, e); 03540 // } 03541 // 03542 // DebugAssert(isGrayShadow(e), "TheoryArithOld::setup: expected grayshadow" + e.toString()); 03543 // 03544 // // Do not add the variable, just the subterm e[0].addToNotify(this, e); 03545 // e[1].addToNotify(this, e); 03546 } 03547 return; 03548 } 03549 int k(0), ar(e.arity()); 03550 for ( ; k < ar; ++k) { 03551 e[k].addToNotify(this, e); 03552 TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), ""); 03553 } 03554 } 03555 03556 03557 void TheoryArithOld::update(const Theorem& e, const Expr& d) 03558 { 03559 TRACE("arith update", "update on " + d.toString() + " with ", e.getRHS().toString(), "."); 03560 03561 if (inconsistent()) return; 03562 03563 // We accept atoms without find, but only inequalities (they come from the buffer) 03564 DebugAssert(d.hasFind() || isIneq(d), "update on a non-inequality term/atom"); 03565 03566 IF_DEBUG(debugger.counter("arith update total")++;) 03567 // if (isGrayShadow(d)) { 03568 // TRACE("shadow update", "updating index of " + d.toString() + " with ", e.getRHS().toString(), "."); 03569 // 03570 // // Substitute e[1] for e[0] in d and enqueue new shadow 03571 // DebugAssert(e.getLHS() == d[1], "Mismatch"); 03572 // Theorem thm = find(d); 03573 // 03574 // // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true"); 03575 // vector<unsigned> changed; 03576 // vector<Theorem> children; 03577 // changed.push_back(1); 03578 // children.push_back(e); 03579 // Theorem thm2 = substitutivityRule(d, changed, children); 03580 // if (thm.getRHS() == trueExpr()) { 03581 // enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2)); 03582 // } 03583 // else { 03584 // enqueueFact(getCommonRules()->iffFalseElim( 03585 // transitivityRule(symmetryRule(thm2), thm))); 03586 // } 03587 // IF_DEBUG(debugger.counter("arith update ineq")++;) 03588 // } 03589 // else 03590 if (isIneq(d)) { 03591 03592 // Substitute e[1] for e[0] in d and enqueue new inequality 03593 DebugAssert(e.getLHS() == d[1], "Mismatch"); 03594 Theorem thm; 03595 if (d.hasFind()) thm = find(d); 03596 03597 // bool diff_logic = false; 03598 // Expr new_rhs = e.getRHS(); 03599 // if (!isPlus(new_rhs)) { 03600 // if (isLeaf(new_rhs)) diff_logic = true; 03601 // } 03602 // else { 03603 // int arity = new_rhs.arity(); 03604 // if (arity == 2) { 03605 // if (new_rhs[0].isRational()) diff_logic = true; 03606 // else { 03607 // Expr ax = new_rhs[0], a, x; 03608 // Expr by = new_rhs[1], b, y; 03609 // separateMonomial(ax, a, x); 03610 // separateMonomial(by, b, y); 03611 // if ((a.getRational() == 1 && b.getRational() == -1) || 03612 // (a.getRational() == -1 && b.getRational() == 1)) 03613 // diff_logic = true; 03614 // } 03615 // } else { 03616 // if (arity == 3 && new_rhs[0].isRational()) { 03617 // Expr ax = new_rhs[1], a, x; 03618 // Expr by = new_rhs[2], b, y; 03619 // separateMonomial(ax, a, x); 03620 // separateMonomial(by, b, y); 03621 // if ((a.getRational() == 1 && b.getRational() == -1) || 03622 // (a.getRational() == -1 && b.getRational() == 1)) 03623 // diff_logic = true; 03624 // } 03625 // } 03626 // } 03627 03628 // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true"); 03629 vector<unsigned> changed; 03630 vector<Theorem> children; 03631 changed.push_back(1); 03632 children.push_back(e); 03633 Theorem thm2 = substitutivityRule(d, changed, children); 03634 Expr newIneq = thm2.getRHS(); 03635 03636 // If this inequality is bufferred but not yet projected, just wait for it 03637 // but don't add the find to the buffer as it will be projected as a find 03638 // We DO want it to pass through all the buffer stuff but NOT get into the buffer 03639 // NOTE: this means that the difference logic WILL get processed 03640 if ((thm.isNull() || thm.getRHS() != falseExpr()) && 03641 bufferedInequalities.find(d) != bufferedInequalities.end() && 03642 alreadyProjected.find(d) == alreadyProjected.end()) { 03643 TRACE("arith update", "simplified but not projected : ", thm2.getRHS(), ""); 03644 dontBuffer[thm2.getRHS()] = true; 03645 } 03646 03647 if (thm.isNull()) { 03648 // This hy is in the buffer, not in the core 03649 // if it has been projected, than it's parent has been projected and will get reprojected 03650 // accuratlz. If it has not been projected, we don't care it's still there 03651 TRACE("arith update", "in udpate, but no find", "", ""); 03652 if (bufferedInequalities.find(d) != bufferedInequalities.end()) { 03653 if (thm2.getRHS()[1].isRational()) enqueueFact(iffMP(bufferedInequalities[d], thm2)); 03654 else if (alreadyProjected.find(d) != alreadyProjected.end()) { 03655 // the parent will get reprojected 03656 alreadyProjected[d] = d; 03657 } 03658 } 03659 } 03660 else if (thm.getRHS() == trueExpr()) { 03661 if (!newIneq[1].isRational() || newIneq[1].getRational() <= 0) 03662 enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2)); 03663 } 03664 else { 03665 enqueueFact(getCommonRules()->iffFalseElim( 03666 transitivityRule(symmetryRule(thm2), thm))); 03667 } 03668 IF_DEBUG(debugger.counter("arith update ineq")++;) 03669 } 03670 else if (d.isEq()) { 03671 TRACE("arith nonlinear", "TheoryArithOld::update() on equality ", d, ""); 03672 // We get equalitites from the non-solve nonlinear equations 03673 // only the right hand sides get updated 03674 vector<unsigned> changed; 03675 vector<Theorem> children; 03676 changed.push_back(0); 03677 children.push_back(e); 03678 Theorem thm = substitutivityRule(d, changed, children); 03679 Expr newEq = thm.getRHS(); 03680 03681 Theorem d_find = find(d); 03682 if (d_find.getRHS() == trueExpr()) enqueueFact(iffMP(getCommonRules()->iffTrueElim(d_find), thm)); 03683 else enqueueFact(getCommonRules()->iffFalseElim(transitivityRule(symmetryRule(thm), d_find))); 03684 } 03685 else if (d.getKind() == IS_INTEGER) { 03686 // This should only happen if !d has been asserted 03687 DebugAssert(e.getRHS() == findExpr(d[0]), "Unexpected"); 03688 if (isInteger(e.getRHS())) { 03689 Theorem thm = substitutivityRule(d, find(d[0])); 03690 thm = transitivityRule(symmetryRule(find(d)), thm); 03691 thm = iffMP(thm, simplify(thm.getExpr())); 03692 setInconsistent(thm); 03693 } 03694 else { 03695 e.getRHS().addToNotify(this, d); 03696 } 03697 } 03698 else if (find(d).getRHS() == d) { 03699 // Theorem thm = canonSimp(d); 03700 // TRACE("arith", "TheoryArithOld::update(): thm = ", thm, ""); 03701 // DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: " 03702 // +thm.getExpr().toString()); 03703 // assertEqualities(transitivityRule(thm, rewrite(thm.getRHS()))); 03704 // IF_DEBUG(debugger.counter("arith update find(d)=d")++;) 03705 Theorem thm = simplify(d); 03706 // If the original is was a shared term, add this one as as a shared term also 03707 if (d_sharedTerms.find(d) != d_sharedTerms.end()) addSharedTerm(thm.getRHS()); 03708 DebugAssert(thm.getRHS().isAtomic(), "Expected atomic"); 03709 assertEqualities(thm); 03710 } 03711 } 03712 03713 03714 Theorem TheoryArithOld::solve(const Theorem& thm) 03715 { 03716 DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), ""); 03717 const Expr& lhs = thm.getLHS(); 03718 const Expr& rhs = thm.getRHS(); 03719 03720 // Check for already solved equalities. 03721 03722 // Have to be careful about the types: integer variable cannot be 03723 // assigned a real term. Also, watch for e[0] being a subexpression 03724 // of e[1]: this would create an unsimplifiable expression. 03725 if (isLeaf(lhs) && !isLeafIn(lhs, rhs) 03726 && (!isInteger(lhs) || isInteger(rhs)) 03727 // && !e[0].subExprOf(e[1]) 03728 ) 03729 return thm; 03730 03731 // Symmetric version is already solved 03732 if (isLeaf(rhs) && !isLeafIn(rhs, lhs) 03733 && (!isInteger(rhs) || isInteger(lhs)) 03734 // && !e[1].subExprOf(e[0]) 03735 ) 03736 return symmetryRule(thm); 03737 03738 return doSolve(thm); 03739 } 03740 03741 03742 void TheoryArithOld::computeModelTerm(const Expr& e, std::vector<Expr>& v) { 03743 switch(e.getKind()) { 03744 case RATIONAL_EXPR: // Skip the constants 03745 break; 03746 case PLUS: 03747 case MULT: 03748 case DIVIDE: 03749 case POW: // This is not a variable; extract the variables from children 03750 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 03751 // getModelTerm(*i, v); 03752 v.push_back(*i); 03753 break; 03754 default: { // Otherwise it's a variable. Check if it has a find pointer 03755 Expr e2(findExpr(e)); 03756 if(e==e2) { 03757 TRACE("model", "TheoryArithOld::computeModelTerm(", e, "): a variable"); 03758 // Leave it alone (it has no descendants) 03759 // v.push_back(e); 03760 } else { 03761 TRACE("model", "TheoryArithOld::computeModelTerm("+e.toString() 03762 +"): has find pointer to ", e2, ""); 03763 v.push_back(e2); 03764 } 03765 } 03766 } 03767 } 03768 03769 03770 Expr TheoryArithOld::computeTypePred(const Type& t, const Expr& e) { 03771 Expr tExpr = t.getExpr(); 03772 switch(tExpr.getKind()) { 03773 case INT: 03774 return Expr(IS_INTEGER, e); 03775 case SUBRANGE: { 03776 std::vector<Expr> kids; 03777 kids.push_back(Expr(IS_INTEGER, e)); 03778 kids.push_back(leExpr(tExpr[0], e)); 03779 kids.push_back(leExpr(e, tExpr[1])); 03780 return andExpr(kids); 03781 } 03782 default: 03783 return e.getEM()->trueExpr(); 03784 } 03785 } 03786 03787 03788 void TheoryArithOld::checkAssertEqInvariant(const Theorem& e) 03789 { 03790 if (e.isRewrite()) { 03791 DebugAssert(e.getLHS().isTerm(), "Expected equation"); 03792 if (isLeaf(e.getLHS())) { 03793 // should be in solved form 03794 DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()), 03795 "Not in solved form: lhs appears in rhs"); 03796 } 03797 else { 03798 DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find"); 03799 DebugAssert(!leavesAreSimp(e.getLHS()), 03800 "Expected at least one unsimplified leaf on lhs"); 03801 } 03802 DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(), 03803 "Expected canonSimp(rhs) = canonSimp(rhs)"); 03804 } 03805 else { 03806 Expr expr = e.getExpr(); 03807 if (expr.isFalse()) return; 03808 03809 vector<Theorem> eqs; 03810 Theorem thm; 03811 int index, index2; 03812 03813 for (index = 0; index < expr.arity(); ++index) { 03814 thm = getCommonRules()->andElim(e, index); 03815 eqs.push_back(thm); 03816 if (thm.getExpr().isFalse()) return; 03817 DebugAssert(eqs[index].isRewrite() && 03818 eqs[index].getLHS().isTerm(), "Expected equation"); 03819 } 03820 03821 // Check for solved form 03822 for (index = 0; index < expr.arity(); ++index) { 03823 DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs"); 03824 DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(), 03825 "Expected canonSimp(rhs) = canonSimp(rhs)"); 03826 DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()), 03827 "Failed recursive canonSimp check"); 03828 for (index2 = 0; index2 < expr.arity(); ++index2) { 03829 DebugAssert(index == index2 || 03830 eqs[index].getLHS() != eqs[index2].getLHS(), 03831 "Not in solved form: repeated lhs"); 03832 DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()), 03833 "Not in solved form: lhs appears in rhs"); 03834 } 03835 } 03836 } 03837 } 03838 03839 03840 void TheoryArithOld::checkType(const Expr& e) 03841 { 03842 switch (e.getKind()) { 03843 case INT: 03844 case REAL: 03845 if (e.arity() > 0) { 03846 throw Exception("Ill-formed arithmetic type: "+e.toString()); 03847 } 03848 break; 03849 case SUBRANGE: 03850 if (e.arity() != 2 || 03851 !isIntegerConst(e[0]) || 03852 !isIntegerConst(e[1]) || 03853 e[0].getRational() > e[1].getRational()) { 03854 throw Exception("bad SUBRANGE type expression"+e.toString()); 03855 } 03856 break; 03857 default: 03858 DebugAssert(false, "Unexpected kind in TheoryArithOld::checkType" 03859 +getEM()->getKindName(e.getKind())); 03860 } 03861 } 03862 03863 03864 Cardinality TheoryArithOld::finiteTypeInfo(Expr& e, Unsigned& n, 03865 bool enumerate, bool computeSize) 03866 { 03867 Cardinality card = CARD_INFINITE; 03868 switch (e.getKind()) { 03869 case SUBRANGE: { 03870 card = CARD_FINITE; 03871 Expr typeExpr = e; 03872 if (enumerate) { 03873 Rational r = typeExpr[0].getRational() + n; 03874 if (r <= typeExpr[1].getRational()) { 03875 e = rat(r); 03876 } 03877 else e = Expr(); 03878 } 03879 if (computeSize) { 03880 Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1; 03881 n = r.getUnsigned(); 03882 } 03883 break; 03884 } 03885 default: 03886 break; 03887 } 03888 return card; 03889 } 03890 03891 03892 void TheoryArithOld::computeType(const Expr& e) 03893 { 03894 switch (e.getKind()) { 03895 case REAL_CONST: 03896 e.setType(d_realType); 03897 break; 03898 case RATIONAL_EXPR: 03899 if(e.getRational().isInteger()) 03900 e.setType(d_intType); 03901 else 03902 e.setType(d_realType); 03903 break; 03904 case UMINUS: 03905 case PLUS: 03906 case MINUS: 03907 case MULT: 03908 case POW: { 03909 bool isInt = true; 03910 for(int k = 0; k < e.arity(); ++k) { 03911 if(d_realType != getBaseType(e[k])) 03912 throw TypecheckException("Expecting type REAL with `" + 03913 getEM()->getKindName(e.getKind()) + "',\n"+ 03914 "but got a " + getBaseType(e[k]).toString()+ 03915 " for:\n" + e.toString()); 03916 if(isInt && !isInteger(e[k])) 03917 isInt = false; 03918 } 03919 if(isInt) 03920 e.setType(d_intType); 03921 else 03922 e.setType(d_realType); 03923 break; 03924 } 03925 case DIVIDE: { 03926 Expr numerator = e[0]; 03927 Expr denominator = e[1]; 03928 if (getBaseType(numerator) != d_realType || 03929 getBaseType(denominator) != d_realType) { 03930 throw TypecheckException("Expecting only REAL types with `DIVIDE',\n" 03931 "but got " + getBaseType(numerator).toString()+ 03932 " and " + getBaseType(denominator).toString() + 03933 " for:\n" + e.toString()); 03934 } 03935 if(denominator.isRational() && 1 == denominator.getRational()) 03936 e.setType(numerator.getType()); 03937 else 03938 e.setType(d_realType); 03939 break; 03940 } 03941 case LT: 03942 case LE: 03943 case GT: 03944 case GE: 03945 case GRAY_SHADOW: 03946 // Need to know types for all exprs -Clark 03947 // e.setType(boolType()); 03948 // break; 03949 case DARK_SHADOW: 03950 for (int k = 0; k < e.arity(); ++k) { 03951 if (d_realType != getBaseType(e[k])) 03952 throw TypecheckException("Expecting type REAL with `" + 03953 getEM()->getKindName(e.getKind()) + "',\n"+ 03954 "but got a " + getBaseType(e[k]).toString()+ 03955 " for:\n" + e.toString()); 03956 } 03957 03958 e.setType(boolType()); 03959 break; 03960 case IS_INTEGER: 03961 if(d_realType != getBaseType(e[0])) 03962 throw TypecheckException("Expected type REAL, but got " 03963 +getBaseType(e[0]).toString() 03964 +"\n\nExpr = "+e.toString()); 03965 e.setType(boolType()); 03966 break; 03967 default: 03968 DebugAssert(false,"TheoryArithOld::computeType: unexpected expression:\n " 03969 +e.toString()); 03970 break; 03971 } 03972 } 03973 03974 03975 Type TheoryArithOld::computeBaseType(const Type& t) { 03976 IF_DEBUG(int kind = t.getExpr().getKind();) 03977 DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE, 03978 "TheoryArithOld::computeBaseType("+t.toString()+")"); 03979 return realType(); 03980 } 03981 03982 03983 Expr 03984 TheoryArithOld::computeTCC(const Expr& e) { 03985 Expr tcc(Theory::computeTCC(e)); 03986 switch(e.getKind()) { 03987 case DIVIDE: 03988 DebugAssert(e.arity() == 2, ""); 03989 return tcc.andExpr(!(e[1].eqExpr(rat(0)))); 03990 default: 03991 return tcc; 03992 } 03993 } 03994 03995 /////////////////////////////////////////////////////////////////////////////// 03996 //parseExprOp: 03997 //translating special Exprs to regular EXPR?? 03998 /////////////////////////////////////////////////////////////////////////////// 03999 Expr 04000 TheoryArithOld::parseExprOp(const Expr& e) { 04001 TRACE("parser", "TheoryArithOld::parseExprOp(", e, ")"); 04002 //std::cout << "Were here"; 04003 // If the expression is not a list, it must have been already 04004 // parsed, so just return it as is. 04005 switch(e.getKind()) { 04006 case ID: { 04007 int kind = getEM()->getKind(e[0].getString()); 04008 switch(kind) { 04009 case NULL_KIND: return e; // nothing to do 04010 case REAL: 04011 case INT: 04012 case NEGINF: 04013 case POSINF: return getEM()->newLeafExpr(kind); 04014 default: 04015 DebugAssert(false, "Bad use of bare keyword: "+e.toString()); 04016 return e; 04017 } 04018 } 04019 case RAW_LIST: break; // break out of switch, do the hard work 04020 default: 04021 return e; 04022 } 04023 04024 DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0, 04025 "TheoryArithOld::parseExprOp:\n e = "+e.toString()); 04026 04027 const Expr& c1 = e[0][0]; 04028 int kind = getEM()->getKind(c1.getString()); 04029 switch(kind) { 04030 case UMINUS: { 04031 if(e.arity() != 2) 04032 throw ParserException("UMINUS requires exactly one argument: " 04033 +e.toString()); 04034 return uminusExpr(parseExpr(e[1])); 04035 } 04036 case PLUS: { 04037 vector<Expr> k; 04038 Expr::iterator i = e.begin(), iend=e.end(); 04039 // Skip first element of the vector of kids in 'e'. 04040 // The first element is the operator. 04041 ++i; 04042 // Parse the kids of e and push them into the vector 'k' 04043 for(; i!=iend; ++i) k.push_back(parseExpr(*i)); 04044 return plusExpr(k); 04045 } 04046 case MINUS: { 04047 if(e.arity() == 2) { 04048 if (false && getEM()->getInputLang() == SMTLIB_LANG) { 04049 throw ParserException("Unary Minus should use '~' instead of '-' in SMT-LIB expr:" 04050 +e.toString()); 04051 } 04052 else { 04053 return uminusExpr(parseExpr(e[1])); 04054 } 04055 } 04056 else if(e.arity() == 3) 04057 return minusExpr(parseExpr(e[1]), parseExpr(e[2])); 04058 else 04059 throw ParserException("MINUS requires one or two arguments:" 04060 +e.toString()); 04061 } 04062 case MULT: { 04063 vector<Expr> k; 04064 Expr::iterator i = e.begin(), iend=e.end(); 04065 // Skip first element of the vector of kids in 'e'. 04066 // The first element is the operator. 04067 ++i; 04068 // Parse the kids of e and push them into the vector 'k' 04069 for(; i!=iend; ++i) k.push_back(parseExpr(*i)); 04070 return multExpr(k); 04071 } 04072 case POW: { 04073 return powExpr(parseExpr(e[1]), parseExpr(e[2])); 04074 } 04075 case DIVIDE: 04076 { return divideExpr(parseExpr(e[1]), parseExpr(e[2])); } 04077 case LT: 04078 { return ltExpr(parseExpr(e[1]), parseExpr(e[2])); } 04079 case LE: 04080 { return leExpr(parseExpr(e[1]), parseExpr(e[2])); } 04081 case GT: 04082 { return gtExpr(parseExpr(e[1]), parseExpr(e[2])); } 04083 case GE: 04084 { return geExpr(parseExpr(e[1]), parseExpr(e[2])); } 04085 case INTDIV: 04086 case MOD: 04087 case SUBRANGE: { 04088 vector<Expr> k; 04089 Expr::iterator i = e.begin(), iend=e.end(); 04090 // Skip first element of the vector of kids in 'e'. 04091 // The first element is the operator. 04092 ++i; 04093 // Parse the kids of e and push them into the vector 'k' 04094 for(; i!=iend; ++i) 04095 k.push_back(parseExpr(*i)); 04096 return Expr(kind, k, e.getEM()); 04097 } 04098 case IS_INTEGER: { 04099 if(e.arity() != 2) 04100 throw ParserException("IS_INTEGER requires exactly one argument: " 04101 +e.toString()); 04102 return Expr(IS_INTEGER, parseExpr(e[1])); 04103 } 04104 default: 04105 DebugAssert(false, 04106 "TheoryArithOld::parseExprOp: invalid input " + e.toString()); 04107 break; 04108 } 04109 return e; 04110 } 04111 04112 /////////////////////////////////////////////////////////////////////////////// 04113 // Pretty-printing // 04114 /////////////////////////////////////////////////////////////////////////////// 04115 04116 04117 ExprStream& 04118 TheoryArithOld::print(ExprStream& os, const Expr& e) { 04119 switch(os.lang()) { 04120 case SIMPLIFY_LANG: 04121 switch(e.getKind()) { 04122 case RATIONAL_EXPR: 04123 e.print(os); 04124 break; 04125 case SUBRANGE: 04126 os <<"ERROR:SUBRANGE:not supported in Simplify\n"; 04127 break; 04128 case IS_INTEGER: 04129 os <<"ERROR:IS_INTEGER:not supported in Simplify\n"; 04130 break; 04131 case PLUS: { 04132 int i=0, iend=e.arity(); 04133 os << "(+ "; 04134 if(i!=iend) os << e[i]; 04135 ++i; 04136 for(; i!=iend; ++i) os << " " << e[i]; 04137 os << ")"; 04138 break; 04139 } 04140 case MINUS: 04141 os << "(- " << e[0] << " " << e[1]<< ")"; 04142 break; 04143 case UMINUS: 04144 os << "-" << e[0] ; 04145 break; 04146 case MULT: { 04147 int i=0, iend=e.arity(); 04148 os << "(* " ; 04149 if(i!=iend) os << e[i]; 04150 ++i; 04151 for(; i!=iend; ++i) os << " " << e[i]; 04152 os << ")"; 04153 break; 04154 } 04155 case POW: 04156 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")"; 04157 break; 04158 case DIVIDE: 04159 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")"; 04160 break; 04161 case LT: 04162 if (isInt(e[0].getType()) || isInt(e[1].getType())) { 04163 } 04164 os << "(< " << e[0] << " " << e[1] <<")"; 04165 break; 04166 case LE: 04167 os << "(<= " << e[0] << " " << e[1] << ")"; 04168 break; 04169 case GT: 04170 os << "(> " << e[0] << " " << e[1] << ")"; 04171 break; 04172 case GE: 04173 os << "(>= " << e[0] << " " << e[1] << ")"; 04174 break; 04175 case DARK_SHADOW: 04176 case GRAY_SHADOW: 04177 os <<"ERROR:SHADOW:not supported in Simplify\n"; 04178 break; 04179 default: 04180 // Print the top node in the default LISP format, continue with 04181 // pretty-printing for children. 04182 e.print(os); 04183 04184 break; 04185 } 04186 break; // end of case SIMPLIFY_LANG 04187 04188 case TPTP_LANG: 04189 switch(e.getKind()) { 04190 case RATIONAL_EXPR: 04191 e.print(os); 04192 break; 04193 case SUBRANGE: 04194 os <<"ERROR:SUBRANGE:not supported in TPTP\n"; 04195 break; 04196 case IS_INTEGER: 04197 os <<"ERROR:IS_INTEGER:not supported in TPTP\n"; 04198 break; 04199 case PLUS: { 04200 if(!isInteger(e[0])){ 04201 os<<"ERRPR:plus only supports inteters now in TPTP\n"; 04202 break; 04203 } 04204 04205 int i=0, iend=e.arity(); 04206 if(iend <=1){ 04207 os<<"ERROR,plus must have more than two numbers in TPTP\n"; 04208 break; 04209 } 04210 04211 for(i=0; i <= iend-2; ++i){ 04212 os << "$plus_int("; 04213 os << e[i] << ","; 04214 } 04215 04216 os<< e[iend-1]; 04217 04218 for(i=0 ; i <= iend-2; ++i){ 04219 os << ")"; 04220 } 04221 04222 break; 04223 } 04224 case MINUS: 04225 if(!isInteger(e[0])){ 04226 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04227 break; 04228 } 04229 04230 os << "$minus_int(" << e[0] << "," << e[1]<< ")"; 04231 break; 04232 case UMINUS: 04233 if(!isInteger(e[0])){ 04234 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04235 break; 04236 } 04237 04238 os << "$uminus_int(" << e[0] <<")" ; 04239 break; 04240 case MULT: { 04241 if(!isInteger(e[0])){ 04242 os<<"ERRPR:times only supports inteters now in TPTP\n"; 04243 break; 04244 } 04245 04246 int i=0, iend=e.arity(); 04247 if(iend <=1){ 04248 os<<"ERROR:times must have more than two numbers in TPTP\n"; 04249 break; 04250 } 04251 04252 for(i=0; i <= iend-2; ++i){ 04253 os << "$times_int("; 04254 os << e[i] << ","; 04255 } 04256 04257 os<< e[iend-1]; 04258 04259 for(i=0 ; i <= iend-2; ++i){ 04260 os << ")"; 04261 } 04262 04263 break; 04264 } 04265 case POW: 04266 04267 if(!isInteger(e[0])){ 04268 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04269 break; 04270 } 04271 04272 os << "$power_int(" << push << e[1] << space << "^ " << e[0] << push << ")"; 04273 break; 04274 04275 case DIVIDE: 04276 if(!isInteger(e[0])){ 04277 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04278 break; 04279 } 04280 04281 os << "divide_int(" <<e[0] << "," << e[1] << ")"; 04282 break; 04283 04284 case LT: 04285 if(!isInteger(e[0])){ 04286 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04287 break; 04288 } 04289 os << "$less_int(" << e[0] << "," << e[1] <<")"; 04290 break; 04291 04292 case LE: 04293 if(!isInteger(e[0])){ 04294 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04295 break; 04296 } 04297 04298 os << "$lesseq_int(" << e[0] << "," << e[1] << ")"; 04299 break; 04300 04301 case GT: 04302 if(!isInteger(e[0])){ 04303 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04304 break; 04305 } 04306 04307 os << "$greater_int(" << e[0] << "," << e[1] << ")"; 04308 break; 04309 04310 case GE: 04311 if(!isInteger(e[0])){ 04312 os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n"; 04313 break; 04314 } 04315 04316 os << "$greatereq_int(" << e[0] << "," << e[1] << ")"; 04317 break; 04318 case DARK_SHADOW: 04319 case GRAY_SHADOW: 04320 os <<"ERROR:SHADOW:not supported in TPTP\n"; 04321 break; 04322 04323 case INT: 04324 os <<"$int"; 04325 break; 04326 case REAL: 04327 os <<"ERROR:REAL not supported in TPTP\n"; 04328 default: 04329 // Print the top node in the default LISP format, continue with 04330 // pretty-printing for children. 04331 e.print(os); 04332 04333 break; 04334 } 04335 break; // end of case TPTP_LANG 04336 04337 case PRESENTATION_LANG: 04338 switch(e.getKind()) { 04339 case REAL: 04340 os << "REAL"; 04341 break; 04342 case INT: 04343 os << "INT"; 04344 break; 04345 case RATIONAL_EXPR: 04346 e.print(os); 04347 break; 04348 case NEGINF: 04349 os << "NEGINF"; 04350 break; 04351 case POSINF: 04352 os << "POSINF"; 04353 break; 04354 case SUBRANGE: 04355 if(e.arity() != 2) e.printAST(os); 04356 else 04357 os << "[" << push << e[0] << ".." << e[1] << push << "]"; 04358 break; 04359 case IS_INTEGER: 04360 if(e.arity() == 1) 04361 os << "IS_INTEGER(" << push << e[0] << push << ")"; 04362 else 04363 e.printAST(os); 04364 break; 04365 case PLUS: { 04366 int i=0, iend=e.arity(); 04367 os << "(" << push; 04368 if(i!=iend) os << e[i]; 04369 ++i; 04370 for(; i!=iend; ++i) os << space << "+ " << e[i]; 04371 os << push << ")"; 04372 break; 04373 } 04374 case MINUS: 04375 os << "(" << push << e[0] << space << "- " << e[1] << push << ")"; 04376 break; 04377 case UMINUS: 04378 os << "-(" << push << e[0] << push << ")"; 04379 break; 04380 case MULT: { 04381 int i=0, iend=e.arity(); 04382 os << "(" << push; 04383 if(i!=iend) os << e[i]; 04384 ++i; 04385 for(; i!=iend; ++i) os << space << "* " << e[i]; 04386 os << push << ")"; 04387 break; 04388 } 04389 case POW: 04390 os << "(" << push << e[1] << space << "^ " << e[0] << push << ")"; 04391 break; 04392 case DIVIDE: 04393 os << "(" << push << e[0] << space << "/ " << e[1] << push << ")"; 04394 break; 04395 case LT: 04396 if (isInt(e[0].getType()) || isInt(e[1].getType())) { 04397 } 04398 os << "(" << push << e[0] << space << "< " << e[1] << push << ")"; 04399 break; 04400 case LE: 04401 os << "(" << push << e[0] << space << "<= " << e[1] << push << ")"; 04402 break; 04403 case GT: 04404 os << "(" << push << e[0] << space << "> " << e[1] << push << ")"; 04405 break; 04406 case GE: 04407 os << "(" << push << e[0] << space << ">= " << e[1] << push << ")"; 04408 break; 04409 case DARK_SHADOW: 04410 os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")"; 04411 break; 04412 case GRAY_SHADOW: 04413 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1] 04414 << "," << space << e[2] << "," << space << e[3] << push << ")"; 04415 break; 04416 default: 04417 // Print the top node in the default LISP format, continue with 04418 // pretty-printing for children. 04419 e.printAST(os); 04420 04421 break; 04422 } 04423 break; // end of case PRESENTATION_LANG 04424 case SMTLIB_LANG: { 04425 switch(e.getKind()) { 04426 case REAL_CONST: 04427 printRational(os, e[0].getRational(), true); 04428 break; 04429 case RATIONAL_EXPR: 04430 printRational(os, e.getRational()); 04431 break; 04432 case REAL: 04433 os << "Real"; 04434 break; 04435 case INT: 04436 os << "Int"; 04437 break; 04438 case SUBRANGE: 04439 throw SmtlibException("TheoryArithOld::print: SMTLIB: SUBRANGE not implemented"); 04440 // if(e.arity() != 2) e.print(os); 04441 // else 04442 // os << "(" << push << "SUBRANGE" << space << e[0] 04443 // << space << e[1] << push << ")"; 04444 break; 04445 case IS_INTEGER: 04446 if(e.arity() == 1) 04447 os << "(" << push << "IsInt" << space << e[0] << push << ")"; 04448 else 04449 throw SmtlibException("TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly"); 04450 break; 04451 case PLUS: { 04452 os << "(" << push << "+"; 04453 Expr::iterator i = e.begin(), iend = e.end(); 04454 for(; i!=iend; ++i) { 04455 os << space << (*i); 04456 } 04457 os << push << ")"; 04458 break; 04459 } 04460 case MINUS: { 04461 os << "(" << push << "- " << e[0] << space << e[1] << push << ")"; 04462 break; 04463 } 04464 case UMINUS: { 04465 os << "(" << push << "~" << space << e[0] << push << ")"; 04466 break; 04467 } 04468 case MULT: { 04469 int i=0, iend=e.arity(); 04470 for(; i!=iend; ++i) { 04471 if (i < iend-1) { 04472 os << "(" << push << "*"; 04473 } 04474 os << space << e[i]; 04475 } 04476 for (i=0; i < iend-1; ++i) os << push << ")"; 04477 break; 04478 } 04479 case POW: 04480 if (e[0].isRational() && e[0].getRational().isInteger()) { 04481 int i=0, iend=e[0].getRational().getInt(); 04482 for(; i!=iend; ++i) { 04483 if (i < iend-1) { 04484 os << "(" << push << "*"; 04485 } 04486 os << space << e[1]; 04487 } 04488 for (i=0; i < iend-1; ++i) os << push << ")"; 04489 } 04490 else 04491 throw SmtlibException("TheoryArithOld::print: SMTLIB: POW not supported: " + e.toString(PRESENTATION_LANG)); 04492 // os << "(" << push << "^ " << e[1] << space << e[0] << push << ")"; 04493 break; 04494 case DIVIDE: { 04495 throw SmtlibException("TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE"); 04496 break; 04497 } 04498 case LT: { 04499 Rational r; 04500 os << "(" << push << "<" << space; 04501 os << e[0] << space << e[1] << push << ")"; 04502 break; 04503 } 04504 case LE: { 04505 Rational r; 04506 os << "(" << push << "<=" << space; 04507 os << e[0] << space << e[1] << push << ")"; 04508 break; 04509 } 04510 case GT: { 04511 Rational r; 04512 os << "(" << push << ">" << space; 04513 os << e[0] << space << e[1] << push << ")"; 04514 break; 04515 } 04516 case GE: { 04517 Rational r; 04518 os << "(" << push << ">=" << space; 04519 os << e[0] << space << e[1] << push << ")"; 04520 break; 04521 } 04522 case DARK_SHADOW: 04523 throw SmtlibException("TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported"); 04524 os << "(" << push << "DARK_SHADOW" << space << e[0] 04525 << space << e[1] << push << ")"; 04526 break; 04527 case GRAY_SHADOW: 04528 throw SmtlibException("TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported"); 04529 os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1] 04530 << "," << space << e[2] << "," << space << e[3] << push << ")"; 04531 break; 04532 default: 04533 throw SmtlibException("TheoryArithOld::print: SMTLIB: default not supported"); 04534 // Print the top node in the default LISP format, continue with 04535 // pretty-printing for children. 04536 e.printAST(os); 04537 04538 break; 04539 } 04540 break; // end of case SMTLIB_LANG 04541 } 04542 case LISP_LANG: 04543 switch(e.getKind()) { 04544 case REAL: 04545 case INT: 04546 case RATIONAL_EXPR: 04547 case NEGINF: 04548 case POSINF: 04549 e.print(os); 04550 break; 04551 case SUBRANGE: 04552 if(e.arity() != 2) e.printAST(os); 04553 else 04554 os << "(" << push << "SUBRANGE" << space << e[0] 04555 << space << e[1] << push << ")"; 04556 break; 04557 case IS_INTEGER: 04558 if(e.arity() == 1) 04559 os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")"; 04560 else 04561 e.printAST(os); 04562 break; 04563 case PLUS: { 04564 int i=0, iend=e.arity(); 04565 os << "(" << push << "+"; 04566 for(; i!=iend; ++i) os << space << e[i]; 04567 os << push << ")"; 04568 break; 04569 } 04570 case MINUS: 04571 //os << "(" << push << e[0] << space << "- " << e[1] << push << ")"; 04572 os << "(" << push << "- " << e[0] << space << e[1] << push << ")"; 04573 break; 04574 case UMINUS: 04575 os << "(" << push << "-" << space << e[0] << push << ")"; 04576 break; 04577 case MULT: { 04578 int i=0, iend=e.arity(); 04579 os << "(" << push << "*"; 04580 for(; i!=iend; ++i) os << space << e[i]; 04581 os << push << ")"; 04582 break; 04583 } 04584 case POW: 04585 os << "(" << push << "^ " << e[1] << space << e[0] << push << ")"; 04586 break; 04587 case DIVIDE: 04588 os << "(" << push << "/ " << e[0] << space << e[1] << push << ")"; 04589 break; 04590 case LT: 04591 os << "(" << push << "< " << e[0] << space << e[1] << push << ")"; 04592 break; 04593 case LE: 04594 os << "(" << push << "<= " << e[0] << space << e[1] << push << ")"; 04595 break; 04596 case GT: 04597 os << "(" << push << "> " << e[1] << space << e[0] << push << ")"; 04598 break; 04599 case GE: 04600 os << "(" << push << ">= " << e[0] << space << e[1] << push << ")"; 04601 break; 04602 case DARK_SHADOW: 04603 os << "(" << push << "DARK_SHADOW" << space << e[0] 04604 << space << e[1] << push << ")"; 04605 break; 04606 case GRAY_SHADOW: 04607 os << "(" << push << "GRAY_SHADOW" << space << e[0] << space 04608 << e[1] << space << e[2] << space << e[3] << push << ")"; 04609 break; 04610 default: 04611 // Print the top node in the default LISP format, continue with 04612 // pretty-printing for children. 04613 e.printAST(os); 04614 04615 break; 04616 } 04617 break; // end of case LISP_LANG 04618 default: 04619 // Print the top node in the default LISP format, continue with 04620 // pretty-printing for children. 04621 e.printAST(os); 04622 } 04623 return os; 04624 } 04625 04626 Theorem TheoryArithOld::inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS) { 04627 04628 // Which side of the inequality 04629 int index = (normalizeRHS ? 1 : 0); 04630 04631 TRACE("arith find", "inequalityToFind(", int2string(index) + ", " + inequalityThm.getExpr().toString(), ")"); 04632 04633 // Get the inequality expression 04634 const Expr& inequality = inequalityThm.getExpr(); 04635 04636 // The theorem we will return 04637 Theorem inequalityFindThm; 04638 04639 // If the inequality side has a find 04640 if (inequality[index].hasFind()) { 04641 // Get the find of the rhs (lhs) 04642 Theorem rhsFindThm = inequality[index].getFind(); 04643 // Get the theorem simplifys the find (in case the updates haven't updated all the finds yet 04644 // Fixed with d_theroyCore.inUpdate() 04645 rhsFindThm = transitivityRule(rhsFindThm, simplify(rhsFindThm.getRHS())); 04646 // If not the same as the original 04647 Expr rhsFind = rhsFindThm.getRHS(); 04648 if (rhsFind != inequality[index]) { 04649 // Substitute in the inequality 04650 vector<unsigned> changed; 04651 vector<Theorem> children; 04652 changed.push_back(index); 04653 children.push_back(rhsFindThm); 04654 rhsFindThm = iffMP(inequalityThm, substitutivityRule(inequality, changed, children)); 04655 // If on the left-hand side, we are done 04656 if (index == 0) 04657 inequalityFindThm = rhsFindThm; 04658 else 04659 // If on the right-hand side and left-hand side is 0, normalize it 04660 if (inequality[0].isRational() && inequality[0].getRational() == 0) 04661 inequalityFindThm = normalize(rhsFindThm); 04662 else 04663 inequalityFindThm = rhsFindThm; 04664 } else 04665 inequalityFindThm = inequalityThm; 04666 } else 04667 inequalityFindThm = inequalityThm; 04668 04669 04670 TRACE("arith find", "inequalityToFind ==>", inequalityFindThm.getExpr(), ""); 04671 04672 return inequalityFindThm; 04673 } 04674 04675 void TheoryArithOld::registerAtom(const Expr& e) { 04676 // Trace it 04677 TRACE("arith atoms", "registerAtom(", e.toString(), ")"); 04678 04679 // Mark it 04680 formulaAtoms[e] = true; 04681 04682 // If it is a atomic formula, add it to the map 04683 if (e.isAbsAtomicFormula() && isIneq(e)) { 04684 Expr rightSide = e[1]; 04685 Rational leftSide = e[0].getRational(); 04686 04687 //Get the terms for : c1 op t1 and t2 -op c2 04688 Expr t1, t2; 04689 Rational c1, c2; 04690 extractTermsFromInequality(e, c1, t1, c2, t2); 04691 04692 if (true) { 04693 TRACE("arith atoms", "registering lower bound for ", t1.toString(), " = " + c1.toString() + ")"); 04694 formulaAtomLowerBound[t1].insert(pair<Rational, Expr>(c1, e)); 04695 04696 // See if the bounds on the registered term can infered from already asserted facts 04697 CDMap<Expr, Rational>::iterator lowerBoundFind = termLowerBound.find(t1); 04698 if (lowerBoundFind != termLowerBound.end()) { 04699 Rational boundValue = (*lowerBoundFind).second; 04700 Theorem boundThm = termLowerBoundThm[t1]; 04701 Expr boundIneq = boundThm.getExpr(); 04702 if (boundValue > c1 || (boundValue == c1 && !(boundIneq.getKind() == LE && e.getKind() == LT))) { 04703 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyWeakerInequality(boundIneq, e))); 04704 } 04705 } 04706 04707 // See if the bounds on the registered term can falsified from already asserted facts 04708 CDMap<Expr, Rational>::iterator upperBoundFind = termUpperBound.find(t1); 04709 if (upperBoundFind != termUpperBound.end()) { 04710 Rational boundValue = (*upperBoundFind).second; 04711 Theorem boundThm = termUpperBoundThm[t1]; 04712 Expr boundIneq = boundThm.getExpr(); 04713 if (boundValue < c1 || (boundValue == c1 && boundIneq.getKind() == LT && e.getKind() == LT)) { 04714 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyNegatedInequality(boundIneq, e))); 04715 } 04716 } 04717 04718 TRACE("arith atoms", "registering upper bound for ", t2.toString(), " = " + c2.toString() + ")"); 04719 formulaAtomUpperBound[t2].insert(pair<Rational, Expr>(c2, e)); 04720 } 04721 } 04722 } 04723 04724 TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph(TheoryArithOld* arith, TheoryCore* core, ArithProofRules* rules, Context* context) 04725 : d_pathLenghtThres(&(core->getFlags()["pathlength-threshold"].getInt())), 04726 arith(arith), 04727 core(core), 04728 rules(rules), 04729 unsat_theorem(context), 04730 biggestEpsilon(context, 0, 0), 04731 smallestPathDifference(context, 1, 0), 04732 leGraph(context), 04733 varInCycle(context) 04734 { 04735 } 04736 04737 Theorem TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem() { 04738 return unsat_theorem; 04739 } 04740 04741 bool TheoryArithOld::DifferenceLogicGraph::isUnsat() { 04742 return !getUnsatTheorem().isNull(); 04743 } 04744 04745 bool TheoryArithOld::DifferenceLogicGraph::existsEdge(const Expr& x, const Expr& y) { 04746 Expr index = x - y; 04747 04748 Graph::iterator find_le = leGraph.find(index); 04749 if (find_le != leGraph.end()) { 04750 EdgeInfo edge_info = (*find_le).second; 04751 if (edge_info.isDefined()) return true; 04752 } 04753 04754 return false; 04755 } 04756 04757 bool TheoryArithOld::DifferenceLogicGraph::inCycle(const Expr& x) { 04758 return (varInCycle.find(x) != varInCycle.end()); 04759 } 04760 04761 TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference TheoryArithOld::DifferenceLogicGraph::getEdge(const Expr& x, const Expr& y) { 04762 Expr index = x - y; 04763 Graph::ElementReference edge_info = leGraph[index]; 04764 04765 // If a new edge and x != y, then add vertices to the apropriate lists 04766 if (x != y && !edge_info.get().isDefined()) { 04767 04768 // Adding a new edge, take a resource 04769 core->getResource(); 04770 04771 EdgesList::iterator y_it = incomingEdges.find(y); 04772 if (y_it == incomingEdges.end() || (*y_it).second == 0) { 04773 CDList<Expr>* list = new(true) CDList<Expr>(core->getCM()->getCurrentContext()); 04774 list->push_back(x); 04775 incomingEdges[y] = list; 04776 } else 04777 ((*y_it).second)->push_back(x); 04778 04779 EdgesList::iterator x_it = outgoingEdges.find(x); 04780 if (x_it == outgoingEdges.end() || (*x_it).second == 0) { 04781 CDList<Expr>* list = new(true) CDList<Expr>(core->getCM()->getCurrentContext()); 04782 list->push_back(y); 04783 outgoingEdges[x] = list; 04784 } else 04785 ((*x_it).second)->push_back(y); 04786 } 04787 04788 return edge_info; 04789 } 04790 04791 TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(const Expr& x, const Expr& y) { 04792 if (!existsEdge(x, y)) 04793 return EpsRational::PlusInfinity; 04794 else { 04795 EdgeInfo edgeInfo = getEdge(x, y).get(); 04796 return edgeInfo.length; 04797 } 04798 } 04799 04800 04801 void TheoryArithOld::DifferenceLogicGraph::addEdge(const Expr& x, const Expr& y, const Rational& bound, const Theorem& edge_thm) { 04802 04803 TRACE("arith diff", x, " --> ", y); 04804 DebugAssert(x != y, "addEdge, given two equal expressions!"); 04805 04806 if (isUnsat()) return; 04807 04808 // If out of resources, bail out 04809 if (core->outOfResources()) return; 04810 04811 // Get the kind of the inequality (NOTE isNull -- for model computation we add a vertex with no theorem) 04812 // FIXME: Later, add a debug assert for the theorem that checks that this variable is cvc3diffLogicSource 04813 int kind = (edge_thm.isNull() ? LE : edge_thm.getExpr().getKind()); 04814 DebugAssert(kind == LT || kind == LE, "addEdge, not an <= or <!"); 04815 04816 // Get the EpsRational bound 04817 Rational k = (kind == LE ? 0 : -1); 04818 EpsRational c(bound, k); 04819 04820 // Get the current (or a fresh new edge info) 04821 Graph::ElementReference edgeInfoRef = getEdge(x, y); 04822 // If uninitialized, or smaller length (we prefer shorter paths, so one edge is better) 04823 EdgeInfo edgeInfo = edgeInfoRef.get(); 04824 // If the edge changed to the better, do the work 04825 if (!edgeInfo.isDefined() || c <= edgeInfo.length) { 04826 04827 // Update model generation data 04828 if (edgeInfo.isDefined()) { 04829 EpsRational difference = edgeInfo.length - c; 04830 Rational rationalDifference = difference.getRational(); 04831 if (rationalDifference > 0 && rationalDifference < smallestPathDifference) { 04832 smallestPathDifference = rationalDifference; 04833 TRACE("diff model", "smallest path difference : ", smallestPathDifference, ""); 04834 } 04835 } 04836 Rational newEpsilon = - c.getEpsilon(); 04837 if (newEpsilon > biggestEpsilon) { 04838 biggestEpsilon = newEpsilon; 04839 TRACE("diff model", "biggest epsilon : ", biggestEpsilon, ""); 04840 } 04841 04842 // Set the edge info 04843 edgeInfo.length = c; 04844 edgeInfo.explanation = edge_thm; 04845 edgeInfo.path_length_in_edges = 1; 04846 edgeInfoRef = edgeInfo; 04847 04848 04849 // Try simple cycle x --> y --> x, to keep invariants (no cycles or one negative) 04850 if (existsEdge(y, x)) { 04851 varInCycle[x] = true; 04852 varInCycle[y] = true; 04853 tryUpdate(x, y, x); 04854 if (isUnsat()) 04855 return; 04856 } 04857 04858 // For all edges coming into x, z ---> x, update z ---> y and add updated ones to the updated_in_y vector 04859 CDList<Expr>* in_x = incomingEdges[x]; 04860 vector<Expr> updated_in_y; 04861 updated_in_y.push_back(x); 04862 04863 // If there 04864 if (in_x) { 04865 IF_DEBUG(int total = 0; int updated = 0;); 04866 for (unsigned it = 0; it < in_x->size() && !isUnsat(); it ++) { 04867 const Expr& z = (*in_x)[it]; 04868 if (z != arith->zero && z.hasFind() && core->find(z).getRHS() != z) continue; 04869 if (z != y && z != x && x != y) { 04870 IF_DEBUG(total ++;); 04871 TRACE("diff update", "trying with ", z.toString() + " --> ", x.toString()); 04872 if (tryUpdate(z, x, y)) { 04873 updated_in_y.push_back(z); 04874 IF_DEBUG(updated++;); 04875 } 04876 } 04877 } 04878 TRACE("diff updates", "Updates : ", int2string(updated), " of " + int2string(total)); 04879 } 04880 04881 // For all edges coming into y, z_1 ---> y, and all edges going out of y, y ---> z_2, update z1 --> z_2 04882 CDList<Expr>* out_y = outgoingEdges[y]; 04883 if (out_y) 04884 for (unsigned it_z1 = 0; it_z1 < updated_in_y.size() && !isUnsat(); it_z1 ++) { 04885 for (unsigned it_z2 = 0; it_z2 < out_y->size() && !isUnsat(); it_z2 ++) { 04886 const Expr& z1 = updated_in_y[it_z1]; 04887 const Expr& z2 = (*out_y)[it_z2]; 04888 if (z2 != arith->zero && z2.hasFind() && core->find(z2).getRHS() != z2) continue; 04889 if (z1 != z2 && z1 != y && z2 != y) 04890 tryUpdate(z1, y, z2); 04891 } 04892 } 04893 04894 } else { 04895 TRACE("arith propagate", "could have propagated ", edge_thm.getExpr(), edge_thm.isAssump() ? " ASSUMPTION " : "not assumption"); 04896 04897 } 04898 04899 } 04900 04901 void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(const Expr& x, const Expr& z, const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems) { 04902 TRACE("arith diff", "Getting theorems from ", x, " to " + z.toString() + " length = " + edgeInfo.length.toString() + ", edge_length = " + int2string(edgeInfo.path_length_in_edges)); 04903 04904 if (edgeInfo.path_length_in_edges == 1) { 04905 DebugAssert(x == sourceVertex || z == sourceVertex || !edgeInfo.explanation.isNull(), "Edge from " + x.toString() + " to " + z.toString() + " has no theorem!"); 04906 if (x != sourceVertex && z != sourceVertex) 04907 outputTheorems.push_back(edgeInfo.explanation); 04908 } 04909 else { 04910 const Expr& y = edgeInfo.in_path_vertex; 04911 EdgeInfo x_y = getEdge(x, y); 04912 DebugAssert(x_y.isDefined(), "getEdgeTheorems: the cycle edge is not defined!"); 04913 EdgeInfo y_z = getEdge(y, z); 04914 DebugAssert(y_z.isDefined(), "getEdgeTheorems: the cycle edge is not defined!"); 04915 getEdgeTheorems(x, y, x_y, outputTheorems); 04916 getEdgeTheorems(y, z, y_z, outputTheorems); 04917 } 04918 } 04919 04920 void TheoryArithOld::DifferenceLogicGraph::analyseConflict(const Expr& x, int kind) { 04921 04922 // Get the cycle info 04923 Graph::ElementReference x_x_cycle_ref = getEdge(x, x); 04924 EdgeInfo x_x_cycle = x_x_cycle_ref.get(); 04925 04926 DebugAssert(x_x_cycle.isDefined(), "analyseConflict: the cycle edge is not defined!"); 04927 04928 // Vector to keep the theorems in 04929 vector<Theorem> inequalities; 04930 04931 // Get the theorems::analyse 04932 getEdgeTheorems(x, x, x_x_cycle, inequalities); 04933 04934 // Set the unsat theorem 04935 unsat_theorem = rules->cycleConflict(inequalities); 04936 04937 TRACE("diff unsat", "negative cycle : ", int2string(inequalities.size()), " vertices."); 04938 } 04939 04940 bool TheoryArithOld::DifferenceLogicGraph::tryUpdate(const Expr& x, const Expr& y, const Expr& z) { 04941 04942 // x -> y -> z, if z -> x they are all in a cycle 04943 if (existsEdge(z, x)) { 04944 varInCycle[x] = true; 04945 varInCycle[y] = true; 04946 varInCycle[z] = true; 04947 } 04948 04949 //Get all the edges 04950 Graph::ElementReference x_y_le_ref = getEdge(x, y); 04951 EdgeInfo x_y_le = x_y_le_ref; 04952 if (*d_pathLenghtThres >= 0 && x_y_le.path_length_in_edges > *d_pathLenghtThres) return false; 04953 04954 Graph::ElementReference y_z_le_ref = getEdge(y, z); 04955 EdgeInfo y_z_le = y_z_le_ref; 04956 if (*d_pathLenghtThres >= 0 && y_z_le.path_length_in_edges > *d_pathLenghtThres) return false; 04957 04958 Graph::ElementReference x_z_le_ref = getEdge(x, z); 04959 EdgeInfo x_z_le = x_z_le_ref; 04960 04961 bool cycle = (x == z); 04962 bool updated = false; 04963 04964 // Try <= + <= --> <= 04965 if (!isUnsat() && x_y_le.isDefined() && y_z_le.isDefined()) { 04966 EpsRational combined_length = x_y_le.length + y_z_le.length; 04967 int combined_edge_length = x_y_le.path_length_in_edges + y_z_le.path_length_in_edges; 04968 04969 if (!x_z_le.isDefined() || combined_length < x_z_le.length || 04970 (combined_length == x_z_le.length && (combined_edge_length < x_z_le.path_length_in_edges))) { 04971 04972 if (!cycle || combined_length <= EpsRational::Zero) { 04973 04974 if (!cycle || combined_length < EpsRational::Zero) { 04975 04976 // Remember the path differences 04977 if (!cycle) { 04978 EpsRational difference = x_z_le.length - combined_length; 04979 Rational rationalDifference = difference.getRational(); 04980 Rational newEpsilon = - x_z_le.length.getEpsilon(); 04981 if (rationalDifference > 0 && rationalDifference < smallestPathDifference) { 04982 smallestPathDifference = rationalDifference; 04983 TRACE("diff model", "smallest path difference : ", smallestPathDifference, ""); 04984 } 04985 if (newEpsilon > biggestEpsilon) { 04986 biggestEpsilon = newEpsilon; 04987 TRACE("diff model", "biggest epsilon : ", biggestEpsilon, ""); 04988 } 04989 } 04990 04991 // If we have a constraint among two integers variables strenghten it 04992 bool addAndEnqueue = false; 04993 if (core->okToEnqueue() && !combined_length.isInteger()) 04994 if (x.getType() == arith->intType() && z.getType() == arith->intType()) 04995 addAndEnqueue = true; 04996 04997 x_z_le.length = combined_length; 04998 x_z_le.path_length_in_edges = combined_edge_length; 04999 x_z_le.in_path_vertex = y; 05000 x_z_le_ref = x_z_le; 05001 05002 if (addAndEnqueue) { 05003 vector<Theorem> pathTheorems; 05004 getEdgeTheorems(x, z, x_z_le, pathTheorems); 05005 core->enqueueFact(rules->addInequalities(pathTheorems)); 05006 } 05007 05008 TRACE("arith diff", x.toString() + " -- > " + z.toString(), " : ", combined_length.toString()); 05009 updated = true; 05010 } else 05011 if (core->okToEnqueue()) { 05012 // 0 length cycle 05013 vector<Theorem> antecedentThms; 05014 getEdgeTheorems(x, y, x_y_le, antecedentThms); 05015 getEdgeTheorems(y, z, y_z_le, antecedentThms); 05016 core->enqueueFact(rules->implyEqualities(antecedentThms)); 05017 } 05018 05019 // Try to propagate somthing in the original formula 05020 if (updated && !cycle && x != sourceVertex && z != sourceVertex && core->okToEnqueue()) 05021 arith->tryPropagate(x, z, x_z_le, LE); 05022 05023 } 05024 05025 if (cycle && combined_length < EpsRational::Zero) 05026 analyseConflict(x, LE); 05027 } 05028 } 05029 05030 return updated; 05031 } 05032 05033 void TheoryArithOld::DifferenceLogicGraph::expandSharedTerm(const Expr& x) { 05034 05035 } 05036 05037 TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph() { 05038 for (EdgesList::iterator it = incomingEdges.begin(), it_end = incomingEdges.end(); it != it_end; it ++) { 05039 if ((*it).second) { 05040 delete (*it).second; 05041 free ((*it).second); 05042 } 05043 } 05044 for (EdgesList::iterator it = outgoingEdges.begin(), it_end = outgoingEdges.end(); it != it_end; it ++) { 05045 if ((*it).second) { 05046 delete (*it).second; 05047 free ((*it).second); 05048 } 05049 } 05050 } 05051 05052 void TheoryArithOld::tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind) { 05053 05054 TRACE("diff atoms", "trying propagation", " x = " + x.toString(), " y = " + y.toString()); 05055 05056 // bail on non representative terms (we don't pass non-representative terms) 05057 // if (x.hasFind() && find(x).getRHS() != x) return; 05058 // if (y.hasFind() && find(y).getRHS() != y) return; 05059 05060 // given edge x - z (kind) lenth 05061 05062 // Make the index (c1 <= y - x) 05063 vector<Expr> t1_summands; 05064 t1_summands.push_back(rat(0)); 05065 if (y != zero) t1_summands.push_back(y); 05066 // We have to canonize in case it is nonlinear 05067 // nonlinear terms are canonized with a constants --> 1*x*y, hence (-1)*1*x*y will not be canonical 05068 if (x != zero) t1_summands.push_back(canon(rat(-1)*x).getRHS()); 05069 Expr t1 = canon(plusExpr(t1_summands)).getRHS(); 05070 05071 TRACE("diff atoms", "trying propagation", " t1 = " + t1.toString(), ""); 05072 05073 // The constant c1 <= y - x 05074 Rational c1 = - x_y_edge.length.getRational(); 05075 05076 // See if we can propagate anything to the formula atoms 05077 // c1 <= t1 ===> c <= t1 for c < c1 05078 AtomsMap::iterator find = formulaAtomLowerBound.find(t1); 05079 AtomsMap::iterator find_end = formulaAtomLowerBound.end(); 05080 if (find != find_end) { 05081 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin(); 05082 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end(); 05083 while (bounds != bounds_end) { 05084 const Expr& implied = (*bounds).second; 05085 // Try to do some theory propagation 05086 if ((*bounds).first < c1 || (implied.getKind() == LE && (*bounds).first == c1)) { 05087 TRACE("diff atoms", "found propagation", "", ""); 05088 // c1 <= t1 => c <= t1 (for c <= c1) 05089 // c1 < t1 => c <= t1 (for c <= c1) 05090 // c1 <= t1 => c < t1 (for c < c1) 05091 vector<Theorem> antecedentThms; 05092 diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms); 05093 Theorem impliedThm = d_rules->implyWeakerInequalityDiffLogic(antecedentThms, implied); 05094 enqueueFact(impliedThm); 05095 } 05096 bounds ++; 05097 } 05098 } 05099 05100 // 05101 // c1 <= t1 ==> !(t1 <= c) for c < c1 05102 // ==> !(-c <= t2) 05103 // i.e. all coefficient in in the implied are opposite of t1 05104 find = formulaAtomUpperBound.find(t1); 05105 find_end = formulaAtomUpperBound.end(); 05106 if (find != find_end) { 05107 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin(); 05108 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end(); 05109 while (bounds != bounds_end) { 05110 const Expr& implied = (*bounds).second; 05111 // Try to do some theory propagation 05112 if ((*bounds).first < c1) { 05113 TRACE("diff atoms", "found negated propagation", "", ""); 05114 vector<Theorem> antecedentThms; 05115 diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms); 05116 Theorem impliedThm = d_rules->implyNegatedInequalityDiffLogic(antecedentThms, implied); 05117 enqueueFact(impliedThm); 05118 } 05119 bounds ++; 05120 } 05121 } 05122 } 05123 05124 void TheoryArithOld::DifferenceLogicGraph::computeModel() { 05125 05126 // If source vertex is null, create it 05127 if (sourceVertex.isNull()) { 05128 Theorem thm_exists_zero = arith->getCommonRules()->varIntroSkolem(arith->zero); 05129 sourceVertex = thm_exists_zero.getExpr()[1]; 05130 } 05131 05132 // The empty theorem to pass around 05133 Theorem thm; 05134 05135 // Add an edge to all the vertices 05136 EdgesList::iterator vertexIt = incomingEdges.begin(); 05137 EdgesList::iterator vertexItEnd = incomingEdges.end(); 05138 for (; vertexIt != vertexItEnd; vertexIt ++) { 05139 Expr vertex = (*vertexIt).first; 05140 if (core->find(vertex).getRHS() != vertex) continue; 05141 if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex)) 05142 addEdge(sourceVertex, vertex, 0, thm); 05143 } 05144 vertexIt = outgoingEdges.begin(); 05145 vertexItEnd = outgoingEdges.end(); 05146 for (; vertexIt != vertexItEnd; vertexIt ++) { 05147 Expr vertex = (*vertexIt).first; 05148 if (core->find(vertex).getRHS() != vertex) continue; 05149 if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex)) 05150 addEdge(sourceVertex, vertex, 0, thm); 05151 } 05152 05153 // Also add an edge to cvcZero 05154 if (!existsEdge(sourceVertex, arith->zero)) 05155 addEdge(sourceVertex, arith->zero, 0, thm); 05156 05157 // For the < edges we will have a small enough epsilon to add 05158 // So, we will upper-bound the number of vertices and then divide 05159 // the smallest edge with that number so as to not be able to bypass 05160 05161 } 05162 05163 Rational TheoryArithOld::DifferenceLogicGraph::getValuation(const Expr& x) { 05164 05165 // For numbers, return it's value 05166 if (x.isRational()) return x.getRational(); 05167 05168 // For the source vertex, we don't care 05169 if (x == sourceVertex) return 0; 05170 05171 // The path from source to targer vertex 05172 Graph::ElementReference x_le_c_ref = getEdge(sourceVertex, x); 05173 EdgeInfo x_le_c = x_le_c_ref; 05174 05175 // The path from source to zero (adjusment) 05176 Graph::ElementReference zero_le_c_ref = getEdge(sourceVertex, arith->zero); 05177 EdgeInfo zero_le_c = zero_le_c_ref; 05178 05179 TRACE("diff model", "zero adjustment: ", zero_le_c.length.getRational(), ""); 05180 TRACE("diff model", "zero adjustment (eps): ", zero_le_c.length.getEpsilon(), ""); 05181 05182 // Value adjusted with the epsilon 05183 Rational epsAdjustment = (biggestEpsilon > 0 ? (x_le_c.length.getEpsilon() - zero_le_c.length.getEpsilon()) * smallestPathDifference / (2 * (biggestEpsilon + 1)) : 0); 05184 Rational value = x_le_c.length.getRational() + epsAdjustment; 05185 05186 TRACE("diff model" , "biggest epsilon: ", biggestEpsilon, ""); 05187 TRACE("diff model" , "smallestPathDifference: ", smallestPathDifference, ""); 05188 TRACE("diff model" , "x_le_c.getEpsilon: ", x_le_c.length.getEpsilon(), ""); 05189 TRACE("diff model" , "x_le_c.length: ", x_le_c.length.getRational(), ""); 05190 05191 // Value adjusted with the shift for zero 05192 value = zero_le_c.length.getRational() - value; 05193 05194 TRACE("diff model", "Value of ", x, " : " + value.toString()); 05195 05196 // Return it 05197 return value; 05198 } 05199 05200 // The infinity constant 05201 const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::PlusInfinity(PLUS_INFINITY); 05202 // The negative infinity constant 05203 const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::MinusInfinity(MINUS_INFINITY); 05204 // The negative infinity constant 05205 const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::Zero; 05206 05207 void TheoryArithOld::addMultiplicativeSignSplit(const Theorem& case_split_thm) { 05208 multiplicativeSignSplits.push_back(case_split_thm); 05209 } 05210 05211 bool TheoryArithOld::addPairToArithOrder(const Expr& smaller, const Expr& bigger) { 05212 TRACE("arith var order", "addPairToArithOrder(" + smaller.toString(), ", ", bigger.toString() + ")"); 05213 // We only accept arithmetic terms 05214 if (!isReal(smaller.getType()) && !isInt(smaller.getType())) return false; 05215 if (!isReal(bigger.getType()) && !isInt(bigger.getType())) return false; 05216 // We don't want to introduce loops 05217 FatalAssert(!d_graph.lessThan(smaller, bigger), "The pair (" + bigger.toString() + "," + smaller.toString() + ") is already in the order"); 05218 // Update the graph 05219 d_graph.addEdge(smaller, bigger); 05220 return true; 05221 } 05222 05223 bool TheoryArithOld::isNonlinearSumTerm(const Expr& term) { 05224 if (isPow(term)) return true; 05225 if (!isMult(term)) return false; 05226 int vars = 0; 05227 for (int j = 0; j < term.arity(); j ++) 05228 if (isPow(term[j])) return true; 05229 else if (isLeaf(term[j])) { 05230 vars ++; 05231 if (vars > 1) return true; 05232 } 05233 return false; 05234 } 05235 05236 bool TheoryArithOld::isNonlinearEq(const Expr& e) { 05237 05238 DebugAssert(e.isEq(), "TheoryArithOld::isNonlinear: expecting an equation" + e.toString()); 05239 05240 const Expr& lhs = e[0]; 05241 const Expr& rhs = e[1]; 05242 05243 if (isNonlinearSumTerm(lhs) || isNonlinearSumTerm(rhs)) return true; 05244 05245 // Check the right-hand side 05246 for (int i = 0; i < lhs.arity(); i ++) 05247 if (isNonlinearSumTerm(lhs[i])) return true; 05248 05249 // Check the left hand side 05250 for (int i = 0; i < rhs.arity(); i ++) 05251 if (isNonlinearSumTerm(rhs[i])) return true; 05252 05253 return false; 05254 } 05255 05256 05257 bool TheoryArithOld::isPowersEquality(const Expr& eq, Expr& power1, Expr& power2) { 05258 // equality should be in the form 0 + x1^n - x2^n = 0 05259 DebugAssert(eq.isEq(), "TheoryArithOld::isPowersEquality, expecting an equality got " + eq.toString()); 05260 05261 if (!isPlus(eq[0])) return false; 05262 if (eq[0].arity() != 3) return false; 05263 if (!(eq[0][0].isRational()) || !(eq[0][0].getRational() == 0)) return false; 05264 05265 // Process the first term 05266 Expr term1 = eq[0][1]; 05267 Rational term1_c; 05268 if (isPow(term1)) { 05269 term1_c = 1; 05270 power1 = term1; 05271 } else 05272 if (isMult(term1) && term1.arity() == 2) { 05273 if (term1[0].isRational()) { 05274 term1_c = term1[0].getRational(); 05275 if (isPow(term1[1])) { 05276 if (term1_c == 1) power1 = term1[1]; 05277 else if (term1_c == -1) power2 = term1[1]; 05278 else return false; 05279 } else return false; 05280 } else return false; 05281 } else return false; 05282 05283 // Process the second term 05284 Expr term2 = eq[0][2]; 05285 Rational term2_c; 05286 if (isPow(term2)) { 05287 term2_c = 1; 05288 power1 = term2; 05289 } else 05290 if (isMult(term2) && term2.arity() == 2) { 05291 if (term2[0].isRational()) { 05292 term2_c = term2[0].getRational(); 05293 if (isPow(term2[1])) { 05294 if (term2_c == 1) power1 = term2[1]; 05295 else if (term2_c == -1) power2 = term2[1]; 05296 else return false; 05297 } else return false; 05298 } else return false; 05299 } else return false; 05300 05301 // Check that they are of opposite signs 05302 if (term1_c == term2_c) return false; 05303 05304 // Check that the powers are equal numbers 05305 if (!power1[0].isRational()) return false; 05306 if (!power2[0].isRational()) return false; 05307 if (power1[0].getRational() != power2[0].getRational()) return false; 05308 05309 // Everything is fine 05310 return true; 05311 } 05312 05313 bool TheoryArithOld::isPowerEquality(const Expr& eq, Rational& constant, Expr& power1) { 05314 DebugAssert(eq.isEq(), "TheoryArithOld::isPowerEquality, expecting an equality got " + eq.toString()); 05315 05316 if (!isPlus(eq[0])) return false; 05317 if (eq[0].arity() != 2) return false; 05318 if (!eq[0][0].isRational()) return false; 05319 05320 constant = eq[0][0].getRational(); 05321 05322 Expr term = eq[0][1]; 05323 if (isPow(term)) { 05324 power1 = term; 05325 constant = -constant; 05326 } else 05327 if (isMult(term) && term.arity() == 2) { 05328 if (term[0].isRational() && isPow(term[1])) { 05329 Rational term2_c = term[0].getRational(); 05330 if (term2_c == 1) { 05331 power1 = term[1]; 05332 constant = -constant; 05333 } else if (term2_c == -1) { 05334 power1 = term[1]; 05335 return true; 05336 } else return false; 05337 } else return false; 05338 } else return false; 05339 05340 // Check that the power is an integer 05341 if (!power1[0].isRational()) return false; 05342 if (!power1[0].getRational().isInteger()) return false; 05343 05344 return true; 05345 } 05346 05347 int TheoryArithOld::termDegree(const Expr& e) { 05348 if (isLeaf(e)) return 1; 05349 if (isPow(e)) return termDegree(e[1]) * e[0].getRational().getInt(); 05350 if (isMult(e)) { 05351 int degree = 0; 05352 for (int i = 0; i < e.arity(); i ++) degree += termDegree(e[i]); 05353 return degree; 05354 } 05355 return 0; 05356 } 05357 05358 bool TheoryArithOld::canPickEqMonomial(const Expr& right) 05359 { 05360 Expr::iterator istart = right.begin(); 05361 Expr::iterator iend = right.end(); 05362 05363 // Skip the first one 05364 istart++; 05365 for(Expr::iterator i = istart; i != iend; ++i) { 05366 05367 Expr leaf; 05368 Rational coeff; 05369 05370 // Check if linear term 05371 if (isLeaf(*i)) { 05372 leaf = *i; 05373 coeff = 1; 05374 } else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) { 05375 leaf = (*i)[1]; 05376 coeff = abs((*i)[0].getRational()); 05377 } else 05378 continue; 05379 05380 // If integer, must be coeff 1/-1 05381 if (!isIntegerThm(leaf).isNull()) 05382 if (coeff != 1 && coeff != -1) 05383 continue; 05384 05385 // Check if a leaf in other ones 05386 Expr::iterator j; 05387 for (j = istart; j != iend; ++j) 05388 if (j != i && isLeafIn(leaf, *j)) 05389 break; 05390 if (j == iend) 05391 return true; 05392 } 05393 05394 return false; 05395 } 05396 05397 bool TheoryArithOld::isBounded(const Expr& t, BoundsQueryType queryType) { 05398 TRACE("arith shared", "isBounded(", t.toString(), ")"); 05399 return hasUpperBound(t, queryType) && hasLowerBound(t, queryType); 05400 } 05401 05402 TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::getUpperBound(const Expr& t, BoundsQueryType queryType) 05403 { 05404 TRACE("arith shared", "getUpperBound(", t.toString(), ")"); 05405 05406 // If t is a constant it's bounded 05407 if (t.isRational()) { 05408 TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + t.getRational().toString()); 05409 return t.getRational(); 05410 } 05411 05412 // If buffered, just return it 05413 CDMap<Expr, DifferenceLogicGraph::EpsRational>::iterator find_t = termUpperBounded.find(t); 05414 if (find_t != termUpperBounded.end()) { 05415 TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + (*find_t).second.toString()); 05416 return (*find_t).second; 05417 } else if (queryType == QueryWithCacheAll) { 05418 // Asked for cache query, so no bound is found 05419 TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> +inf"); 05420 return DifferenceLogicGraph::EpsRational::PlusInfinity; 05421 } 05422 05423 // Assume it's not bounded 05424 DifferenceLogicGraph::EpsRational upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity; 05425 05426 // We always buffer the leaves, so all that's left are the terms 05427 if (!isLeaf(t)) { 05428 if (isMult(t)) { 05429 // We only handle linear terms 05430 if (!isNonlinearSumTerm(t)) { 05431 // Separate the multiplication 05432 Expr c, v; 05433 separateMonomial(t, c, v); 05434 // Get the upper-bound for the variable 05435 if (c.getRational() > 0) upperBound = getUpperBound(v); 05436 else upperBound = getLowerBound(v); 05437 if (upperBound.isFinite()) upperBound = upperBound * c.getRational(); 05438 else upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity; 05439 } 05440 } else if (isPlus(t)) { 05441 // If one of them is unconstrained then the term itself is unconstrained 05442 upperBound = DifferenceLogicGraph::EpsRational::Zero; 05443 for (int i = 0; i < t.arity(); i ++) { 05444 Expr t_i = t[i]; 05445 DifferenceLogicGraph::EpsRational t_i_upperBound = getUpperBound(t_i, queryType); 05446 if (t_i_upperBound.isFinite()) upperBound = upperBound + t_i_upperBound; 05447 else { 05448 upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity; 05449 // Not-bounded, check for constrained 05450 if (queryType == QueryWithCacheLeavesAndConstrainedComputation) { 05451 for(; i < t.arity() && isConstrainedAbove(t[i], QueryWithCacheLeaves); i ++); 05452 if (i == t.arity()) { 05453 TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> constrained"); 05454 termConstrainedAbove[t] = true; 05455 } 05456 break; 05457 } else break; 05458 } 05459 } 05460 } 05461 } 05462 05463 // Buffer it 05464 if (upperBound.isFinite()) { 05465 termUpperBounded[t] = upperBound; 05466 termConstrainedAbove[t] = true; 05467 } 05468 05469 // Return if bounded or not 05470 TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + upperBound.toString()); 05471 return upperBound; 05472 } 05473 05474 TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::getLowerBound(const Expr& t, BoundsQueryType queryType) 05475 { 05476 TRACE("arith shared", "getLowerBound(", t.toString(), ")"); 05477 05478 // If t is a constant it's bounded 05479 if (t.isRational()) { 05480 TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + t.getRational().toString()); 05481 return t.getRational(); 05482 } 05483 05484 // If buffered, just return it 05485 CDMap<Expr, DifferenceLogicGraph::EpsRational>::iterator t_find = termLowerBounded.find(t); 05486 if (t_find != termLowerBounded.end()) { 05487 TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + (*t_find).second.toString()); 05488 return (*t_find).second; 05489 } else if (queryType == QueryWithCacheAll) { 05490 // Asked for cache query, so no bound is found 05491 TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> -inf"); 05492 return DifferenceLogicGraph::EpsRational::MinusInfinity; 05493 } 05494 05495 // Assume it's not bounded 05496 DifferenceLogicGraph::EpsRational lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity; 05497 05498 // Leaves are always buffered 05499 if (!isLeaf(t)) { 05500 if (isMult(t)) { 05501 // We only handle linear terms 05502 if (!isNonlinearSumTerm(t)) { 05503 // Separate the multiplication 05504 Expr c, v; 05505 separateMonomial(t, c, v); 05506 // Get the upper-bound for the variable 05507 if (c.getRational() > 0) lowerBound = getLowerBound(v); 05508 else lowerBound = getUpperBound(v); 05509 if (lowerBound.isFinite()) lowerBound = lowerBound * c.getRational(); 05510 else lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity; 05511 } 05512 } else if (isPlus(t)) { 05513 // If one of them is unconstrained then the term itself is unconstrained 05514 lowerBound = DifferenceLogicGraph::EpsRational::Zero; 05515 for (int i = 0; i < t.arity(); i ++) { 05516 Expr t_i = t[i]; 05517 DifferenceLogicGraph::EpsRational t_i_lowerBound = getLowerBound(t_i, queryType); 05518 if (t_i_lowerBound.isFinite()) lowerBound = lowerBound + t_i_lowerBound; 05519 else { 05520 lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity; 05521 // Not-bounded, check for constrained 05522 if (queryType == QueryWithCacheLeavesAndConstrainedComputation) { 05523 for(; i < t.arity() && isConstrainedBelow(t[i], QueryWithCacheLeaves); i ++); 05524 if (i == t.arity()) { 05525 TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> constrained"); 05526 termConstrainedBelow[t] = true; 05527 } 05528 break; 05529 } else break; 05530 } 05531 } 05532 } 05533 } 05534 05535 // Buffer it 05536 if (lowerBound.isFinite()) { 05537 termLowerBounded[t] = lowerBound; 05538 termConstrainedBelow[t] = true; 05539 } 05540 05541 // Return if bounded or not 05542 TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + lowerBound.toString()); 05543 return lowerBound; 05544 } 05545 05546 int TheoryArithOld::computeTermBounds() 05547 { 05548 int computeTermBoundsConstrainedCount = 0; 05549 05550 vector<Expr> sorted_vars; 05551 // Get the variables in the topological order 05552 if (!diffLogicOnly) d_graph.getVerticesTopological(sorted_vars); 05553 // Or if difference logic only, just get them 05554 else { 05555 diffLogicGraph.getVariables(sorted_vars); 05556 IF_DEBUG( 05557 diffLogicGraph.writeGraph(cerr); 05558 ) 05559 } 05560 05561 // Go in the reverse topological order and try to see if the vats are constrained/bounded 05562 for (int i = sorted_vars.size() - 1; i >= 0; i --) 05563 { 05564 // Get the variable 05565 Expr v = sorted_vars[i]; 05566 05567 // If the find is not identity, skip it 05568 if (v.hasFind() && find(v).getRHS() != v) continue; 05569 05570 TRACE("arith shared", "processing: ", v.toString(), ""); 05571 05572 // If the variable is not an integer, it's unconstrained, unless we are in model generation 05573 if (isIntegerThm(v).isNull() && !d_inModelCreation) continue; 05574 05575 // We only do the computation if the variable is not already constrained 05576 if (!isConstrained(v, QueryWithCacheAll)) { 05577 05578 // Recall if we already computed the constraint 05579 bool constrainedAbove = isConstrained(v, QueryWithCacheAll); 05580 05581 // See if it's bounded from above in the difference graph 05582 DifferenceLogicGraph::EpsRational upperBound = diffLogicGraph.getEdgeWeight(v, zero); 05583 if (!constrainedAbove) constrainedAbove = upperBound.isFinite(); 05584 05585 // Try to refine the bound by checking projected inequalities 05586 if (!diffLogicOnly) { 05587 ExprMap<CDList<Ineq> *>::iterator v_left_find = d_inequalitiesLeftDB.find(v); 05588 // If not constraint from one side, it's unconstrained 05589 if (v_left_find != d_inequalitiesLeftDB.end()) { 05590 // Check right hand side for an unconstrained variable 05591 CDList<Ineq>*& left_list = (*v_left_find).second; 05592 if (left_list && left_list->size() > 0) { 05593 for (unsigned ineq_i = 0; ineq_i < left_list->size(); ineq_i ++) { 05594 // Get the inequality 05595 Ineq ineq = (*left_list)[ineq_i]; 05596 // Get the right-hand side (v <= rhs) 05597 Expr rhs = ineq.ineq().getExpr()[1]; 05598 // If rhs changed, skip it 05599 if (rhs.hasFind() && find(rhs).getRHS() != rhs) continue; 05600 // Compute the upper bound while 05601 DifferenceLogicGraph::EpsRational currentUpperBound = getUpperBound(rhs, (constrainedAbove ? QueryWithCacheLeaves : QueryWithCacheLeavesAndConstrainedComputation)); 05602 if (currentUpperBound.isFinite() && (!upperBound.isFinite() || currentUpperBound < upperBound)) { 05603 upperBound = currentUpperBound; 05604 constrainedAbove = true; 05605 } 05606 // If not constrained, check if right-hand-side is constrained 05607 if (!constrainedAbove) constrainedAbove = isConstrainedAbove(rhs, QueryWithCacheAll); 05608 } 05609 } 05610 } 05611 } 05612 // Difference logic case (no projections) 05613 else if (!constrainedAbove) { 05614 // If there is no incoming edges, then the variable is not constrained 05615 if (!diffLogicGraph.hasIncoming(v)) constrainedAbove = false; 05616 // If there is a cycle from t to t, all the variables 05617 // in the graph are constrained by each-other (we could 05618 // choose one, but it's too complicated) 05619 else if (diffLogicGraph.inCycle(v)) constrainedAbove = true; 05620 // Otherwise, since there is no bounds, and the cycles 05621 // can be shifted (since one of them can be taken as 05622 // unconstrained), we can assume that the variables is 05623 // not constrained. Conundrum here is that when in model-generation 05624 // we actually should take it as constrained so that it's 05625 // split on and we are on the safe side 05626 else constrainedAbove = d_inModelCreation; 05627 } 05628 05629 // Cache the upper bound and upper constrained computation 05630 if (constrainedAbove) termConstrainedAbove[v] = true; 05631 if (upperBound.isFinite()) termUpperBounded[v] = upperBound; 05632 05633 // Recall the below computation if it's there 05634 bool constrainedBelow = isConstrainedBelow(v, QueryWithCacheAll); 05635 05636 // See if it's bounded from below in the difference graph 05637 DifferenceLogicGraph::EpsRational lowerBound = diffLogicGraph.getEdgeWeight(zero, v); 05638 if (lowerBound.isFinite()) lowerBound = -lowerBound; 05639 else lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity; 05640 if (!constrainedBelow) constrainedBelow = lowerBound.isFinite(); 05641 05642 // Try to refine the bound by checking projected inequalities 05643 if (!diffLogicOnly) { 05644 ExprMap<CDList<Ineq> *>::iterator v_right_find = d_inequalitiesRightDB.find(v); 05645 // If not constraint from one side, it's unconstrained 05646 if (v_right_find != d_inequalitiesRightDB.end()) { 05647 // Check right hand side for an unconstrained variable 05648 CDList<Ineq>*& right_list = (*v_right_find).second; 05649 if (right_list && right_list->size() > 0) { 05650 for (unsigned ineq_i = 0; ineq_i < right_list->size(); ineq_i ++) { 05651 // Get the inequality 05652 Ineq ineq = (*right_list)[ineq_i]; 05653 // Get the right-hand side (lhs <= 0) 05654 Expr lhs = ineq.ineq().getExpr()[0]; 05655 // If lhs has changed, skip it 05656 if (lhs.hasFind() && find(lhs).getRHS() != lhs) continue; 05657 // Compute the lower bound 05658 DifferenceLogicGraph::EpsRational currentLowerBound = getLowerBound(lhs, (constrainedBelow ? QueryWithCacheLeaves : QueryWithCacheLeavesAndConstrainedComputation)); 05659 if (currentLowerBound.isFinite() && (!lowerBound.isFinite() || currentLowerBound > lowerBound)) { 05660 lowerBound = currentLowerBound; 05661 constrainedBelow = true; 05662 } 05663 // If not constrained, check if right-hand-side is constrained 05664 if (!constrainedBelow) constrainedBelow = isConstrainedBelow(lhs, QueryWithCacheAll); 05665 } 05666 } 05667 } 05668 } 05669 // Difference logic case (no projections) 05670 else if (!constrainedBelow) { 05671 // If there is no incoming edges, then the variable is not constrained 05672 if (!diffLogicGraph.hasOutgoing(v)) constrainedBelow = false; 05673 // If there is a cycle from t to t, all the variables 05674 // in the graph are constrained by each-other (we could 05675 // choose one, but it's too complicated) 05676 else if (diffLogicGraph.inCycle(v)) constrainedBelow = true; 05677 // Otherwise, since there is no bounds, and the cycles 05678 // can be shifted (since one of them can be taken as 05679 // unconstrained), we can assume that the variables is 05680 // not constrained. Conundrum here is that when in model-generation 05681 // we actually should take it as constrained so that it's 05682 // split on and we are on the safe side 05683 else constrainedBelow = d_inModelCreation; 05684 } 05685 05686 // Cache the lower bound and lower constrained computation 05687 if (constrainedBelow) termConstrainedBelow[v] = true; 05688 if (lowerBound.isFinite()) termLowerBounded[v] = lowerBound; 05689 05690 // Is this variable constrained 05691 if (constrainedAbove && constrainedBelow) computeTermBoundsConstrainedCount ++; 05692 05693 TRACE("arith shared", (constrainedAbove && constrainedBelow ? "constrained " : "unconstrained "), "", ""); 05694 } else 05695 computeTermBoundsConstrainedCount ++; 05696 } 05697 05698 TRACE("arith shared", "number of constrained variables : ", int2string(computeTermBoundsConstrainedCount), " of " + int2string(sorted_vars.size())); 05699 05700 return computeTermBoundsConstrainedCount; 05701 } 05702 05703 bool TheoryArithOld::isConstrainedAbove(const Expr& t, BoundsQueryType queryType) 05704 { 05705 TRACE("arith shared", "isConstrainedAbove(", t.toString(), ")"); 05706 05707 // Rational numbers are constrained 05708 if (t.isRational()) { 05709 TRACE("arith shared", "isConstrainedAbove() ==> true", "", ""); 05710 return true; 05711 } 05712 05713 // Look it up in the cache 05714 CDMap<Expr, bool>::iterator t_find = termConstrainedAbove.find(t); 05715 if (t_find != termConstrainedAbove.end()) { 05716 TRACE("arith shared", "isConstrainedAbove() ==> true", "", ""); 05717 return true; 05718 } 05719 else if (queryType == QueryWithCacheAll) { 05720 TRACE("arith shared", "isConstrainedAbove() ==> false", "", ""); 05721 return false; 05722 } 05723 05724 bool constrainedAbove = true; 05725 05726 if (isLeaf(t)) { 05727 // Leaves are always cached 05728 constrainedAbove = false; 05729 } else { 05730 if (isMult(t)) { 05731 // Non-linear terms are constrained by default 05732 // we only deal with the linear stuff 05733 if (!isNonlinearSumTerm(t)) { 05734 // Separate the multiplication 05735 Expr c, v; 05736 separateMonomial(t, c, v); 05737 // Check if the variable is constrained 05738 if (c.getRational() > 0) constrainedAbove = isConstrainedAbove(v, queryType); 05739 else constrainedAbove = isConstrainedBelow(v, queryType); 05740 } 05741 } else if (isPlus(t)) { 05742 // If one of them is unconstrained then the term itself is unconstrained 05743 for (int i = 0; i < t.arity() && constrainedAbove; i ++) 05744 if (!isConstrainedAbove(t[i])) constrainedAbove = false; 05745 } 05746 } 05747 05748 // Remember it 05749 if (constrainedAbove) termConstrainedAbove[t] = true; 05750 05751 TRACE("arith shared", "isConstrainedAbove() ==> ", constrainedAbove ? "true" : "false", ""); 05752 05753 // Return in 05754 return constrainedAbove; 05755 } 05756 05757 bool TheoryArithOld::isConstrainedBelow(const Expr& t, BoundsQueryType queryType) 05758 { 05759 TRACE("arith shared", "isConstrainedBelow(", t.toString(), ")"); 05760 05761 // Rational numbers are constrained 05762 if (t.isRational()) return true; 05763 05764 // Look it up in the cache 05765 CDMap<Expr, bool>::iterator t_find = termConstrainedBelow.find(t); 05766 if (t_find != termConstrainedBelow.end()) { 05767 TRACE("arith shared", "isConstrainedBelow() ==> true", "", ""); 05768 return true; 05769 } 05770 else if (queryType == QueryWithCacheAll) { 05771 TRACE("arith shared", "isConstrainedBelow() ==> false", "", ""); 05772 return false; 05773 } 05774 05775 bool constrainedBelow = true; 05776 05777 if (isLeaf(t)) { 05778 // Leaves are always cached 05779 constrainedBelow = false; 05780 } else { 05781 if (isMult(t)) { 05782 // Non-linear terms are constrained by default 05783 // we only deal with the linear stuff 05784 if (!isNonlinearSumTerm(t)) { 05785 // Separate the multiplication 05786 Expr c, v; 05787 separateMonomial(t, c, v); 05788 // Check if the variable is constrained 05789 if (c.getRational() > 0) constrainedBelow = isConstrainedBelow(v, queryType); 05790 else constrainedBelow = isConstrainedAbove(v, queryType); 05791 } 05792 } else if (isPlus(t)) { 05793 // If one of them is unconstrained then the term itself is unconstrained 05794 constrainedBelow = true; 05795 for (int i = 0; i < t.arity() && constrainedBelow; i ++) 05796 if (!isConstrainedBelow(t[i])) 05797 constrainedBelow = false; 05798 } 05799 } 05800 05801 // Cache it 05802 if (constrainedBelow) termConstrainedBelow[t] = true; 05803 05804 TRACE("arith shared", "isConstrainedBelow() ==> ", constrainedBelow ? "true" : "false", ""); 05805 05806 // Return it 05807 return constrainedBelow; 05808 } 05809 05810 bool TheoryArithOld::isConstrained(const Expr& t, bool intOnly, BoundsQueryType queryType) 05811 { 05812 TRACE("arith shared", "isConstrained(", t.toString(), ")"); 05813 // For the reals we consider them unconstrained if not asked for full check 05814 if (intOnly && isIntegerThm(t).isNull()) return false; 05815 bool result = (isConstrainedAbove(t, queryType) && isConstrainedBelow(t, queryType)); 05816 TRACE("arith shared", "isConstrained(", t.toString(), (result ? ") ==> true " : ") ==> false ") ); 05817 return result; 05818 } 05819 05820 bool TheoryArithOld::DifferenceLogicGraph::hasIncoming(const Expr& x) 05821 { 05822 EdgesList::iterator find_x = incomingEdges.find(x); 05823 05824 // No edges at all meaning no incoming 05825 if (find_x == incomingEdges.end()) return false; 05826 05827 // The pointer being null, also no incoming 05828 CDList<Expr>*& list = (*find_x).second; 05829 if (!list) return false; 05830 05831 // If in model creation, source vertex goes to all vertices 05832 if (sourceVertex.isNull()) 05833 return list->size() > 0; 05834 else 05835 return list->size() > 1; 05836 } 05837 05838 bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing(const Expr& x) 05839 { 05840 EdgesList::iterator find_x = outgoingEdges.find(x); 05841 05842 // No edges at all meaning no incoming 05843 if (find_x == outgoingEdges.end()) return false; 05844 05845 // The pointer being null, also no incoming 05846 CDList<Expr>*& list = (*find_x).second; 05847 if (!list) return false; 05848 05849 // If the list is not empty we have outgoing edges 05850 return list->size() > 0; 05851 } 05852 05853 void TheoryArithOld::DifferenceLogicGraph::getVariables(vector<Expr>& variables) 05854 { 05855 set<Expr> vars_set; 05856 05857 EdgesList::iterator incoming_it = incomingEdges.begin(); 05858 EdgesList::iterator incoming_it_end = incomingEdges.end(); 05859 while (incoming_it != incoming_it_end) { 05860 Expr var = (*incoming_it).first; 05861 if (var != sourceVertex) 05862 vars_set.insert(var); 05863 incoming_it ++; 05864 } 05865 05866 EdgesList::iterator outgoing_it = outgoingEdges.begin(); 05867 EdgesList::iterator outgoing_it_end = outgoingEdges.end(); 05868 while (outgoing_it != outgoing_it_end) { 05869 Expr var = (*outgoing_it).first; 05870 if (var != sourceVertex) 05871 vars_set.insert(var); 05872 outgoing_it ++; 05873 } 05874 05875 set<Expr>::iterator set_it = vars_set.begin(); 05876 set<Expr>::iterator set_it_end = vars_set.end(); 05877 while (set_it != set_it_end) { 05878 variables.push_back(*set_it); 05879 set_it ++; 05880 } 05881 } 05882 05883 void TheoryArithOld::DifferenceLogicGraph::writeGraph(ostream& out) { 05884 return; 05885 out << "digraph G {" << endl; 05886 05887 EdgesList::iterator incoming_it = incomingEdges.begin(); 05888 EdgesList::iterator incoming_it_end = incomingEdges.end(); 05889 while (incoming_it != incoming_it_end) { 05890 05891 Expr var_u = (*incoming_it).first; 05892 05893 CDList<Expr>* edges = (*incoming_it).second; 05894 if (edges) 05895 for (unsigned edge_i = 0; edge_i < edges->size(); edge_i ++) { 05896 Expr var_v = (*edges)[edge_i]; 05897 out << var_u.toString() << " -> " << var_v.toString() << endl; 05898 } 05899 05900 incoming_it ++; 05901 } 05902 05903 out << "}" << endl; 05904 }