CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_core.cpp 00004 * 00005 * Author: Clark Barrett, Vijay Ganesh (CNF converter) 00006 * 00007 * Created: Thu Jan 30 16:57:52 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 #include <locale> 00022 #include <cctype> 00023 #include <ctime> 00024 #include "command_line_flags.h" 00025 #include "expr.h" 00026 #include "notifylist.h" 00027 #include "pretty_printer.h" 00028 #include "common_proof_rules.h" 00029 #include "parser_exception.h" 00030 #include "typecheck_exception.h" 00031 #include "smtlib_exception.h" 00032 #include "eval_exception.h" 00033 #include "theory_core.h" 00034 #include "expr_transform.h" 00035 #include "core_proof_rules.h" 00036 #include "theorem_manager.h" 00037 #include "translator.h" 00038 00039 using namespace std; 00040 00041 00042 namespace CVC3 { 00043 00044 00045 //! Implementation of PrettyPrinter class 00046 /*! \ingroup PrettyPrinting */ 00047 class PrettyPrinterCore: public PrettyPrinter { 00048 private: 00049 TheoryCore *d_core; 00050 //! Disable the default constructor 00051 PrettyPrinterCore() { } 00052 public: 00053 //! Constructor 00054 PrettyPrinterCore(TheoryCore* core): d_core(core) { } 00055 ExprStream& print(ExprStream& os, const Expr& e) 00056 { 00057 if(e.isString()) 00058 return e.print(os); 00059 else if (e.isApply()) 00060 return d_core->theoryOf(e)->print(os, e); 00061 else if(d_core->hasTheory(e.getKind())) 00062 return d_core->theoryOf(e.getKind())->print(os, e); 00063 else 00064 return e.print(os); 00065 } 00066 }; 00067 00068 00069 class TypeComputerCore: public ExprManager::TypeComputer { 00070 TheoryCore *d_core; 00071 public: 00072 TypeComputerCore(TheoryCore* core): d_core(core) { } 00073 void computeType(const Expr& e) 00074 { 00075 DebugAssert(!e.isVar(), "Variables should have a type: "+e.toString()); 00076 Theory* i = d_core->theoryOf(e.getKind()); 00077 if (e.isApply()) i = d_core->theoryOf(e); 00078 i->computeType(e); 00079 DebugAssert(!e.lookupType().getExpr().isNull(), "Type not set by computeType"); 00080 } 00081 void checkType(const Expr& e) 00082 { 00083 if (!e.isType()) throw Exception 00084 ("Tried to use non-type as a type: "+e.toString()); 00085 d_core->theoryOf(e)->checkType(e); 00086 e.setValidType(); 00087 } 00088 Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 00089 bool enumerate, bool computeSize) 00090 { 00091 DebugAssert(e.isType(), "finiteTypeInfo called on non-type"); 00092 return d_core->theoryOf(e)->finiteTypeInfo(e, n, enumerate, computeSize); 00093 } 00094 }; 00095 00096 00097 ostream& operator<<(ostream& os, const NotifyList& l) 00098 { 00099 os << "NotifyList(\n"; 00100 for(size_t i=0,iend=l.size(); i<iend; ++i) { 00101 os << "[" << l.getTheory(i)->getName() << ", " << l.getExpr(i) << "]\n"; 00102 } 00103 return os << ")"; 00104 } 00105 00106 00107 } 00108 00109 00110 using namespace CVC3; 00111 00112 00113 /*****************************************************************************/ 00114 /* 00115 * Private helper functions 00116 */ 00117 /*****************************************************************************/ 00118 00119 00120 bool TheoryCore::processFactQueue(EffortLevel effort) 00121 { 00122 Theorem thm; 00123 vector<Theory*>::iterator i, iend = d_theories.end(); 00124 bool lemmasAdded = false; 00125 do { 00126 processUpdates(); 00127 while (!d_queue.empty() && !d_inconsistent && !timeLimitReached()) { 00128 thm = d_queue.front(); 00129 d_queue.pop(); 00130 assertFactCore(thm); 00131 processUpdates(); 00132 }; 00133 00134 if (d_inconsistent) break; 00135 00136 while (!d_queueSE.empty() && !timeLimitReached()) { 00137 // Copy a Theorem by value, to guarantee valid reference down 00138 // the call chain 00139 lemmasAdded = true; 00140 Theorem thm(d_queueSE.back()); 00141 d_queueSE.pop_back(); 00142 d_coreSatAPI->addLemma(thm); 00143 } 00144 00145 if (effort > LOW) { 00146 for(i = d_theories.begin(); d_update_thms.empty() && d_queue.empty() && i != iend && !d_inconsistent && !timeLimitReached(); ++i) { 00147 (*i)->checkSat(effort == FULL && !lemmasAdded); 00148 } 00149 } 00150 } while ((!d_queue.empty() || !d_update_thms.empty()) && !d_inconsistent && !timeLimitReached()); 00151 00152 if (d_inconsistent) { 00153 d_update_thms.clear(); 00154 d_update_data.clear(); 00155 while(d_queue.size()) d_queue.pop(); 00156 d_queueSE.clear(); 00157 return false; 00158 } 00159 00160 if (timeLimitReached()) { 00161 // clear all work queues to satisfy invariants 00162 d_update_thms.clear(); 00163 d_update_data.clear(); 00164 while (!d_queue.empty()) d_queue.pop(); 00165 d_queueSE.clear(); 00166 } 00167 00168 return lemmasAdded; 00169 } 00170 00171 00172 void TheoryCore::processNotify(const Theorem& e, NotifyList *L) 00173 { 00174 ++d_inUpdate; 00175 DebugAssert(L, "Expected non-NULL notify list"); 00176 for(unsigned k = 0; k < L->size() && !d_inconsistent; ++k) { 00177 L->getTheory(k)->update(e, L->getExpr(k)); 00178 } 00179 --d_inUpdate; 00180 } 00181 00182 00183 Theorem TheoryCore::simplify(const Expr& e) 00184 { 00185 DebugAssert(d_simpStack.count(e) == 0, "TheoryCore::simplify: loop detected over e =\n" 00186 +e.toString()); 00187 DebugAssert(d_simpStack.size() < 10000, 00188 "TheoryCore::simplify: too deep recursion depth"); 00189 IF_DEBUG(d_simpStack[e] = true;) 00190 00191 // Normally, if an expr has a find, we don't need to simplify, just return the find. 00192 // However, if we are in the middle of an update, the find may not yet be updated, so 00193 // we should do a full simplify. The exception is expressions like 00194 // uninterp. functions or reads that use a congruence closure algorithm that 00195 // relies on not simplifying inside of expressions that have finds. 00196 if (e.hasFind()) { 00197 DebugAssert((find(e).getRHS().hasFind() && find(e).getRHS().isTerm()) 00198 || find(e).getRHS().isTrue() 00199 || find(e).getRHS().isFalse(), "Unexpected find pointer"); 00200 if (d_inUpdate) { 00201 if (e.usesCC()) { 00202 Theorem thm = find(e); 00203 if (!thm.isRefl()) { 00204 thm = transitivityRule(thm, simplify(thm.getRHS())); 00205 } 00206 IF_DEBUG(d_simpStack.erase(e);) 00207 return thm; 00208 } 00209 } 00210 else { 00211 IF_DEBUG(d_simpStack.erase(e);) 00212 return find(e); 00213 } 00214 } 00215 00216 if(e.validSimpCache()) { 00217 IF_DEBUG(d_simpStack.erase(e);) 00218 return e.getSimpCache(); 00219 } 00220 00221 Theorem thm; 00222 if (e.isVar()) { 00223 thm = rewriteCore(e); 00224 } 00225 else { 00226 thm = rewriteCore(theoryOf(e.getOpKind())->simplifyOp(e)); 00227 } 00228 00229 const Expr& e2 = thm.getRHS(); 00230 #ifdef _CVC3_DEBUG_MODE 00231 if (!e2.usesCC()) { //2.isTerm() || !e2.hasFind()) { 00232 // The rewriter should guarantee that all of its children are simplified. 00233 for (int k=0; k<e2.arity(); ++k) { 00234 Expr simplified(simplify(e2[k]).getRHS()); 00235 DebugAssert(e2[k]==simplified,"Simplify Error 1:\n e2[k="+int2string(k) 00236 +"] = " 00237 +e2[k].toString() + "\nSimplified = " 00238 +simplified.toString() 00239 +"\ne2 = "+e2.toString()); 00240 } 00241 } 00242 Expr rewritten(rewriteCore(e2).getRHS()); 00243 DebugAssert(e2==rewritten,"Simplify Error 2: e2 = \n" 00244 +e2.toString() + "\nSimplified rewritten = \n" 00245 +rewritten.toString()); 00246 #endif 00247 e.setSimpCache(thm); 00248 if (e != e2 && !e2.hasFind()) { 00249 e2.setSimpCache(reflexivityRule(e2)); 00250 } 00251 IF_DEBUG(d_simpStack.erase(e);) 00252 return thm; 00253 } 00254 00255 00256 Theorem TheoryCore::rewriteCore(const Theorem& e) 00257 { 00258 DebugAssert(e.isRewrite(), 00259 "rewriteCore(thm): not equality or iff:\n " + e.toString()); 00260 return transitivityRule(e, rewriteCore(e.getRHS())); 00261 } 00262 00263 00264 /* Recurse through s looking for atomic formulas (or terms in the case of 00265 * then/else branches of ite's) and use the notifylist mechanism to indicate 00266 * that the atomic formula e depends on these atomic formulas and terms. Used 00267 * by registerAtom. */ 00268 void TheoryCore::setupSubFormulas(const Expr& s, const Expr& e, 00269 const Theorem& thm) 00270 { 00271 if (s.isAtomic()) { 00272 setupTerm(s, theoryOf(s), thm); 00273 s.addToNotify(this, e); 00274 } 00275 else if (s.isAbsAtomicFormula()) { 00276 setupTerm(s, theoryOf(s), thm); 00277 for (int i = 0; i < s.arity(); ++i) { 00278 s[i].addToNotify(this, e); 00279 } 00280 if (s != e) s.addToNotify(this, e); 00281 } 00282 else { 00283 for (int i = 0; i < s.arity(); ++i) { 00284 setupSubFormulas(s[i], e, thm); 00285 } 00286 } 00287 } 00288 00289 00290 void TheoryCore::processUpdates() 00291 { 00292 Theorem e; 00293 Expr d; 00294 DebugAssert(d_update_thms.size() == d_update_data.size(), 00295 "Expected same size"); 00296 while (!d_inconsistent && !d_update_thms.empty()) { 00297 e = d_update_thms.back(); 00298 d_update_thms.pop_back(); 00299 d = d_update_data.back(); 00300 d_update_data.pop_back(); 00301 00302 DebugAssert(d.isAbsAtomicFormula(), "Expected atomic formula"); 00303 Theorem thm = simplify(d); 00304 if (thm.getRHS().isTrue()) { 00305 setFindLiteral(d_commonRules->iffTrueElim(thm)); 00306 } 00307 else if (thm.getRHS().isFalse()) { 00308 setFindLiteral(d_commonRules->iffFalseElim(thm)); 00309 } 00310 else { 00311 DebugAssert(e.isRewrite(), "Unexpected theorem in TheoryCore::update"); 00312 if (e.getRHS().getType().isBool()) continue; 00313 find(e.getRHS()).getRHS().addToNotify(this, d); 00314 if (thm.getRHS().isAbsAtomicFormula()) thm.getRHS().addToNotify(this, d); 00315 } 00316 } 00317 } 00318 00319 00320 void TheoryCore::assertFactCore(const Theorem& e) 00321 { 00322 IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 00323 TRACE("assertFactCore", indentStr, "AssertFactCore: ", e.getExpr().toString(PRESENTATION_LANG)); 00324 00325 Theorem estarThm(e); 00326 Expr estar = e.getExpr(); 00327 IF_DEBUG(Expr e2 = estar;) 00328 Theorem equiv = simplify(estar); 00329 if (!equiv.isRefl()) { 00330 estarThm = iffMP(e, equiv); 00331 // Make sure originally asserted atomic formulas have a find pointer 00332 if (!estar.isTrue() && estar.isAbsLiteral()) { 00333 setFindLiteral(e); 00334 } 00335 estar = estarThm.getExpr(); 00336 } 00337 if (estar.isAbsLiteral()) { 00338 if (estar.isEq()) { 00339 Theorem solvedThm(solve(estarThm)); 00340 if(estar != solvedThm.getExpr()) setFindLiteral(estarThm); 00341 if (!solvedThm.getExpr().isTrue()) 00342 assertEqualities(solvedThm); 00343 } 00344 else if (estar.isFalse()) { 00345 IF_DEBUG(debugger.counter("conflicts from simplifier")++;) 00346 setInconsistent(estarThm); 00347 } 00348 else if (!estar.isTrue()) { 00349 assertFormula(estarThm); 00350 } 00351 else { 00352 // estar is true, nothing will be done 00353 // Make sure equivalence classes of equations between two terms with finds get merged 00354 // We skip this check for now because unsolvable nonlinear equations bring up this kind of 00355 // problems, i.e. x^2 + y^2 = z^2 is not solved, it is true, but the find of LHS and RHS are 00356 // different 00357 if (!incomplete() && e.isRewrite() && 00358 e.getLHS().hasFind() && e.getRHS().hasFind() && 00359 find(e.getLHS()).getRHS() != find(e.getRHS()).getRHS()) { 00360 TRACE("assertFactCore", "Problem (LHS of): ", e.getExpr(), ""); 00361 TRACE("assertFactCore", find(e.getLHS()).getRHS(), " vs ", find(e.getRHS()).getRHS()); 00362 IF_DEBUG(cerr << "Warning: Equivalence classes didn't get merged" << endl;) 00363 } 00364 } 00365 } else if (estar.isAnd()) { 00366 for(int i=0,iend=estar.arity(); i<iend && !d_inconsistent; ++i) 00367 assertFactCore(d_commonRules->andElim(estarThm, i)); 00368 return; 00369 } 00370 else { 00371 // Notify the search engine 00372 enqueueSE(estarThm); 00373 } 00374 00375 DebugAssert(!e2.isAbsLiteral() || e2.hasFind() 00376 || (e2.isNot() && e2[0].hasFind()), 00377 "assertFactCore: e2 = "+e2.toString()); 00378 DebugAssert(!estar.isAbsLiteral() || estar.hasFind() 00379 || (estar.isNot() && estar[0].hasFind()), 00380 "assertFactCore: estar = "+estar.toString()); 00381 } 00382 00383 00384 void TheoryCore::assertFormula(const Theorem& thm) 00385 { 00386 const Expr& e = thm.getExpr(); 00387 DebugAssert(e.isAbsLiteral(),"assertFormula: nonliteral asserted:\n " 00388 +thm.toString()); 00389 IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 00390 TRACE("assertFormula",indentStr,"AssertFormula: ", e.toString(PRESENTATION_LANG)); 00391 00392 Theory* i = theoryOf(e); 00393 Theory* i2 = i; 00394 00395 // Recursively set up terms in this formula 00396 setupTerm(e,i,thm); 00397 00398 // Use find to force af to rewrite to TRUE and NOT af to rewrite to FALSE, 00399 // where af is an atomic formula. If af is an equality, make sure its lhs 00400 // is greater than its rhs so the simplifier will be able to use the find. 00401 DebugAssert(!e.isNot() || (!e.hasFind() && !e[0].hasFind()), 00402 "Expected negated argument to assertFormula to not have find"); 00403 setFindLiteral(thm); 00404 00405 // Special processing for existentials, equalities, disequalities 00406 switch (e.getKind()) { 00407 case EXISTS: 00408 // Do not send existential quantifiers to DPs; instead, skolemize them 00409 enqueueFact(d_commonRules->skolemize(thm)); 00410 return; 00411 case NOT: 00412 if (e[0].isEq()) { 00413 00414 // Save the disequality for later processing 00415 e[0][0].addToNotify(this, e); 00416 e[0][1].addToNotify(this, e); 00417 i2 = theoryOf(getBaseType(e[0][0])); 00418 DebugAssert(e[0][0] > e[0][1], "Expected lhs of diseq to be greater"); 00419 // if(e[0][0] < e[0][1]) { 00420 // Expr e2 = e[0][1].eqExpr(e[0][0]); 00421 // DebugAssert(!e2.hasFind(), "already has find"); 00422 // thm2 = transitivityRule(d_commonRules->rewriteUsingSymmetry(e2), 00423 // d_commonRules->notToIff(thm)); 00424 // setFindLiteral(d_commonRules->iffFalseElim(thm2)); 00425 // } 00426 } 00427 break; 00428 case EQ: 00429 i2 = theoryOf(getBaseType(e[0])); 00430 if (e[0] < e[1]) { 00431 // this can happen because of the solver 00432 Expr e2 = e[1].eqExpr(e[0]); 00433 if (!e2.hasFind()) { 00434 Theorem thm2 = 00435 transitivityRule(d_commonRules->rewriteUsingSymmetry(e2), 00436 d_commonRules->iffTrue(thm)); 00437 setFindLiteral(d_commonRules->iffTrueElim(thm2)); 00438 } 00439 } 00440 break; 00441 default: 00442 break; 00443 } 00444 00445 // Send formula to the appropriate DP 00446 i->assertFact(thm); 00447 00448 // Equalities and disequalities are also asserted to the theories of 00449 // their types 00450 if (i != i2) i2->assertFact(thm); 00451 } 00452 00453 00454 Theorem CVC3::TheoryCore::rewriteCore(const Expr& e) 00455 { 00456 // Normally, if an expr has a find, we don't need to rewrite, just return the find. 00457 // However, if we are in the middle of an update, the find may not yet be updated, so 00458 // we should simplify the result. 00459 if (e.hasFind()) { 00460 Theorem thm = find(e); 00461 if (d_inUpdate && !thm.isRefl()) { 00462 thm = transitivityRule(thm, simplify(thm.getRHS())); 00463 } 00464 return thm; 00465 } 00466 00467 if (e.isRewriteNormal()) { 00468 IF_DEBUG( 00469 // Check that the RewriteNormal flag is set properly. Note that we 00470 // assume theory-specific rewrites are idempotent 00471 e.clearRewriteNormal(); 00472 Expr rewritten(rewriteCore(e).getRHS()); 00473 e.setRewriteNormal(); // Restore the flag 00474 DebugAssert(rewritten == e, 00475 "Expected no change: e = " + e.toString() 00476 +"\n rewriteCore(e) = "+rewritten.toString()); 00477 ) 00478 return reflexivityRule(e); 00479 } 00480 switch (e.getKind()) { 00481 case EQ: 00482 if (e[0] < e[1]) 00483 return rewriteCore(d_commonRules->rewriteUsingSymmetry(e)); 00484 else if (e[0] == e[1]) 00485 return d_commonRules->rewriteReflexivity(e); 00486 break; 00487 case NOT: 00488 if (e[0].isNot()) 00489 return rewriteCore(d_commonRules->rewriteNotNot(e)); 00490 break; 00491 default: 00492 break; 00493 } 00494 Theorem thm = theoryOf(e)->rewrite(e); 00495 const Expr& e2 = thm.getRHS(); 00496 00497 // Theory-specific rewrites for equality should ensure that lhs >= rhs, or 00498 // there is danger of an infinite loop. 00499 DebugAssert(!e2.isEq() || e2[0] >= e2[1], 00500 "theory-specific rewrites for equality should ensure lhs >= rhs"); 00501 if (e != e2) { 00502 thm = rewriteCore(thm); 00503 } 00504 return thm; 00505 } 00506 00507 00508 void TheoryCore::setFindLiteral(const Theorem& thm) 00509 { 00510 const Expr& e = thm.getExpr(); 00511 NotifyList* L; 00512 if (e.isNot()) { 00513 const Expr& e0 = e[0]; 00514 if (!e0.hasFind()) { 00515 IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 00516 TRACE("setFindLiteral", indentStr, "SFL: ", e.toString(PRESENTATION_LANG)); 00517 Theorem findThm = d_commonRules->notToIff(thm); 00518 e0.setFind(findThm); 00519 if (e0.isRegisteredAtom()) { 00520 DebugAssert(!e.isImpliedLiteral(), "Should be new implied lit"); 00521 e.setImpliedLiteral(); 00522 d_impliedLiterals.push_back(thm); 00523 } 00524 d_em->invalidateSimpCache(); 00525 L = e0.getNotify(); 00526 if (L) processNotify(findThm, L); 00527 } 00528 else { 00529 Theorem findThm = find(e0); 00530 if (findThm.getRHS().isTrue()) { 00531 setInconsistent(iffMP(d_commonRules->iffTrueElim(findThm), 00532 d_commonRules->notToIff(thm))); 00533 } 00534 } 00535 } 00536 else if (!e.hasFind()) { 00537 IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 00538 TRACE("setFindLiteral", indentStr, "SFL: ", e.toString(PRESENTATION_LANG)); 00539 Theorem findThm = d_commonRules->iffTrue(thm); 00540 e.setFind(findThm); 00541 if (e.isRegisteredAtom()) { 00542 DebugAssert(!e.isImpliedLiteral(), "Should be new implied lit"); 00543 e.setImpliedLiteral(); 00544 d_impliedLiterals.push_back(thm); 00545 } 00546 d_em->invalidateSimpCache(); 00547 L = e.getNotify(); 00548 if (L) processNotify(findThm, L); 00549 } 00550 else { 00551 Theorem findThm = find(e); 00552 if (findThm.getRHS().isFalse()) { 00553 setInconsistent(iffMP(thm, findThm)); 00554 } 00555 } 00556 } 00557 00558 00559 Theorem TheoryCore::rewriteLitCore(const Expr& e) 00560 { 00561 switch (e.getKind()) { 00562 case EQ: 00563 if (e[0] == e[1]) 00564 return d_commonRules->rewriteReflexivity(e); 00565 else if (e[0] < e[1]) 00566 return d_commonRules->rewriteUsingSymmetry(e); 00567 break; 00568 case NOT: 00569 if (e[0].isTrue()) 00570 return d_commonRules->rewriteNotTrue(e); 00571 else if (e[0].isFalse()) 00572 return d_commonRules->rewriteNotFalse(e); 00573 else if (e[0].isNot()) 00574 return d_commonRules->rewriteNotNot(e); 00575 break; 00576 default: 00577 DebugAssert(false, 00578 "TheoryCore::rewriteLitCore(" 00579 + e.toString() 00580 + "): Not implemented"); 00581 break; 00582 } 00583 return reflexivityRule(e); 00584 } 00585 00586 00587 void TheoryCore::enqueueSE(const Theorem& thm) 00588 { 00589 DebugAssert(okToEnqueue(), "enqueueSE()"); 00590 d_queueSE.push_back(thm); 00591 } 00592 00593 00594 Theorem TheoryCore::getModelValue(const Expr& e) 00595 { 00596 ExprHashMap<Theorem>::iterator i=d_varAssignments.find(e), 00597 iend=d_varAssignments.end(); 00598 if(i!=iend) return (*i).second; 00599 else return find(e); 00600 } 00601 00602 00603 //! An auxiliary recursive function to process COND expressions into ITE 00604 Expr TheoryCore::processCond(const Expr& e, int i) 00605 { 00606 DebugAssert(i < e.arity()-1, "e = "+e.toString()+", i = "+int2string(i)); 00607 if(i == e.arity()-2) { 00608 if(e[i].getKind() == RAW_LIST && e[i].arity() == 2 00609 && e[i+1].getKind() == RAW_LIST && e[i+1].arity() == 2 00610 && e[i+1][0].getKind() == ID && e[i+1][0][0].getString() == "_ELSE") { 00611 Expr c(parseExpr(e[i][0])); 00612 Expr e1(parseExpr(e[i][1])); 00613 Expr e2(parseExpr(e[i+1][1])); 00614 return c.iteExpr(e1,e2); 00615 } 00616 } else { 00617 if(e[i].getKind() == RAW_LIST && e[i].arity() == 2 00618 && e[i+1].getKind() == RAW_LIST && e[i+1].arity() == 2) { 00619 Expr c(parseExpr(e[i][0])); 00620 Expr e1(parseExpr(e[i][1])); 00621 Expr e2(processCond(e, i+1)); 00622 return c.iteExpr(e1,e2); 00623 } 00624 } 00625 throw ParserException("Parse Error: bad COND expression: "+e.toString()); 00626 } 00627 00628 00629 bool TheoryCore::isBasicKind(int kind) 00630 { 00631 switch (kind) { 00632 case VARDECLS: 00633 case LETDECLS: 00634 case HELP: 00635 case DUMP_PROOF: 00636 case DUMP_ASSUMPTIONS: 00637 case DUMP_SIG: 00638 case DUMP_TCC: 00639 case DUMP_TCC_ASSUMPTIONS: 00640 case DUMP_TCC_PROOF: 00641 case DUMP_CLOSURE: 00642 case DUMP_CLOSURE_PROOF: 00643 case WHERE: 00644 case ASSERTIONS: 00645 case ASSUMPTIONS: 00646 case COUNTEREXAMPLE: 00647 case COUNTERMODEL: 00648 case ASSERT: 00649 case PRINT: 00650 case QUERY: 00651 case CHECKSAT: 00652 case CONTINUE: 00653 case RESTART: 00654 case TRACE: 00655 case ECHO: 00656 case UNTRACE: 00657 case VARLIST: 00658 case FORGET: 00659 case GET_TYPE: 00660 case IFF: 00661 case IMPLIES: 00662 case TYPEDEF: 00663 case OPTION: 00664 case AND: 00665 case OR: 00666 case XOR: 00667 case NOT: 00668 case DISTINCT: 00669 case CALL: 00670 case TRANSFORM: 00671 case CHECK_TYPE: 00672 case VARDECL: 00673 case GET_CHILD: 00674 case SUBSTITUTE: 00675 case SEQ: 00676 case DBG: 00677 case PUSH: 00678 case POP: 00679 case POPTO: 00680 case PUSH_SCOPE: 00681 case POP_SCOPE: 00682 case POPTO_SCOPE: 00683 case RESET: 00684 case LETDECL: 00685 case ELSE: 00686 case CONTEXT: 00687 return true; 00688 default: 00689 break; 00690 } 00691 return false; 00692 } 00693 00694 00695 TheoryCore::TheoryCore(ContextManager* cm, 00696 ExprManager* em, 00697 TheoremManager* tm, 00698 Translator* translator, 00699 const CLFlags& flags, 00700 Statistics& statistics) 00701 : Theory(), d_cm(cm), d_tm(tm), d_flags(flags), d_statistics(statistics), 00702 d_translator(translator), 00703 d_inconsistent(cm->getCurrentContext(), false, 0), 00704 d_incomplete(cm->getCurrentContext()), 00705 d_incThm(cm->getCurrentContext()), 00706 d_terms(cm->getCurrentContext()), 00707 // d_termTheorems(cm->getCurrentContext()), 00708 d_predicates(cm->getCurrentContext()), 00709 d_vars(cm->getCurrentContext()), 00710 d_solver(NULL), 00711 d_simplifyInPlace(false), 00712 d_currentRecursiveSimplifier(NULL), 00713 d_resourceLimit(0), 00714 d_timeBase(0), 00715 d_timeLimit(0), 00716 d_inCheckSATCore(false), d_inAddFact(false), 00717 d_inRegisterAtom(false), d_inPP(false), 00718 d_notifyObj(this, cm->getCurrentContext()), 00719 d_impliedLiterals(cm->getCurrentContext()), 00720 d_impliedLiteralsIdx(cm->getCurrentContext(), 0, 0), 00721 d_notifyEq(cm->getCurrentContext()), 00722 d_inUpdate(0), 00723 d_coreSatAPI(NULL) 00724 { 00725 d_em = em; 00726 // Since we are in the middle of creating TheoryCore, we set the pointer to 00727 // TheoryCore in the Theory base class ourselves. 00728 d_theoryCore = this; 00729 d_commonRules = tm->getRules(); 00730 d_name = "Core"; 00731 d_theoryUsed = false; 00732 00733 d_rules = createProofRules(tm); 00734 d_printer = new PrettyPrinterCore(this); 00735 d_typeComputer = new TypeComputerCore(this); 00736 d_em->registerTypeComputer(d_typeComputer); 00737 d_exprTrans = new ExprTransform(this); 00738 00739 // Register the pretty-printer 00740 d_em->registerPrettyPrinter(*d_printer); 00741 00742 // for (int i = 0; i < LAST_KIND; ++i) d_theoryMap[i] = NULL; 00743 00744 vector<int> kinds; 00745 kinds.push_back(RAW_LIST); 00746 kinds.push_back(BOOLEAN); 00747 kinds.push_back(ANY_TYPE); 00748 kinds.push_back(SUBTYPE); 00749 kinds.push_back(STRING_EXPR); 00750 kinds.push_back(ID); 00751 kinds.push_back(TRUE_EXPR); 00752 kinds.push_back(FALSE_EXPR); 00753 kinds.push_back(UCONST); 00754 kinds.push_back(BOUND_VAR); 00755 kinds.push_back(SKOLEM_VAR); 00756 kinds.push_back(EQ); 00757 kinds.push_back(NEQ); 00758 kinds.push_back(DISTINCT); 00759 kinds.push_back(ECHO); 00760 kinds.push_back(DBG); 00761 kinds.push_back(TRACE); 00762 kinds.push_back(UNTRACE); 00763 kinds.push_back(OPTION); 00764 kinds.push_back(HELP); 00765 kinds.push_back(AND); 00766 kinds.push_back(OR); 00767 kinds.push_back(IFTHEN); 00768 kinds.push_back(IF); 00769 kinds.push_back(ELSE); 00770 kinds.push_back(COND); 00771 kinds.push_back(XOR); 00772 kinds.push_back(NOT); 00773 kinds.push_back(ITE); 00774 kinds.push_back(IFF); 00775 kinds.push_back(IMPLIES); 00776 kinds.push_back(APPLY); 00777 // For printing LET expressions (in DAG printing mode) 00778 kinds.push_back(LET); 00779 kinds.push_back(LETDECLS); 00780 kinds.push_back(LETDECL); 00781 // For printing raw parsed quantifier expressions 00782 kinds.push_back(VARLIST); 00783 kinds.push_back(VARDECLS); 00784 kinds.push_back(VARDECL); 00785 00786 // Type declarations and definitions 00787 kinds.push_back(TYPE); 00788 // For printing type declarations (or definitions) 00789 kinds.push_back(CONST); 00790 00791 kinds.push_back(TYPEDEF); 00792 kinds.push_back(DEFUN); 00793 // Printing proofs 00794 kinds.push_back(PF_APPLY); 00795 kinds.push_back(PF_HOLE); 00796 // Register commands for pretty-printing. Currently, only ASSERT 00797 // needs to be printed. 00798 kinds.push_back(ASSERT); 00799 kinds.push_back(QUERY); 00800 kinds.push_back(PRINT); 00801 00802 kinds.push_back(DUMP_PROOF); 00803 kinds.push_back(DUMP_ASSUMPTIONS); 00804 kinds.push_back(DUMP_SIG); 00805 kinds.push_back(DUMP_TCC); 00806 kinds.push_back(DUMP_TCC_ASSUMPTIONS); 00807 kinds.push_back(DUMP_TCC_PROOF); 00808 kinds.push_back(DUMP_CLOSURE); 00809 kinds.push_back(DUMP_CLOSURE_PROOF); 00810 kinds.push_back(TRANSFORM); 00811 kinds.push_back(CALL); 00812 kinds.push_back(WHERE); 00813 kinds.push_back(ASSERTIONS); 00814 kinds.push_back(ASSUMPTIONS); 00815 kinds.push_back(COUNTEREXAMPLE); 00816 kinds.push_back(COUNTERMODEL); 00817 kinds.push_back(PUSH); 00818 kinds.push_back(POP); 00819 kinds.push_back(POPTO); 00820 kinds.push_back(PUSH_SCOPE); 00821 kinds.push_back(POP_SCOPE); 00822 kinds.push_back(POPTO_SCOPE); 00823 kinds.push_back(RESET); 00824 kinds.push_back(CONTEXT); 00825 kinds.push_back(FORGET); 00826 kinds.push_back(GET_TYPE); 00827 kinds.push_back(CHECK_TYPE); 00828 kinds.push_back(GET_CHILD); 00829 kinds.push_back(SUBSTITUTE); 00830 kinds.push_back(SEQ); 00831 kinds.push_back(ARITH_VAR_ORDER); 00832 kinds.push_back(THEOREM_KIND); 00833 00834 kinds.push_back(AND_R); 00835 kinds.push_back(IFF_R); 00836 kinds.push_back(ITE_R); 00837 00838 registerTheory(this, kinds); 00839 } 00840 00841 00842 TheoryCore::~TheoryCore() 00843 { 00844 delete d_exprTrans; 00845 delete d_rules; 00846 delete d_typeComputer; 00847 d_em->unregisterPrettyPrinter(); 00848 delete d_printer; 00849 } 00850 00851 00852 Theorem TheoryCore::callTheoryPreprocess(const Expr& e) 00853 { 00854 Theorem thm = reflexivityRule(e); 00855 for(unsigned i=1; i<d_theories.size(); ++i) { 00856 thm = transitivityRule(thm, d_theories[i]->theoryPreprocess(thm.getRHS())); 00857 } 00858 processFactQueue(LOW); 00859 return thm; 00860 } 00861 00862 00863 Theorem TheoryCore::getTheoremForTerm(const Expr& e){ 00864 00865 // <<<<<<< theory_core_sat.cpp 00866 // // DebugAssert(e.hasFind(), "getTheoremForTerm called on term without find"); 00867 // CDMap<Expr, Theorem>::iterator i = d_termTheorems.find(e); 00868 // if( i == d_termTheorems.end()){ 00869 // TRACE("quantlevel", "getTheoremForTerm: no theorem found: ", e , ""); 00870 // Theorem nul; 00871 // return nul; 00872 // } 00873 // // DebugAssert(i != d_termTheorems.end(), "getTheoremForTerm: no theorem found"); 00874 // ======= 00875 // DebugAssert(e.hasFind() || e.isStoredPredicate(), "getTheoremForTerm called on invalid term"); 00876 00877 hash_map<Expr, Theorem>::iterator i = d_termTheorems.find(e); 00878 // yeting, I think we should use CDMap here, but a static map works better. 00879 // CDMap<Expr, Theorem>::iterator i = d_termTheorems.find(e); 00880 00881 // DebugAssert(i != d_termTheorems.end(), "getTheoremForTerm: no theorem found"); 00882 00883 if(i != d_termTheorems.end()){ 00884 return (*i).second; 00885 } 00886 else{ 00887 TRACE("quantlevel", "getTheoremForTerm: no theorem found: ", e , ""); 00888 Theorem x; 00889 return x; 00890 } 00891 } 00892 00893 #ifdef _CVC3_DEBUG_MODE 00894 int TheoryCore::getCurQuantLevel(){ 00895 return theoryOf(FORALL)->help(1); 00896 } 00897 #endif 00898 00899 unsigned TheoryCore::getQuantLevelForTerm(const Expr& e) 00900 { 00901 00902 00903 /* 00904 if (!e.hasFind() && !e.isStoredPredicate()) { 00905 TRACE("quantlevel", "get 0 ", e , ""); 00906 return 0; 00907 } 00908 */ 00909 TRACE("quantlevel", "trying get level for (" + e.toString() + ") with index ", "", e.getIndex()); 00910 Theorem thm = getTheoremForTerm(e); 00911 if (thm.isNull()) { 00912 if(e.isNot()){ 00913 thm = getTheoremForTerm(e[0]); 00914 } 00915 } 00916 00917 if(thm.isNull()){ 00918 if (e.inUserAssumption()) { 00919 return 0 ; 00920 } 00921 else{ 00922 TRACE("quantlevel", "expr get null :", e.getIndex(), "" ); 00923 if( ! (e.isNot() || e.isIff())){ 00924 TRACE("quantlevel", "cannot find expr: " , e, ""); 00925 } 00926 return 0; 00927 } 00928 } 00929 00930 TRACE("quantlevel", "expr get level:", thm.getQuantLevel(), ""); 00931 00932 /* 00933 if(thm.getQuantLevel() != thm.getQuantLevelDebug()){ 00934 cout << "theorem: " << thm.getExpr().toString() <<endl; 00935 cout << "quant level : " << thm.getQuantLevel()<<endl; 00936 cout << "debug quant level : " << thm.getQuantLevelDebug() <<endl; 00937 cout << "the proof is " << thm.getProof() << endl; 00938 } 00939 */ 00940 00941 return thm.getQuantLevel(); 00942 /* 00943 unsigned ql = thm.getQuantLevel(); 00944 unsigned qld = thm.getQuantLevelDebug(); 00945 return (ql > qld ? ql : qld); 00946 */ 00947 } 00948 00949 00950 /////////////////////////////////////////////////////////////////////////////// 00951 // Theory interface implementaion // 00952 /////////////////////////////////////////////////////////////////////////////// 00953 00954 00955 void TheoryCore::assertFact(const Theorem& e) 00956 { 00957 DebugAssert(e.getExpr().unnegate().getKind() == SKOLEM_VAR || 00958 e.getExpr().unnegate().getKind() == UCONST, 00959 "TheoryCore::assertFact("+e.toString()+")"); 00960 } 00961 00962 00963 Theorem TheoryCore::rewrite(const Expr& e) 00964 { 00965 Theorem thm; 00966 switch (e.getKind()) { 00967 case TRUE_EXPR: 00968 case FALSE_EXPR: 00969 case UCONST: 00970 case BOUND_VAR: 00971 case SKOLEM_VAR: 00972 thm = reflexivityRule(e); 00973 break; // do not rewrite 00974 case LETDECL: 00975 // Replace LETDECL with its definition. The 00976 // typechecker makes sure it's type-safe to do so. 00977 thm = d_rules->rewriteLetDecl(e); 00978 break; 00979 case APPLY: 00980 //TODO: this is a bit of a hack 00981 if (e.getOpKind() == LAMBDA) 00982 thm = theoryOf(LAMBDA)->rewrite(e); 00983 else thm = reflexivityRule(e); 00984 break; 00985 case EQ: 00986 case NOT: 00987 thm = rewriteLitCore(e); 00988 break; 00989 case DISTINCT: { 00990 Theorem thm1 = d_rules->rewriteDistinct(e); 00991 thm = transitivityRule(thm1, simplify(thm1.getRHS())); 00992 break; 00993 } 00994 case IMPLIES: { 00995 thm = d_rules->rewriteImplies(e); 00996 const Expr& rhs = thm.getRHS(); 00997 // rhs = OR(!e1, e2). Rewrite !e1, then top-level OR(). 00998 DebugAssert(rhs.isOr() && rhs.arity() == 2, 00999 "TheoryCore::rewrite[IMPLIES]: rhs = "+rhs.toString()); 01000 Theorem rw = rewriteCore(rhs[0]); 01001 if (!rw.isRefl()) { 01002 vector<unsigned> changed; 01003 vector<Theorem> thms; 01004 changed.push_back(0); 01005 thms.push_back(rw); 01006 rw = substitutivityRule(rhs, changed, thms); 01007 // Simplify to the find pointer of the result 01008 rw = transitivityRule(rw, find(rw.getRHS())); 01009 // Now rw = Theorem(rhs = rhs') 01010 rw = transitivityRule(rw, rewrite(rw.getRHS())); 01011 } else 01012 rw = rewrite(rhs); 01013 thm = transitivityRule(thm, rw); 01014 // thm = transitivityRule(thm, simplify(thm.getRHS())); 01015 break; 01016 } 01017 case XOR: { 01018 thm = d_commonRules->xorToIff(e); 01019 thm = transitivityRule(thm, simplify(thm.getRHS())); 01020 break; 01021 } 01022 case IFF: { 01023 thm = d_commonRules->rewriteIff(e); 01024 Expr e1 = thm.getRHS(); 01025 // The only time we need to rewrite the result (e1) is when 01026 // e==(FALSE<=>e[1]) or (e[1]<=>FALSE), so e1==!e[1]. 01027 if (e != e1 && e1.isNot()) 01028 thm = transitivityRule(thm, rewriteCore(e1)); 01029 break; 01030 } 01031 case ITE: 01032 thm = rewriteIte(e); 01033 if (!thm.isRefl()) break; 01034 else if (getFlags()["un-ite-ify"].getBool()) { 01035 // undo the rewriting of Boolean connectives to ITEs. 01036 // helpful for examples converted from SVC. 01037 // must rewrite again because we might create expressions 01038 // that can be further rewritten, and we must normalize. 01039 if (e[1].isFalse() && e[2].isTrue()) 01040 thm = rewriteCore(d_rules->rewriteIteToNot(e)); 01041 else if (e[1].isTrue()) 01042 thm = rewriteCore(d_rules->rewriteIteToOr(e)); 01043 else if (e[2].isFalse()) 01044 thm = rewriteCore(d_rules->rewriteIteToAnd(e)); 01045 else if (e[2].isTrue()) 01046 thm = rewriteCore(d_rules->rewriteIteToImp(e)); 01047 else if (e[1] == e[2].negate()) 01048 thm = rewriteCore(d_rules->rewriteIteToIff(e)); 01049 else thm = reflexivityRule(e); 01050 } 01051 else if(getFlags()["ite-cond-simp"].getBool()) { 01052 thm = d_rules->rewriteIteCond(e); 01053 if (!thm.isRefl()) { 01054 thm = transitivityRule(thm, simplify(thm.getRHS())); 01055 } 01056 } 01057 else thm = reflexivityRule(e); 01058 break; 01059 case AND: { 01060 thm = rewriteAnd(e); 01061 Expr ee = thm.getRHS(); 01062 break; 01063 } 01064 case OR: { 01065 thm = rewriteOr(e); 01066 Expr ee = thm.getRHS(); 01067 break; 01068 } 01069 // Quantifiers 01070 case FORALL: 01071 case EXISTS: 01072 thm = d_commonRules->reflexivityRule(e); 01073 break; 01074 // don't need to rewrite these 01075 case AND_R: 01076 case IFF_R: 01077 case ITE_R: 01078 thm = reflexivityRule(e); 01079 break; 01080 default: 01081 DebugAssert(false, 01082 "TheoryCore::rewrite(" 01083 + e.toString() + " : " + e.getType().toString() 01084 + "): Not implemented"); 01085 break; 01086 } 01087 01088 DebugAssert(thm.getLHS() == e, "TheoryCore::rewrite("+e.toString() 01089 +") = "+thm.getExpr().toString()); 01090 01091 Expr rhs = thm.getRHS(); 01092 // Advanced Boolean rewrites 01093 switch(rhs.getKind()) { 01094 case AND: 01095 if(getFlags()["simp-and"].getBool()) { 01096 Theorem tmp(reflexivityRule(rhs)); 01097 for(int i=0, iend=rhs.arity(); i<iend; ++i) { 01098 tmp = transitivityRule 01099 (tmp, d_rules->rewriteAndSubterms(tmp.getRHS(), i)); 01100 } 01101 if(tmp.getRHS() != rhs) { // Something changed: simplify recursively 01102 thm = transitivityRule(thm, tmp); 01103 thm = transitivityRule(thm, simplify(thm.getRHS())); 01104 rhs = thm.getRHS(); 01105 } 01106 } 01107 break; 01108 case OR: 01109 if(getFlags()["simp-or"].getBool()) { 01110 Theorem tmp(reflexivityRule(rhs)); 01111 for(int i=0, iend=rhs.arity(); i<iend; ++i) { 01112 tmp = transitivityRule 01113 (tmp, d_rules->rewriteOrSubterms(tmp.getRHS(), i)); 01114 } 01115 if(tmp.getRHS() != rhs) { // Something changed: simplify recursively 01116 thm = transitivityRule(thm, tmp); 01117 thm = transitivityRule(thm, simplify(thm.getRHS())); 01118 rhs = thm.getRHS(); 01119 } 01120 } 01121 break; 01122 default: 01123 break; 01124 } 01125 if (theoryOf(rhs) == this) { 01126 // Core rewrites are idempotent (FIXME: are they, still?) 01127 rhs.setRewriteNormal(); 01128 } 01129 return thm; 01130 } 01131 01132 01133 /*! We use the update method of theory core to track registered atomic 01134 * formulas. Updates are recorded and then processed by calling processUpdates 01135 * once all equalities have been processed. */ 01136 void TheoryCore::update(const Theorem& e, const Expr& d) 01137 { 01138 // Disequalities 01139 if (d.isNot()) { 01140 const Expr& eq = d[0]; 01141 DebugAssert(eq.isEq(), "Expected equality"); 01142 Theorem thm1(find(eq[0])); 01143 Theorem thm2(find(eq[1])); 01144 const Expr& newlhs = thm1.getRHS(); 01145 const Expr& newrhs = thm2.getRHS(); 01146 if (newlhs == newrhs) { 01147 Theorem thm = find(eq); 01148 DebugAssert(thm.getRHS().isFalse(), "Expected disequality"); 01149 Theorem leftEqRight = transitivityRule(thm1, symmetryRule(thm2)); 01150 setInconsistent(iffMP(leftEqRight, thm)); 01151 } 01152 else { 01153 e.getRHS().addToNotify(this, d); 01154 // propagate new disequality 01155 Theorem thm = d_commonRules->substitutivityRule(eq, thm1, thm2); 01156 if (newlhs < newrhs) { 01157 thm = transitivityRule(thm, d_commonRules->rewriteUsingSymmetry(thm.getRHS())); 01158 } 01159 const Expr& newEq = thm.getRHS(); 01160 if (newEq.hasFind()) { 01161 Theorem thm2 = find(newEq); 01162 if (thm2.getRHS().isTrue()) { 01163 thm2 = transitivityRule(thm, thm2); 01164 thm = find(eq); 01165 DebugAssert(thm.getRHS().isFalse(), "Expected disequality"); 01166 thm = transitivityRule(symmetryRule(thm), thm2); 01167 setInconsistent(d_commonRules->iffTrueElim(thm)); 01168 } 01169 // else if thm2.getRHS().isFalse(), nothing to do 01170 } 01171 else { 01172 Theorem thm2 = find(eq); 01173 DebugAssert(thm2.getRHS().isFalse(), "Expected disequality"); 01174 thm2 = transitivityRule(symmetryRule(thm),thm2); 01175 setFindLiteral(d_commonRules->iffFalseElim(thm2)); 01176 } 01177 } 01178 } 01179 // Registered atoms 01180 else { 01181 DebugAssert(d.isRegisteredAtom(), "Expected registered atom"); 01182 if (!d.isImpliedLiteral()) { 01183 d_update_thms.push_back(e); 01184 d_update_data.push_back(d); 01185 } 01186 } 01187 } 01188 01189 01190 void TheoryCore::checkEquation(const Theorem& thm) 01191 { 01192 Expr e2 = thm.getExpr(); 01193 DebugAssert(e2.isEq(), "Expected equation"); 01194 Expr solved; 01195 if (d_solver) { 01196 solved = d_solver->solve(thm).getExpr(); 01197 DebugAssert(solved == e2, "e2 = "+e2.toString() 01198 +"\nsolved = "+solved.toString()); 01199 } 01200 Theory* i = theoryOf(e2); 01201 if (d_solver != i) { 01202 solved = i->solve(thm).getExpr(); 01203 DebugAssert(solved == e2, "e2 = "+e2.toString() 01204 +"\nsolved = "+solved.toString()); 01205 } 01206 Theory* j = theoryOf(e2[0].getType()); 01207 if (d_solver != j && i != j) { 01208 solved = j->solve(thm).getExpr(); 01209 DebugAssert(solved == e2, "e2 = "+e2.toString() 01210 +"\nsolved = "+solved.toString()); 01211 } 01212 } 01213 01214 01215 void TheoryCore::checkSolved(const Theorem& thm) 01216 { 01217 Expr e2 = thm.getExpr(); 01218 if (e2.isAnd()) { 01219 for (int index = 0; index < e2.arity(); ++index) { 01220 checkEquation(d_commonRules->andElim(thm, index)); 01221 } 01222 } 01223 else if (!e2.isBoolConst()) checkEquation(thm); 01224 } 01225 01226 01227 /*****************************************************************************/ 01228 /*! 01229 * Function: TheoryCore::solve 01230 * 01231 * Author: Clark Barrett 01232 * 01233 * Created: Wed Feb 26 16:17:54 2003 01234 * 01235 * This is a generalization of what's in my thesis. The goal is to rewrite e 01236 * into an equisatisfiable conjunction of equations such that the left-hand 01237 * side of each equation is a variable which does not appear as an i-leaf of 01238 * the rhs, where i is the theory of the primary solver. Any solution which 01239 * satisfies this is fine. "Solvers" from other theories can do whatever they 01240 * want as long as we eventually reach this form. 01241 */ 01242 /*****************************************************************************/ 01243 Theorem TheoryCore::solve(const Theorem& eThm) 01244 { 01245 const Expr& e = eThm.getExpr(); 01246 Theorem thm; 01247 Expr e2; 01248 01249 DebugAssert(eThm.isRewrite() && eThm.getLHS().isTerm(), "Expected equation"); 01250 01251 // Invoke the primary solver 01252 if (d_solver) { 01253 thm = d_solver->solve(eThm); 01254 e2 = thm.getExpr(); 01255 if (e2.isBoolConst() || e2.isAnd()) { 01256 // We expect a conjunction of equations, each of which is terminally solved 01257 IF_DEBUG(checkSolved(thm)); 01258 return thm; 01259 } 01260 } 01261 else { 01262 thm = eThm; 01263 e2 = e; 01264 } 01265 01266 // Invoke solver based on owner of equation 01267 DebugAssert(e2.isEq(), "Expected equation"); 01268 Theory* i = theoryOf(e2); 01269 if (d_solver != i) thm = i->solve(thm); 01270 e2 = thm.getExpr(); 01271 if (e2.isBoolConst() || e2.isAnd()) { 01272 // We expect a conjunction of equations, each of which is solved 01273 IF_DEBUG(checkSolved(thm)); 01274 return thm; 01275 } 01276 01277 // Invoke solver based on type of terms in equation 01278 DebugAssert(e2.isEq(), "Expected equation"); 01279 Theory* j = theoryOf(getBaseType(e2[0])); 01280 if (d_solver != j && i != j) thm = j->solve(thm); 01281 01282 IF_DEBUG(checkSolved(thm)); 01283 return thm; 01284 } 01285 01286 01287 Theorem TheoryCore::simplifyOp(const Expr& e) 01288 { 01289 int kind(e.getKind()); 01290 01291 switch(kind) { 01292 case EQ: 01293 case IFF: 01294 if(e[0]==e[1]) { 01295 IF_DEBUG(debugger.counter("simplified x=x")++;) 01296 return d_commonRules->iffTrue(reflexivityRule(e[0])); 01297 } 01298 return Theory::simplifyOp(e); 01299 case AND: 01300 case OR: { 01301 // Stop when a child has this kind 01302 int endKind = (kind==AND)? FALSE_EXPR : TRUE_EXPR; 01303 int ar = e.arity(); 01304 // Optimization: before simplifying anything recursively, check if 01305 // any kid is already TRUE or FALSE, and just return at that point 01306 int l(0); 01307 for(; l<ar && e[l].getKind() != endKind; ++l); 01308 if(l < ar) { // Found TRUE or FALSE: e simplifies to a const 01309 IF_DEBUG(debugger.counter("simplified AND/OR topdown")++;) 01310 if(kind==AND) 01311 return rewriteAnd(e); 01312 else 01313 return rewriteOr(e); 01314 } 01315 vector<Theorem> newChildrenThm; 01316 vector<unsigned> changed; 01317 for(int k = 0; k < ar; ++k) { 01318 // Recursively simplify the kids 01319 Theorem thm = simplify(e[k]); 01320 if (!thm.isRefl()) { 01321 if (thm.getRHS().getKind() == endKind) { 01322 newChildrenThm.clear(); 01323 changed.clear(); 01324 newChildrenThm.push_back(thm); 01325 changed.push_back(k); 01326 thm = substitutivityRule(e, changed, newChildrenThm); 01327 // Simplify to TRUE or FALSE 01328 if(kind==AND) 01329 thm = transitivityRule(thm, rewriteAnd(thm.getRHS())); 01330 else 01331 thm = transitivityRule(thm, rewriteOr(thm.getRHS())); 01332 IF_DEBUG(debugger.counter("simplified AND/OR: skipped kids") 01333 += ar-k-1;) 01334 return thm; 01335 } else { // Child simplified to something else 01336 newChildrenThm.push_back(thm); 01337 changed.push_back(k); 01338 } 01339 } 01340 } 01341 if(changed.size() > 0) 01342 return substitutivityRule(e, changed, newChildrenThm); 01343 break; 01344 } 01345 case ITE: { 01346 DebugAssert(e.arity()==3, "Bad ITE in TheoryCore::simplify(e=" 01347 +e.toString()+")"); 01348 // Optimization: check if the two branches are the same, so we 01349 // don't have to simplify the condition 01350 if(e[1]==e[2]) { 01351 IF_DEBUG(debugger.counter("simplified ITE(c,e,e)")++;) 01352 Theorem res = d_commonRules->rewriteIteSame(e); 01353 return transitivityRule(res, simplify(res.getRHS())); 01354 } 01355 01356 // First, simplify the conditional 01357 vector<Theorem> newChildrenThm; 01358 vector<unsigned> changed; 01359 Theorem thm = simplify(e[0]); 01360 if (!thm.isRefl()) { 01361 newChildrenThm.push_back(thm); 01362 changed.push_back(0); 01363 } 01364 Expr cond = thm.getRHS(); 01365 01366 for(int k=1; k<=2; ++k) { 01367 // If condition value is known, only the appropriate branch 01368 // needs to be simplified 01369 if (cond.isBoolConst()) { 01370 if((k==1 && cond.isFalse()) || (k==2 && cond.isTrue())) { 01371 IF_DEBUG(debugger.counter("simplified ITE: skiped one branch")++;) 01372 continue; 01373 } 01374 } 01375 thm = simplify(e[k]); 01376 if (!thm.isRefl()) { 01377 newChildrenThm.push_back(thm); 01378 changed.push_back(k); 01379 } 01380 } 01381 if(changed.size() > 0) 01382 return substitutivityRule(e, changed, newChildrenThm); 01383 break; 01384 } 01385 case NOT: { 01386 Theorem res = simplify(e[0]); 01387 if (!res.isRefl()) { 01388 return d_commonRules->substitutivityRule(e, res); 01389 } 01390 break; 01391 } 01392 case IMPLIES: { 01393 Theorem res = d_rules->rewriteImplies(e); 01394 return transitivityRule(res, simplifyOp(res.getRHS())); 01395 } 01396 default: 01397 return Theory::simplifyOp(e); 01398 } 01399 return reflexivityRule(e); 01400 } 01401 01402 01403 void TheoryCore::checkType(const Expr& e) 01404 { 01405 switch (e.getKind()) { 01406 case BOOLEAN: 01407 if (e.arity() > 0) { 01408 throw Exception("Ill-formed Boolean type:\n\n"+e.toString()); 01409 } 01410 break; 01411 case SUBTYPE: { 01412 if (e.arity() != 1) 01413 throw Exception("Ill-formed SUBTYPE expression:\n\n"+e.toString()); 01414 Type t = e[0].getType(); 01415 if (!t.isFunction()) 01416 throw Exception 01417 ("Non-function argument to SUBTYPE:\n\n" 01418 +e.toString()); 01419 if (!t[1].isBool()) 01420 throw Exception 01421 ("Non-predicate argument to SUBTYPE:\n\n" 01422 +e.toString()); 01423 } 01424 break; 01425 case ANY_TYPE: { 01426 if (e.arity() != 0) { 01427 throw Exception("Expected no children: "+e.toString()); 01428 } 01429 break; 01430 } 01431 default: 01432 FatalAssert(false, "Unexpected kind in TheoryCore::checkType" 01433 +getEM()->getKindName(e.getKind())); 01434 } 01435 } 01436 01437 01438 Cardinality TheoryCore::finiteTypeInfo(Expr& e, Unsigned& n, 01439 bool enumerate, bool computeSize) 01440 { 01441 Cardinality card = CARD_INFINITE; 01442 switch (e.getKind()) { 01443 case BOOLEAN: 01444 card = CARD_FINITE; 01445 if (enumerate) { 01446 e = (n == 0) ? falseExpr() : (n == 1) ? trueExpr() : Expr(); 01447 } 01448 if (computeSize) { 01449 n = 2; 01450 } 01451 break; 01452 case SUBTYPE: 01453 card = CARD_UNKNOWN; 01454 break; 01455 case ANY_TYPE: 01456 card = CARD_UNKNOWN; 01457 break; 01458 default: 01459 FatalAssert(false, "Unexpected kind in TheoryCore::finiteTypeInfo" 01460 +getEM()->getKindName(e.getKind())); 01461 } 01462 return card; 01463 } 01464 01465 01466 void TheoryCore::computeType(const Expr& e) 01467 { 01468 switch (e.getKind()) { 01469 case ITE: { 01470 Type t1(getBaseType(e[1])), t2(getBaseType(e[2])); 01471 if (e[0].getType() != boolType()) 01472 throw TypecheckException 01473 ("The conditional in IF-THEN-ELSE must be BOOLEAN, but is:\n\n" 01474 +e[0].getType().toString() 01475 +"\n\nIn the expression:\n\n " 01476 +e.toString()); 01477 if(t1 != t2) { 01478 throw TypecheckException 01479 ("The types of the IF-THEN-ELSE branches do not match.\n" 01480 "THEN branch has the type:\n\n " 01481 +e[1].getType().toString() 01482 +"\n\nELSE branch has the type:\n\n " 01483 +e[2].getType().toString() 01484 +"\n\nIn expression:\n\n "+e.toString()); 01485 } 01486 Type res(e[1].getType()); 01487 // If the precise types match in both branches, use it as the 01488 // result type. 01489 if(res == e[2].getType()) { 01490 e.setType(res); 01491 } 01492 else 01493 // Note: setting the base type, since e[1] and e[2] have 01494 // different exact types, and the base type is a conservative 01495 // approximation we can easily compute. 01496 e.setType(t1); 01497 } 01498 break; 01499 case EQ: { 01500 Type t0(getBaseType(e[0])), t1(getBaseType(e[1])); 01501 if (t0.isBool() || t1.isBool()) { 01502 throw TypecheckException 01503 ("Cannot use EQ ('=') for BOOLEAN type; use IFF ('<=>') instead.\n" 01504 "Error in the following expression:\n"+e.toString()); 01505 } 01506 if (t0 != t1) { 01507 throw TypecheckException 01508 ("Type mismatch in equality:\n\n LHS type:\n"+t0.toString() 01509 +"\n\n RHS type: \n"+t1.toString() 01510 +"\n\n in expression: \n"+e.toString()); 01511 } 01512 e.setType(boolType()); 01513 break; 01514 } 01515 case DISTINCT: { 01516 Type t0(getBaseType(e[0])); 01517 for (int i = 1; i < e.arity(); ++i) { 01518 if (t0 != getBaseType(e[i])) { 01519 throw TypecheckException 01520 ("Type mismatch in distinct:\n\n types:\n"+t0.toString() 01521 +"\n\n and type: \n"+getBaseType(e[i]).toString() 01522 +"\n\n in expression: \n"+e.toString()); 01523 } 01524 } 01525 e.setType(boolType()); 01526 break; 01527 } 01528 case NOT: 01529 case AND: 01530 case OR: 01531 case XOR: 01532 case IFF: 01533 case IMPLIES: 01534 01535 case AND_R: 01536 case IFF_R: 01537 case ITE_R: 01538 01539 for (int k = 0; k < e.arity(); ++k) { 01540 if (e[k].getType() != boolType()) { 01541 throw TypecheckException(e.toString()); 01542 } 01543 } 01544 e.setType(boolType()); 01545 break; 01546 case LETDECL: { 01547 Type varTp(getBaseType(e[0])); 01548 Type valTp(getBaseType(e[1])); 01549 if(valTp != varTp) { 01550 throw TypecheckException("Type mismatch for "+e[0].toString()+":" 01551 +"\n declared: " 01552 + varTp.toString() 01553 +"\n derived: "+ valTp.toString()); 01554 } 01555 e.setType(e[0].getType()); 01556 } 01557 break; 01558 case APPLY: 01559 { 01560 DebugAssert(e.isApply(), "Should be application"); 01561 DebugAssert(e.arity() > 0, "Expected non-zero arity in APPLY"); 01562 Expr funExpr = e.getOpExpr(); 01563 Type funType = funExpr.getType(); 01564 01565 if(!funType.isFunction()) { 01566 throw TypecheckException 01567 ("Expected function type for:\n\n" 01568 + funExpr.toString() + "\n\n but got this: " 01569 +funType.getExpr().toString() 01570 +"\n\n in function application:\n\n"+e.toString()); 01571 } 01572 01573 if(funType.arity() != e.arity()+1) 01574 throw TypecheckException("Type mismatch for expression:\n\n " 01575 + e.toString() 01576 + "\n\nFunction \""+funExpr.toString() 01577 +"\" expects "+int2string(funType.arity()-1) 01578 +" argument" 01579 +string((funType.arity()==2)? "" : "s") 01580 +", but received " 01581 +int2string(e.arity())+"."); 01582 01583 for (int k = 0; k < e.arity(); ++k) { 01584 Type valType(getBaseType(e[k])); 01585 if (funType[k] != Type::anyType(d_em) && !(valType == getBaseType(funType[k]) || valType == Type::anyType(d_em)) ) { 01586 throw TypecheckException("Type mismatch for expression:\n\n " 01587 + e[k].toString() 01588 + "\n\nhas the following type:\n\n " 01589 + e[k].getType().toString() 01590 + "\n\nbut the expected type is:\n\n " 01591 + funType[k].getExpr().toString() 01592 + "\n\nin function application:\n\n " 01593 + e.toString()); 01594 } 01595 } 01596 e.setType(funType[funType.arity()-1]); 01597 break; 01598 } 01599 case RAW_LIST: 01600 throw TypecheckException("computeType called on RAW_LIST"); 01601 break; 01602 default: 01603 DebugAssert(false,"TheoryCore::computeType(" + e.toString() 01604 + "):\nNot implemented"); 01605 break; 01606 } 01607 } 01608 01609 01610 Type TheoryCore::computeBaseType(const Type& tp) 01611 { 01612 const Expr& e = tp.getExpr(); 01613 Type res; 01614 switch(e.getKind()) { 01615 case SUBTYPE: { 01616 DebugAssert(e.arity() == 1, "Expr::computeBaseType(): "+e.toString()); 01617 Type lambdaTp = e[0].getType(); 01618 Type lambdaBaseTp = getBaseType(lambdaTp); 01619 DebugAssert(lambdaBaseTp.isFunction(), 01620 "Expr::computeBaseType(): lambdaBaseTp = " 01621 +lambdaBaseTp.toString()+" in e = "+e.toString()); 01622 res = lambdaBaseTp[0]; 01623 break; 01624 } 01625 case BOOLEAN: 01626 case ANY_TYPE: 01627 res = tp; 01628 break; 01629 case TYPEDEF: // Compute the base type of the definition 01630 res = getBaseType(Type(e[1])); 01631 break; 01632 default: 01633 DebugAssert(false, "TheoryCore::computeBaseType("+tp.toString()+")"); 01634 res = tp; 01635 } 01636 return res; 01637 } 01638 01639 01640 Expr TheoryCore::computeTCC(const Expr& e) 01641 { 01642 Expr res; 01643 switch (e.getKind()) { 01644 case NOT: 01645 res = getTCC(e[0]); 01646 break; 01647 case AND: { 01648 // ( (tcc(e1) & !e1) \/ ... \/ (tcc(en) & !en) \/ (tcc(e1)&...&tcc(en)) 01649 vector<Expr> tccs; 01650 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 01651 tccs.push_back(getTCC(*i)); 01652 vector<Expr> pairs; 01653 pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS()); 01654 for(size_t i=0, iend=tccs.size(); i<iend; ++i) 01655 pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i].negate())).getRHS()); 01656 res = rewriteOr(orExpr(pairs)).getRHS(); 01657 break; 01658 } 01659 case OR: { 01660 // ( (tcc(e1) & e1) \/ ... \/ (tcc(en) & en) \/ (tcc(e1)&...&tcc(en)) 01661 vector<Expr> tccs; 01662 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 01663 tccs.push_back(getTCC(*i)); 01664 vector<Expr> pairs; 01665 pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS()); 01666 for(size_t i=0, iend=tccs.size(); i<iend; ++i) 01667 pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i])).getRHS()); 01668 res = rewriteOr(orExpr(pairs)).getRHS(); 01669 break; 01670 } 01671 case ITE: { 01672 Expr tcc1(getTCC(e[1])), tcc2(getTCC(e[2])); 01673 // Optimize: if TCCs on both branches are the same, skip the ITE 01674 Expr tccITE((tcc1 == tcc2)? tcc1 : e[0].iteExpr(tcc1, tcc2)); 01675 res = rewriteAnd(getTCC(e[0]).andExpr(tccITE)).getRHS(); 01676 break; 01677 } 01678 case IMPLIES: 01679 res = getTCC(e[0].negate().orExpr(e[1])); 01680 break; 01681 case APPLY: { 01682 Theory* i = theoryOf(e); 01683 if (i != this) return i->computeTCC(e); 01684 // fall through 01685 } 01686 default: // All the other operators are strict 01687 res = Theory::computeTCC(e); 01688 break; 01689 } 01690 return res; 01691 } 01692 01693 01694 Expr TheoryCore::computeTypePred(const Type& t, const Expr& e) 01695 { 01696 Expr tExpr = t.getExpr(); 01697 switch(tExpr.getKind()) { 01698 case SUBTYPE: { 01699 Expr pred = tExpr[0]; 01700 const Type& argTp = pred.lookupType()[0]; 01701 return Expr(pred.mkOp(), e).andExpr(getTypePred(argTp, e)); 01702 } 01703 case APPLY: { 01704 Theory* i = theoryOf(e); 01705 if (i != this) return i->computeTypePred(t, e); 01706 // fall through 01707 } 01708 default: 01709 return e.getEM()->trueExpr(); 01710 } 01711 } 01712 01713 01714 Expr TheoryCore::parseExprOp(const Expr& e) 01715 { 01716 // If the expression is not a list, it must have been already 01717 // parsed, so just return it as is. 01718 switch(e.getKind()) { 01719 case ID: { 01720 int kind = getEM()->getKind(e[0].getString()); 01721 switch(kind) { 01722 case NULL_KIND: return e; // nothing to do 01723 case TRUE_EXPR: 01724 case FALSE_EXPR: 01725 case TYPE: 01726 case BOOLEAN: return getEM()->newLeafExpr(kind); 01727 default: 01728 DebugAssert(false, "Bad use of bare keyword: "+e.toString()); 01729 return e; 01730 } 01731 } 01732 case RAW_LIST: break; // break out of switch, do the work 01733 default: 01734 return e; 01735 } 01736 DebugAssert(e.getKind()==RAW_LIST && e.arity() > 0 && e[0].getKind()==ID, 01737 "TheoryCore::parseExprOp:\n e = "+e.toString()); 01738 /* The first element of the list (e[0] is an ID of the operator. 01739 ID string values are the dirst element of the expression */ 01740 const Expr& c1 = e[0][0]; 01741 int kind = getEM()->getKind(c1.getString()); 01742 01743 if (isBasicKind(kind)) { 01744 vector<Expr> operatorStack; 01745 vector<Expr> operandStack; 01746 vector<int> childStack; 01747 Expr e2; 01748 01749 operatorStack.push_back(e); 01750 childStack.push_back(1); 01751 01752 while (!operatorStack.empty()) { 01753 DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated"); 01754 01755 if (childStack.back() < operatorStack.back().arity()) { 01756 01757 e2 = operatorStack.back()[childStack.back()++]; 01758 01759 ExprMap<Expr>::iterator iParseCache = d_parseCache.find(e2); 01760 if (iParseCache != d_parseCache.end()) { 01761 operandStack.push_back((*iParseCache).second); 01762 } 01763 else if (e2.getKind() == RAW_LIST && 01764 e2.arity() > 0 && 01765 e2[0].getKind() == ID && 01766 isBasicKind(getEM()->getKind(e2[0][0].getString()))) { 01767 operatorStack.push_back(e2); 01768 childStack.push_back(1); 01769 } 01770 else { 01771 operandStack.push_back(parseExpr(e2)); 01772 } 01773 } 01774 else { 01775 e2 = operatorStack.back(); 01776 operatorStack.pop_back(); 01777 childStack.pop_back(); 01778 vector<Expr> children; 01779 vector<Expr>::iterator childStart = operandStack.end() - (e2.arity() - 1); 01780 children.insert(children.begin(), childStart, operandStack.end()); 01781 operandStack.erase(childStart, operandStack.end()); 01782 kind = getEM()->getKind(e2[0][0].getString()); 01783 operandStack.push_back(Expr(kind, children, e2.getEM())); 01784 d_parseCache[e2] = operandStack.back(); 01785 if (!getEM()->isTypeKind(operandStack.back().getKind())) { 01786 operandStack.back().getType(); 01787 } 01788 } 01789 } 01790 DebugAssert(childStack.empty(), "Invariant violated"); 01791 DebugAssert(operandStack.size() == 1, "Expected single operand left"); 01792 return operandStack.back(); 01793 } 01794 01795 switch(kind) { 01796 case SUBTYPE: 01797 if (e.arity() <= 3) { 01798 Expr witness; 01799 if (e.arity() == 3) { 01800 witness = parseExpr(e[2]); 01801 } 01802 return newSubtypeExpr(parseExpr(e[1]), witness).getExpr(); 01803 } 01804 else { 01805 throw ParserException("Expected one or two arguments to SUBTYPE"); 01806 } 01807 case EQ: 01808 if(e.arity()==3) { 01809 Expr e1 = parseExpr(e[1]); 01810 Expr e2 = parseExpr(e[2]); 01811 if (e1.getType() == boolType() && 01812 getFlags()["convert-eq-iff"].getBool()) { 01813 return e1.iffExpr(e2); 01814 } 01815 else { 01816 return e1.eqExpr(e2); 01817 } 01818 } 01819 else 01820 throw ParserException("Equality requires exactly two arguments: " 01821 +e.toString()); 01822 break; 01823 01824 case NEQ: 01825 if(e.arity()==3) 01826 return !(parseExpr(e[1]).eqExpr(parseExpr(e[2]))); 01827 else 01828 throw ParserException("Disequality requires exactly two arguments: " 01829 +e.toString()); 01830 break; 01831 case TYPE: { 01832 if(e.arity()==2) { 01833 const Expr& types = e[1]; 01834 if(types.getKind() == RAW_LIST) { 01835 vector<Expr> names; 01836 for(Expr::iterator i=types.begin(), iend=types.end(); i!=iend; ++i) 01837 names.push_back(*i); 01838 return Expr(TYPEDECL, names, getEM()); 01839 } 01840 } 01841 else if(e.arity() == 3 && e[1].getKind() == ID) 01842 return Expr(TYPEDEF, e[1], parseExpr(e[2])); 01843 throw ParserException("Bad TYPE declaration: "+e.toString()); 01844 break; 01845 } 01846 //TODO: Is IF still used? 01847 case IF: 01848 if(e.arity() == 4) { 01849 Expr c(parseExpr(e[1])); 01850 Expr e1(parseExpr(e[2])); 01851 Expr e2(parseExpr(e[3])); 01852 return c.iteExpr(e1, e2); 01853 } else 01854 throw ParserException("Bad IF-THEN-ELSE expression: " 01855 +e.toString()); 01856 case COND: { 01857 if(e.arity() >= 3) 01858 return processCond(e, 1); 01859 else 01860 throw ParserException("Bad COND expression: "+e.toString()); 01861 break; 01862 } 01863 case LET: { // (LET ((v1 e1) (v2 e2) ... ) body) 01864 Expr e2(e); 01865 while (true) { 01866 if(!(e2.arity() == 3 && e2[1].getKind() == RAW_LIST && e2[1].arity() > 0)) 01867 throw ParserException("Bad LET expression: "+e2.toString()); 01868 01869 // Iterate through the bound variables 01870 for(Expr::iterator i=e2[1].begin(), iend=e2[1].end(); i!=iend; ++i) { 01871 const Expr& decl = *i; 01872 if (decl.getKind() != RAW_LIST || decl.arity() != 2) 01873 throw ParserException("Bad variable declaration block in LET " 01874 "expression: "+decl.toString()+ 01875 "\n e2 = "+e2.toString()); 01876 if (decl[0].getKind() != ID) 01877 throw ParserException("Variable must be an identifier in LET " 01878 "expression: "+decl[0].toString()+ 01879 "\n e2 = "+e2.toString()); 01880 addBoundVar(decl[0][0].getString(), Type(), parseExpr(decl[1])); 01881 } 01882 // Optimization for nested LETs: 01883 if (e2[2].getKind()==RAW_LIST && e2[2].arity() > 0 && 01884 e2[2][0].getKind()==ID && getEM()->getKind(e2[2][0][0].getString()) == LET) { 01885 e2 = e2[2]; 01886 } else break; 01887 } 01888 // Parse the body recursively and return it (nuke the LET) 01889 return parseExpr(e2[2]); 01890 } 01891 case TRUE_EXPR: { return e.getEM()->trueExpr(); } 01892 case FALSE_EXPR: { return e.getEM()->falseExpr();} 01893 case BOOLEAN: { return e.getEM()->boolExpr(); } 01894 break; 01895 default: 01896 DebugAssert(false, 01897 "TheoryCore::parseExprOp: invalid command or expression: " 01898 + e.toString()); 01899 break; 01900 } 01901 return e; 01902 } 01903 01904 01905 ExprStream& TheoryCore::print(ExprStream& os, const Expr& e) 01906 { 01907 switch(os.lang()) { 01908 case SIMPLIFY_LANG: 01909 switch(e.getKind()) { 01910 case TRUE_EXPR: os << "TRUE"; break; 01911 case FALSE_EXPR: os << "FALSE"; break; 01912 case TYPE: 01913 break; // no type for Simplify 01914 case ID: 01915 if(e.arity() == 1 && e[0].isString()) os << e[0].getString(); 01916 else e.print(os); 01917 break; 01918 case CONST: 01919 // os << "ERROR:const to be supported\n"; simplify do not need this 01920 break; 01921 case SUBTYPE: 01922 break; 01923 case TYPEDEF: { 01924 break; 01925 } 01926 case EQ: 01927 os << "(EQ " << e[0] << " " << e[1] << ")"; 01928 break; 01929 case NOT: os << "(NOT " << e[0] << ")"; break; 01930 case AND: { 01931 int i=0, iend=e.arity(); 01932 os << "(AND "; 01933 if(i!=iend) { os << e[i]; ++i; } 01934 for(; i!=iend; ++i) os << " " << e[i]; 01935 os << ")"; 01936 } 01937 break; 01938 case OR: { 01939 int i=0, iend=e.arity(); 01940 os << "(OR "; 01941 if(i!=iend) { os << e[i]; ++i; } 01942 for(; i!=iend; ++i) os << " " << e[i]; 01943 os << ")"; 01944 } 01945 break; 01946 case ITE: 01947 os<<"ERROR:ITE:not supported yet\n"; 01948 break; 01949 case IFF: 01950 if(e.arity() == 2) 01951 os << "(IFF " << e[0] << " " << e[1] << ")"; 01952 else 01953 e.print(os); 01954 break; 01955 case IMPLIES: 01956 os << "(IMPLIES " <<e[0] << " " << e[1] << ")"; 01957 break; 01958 // Commands 01959 case ASSERT: 01960 os << "(BG_PUSH " << e[0] << ")\n"; 01961 break; 01962 case TRANSFORM: 01963 os << "ERROR:TRANSFORM:not supported in Simplify " << push << e[0] << push << "\n"; 01964 break; 01965 case QUERY: 01966 os << e[0] <<"\n"; 01967 break; 01968 case WHERE: 01969 os << "ERROR:WHERE:not supported in Simplify\n"; 01970 break; 01971 case ASSERTIONS: 01972 os << "ERROR:ASSERTIONS:not supported in Simplify\n"; 01973 break; 01974 case ASSUMPTIONS: 01975 os << "ERROR:ASSUMPTIONS:not supported in Simplify\n"; 01976 break; 01977 case COUNTEREXAMPLE: 01978 os << "ERROR:COUNTEREXAMPLE:not supported in Simplify\n"; 01979 break; 01980 case COUNTERMODEL: 01981 os << "ERROR:COUNTERMODEL:not supported in Simplify\n"; 01982 break; 01983 case PUSH: 01984 case POP: 01985 case POPTO: 01986 case PUSH_SCOPE: 01987 case POP_SCOPE: 01988 case POPTO_SCOPE: 01989 case RESET: 01990 os << "ERROR:PUSH and POP:not supported in Simplify\n"; 01991 break; 01992 // case CONSTDEF: 01993 case LETDECL: 01994 os << "LETDECL not supported in Simplify\n"; 01995 break; 01996 case LET: { 01997 // (LET (LETDECLS (LETDECL var [ type ] val) .... ) body) 01998 /* bool first(true); 01999 os << "(" << push << "LET" << space << push; 02000 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02001 if(!first) os << push << "," << pop << endl; 02002 else first = false; 02003 if(i->arity() == 3) { 02004 os << (*i)[0] << ":" << space << push << (*i)[1] 02005 << space << "= " << push << nodag << (*i)[2] << pop << pop; 02006 } else { 02007 os << (*i)[0]; 02008 Type tp((*i)[0].lookupType()); 02009 if(!tp.isNull()) os << ":" << space << push << tp.getExpr(); 02010 else os << push; 02011 os << space << "= " << push << nodag << (*i)[1] << pop << pop; 02012 } 02013 } 02014 os << pop << endl << "IN" << space << push << e[1] << push << ")"; 02015 */ 02016 os << "LET not supported in Simplify\n"; 02017 break; 02018 02019 } 02020 case BOUND_VAR: 02021 // os << e.getName()+"_"+e.getUid(); // by yeting for a neat output 02022 os << e.getName(); 02023 break; 02024 case SKOLEM_VAR: 02025 os << "SKOLEM_" + int2string((int)e.getIndex()); 02026 break; 02027 case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory 02028 /* DebugAssert(e.arity() > 0, "TheoryCore::print(): " 02029 "Proof rule application must have at " 02030 "least one argument (rule name):\n "+e.toString()); 02031 os << e[0]; 02032 if(e.arity() > 1) { // Print the arguments 02033 os << push << "(" << push; 02034 bool first(true); 02035 for(int i=1; i<e.arity(); i++) { 02036 if(first) first=false; 02037 else os << push << "," << pop << space; 02038 os << e[i]; 02039 } 02040 os << push << ")"; 02041 }*/ 02042 02043 os << "PR_APPLY not supported in Simplify\n"; 02044 break; 02045 case RAW_LIST: { 02046 /* os << "[" << push; 02047 bool firstTime(true); 02048 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02049 if(firstTime) firstTime = false; 02050 else os << push << "," << pop << space; 02051 os << *i; 02052 } 02053 os << push << "]";*/ 02054 os << "RAW_LIST not supported in Simplify\n"; 02055 break; 02056 } 02057 case PF_HOLE: // FIXME: implement this (now fall through to default) 02058 default: 02059 // Print the top node in the default LISP format, continue with 02060 // pretty-printing for children. 02061 e.print(os); 02062 } 02063 break; // end of case simplify_LANG 02064 02065 case TPTP_LANG: { 02066 static int axiom_counter =0; 02067 switch(e.getKind()) { 02068 case TRUE_EXPR: os << "$true"; break; 02069 case FALSE_EXPR: os << "$false"; break; 02070 case TYPE: 02071 break; 02072 if(e.arity() == 0) os << "TYPE"; 02073 else if(e.arity() == 1) { 02074 for (int i=0; i < e[0].arity(); ++i) { 02075 if (i != 0) os << endl; 02076 os << e[0][i] << ": TYPE;"; 02077 } 02078 } 02079 else if(e.arity() == 2) 02080 os << e[0] << ":" << push << " TYPE = " << e[1] << push << ";"; 02081 else e.printAST(os); 02082 break; 02083 case ID: 02084 if(e.arity() == 1 && e[0].isString()) os << e[0].getString(); 02085 else e.print(os); 02086 break; 02087 case CONST: 02088 if(e.arity() == 2) { 02089 string ename = to_lower(e[0].toString()); 02090 os << "tff(" << ename << "_type, type,\n " << ename; 02091 os << ": " << e[1] << "). \n"; 02092 } 02093 else { 02094 os << "ERROR: CONST's arity > 2"; 02095 } 02096 break; 02097 02098 case SUBTYPE: 02099 break; 02100 case TYPEDEF: { 02101 break; 02102 } 02103 case EQ: 02104 os << e[0] << " = " << e[1]; 02105 break; 02106 02107 case DISTINCT: { 02108 int i=0, iend=e.arity(); 02109 os << "$distinct(" ; 02110 os << e[i] ; 02111 i++; 02112 for(; i!=iend; ++i) os << ", " << e[i] ; 02113 os << ")"; 02114 break; 02115 } 02116 02117 case NOT: 02118 os << "~(" << e[0]<<")" ; 02119 break; 02120 02121 case AND: { 02122 int i=0, iend=e.arity(); 02123 if(iend == 1) { 02124 os << e[i]; 02125 } 02126 02127 else if(iend > 1) { 02128 for(i=0 ; i < iend-1; i++) { 02129 os << "(" << e[i] << " \n& " ; 02130 } 02131 os << e[iend-1]; 02132 for(i=0 ; i < iend-1; i++) { 02133 os << ")"; 02134 } 02135 } 02136 else{ 02137 os <<"ERROR:AND has less than 1 parameter\n"; 02138 } 02139 break; 02140 } 02141 case OR: { 02142 int i=0, iend=e.arity(); 02143 if(iend == 1) { 02144 os << e[i]; 02145 } 02146 02147 else if(iend > 1) { 02148 for(i=0 ; i < iend-1; i++) { 02149 os << "(" << e[i] << " \n| " ; 02150 } 02151 os << e[iend-1]; 02152 for(i=0 ; i < iend-1; i++) { 02153 os << ")"; 02154 } 02155 } 02156 else{ 02157 os <<"ERROR:OR has less than 1 parameter\n"; 02158 } 02159 break; 02160 } 02161 case ITE: 02162 os<<"ERROR:ITE:not supported in TPTP yet\n"; 02163 /* os << "(AND (IMPLIES "<< e[0] << " " << e[1]<<")" 02164 << "(IMPLIES (NOT " <<e[0] << ")" << e[2] <<"))"; 02165 */ 02166 break; 02167 case IFF: 02168 if(e.arity() == 2) 02169 os << "(" << e[0] << " \n<=> " << e[1] << ")" ; 02170 else 02171 e.print(os); 02172 break; 02173 case IMPLIES: 02174 os << "(" << e[0] << " \n=> " << e[1] << ")" ; 02175 break; 02176 // Commands 02177 case ASSERT: 02178 os << "tff(" << axiom_counter++ << ", axiom, \n " <<e[0] << ").\n"; 02179 02180 break; 02181 case TRANSFORM: 02182 os << "ERROR:TRANSFORM:not supported in TPTP " << push << e[0] << push << "\n"; 02183 break; 02184 case QUERY: 02185 if(getFlags()["negate-query"].getBool() == true){ 02186 if (e[0].isNot()){ 02187 os << "tff(" << axiom_counter++ << ", conjecture, \n " <<e[0][0] << ").\n"; 02188 } 02189 else{ 02190 os << "tff(" << axiom_counter++ << ", conjecture, \n ~(" << e[0] << ")).\n"; 02191 } 02192 } 02193 else{ 02194 os << "tff(" << axiom_counter++ << ", conjecture, \n " <<e[0] << ").\n"; 02195 } 02196 break; 02197 case WHERE: 02198 os << "ERROR:WHERE:not supported in TPTP\n"; 02199 break; 02200 case ASSERTIONS: 02201 os << "ERROR:ASSERTIONS:not supported in TPTP\n"; 02202 break; 02203 case ASSUMPTIONS: 02204 os << "ERROR:ASSUMPTIONS:not supported in TPTP\n"; 02205 break; 02206 case COUNTEREXAMPLE: 02207 os << "ERROR:COUNTEREXAMPLE:not supported in TPTP\n"; 02208 break; 02209 case COUNTERMODEL: 02210 os << "ERROR:COUNTERMODEL:not supported in TPTP\n"; 02211 break; 02212 case PUSH: 02213 case POP: 02214 case POPTO: 02215 case PUSH_SCOPE: 02216 case POP_SCOPE: 02217 case POPTO_SCOPE: 02218 case RESET: 02219 os << "ERROR:PUSH and POP:not supported in TPTP\n"; 02220 break; 02221 // case CONSTDEF: 02222 case LETDECL: 02223 os << "LETDECL not supported in Simplify\n"; 02224 break; 02225 case LET: { 02226 bool first(true); 02227 os << " := [" ; 02228 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02229 if(!first) os << " , " ; 02230 else first = false; 02231 if(i->arity() == 3) { 02232 os << (*i)[0] << ":" << (*i)[1] 02233 << " ERROR= " << nodag << (*i)[2] ; 02234 } else { 02235 os << (*i)[0]; 02236 os << " := " << nodag << (*i)[1] ; 02237 } 02238 os <<endl; 02239 } 02240 os << "] : " << endl << "(" << e[1] << ")"; 02241 break; 02242 02243 } 02244 02245 case BOUND_VAR:{ 02246 // os << e.getName()+"_"+e.getUid() ; // by yeting 02247 os<< to_upper(e.getName()); 02248 break; 02249 } 02250 case SKOLEM_VAR: 02251 os << "SKOLEM_VAR is not supported in TPTP\n"; 02252 break; 02253 02254 case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory 02255 /* DebugAssert(e.arity() > 0, "TheoryCore::print(): " 02256 "Proof rule application must have at " 02257 "least one argument (rule name):\n "+e.toString()); 02258 os << e[0]; 02259 if(e.arity() > 1) { // Print the arguments 02260 os << push << "(" << push; 02261 bool first(true); 02262 for(int i=1; i<e.arity(); i++) { 02263 if(first) first=false; 02264 else os << push << "," << pop << space; 02265 os << e[i]; 02266 } 02267 os << push << ")"; 02268 }*/ 02269 02270 os << "PR_APPLY not supported in TPTP\n"; 02271 break; 02272 case RAW_LIST: { 02273 /* os << "[" << push; 02274 bool firstTime(true); 02275 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02276 if(firstTime) firstTime = false; 02277 else os << push << "," << pop << space; 02278 os << *i; 02279 } 02280 os << push << "]";*/ 02281 os << "RAW_LIST not supported in TPTP\n"; 02282 break; 02283 } 02284 case PF_HOLE: 02285 os << "PF_HOLE not supported in TPTP\n"; 02286 break; 02287 case UCONST: 02288 {string name = e.getName(); 02289 if(name.length() >= 5){ 02290 if ('C' == name[0] && 'V' == name[1] && 'C' == name[2] && '_' == name[3] && isdigit(name[4])){ 02291 os << to_upper(name); 02292 } 02293 else { 02294 os << to_lower(name); 02295 } 02296 } 02297 else { 02298 os<<to_lower(name); 02299 } 02300 // 02301 // e.print(os); break; 02302 break; 02303 } 02304 case STRING_EXPR: 02305 os <<"ERROR:STRING_EXPR is not suppoerted in TPTP\n"; 02306 e.print(os); break; 02307 case BOOLEAN: 02308 os << "$o"; 02309 break; 02310 default: 02311 // Print the top node in the default LISP format, continue with 02312 // pretty-printing for children. 02313 os<<"unknown "; 02314 // cout<<e.toString(PRESENTATION_LANG)<<endl; 02315 // cout<<getEM()->getKindName(e.getKind())<<endl; 02316 e.print(os); 02317 } 02318 break; // end of case TPTP_LANG 02319 } 02320 02321 02322 case PRESENTATION_LANG: 02323 switch(e.getKind()) { 02324 case TRUE_EXPR: 02325 os << "TRUE"; 02326 break; 02327 case FALSE_EXPR: 02328 os << "FALSE"; 02329 break; 02330 case BOOLEAN: 02331 os << "BOOLEAN"; 02332 break; 02333 case UCONST: 02334 case STRING_EXPR: 02335 e.print(os); break; 02336 case TYPE: 02337 if(e.arity() == 0) os << "TYPE"; 02338 else if(e.arity() == 1) { 02339 for (int i=0; i < e[0].arity(); ++i) { 02340 if (i != 0) os << endl; 02341 os << e[0][i] << ": TYPE;"; 02342 } 02343 } 02344 else if(e.arity() == 2) 02345 os << e[0] << ":" << push << " TYPE = " << e[1] << push << ";"; 02346 else e.printAST(os); 02347 break; 02348 case ID: 02349 if(e.arity() == 1 && e[0].isString()) os << e[0].getString(); 02350 else e.printAST(os); 02351 break; 02352 case CONST: 02353 if(e.arity() == 2) { 02354 if(e[0].getKind() == RAW_LIST) { 02355 bool first(true); 02356 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02357 if(first) first = false; 02358 else os << push << "," << pop << space; 02359 os << (*i); 02360 } 02361 } 02362 else 02363 os << e[0]; 02364 os << ":" << push << space << e[1] << push << ";"; 02365 } else if(e.arity() == 3) 02366 os << e[0] << ":" << push << space << e[1] 02367 << space << "=" << space << push << e[2] << push << ";"; 02368 else 02369 e.printAST(os); 02370 break; 02371 case SUBTYPE: 02372 os << "SUBTYPE(" << push << e[0] << push << ")"; 02373 break; 02374 case TYPEDEF: { 02375 // This is used when dumping declarations to file. Print just 02376 // the name of the type, unless it's a messed-up expression. 02377 if(e.arity() != 2) e.printAST(os); 02378 else if(e[0].isString()) os << e[0].getString(); 02379 else e[0].print(os); 02380 break; 02381 } 02382 case EQ: 02383 // When a separator starts with a space (like " = "), add the 02384 // leading space with 'space' modifier. If this separator goes 02385 // to the next line, the leading spaces must be eaten up to get 02386 // the indentation right; 'space' will tell the indentation 02387 // engine that it is a space that can be eaten. A space in a 02388 // string (like " ") will never be eaten. 02389 os << "(" << push << e[0] << space << "= " << e[1] << push << ")"; 02390 break; 02391 case DISTINCT: { 02392 os << "DISTINCT(" << push; 02393 bool first(true); 02394 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02395 if (!first) os << push << "," << pop << space; 02396 else first = false; 02397 os << (*i); 02398 } 02399 os << push << ")"; 02400 } 02401 break; 02402 case NOT: os << "NOT " << e[0]; break; 02403 case AND: { 02404 int i=0, iend=e.arity(); 02405 os << "(" << push; 02406 if(i!=iend) { os << e[i]; ++i; } 02407 for(; i!=iend; ++i) os << space << "AND " << e[i]; 02408 os << push << ")"; 02409 } 02410 break; 02411 case OR: { 02412 int i=0, iend=e.arity(); 02413 os << "(" << push; 02414 if(i!=iend) { os << e[i]; ++i; } 02415 for(; i!=iend; ++i) os << space << "OR " << e[i]; 02416 os << push << ")"; 02417 } 02418 break; 02419 case XOR: { 02420 int i=0, iend=e.arity(); 02421 os << "(" << push; 02422 if(i!=iend) { os << e[i]; ++i; } 02423 for(; i!=iend; ++i) os << space << "XOR " << e[i]; 02424 os << push << ")"; 02425 } 02426 break; 02427 case ITE: 02428 os << push << "IF " << push << e[0] << popSave 02429 << space << "THEN " << pushRestore << e[1] << popSave 02430 << space << "ELSE " << pushRestore << e[2] << pop 02431 << space << "ENDIF"; 02432 break; 02433 case IFF: 02434 if(e.arity() == 2) 02435 os << "(" << push << e[0] << space << "<=> " << e[1] << push << ")"; 02436 else 02437 e.printAST(os); 02438 break; 02439 case IMPLIES: 02440 os << "(" << push << e[0] << space << "=> " << e[1] << push << ")"; 02441 break; 02442 // Commands 02443 case ASSERT: 02444 os << "ASSERT " << push << e[0] << push << ";"; 02445 break; 02446 case TRANSFORM: 02447 os << "TRANSFORM " << push << e[0] << push << ";"; 02448 break; 02449 case QUERY: 02450 os << "QUERY " << push << e[0] << push << ";"; 02451 break; 02452 case WHERE: 02453 os << "WHERE;"; 02454 break; 02455 case ASSERTIONS: 02456 os << "ASSERTIONS;"; 02457 break; 02458 case ASSUMPTIONS: 02459 os << "ASSUMPTIONS;"; 02460 break; 02461 case COUNTEREXAMPLE: 02462 os << "COUNTEREXAMPLE;"; 02463 break; 02464 case COUNTERMODEL: 02465 os << "COUNTERMODEL;"; 02466 break; 02467 case PUSH: 02468 if(e.arity()==0) 02469 os << "PUSH;"; 02470 else 02471 os << "PUSH" << space << e[0] << push << ";"; 02472 break; 02473 case POP: 02474 if(e.arity()==0) 02475 os << "POP;"; 02476 else 02477 os << "POP" << space << e[0] << push << ";"; 02478 break; 02479 case POPTO: 02480 os << "POPTO" << space << e[0] << push << ";"; break; 02481 case PUSH_SCOPE: 02482 if(e.arity()==0) 02483 os << "PUSH_SCOPE;"; 02484 else 02485 os << "PUSH_SCOPE" << space << e[0] << push << ";"; 02486 break; 02487 case POP_SCOPE: 02488 if(e.arity()==0) 02489 os << "POP_SCOPE;"; 02490 else 02491 os << "POP_SCOPE" << space << e[0] << push << ";"; 02492 break; 02493 case POPTO_SCOPE: 02494 os << "POPTO_SCOPE" << space << e[0] << push << ";"; break; 02495 case RESET: 02496 os << "RESET;"; 02497 break; 02498 case LETDECL: 02499 if(e.arity() == 2) os << e[1]; 02500 else e.printAST(os); 02501 break; 02502 case LET: { 02503 // (LET (LETDECLS (LETDECL var [ type ] val) .... ) body) 02504 bool first(true); 02505 os << "(" << push << "LET" << space << push; 02506 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02507 if(!first) os << push << "," << pop << endl; 02508 else first = false; 02509 if(i->arity() == 3) { 02510 os << (*i)[0] << ":" << space << push << (*i)[1] 02511 << space << "= " << push << nodag << (*i)[2] << pop << pop; 02512 } else { 02513 os << (*i)[0]; 02514 Type tp((*i)[0].lookupType()); 02515 if(!tp.isNull()) os << ":" << space << push << tp.getExpr(); 02516 else os << push; 02517 os << space << "= " << push << nodag << (*i)[1] << pop << pop; 02518 } 02519 } 02520 os << pop << endl << "IN" << space << push << e[1] << push << ")"; 02521 break; 02522 } 02523 case BOUND_VAR: 02524 // os << e.getName()+"_"+e.getUid(); 02525 02526 //by yeting, as requested by Sascha Boehme for proofs 02527 if(getFlags()["print-var-type"].getBool()) { 02528 os << e.getName() << "(" << e.getType() << ")"; 02529 } 02530 else { 02531 os << e.getName(); //for better support of proof translation yeting 02532 } 02533 break; 02534 case SKOLEM_VAR: 02535 os << "SKOLEM_" + int2string((int)e.getIndex()); 02536 break; 02537 case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory 02538 DebugAssert(e.arity() > 0, "TheoryCore::print(): " 02539 "Proof rule application must have at " 02540 "least one argument (rule name):\n "+e.toString()); 02541 // os << e[0]; by yeting 02542 os << e[0] << "\n" ; 02543 if(e.arity() > 1) { // Print the arguments 02544 os << push << "(" << push; 02545 bool first(true); 02546 for(int i=1; i<e.arity(); i++) { 02547 if(first) first=false; 02548 else os << push << "," << pop << space; 02549 // os << e[i]; by yeting 02550 os << e[i] << "\n"; 02551 } 02552 os << push << ")"; 02553 } 02554 break; 02555 case RAW_LIST: { 02556 os << "[" << push; 02557 bool firstTime(true); 02558 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02559 if(firstTime) firstTime = false; 02560 else os << push << "," << pop << space; 02561 os << *i; 02562 } 02563 os << push << "]"; 02564 break; 02565 } 02566 case ANY_TYPE: 02567 os << "ANY_TYPE"; 02568 break; 02569 case ARITH_VAR_ORDER: { 02570 os << "ARITH_VAR_ORDER(" << push; 02571 bool firstTime(true); 02572 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02573 if(firstTime) firstTime = false; 02574 else os << push << "," << pop << space; 02575 os << *i; 02576 } 02577 os << push << ");"; 02578 break; 02579 } 02580 case PF_HOLE: // FIXME: implement this (now fall through to default) 02581 default: 02582 // Print the top node in the default LISP format, continue with 02583 // pretty-printing for children. 02584 e.printAST(os); 02585 } 02586 break; // end of case PRESENTATION_LANG 02587 case SMTLIB_LANG: 02588 switch(e.getKind()) { 02589 case TRUE_EXPR: os << "true"; break; 02590 case FALSE_EXPR: os << "false"; break; 02591 case UCONST: os << d_translator->fixConstName(e.getName()); break; 02592 case BOOLEAN: e.printAST(os); break; 02593 case STRING_EXPR: e.print(os); break; 02594 case TYPE: 02595 if (e.arity() == 1) { 02596 os << " :extrasorts ("; 02597 for (int i=0; i < e[0].arity(); ++i) { 02598 if (i != 0) os << push << space; 02599 os << push << e[0][i]; 02600 } 02601 os << push << ")"; 02602 } 02603 else if (e.arity() == 2) { 02604 break; 02605 } 02606 else { 02607 throw SmtlibException("TheoryCore::print: SMTLIB: Unexpected TYPE expression"); 02608 } 02609 break; 02610 case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs 02611 if(e.arity() == 1 && e[0].isString()) os << e[0].getString(); 02612 else e.printAST(os); 02613 break; 02614 case CONST: 02615 if(e.arity() == 2) { 02616 if (e[1].getKind() == BOOLEAN) { 02617 os << " :extrapreds ((" << push << d_translator->fixConstName(e[0][0].getString()) 02618 << push << "))"; 02619 } 02620 else if (e[1].getKind() == ARROW && e[1][e[1].arity()-1].getKind() == BOOLEAN) { 02621 os << " :extrapreds ((" << push << d_translator->fixConstName(e[0][0].getString()) 02622 << space << nodag << e[1] << push << "))"; 02623 } 02624 else { 02625 os << " :extrafuns ((" << push << d_translator->fixConstName(e[0][0].getString()) 02626 << space << nodag << e[1] << push << "))"; 02627 } 02628 } 02629 else if (e.arity() == 0) e.printAST(os); 02630 else { 02631 throw SmtlibException("TheoryCore::print: SMTLIB: CONST not implemented"); 02632 } 02633 break; 02634 case SUBTYPE: 02635 throw SmtlibException("TheoryCore::print: SMTLIB: SUBTYPE not implemented"); 02636 break; 02637 case TYPEDEF: { 02638 throw SmtlibException("TheoryCore::print: SMTLIB: TYPEDEF not implemented"); 02639 break; 02640 } 02641 case EQ: 02642 os << "(" << push << "=" << space << e[0] 02643 << space << e[1] << push << ")"; 02644 break; 02645 case DISTINCT: { 02646 int i=0, iend=e.arity(); 02647 os << "(" << push << "distinct"; 02648 for(; i!=iend; ++i) os << space << e[i]; 02649 os << push << ")"; 02650 break; 02651 } 02652 case NOT: 02653 os << "(" << push << "not" << space << e[0] << push << ")"; 02654 break; 02655 case AND: { 02656 int i=0, iend=e.arity(); 02657 os << "(" << push << "and"; 02658 for(; i!=iend; ++i) os << space << e[i]; 02659 os << push << ")"; 02660 break; 02661 } 02662 case OR: { 02663 int i=0, iend=e.arity(); 02664 os << "(" << push << "or"; 02665 for(; i!=iend; ++i) os << space << e[i]; 02666 os << push << ")"; 02667 break; 02668 } 02669 case XOR: { 02670 int i=0, iend=e.arity(); 02671 os << "(" << push << "xor"; 02672 for(; i!=iend; ++i) os << space << e[i]; 02673 os << push << ")"; 02674 break; 02675 } 02676 case ITE: 02677 os << "(" << push; 02678 if (e.getType().isBool()) os << "if_then_else"; 02679 else os << "ite"; 02680 os << space << e[0] 02681 << space << e[1] << space << e[2] << push << ")"; 02682 break; 02683 case IFF: 02684 os << "(" << push << "iff" << space 02685 << e[0] << space << e[1] << push << ")"; 02686 break; 02687 case IMPLIES: 02688 os << "(" << push << "implies" << space 02689 << e[0] << space << e[1] << push << ")"; 02690 break; 02691 // Commands 02692 case ASSERT: 02693 os << " :assumption" << space << push << e[0]; 02694 break; 02695 case TRANSFORM: 02696 throw SmtlibException("TheoryCore::print: SMTLIB: TRANSFORM not implemented"); 02697 os << "(" << push << "TRANSFORM" << space << e[0] << push << ")"; 02698 break; 02699 case QUERY: 02700 os << " :formula" << space << push << e[0]; 02701 break; 02702 case LETDECL: 02703 // throw SmtlibException("TheoryCore::print: SMTLIB: LETDECL not implemented"); 02704 if(e.arity() == 2) os << e[1]; 02705 else e.printAST(os); 02706 break; 02707 case LET: { 02708 // (LET ((var [ type ] val) .... ) body) 02709 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02710 os << "(" << push; 02711 Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType()); 02712 DebugAssert(!tp.isNull(), "Unexpected Null type"); 02713 if (tp.getExpr().getKind() == BOOLEAN) { 02714 os << "flet" << space << "(" << push; 02715 } 02716 else { 02717 os << "let" << space << "(" << push; 02718 } 02719 if(i->arity() == 3) { 02720 os << (*i)[0] << space << nodag << (*i)[2]; 02721 } else { 02722 os << (*i)[0] << space << nodag << (*i)[1]; 02723 } 02724 os << push << ")" << pop << pop << space; 02725 } 02726 os << e[1] << push; 02727 for (int j = 0; j < e[0].arity(); ++j) 02728 os << ")"; 02729 break; 02730 } 02731 case BOUND_VAR: 02732 // os << push << "?" << e.getName()+"_"+e.getUid(); 02733 os << push << "?" << e.getName(); //to better support for proof translation 02734 break; 02735 case SKOLEM_VAR: 02736 os << push << "SKOLEM_" + int2string((int)e.getIndex()); 02737 break; 02738 case PF_APPLY: {// FIXME: this will eventually go to the "symsim" theory 02739 throw SmtlibException("TheoryCore::print: SMTLIB: PF_APPLY not implemented"); 02740 break; 02741 } 02742 case RAW_LIST: { 02743 os << "(" << push; 02744 bool firstTime(true); 02745 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02746 if(firstTime) firstTime = false; 02747 else os << space; 02748 os << *i; 02749 } 02750 os << push << ")"; 02751 break; 02752 } 02753 case ANY_TYPE: 02754 os << "ANY_TYPE"; 02755 break; 02756 case WHERE: 02757 os << " :cvc_command \"WHERE\""; 02758 break; 02759 case ASSERTIONS: 02760 os << " :cvc_command \"ASSERTIONS\""; 02761 break; 02762 case ASSUMPTIONS: 02763 os << " :cvc_command \"ASSUMPTIONS\""; 02764 break; 02765 case COUNTEREXAMPLE: 02766 os << " :cvc_command \"COUNTEREXAMPLE\""; 02767 break; 02768 case COUNTERMODEL: 02769 os << " :cvc_command \"COUNTERMODEL\""; 02770 break; 02771 case PUSH: 02772 os << " :cvc_command" << space; 02773 if(e.arity()==0) 02774 os << "\"PUSH\""; 02775 else 02776 os << "\"PUSH" << space << e[0] << push << "\""; 02777 break; 02778 case POP: 02779 os << " :cvc_command" << space; 02780 if(e.arity()==0) 02781 os << "\"POP\""; 02782 else 02783 os << "\"POP" << space << e[0] << push << "\""; 02784 break; 02785 case POPTO: 02786 os << " :cvc_command" << space; 02787 os << "\"POPTO" << space << e[0] << push << "\""; break; 02788 case PUSH_SCOPE: 02789 os << " :cvc_command" << space; 02790 if(e.arity()==0) 02791 os << "\"PUSH_SCOPE\""; 02792 else 02793 os << "\"PUSH_SCOPE" << space << e[0] << push << "\""; 02794 break; 02795 case POP_SCOPE: 02796 os << " :cvc_command" << space; 02797 if(e.arity()==0) 02798 os << "\"POP_SCOPE\""; 02799 else 02800 os << "\"POP_SCOPE" << space << e[0] << push << "\""; 02801 break; 02802 case POPTO_SCOPE: 02803 os << " :cvc_command" << space; 02804 os << "\"POPTO_SCOPE" << space << e[0] << push << "\""; break; 02805 break; 02806 case RESET: 02807 os << " :cvc_command" << space; 02808 os << "\"RESET\""; break; 02809 break; 02810 case PF_HOLE: // FIXME: implement this (now fall through to default) 02811 default: 02812 throw SmtlibException("TheoryCore::print: SMTLIB_LANG: Unexpected expression: " 02813 +getEM()->getKindName(e.getKind())); 02814 } 02815 break; // end of case SMTLIB_LANG 02816 case LISP_LANG: 02817 switch(e.getKind()) { 02818 case TRUE_EXPR: 02819 case FALSE_EXPR: 02820 case UCONST: 02821 e.print(os); break; 02822 case TYPE: 02823 if(e.arity() == 0) os << "TYPE"; 02824 else if(e.arity() == 1) 02825 os << "(" << push << "TYPE" << space << e[0] << push << ")"; 02826 else if(e.arity() == 2) 02827 os << "(" << push << "TYPE" << space << e[0] 02828 << space << e[1] << push << ")"; 02829 else e.printAST(os); 02830 break; 02831 case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs 02832 if(e.arity() == 1 && e[0].isString()) os << e[0].getString(); 02833 else e.printAST(os); 02834 break; 02835 case CONST: 02836 if(e.arity() == 2) 02837 os << "(" << push << "CONST" << space << e[0] 02838 << space << e[1] << push << ")"; 02839 else 02840 e.printAST(os); 02841 break; 02842 case SUBTYPE: 02843 os << "SUBTYPE(" << push << e[0] << push << ")"; 02844 break; 02845 case TYPEDEF: { 02846 // This is used when dumping declarations to file. Print just 02847 // the name of the type, unless it's a messed-up expression. 02848 if(e.arity() != 2) e.printAST(os); 02849 else if(e[0].isString()) os << e[0].getString(); 02850 else e[0].print(os); 02851 break; 02852 } 02853 case EQ: 02854 // When a separator starts with a space (like " = "), add the 02855 // leading space with 'space' modifier. If this separator goes 02856 // to the next line, the leading spaces must be eaten up to get 02857 // the indentation right; 'space' will tell the indentation 02858 // engine that it is a space that can be eaten. A space in a 02859 // string (like " ") will never be eaten. 02860 os << "(" << push << "=" << space << e[0] 02861 << space << e[1] << push << ")"; 02862 break; 02863 case NOT: 02864 os << "(" << push << "NOT" << space << e[0] << push << ")"; 02865 break; 02866 case AND: { 02867 int i=0, iend=e.arity(); 02868 os << "(" << push << "AND"; 02869 for(; i!=iend; ++i) os << space << e[i]; 02870 os << push << ")"; 02871 } 02872 break; 02873 case OR: { 02874 int i=0, iend=e.arity(); 02875 os << "(" << push << "OR"; 02876 for(; i!=iend; ++i) os << space << e[i] << space; 02877 os << push << ")"; 02878 } 02879 break; 02880 case ITE: 02881 os << "(" << push << "IF" << space << e[0] 02882 << space << e[1] << space << e[2] << push << ")"; 02883 break; 02884 case IFF: 02885 os << "(" << push << "<=>" << space 02886 << e[0] << space << e[1] << push << ")"; 02887 break; 02888 case IMPLIES: 02889 os << "(" << push << "=>" << space 02890 << e[0] << space << e[1] << push << ")"; 02891 break; 02892 // Commands 02893 case ASSERT: 02894 os << "(" << push << "ASSERT" << space << e[0] << push << ")"; 02895 break; 02896 case TRANSFORM: 02897 os << "(" << push << "TRANSFORM" << space << e[0] << push << ")"; 02898 break; 02899 case QUERY: 02900 os << "(" << push << "QUERY" << space << e[0] << push << ")"; 02901 break; 02902 case PUSH: 02903 os << "(PUSH)"; break; 02904 case POP: 02905 os << "(POP)"; break; 02906 case POPTO: 02907 os << "(" << push << "POPTO" << space << e[0] << push << ")"; break; 02908 case RESET: 02909 os << "(" << push << "RESET" << push << ")"; break; 02910 case LETDECL: 02911 if(e.arity() == 2) os << e[1]; 02912 else if(e.arity()==3) // It's a declaration of a named Expr 02913 os << e[0] << push << ":" << space << push << e[1] << push << " =" 02914 << pop << pop << space << e[2]; 02915 else e.printAST(os); 02916 break; 02917 case LET: { 02918 // (LET ((var [ type ] val) .... ) body) 02919 bool first(true); 02920 os << "(" << push << "LET" << space << "(" << push; 02921 for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) { 02922 if(!first) os << space; 02923 else first = false; 02924 os << "(" << push; 02925 if(i->arity() == 3) { 02926 os << (*i)[0] << space << (*i)[1] 02927 << space << nodag << (*i)[2]; 02928 } else { 02929 os << (*i)[0]; 02930 Type tp((*i)[0].lookupType()); 02931 if(!tp.isNull()) os << space << tp.getExpr(); 02932 os << space << nodag << (*i)[1]; 02933 } 02934 os << push << ")" << pop << pop; 02935 } 02936 os << push << ")" << pop << pop << space << e[1] << push << ")"; 02937 break; 02938 } 02939 case BOUND_VAR: 02940 // os << e.getName()+"_"+e.getUid(); by yeting 02941 os << e.getName(); 02942 break; 02943 case SKOLEM_VAR: 02944 os << "SKOLEM_" + int2string((int)e.getIndex()); 02945 break; 02946 case PF_APPLY: {// FIXME: this will eventually go to the "symsim" theory 02947 DebugAssert(e.arity() > 0, "TheoryCore::print(): " 02948 "Proof rule application must have at " 02949 "least one argument (rule name):\n "+e.toString()); 02950 os << push << "(" << push; 02951 bool first(true); 02952 for(int i=0; i<e.arity(); i++) { 02953 if(first) first=false; 02954 else os << space; 02955 os << e[i]; 02956 } 02957 os << push << ")"; 02958 break; 02959 } 02960 case RAW_LIST: { 02961 os << "(" << push; 02962 bool firstTime(true); 02963 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 02964 if(firstTime) firstTime = false; 02965 else os << space; 02966 os << *i; 02967 } 02968 os << push << ")"; 02969 break; 02970 } 02971 case ANY_TYPE: 02972 os << "ANY_TYPE"; 02973 break; 02974 case PF_HOLE: // FIXME: implement this (now fall through to default) 02975 default: 02976 // Print the top node in the default LISP format, continue with 02977 // pretty-printing for children. 02978 e.printAST(os); 02979 } 02980 break; // end of case LISP_LANGUAGE 02981 default: 02982 // Print the top node in the default LISP format, continue with 02983 // pretty-printing for children. 02984 e.printAST(os); 02985 } 02986 return os; 02987 } 02988 02989 bool TheoryCore::refineCounterExample(Theorem& thm) 02990 { 02991 // Theory 0 is TheoryCore, skip it 02992 for(int i = 1; i<getNumTheories(); i++) { 02993 if(d_theories[i] != this) 02994 d_theories[i]->refineCounterExample(); 02995 if(inconsistent()) { 02996 thm = inconsistentThm(); 02997 return false; 02998 } 02999 } 03000 return true; 03001 } 03002 03003 void TheoryCore::refineCounterExample() 03004 { 03005 // Theory 0 is TheoryCore, skip it 03006 for(int i = 1; i<getNumTheories(); i++) { 03007 if(d_theories[i] != this) 03008 d_theories[i]->refineCounterExample(); 03009 if(inconsistent()) { 03010 vector<Expr> assump; 03011 inconsistentThm().getLeafAssumptions(assump); 03012 Expr a = Expr(RAW_LIST, assump, d_em); 03013 throw EvalException("Theory["+d_theories[i]->getName() 03014 +"]: Model Creation failed due " 03015 "to the following assumptions:\n\n" 03016 +a.toString() 03017 +"\n\nYou might be using an incomplete logical fragment."); 03018 } 03019 } 03020 } 03021 03022 03023 void TheoryCore::computeModelBasic(const vector<Expr>& v) { 03024 for(vector<Expr>::const_iterator i=v.begin(), iend=v.end(); i!=iend; ++i) { 03025 TRACE("model", "Model var "+i->toString()+" = ", find(*i).getRHS(), ""); 03026 DebugAssert((*i).getType().isBool(), "TheoryCore::computeModel: *i = " 03027 +(*i).toString()); 03028 Expr val = find(*i).getRHS(); 03029 if(!val.isBoolConst()) val = d_em->trueExpr(); 03030 assignValue(*i, val); 03031 } 03032 } 03033 03034 03035 /*****************************************************************************/ 03036 /* 03037 * User-level API methods 03038 */ 03039 /*****************************************************************************/ 03040 03041 03042 void TheoryCore::addFact(const Theorem& e) 03043 { 03044 //<<<<<<< theory_core_sat.cpp 03045 // cout<<"theory_core_sat.cpp asserted fact:"<<e<<endl; 03046 // IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 03047 // TRACE("addFact", indentStr, "Assert: ", e.getExpr().toString(PRESENTATION_LANG)); 03048 //======= 03049 IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');) 03050 TRACE("addFact", indentStr, "Assert: ", e.getExpr().toString(PRESENTATION_LANG)); 03051 //>>>>>>> 1.7 03052 DebugAssert(!d_inAddFact, "Recursive call to addFact() is not allowed"); 03053 DebugAssert(d_queue.empty(), "addFact[start]: Expected empty queue"); 03054 // DebugAssert(d_queueSE.empty(), "addFact[start]: Expected empty queue"); 03055 DebugAssert(d_update_thms.empty() && d_update_data.empty(), 03056 "addFact[start]: Expected empty update list"); 03057 ScopeWatcher sw(&d_inAddFact); 03058 03059 if(!d_inconsistent && !outOfResources()) { 03060 getResource(); 03061 d_queue.push(e); 03062 03063 // cout<<"queue pushed" <<e<<endl; 03064 // cout<<"queue pushed id" <<e.getQuantLevel()<<endl; 03065 03066 if (outOfResources()) { 03067 // No more resources: ignore all the remaining facts and fail 03068 // gracefully 03069 setIncomplete("Exhausted user-specified resource"); 03070 } 03071 processFactQueue(); 03072 } 03073 03074 DebugAssert(d_queue.empty(), "addFact[end]: Expected empty queue"); 03075 DebugAssert(d_queueSE.empty(), "addFact[end]: Expected empty queue"); 03076 DebugAssert(d_update_thms.empty() && d_update_data.empty(), 03077 "addFact[end]: Expected empty update list"); 03078 } 03079 03080 03081 bool TheoryCore::checkSATCore() 03082 { 03083 DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue"); 03084 DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue"); 03085 DebugAssert(!d_inCheckSATCore, "Recursive call to checkSATCore is not allowed!"); 03086 ScopeWatcher sw(&d_inCheckSATCore); 03087 IF_DEBUG(debugger.counter("DP checkSAT(fullEffort) calls")++;) 03088 DebugAssert(d_update_thms.empty() && d_update_data.empty(), 03089 "addFact[start]: Expected empty update list"); 03090 03091 bool lemmas = processFactQueue(FULL); 03092 03093 DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue"); 03094 DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue"); 03095 DebugAssert(d_update_thms.empty() && d_update_data.empty(), 03096 "addFact[end]: Expected empty update list"); 03097 03098 return !lemmas; 03099 } 03100 03101 03102 bool TheoryCore::incomplete(vector<string>& reasons) 03103 { 03104 if(d_incomplete.size() > 0) { 03105 for(CDMap<string,bool>::iterator i=d_incomplete.begin(), 03106 iend=d_incomplete.end(); i!=iend; ++i) 03107 reasons.push_back((*i).first); 03108 return true; 03109 } 03110 else 03111 return false; 03112 } 03113 03114 03115 void TheoryCore::registerAtom(const Expr& e, const Theorem& thm) 03116 { 03117 DebugAssert(!e.isEq() || e[0] != e[1], "expected non-reflexive"); 03118 DebugAssert(!e.isRegisteredAtom(), "atom registered more than once"); 03119 // if (e.isQuantifier()) return; 03120 e.setRegisteredAtom(); 03121 if(d_termTheorems.find(e) != d_termTheorems.end()){ 03122 // cout<<"found this before 1 : "<<e<<endl; 03123 } 03124 // cout<<"#1# get into "<<e<<endl; 03125 d_termTheorems[e] = thm; 03126 DebugAssert(e.isAbsAtomicFormula(), "Expected atomic formula"); 03127 ScopeWatcher sw(&d_inRegisterAtom); 03128 Theorem thm2 = simplify(e); 03129 if (thm2.getRHS().isTrue()) { 03130 setFindLiteral(d_commonRules->iffTrueElim(thm2)); 03131 } 03132 else if (thm2.getRHS().isFalse()) { 03133 setFindLiteral(d_commonRules->iffFalseElim(thm2)); 03134 } 03135 else { 03136 //TODO: why does arith need thm2.getRHS() instead of e? 03137 // theoryOf(e)->registerAtom(e); 03138 theoryOf(thm2.getRHS())->registerAtom(thm2.getRHS()); 03139 setupSubFormulas(thm2.getRHS(), e, thm); 03140 } 03141 processFactQueue(LOW); 03142 } 03143 03144 03145 Theorem TheoryCore::getImpliedLiteral(void) 03146 { 03147 Theorem res; 03148 if (d_impliedLiteralsIdx < d_impliedLiterals.size()) { 03149 res = d_impliedLiterals[d_impliedLiteralsIdx]; 03150 d_impliedLiteralsIdx = d_impliedLiteralsIdx + 1; 03151 } 03152 return res; 03153 } 03154 03155 03156 Theorem TheoryCore::getImpliedLiteralByIndex(unsigned index) 03157 { 03158 DebugAssert(index < d_impliedLiterals.size(), "index out of bounds"); 03159 return d_impliedLiterals[index]; 03160 } 03161 03162 03163 Expr TheoryCore::parseExpr(const Expr& e) 03164 { 03165 // check cache 03166 ExprMap<Expr>::iterator iParseCache = d_parseCache.find(e); 03167 if (iParseCache != d_parseCache.end()) { 03168 return (*iParseCache).second; 03169 } 03170 // Remember the current size of the bound variable stack 03171 size_t boundVarSize = d_boundVarStack.size(); 03172 03173 // Compute the kind to determine what to do with the expression 03174 int kind = NULL_KIND; 03175 Expr res; 03176 03177 switch(e.getKind()) { 03178 case ID: { 03179 const Expr c1 = e[0]; 03180 kind = getEM()->getKind(c1.getString()); 03181 if(kind == NULL_KIND) { // It's an identifier; try to resolve it 03182 res = resolveID(e[0].getString()); 03183 if(res.isNull()) 03184 throw ParserException("cannot resolve an identifier: " 03185 +e[0].toString()); 03186 else { 03187 DebugAssert(!e.isApply(), "Unexpected apply function"); 03188 } 03189 } 03190 // Otherwise exit the switch and use DP-specific parsing 03191 break; 03192 } 03193 case RAW_LIST: { 03194 if(e.arity() == 0) 03195 throw ParserException("Empty list is not an expression!"); 03196 const Expr& op = e[0]; 03197 // First, resolve the operator 03198 switch(op.getKind()) { 03199 case ID: { // The operator in the list is ID: is it keyword or variable? 03200 kind = getEM()->getKind(op[0].getString()); 03201 if(kind == NULL_KIND) { 03202 // It's a named function application. Resolve the ID. 03203 res = resolveID(op[0].getString()); 03204 if(res.isNull()){ 03205 // cout<<"stop here: " << e << endl; 03206 // cout<<"stop here op: " << op << endl; 03207 // cout<<"stop here op[0]: " << op[0] << endl; 03208 throw ParserException("cannot resolve an identifier: " 03209 +op[0].toString()); 03210 } 03211 if(e.arity() < 2) 03212 throw ParserException("Bad function application: "+e.toString()); 03213 Expr::iterator i=e.begin(), iend=e.end(); 03214 ++i; 03215 vector<Expr> args; 03216 for(; i!=iend; ++i) args.push_back(parseExpr(*i)); 03217 res = Expr(res.mkOp(), args); 03218 } 03219 // Proceed to DP-specific parsing 03220 break; 03221 } 03222 case RAW_LIST: 03223 // This can only be a lambda expression application. 03224 kind = LAMBDA; 03225 break; 03226 default: 03227 throw ParserException("Bad operator in "+e.toString()); 03228 } 03229 break; // Exit the top-level switch, proceed to DP-specific parsing 03230 } 03231 default: // Can only be a string or a number. 03232 res = e; 03233 } 03234 03235 // DP-specific parsing 03236 if(res.isNull()) { 03237 if (hasTheory(kind)) { 03238 res = theoryOf(kind)->parseExprOp(e); 03239 // Restore the bound variable stack 03240 if (d_boundVarStack.size() > boundVarSize) { 03241 d_parseCache.clear(); 03242 while(d_boundVarStack.size() > boundVarSize) { 03243 pair<string,Expr>& bv = d_boundVarStack.back(); 03244 hash_map<string,Expr>::iterator iBoundVarMap = d_boundVarMap.find(bv.first); 03245 DebugAssert(iBoundVarMap != d_boundVarMap.end(), "Expected bv in map"); 03246 if ((*iBoundVarMap).second.getKind() == RAW_LIST) { 03247 (*iBoundVarMap).second = (*iBoundVarMap).second[1]; 03248 } 03249 else d_boundVarMap.erase(bv.first); 03250 d_boundVarStack.pop_back(); 03251 } 03252 } 03253 } 03254 else { 03255 res = e; 03256 } 03257 } 03258 d_parseCache[e] = res; 03259 if (!getEM()->isTypeKind(res.getOpKind())) res.getType(); 03260 return res; 03261 } 03262 03263 03264 void TheoryCore::assignValue(const Expr& t, const Expr& val) 03265 { 03266 DebugAssert(d_varAssignments.count(t) == 0 03267 || d_varAssignments[t].getRHS() == val, 03268 "TheoryCore::assignValue("+t.toString()+" := "+val.toString() 03269 +")\n variable already has a different value"); 03270 // Check if the assignment theorem can be derived from the find of t 03271 Theorem thm(find(t)); 03272 Expr t2 = thm.getRHS(); 03273 03274 if(t2!=val) { 03275 bool isBool(t2.getType().isBool()); 03276 Expr assump = (isBool)? t2.iffExpr(val) : t2.eqExpr(val); 03277 Theorem assertThm = d_coreSatAPI->addAssumption(assump); 03278 addFact(assertThm); 03279 thm = transitivityRule(thm, assertThm); 03280 } 03281 d_varAssignments[t] = thm; 03282 } 03283 03284 03285 void TheoryCore::assignValue(const Theorem& thm) 03286 { 03287 DebugAssert(thm.isRewrite(), "TheoryCore::assignValue("+thm.toString()+")"); 03288 const Expr& t = thm.getLHS(); 03289 const Expr& val = thm.getRHS(); 03290 DebugAssert(d_varAssignments.count(t) == 0 03291 || d_varAssignments[t].getRHS() == val, 03292 "TheoryCore::assignValue("+thm.getExpr().toString() 03293 +")\n variable already has a different value:\n " 03294 +d_varAssignments[t].getExpr().toString()); 03295 d_varAssignments[t] = thm; 03296 // Check if the assignment theorem can be derived from the find of t 03297 Theorem findThm(find(t)); 03298 const Expr& t2 = findThm.getRHS(); 03299 03300 if(t2!=val) { 03301 Theorem thm2 = transitivityRule(symmetryRule(findThm), thm); 03302 addFact(thm2); 03303 } 03304 } 03305 03306 03307 void TheoryCore::addToVarDB(const Expr& e) 03308 { 03309 TRACE("model", "TheoryCore::addToVarDB(", e, ")"); 03310 d_vars.push_back(e); 03311 } 03312 03313 03314 void TheoryCore::collectBasicVars() 03315 { 03316 TRACE_MSG("model", "collectBasicVars() {"); 03317 // Clear caches 03318 d_varModelMap.clear(); 03319 d_varAssignments.clear(); 03320 d_basicModelVars.clear(); 03321 d_simplifiedModelVars.clear(); 03322 // Current stack of variables to process 03323 vector<Expr> stack(d_vars.begin(), d_vars.end()); 03324 size_t lastSize(0); 03325 while(stack.size() > 0) { 03326 Expr var(stack.back()); 03327 stack.pop_back(); 03328 if(d_varModelMap.count(var) > 0) continue; // Already processed 03329 Theorem findThm(find(var)); 03330 if(findThm.getRHS()!=var) { // Replace var with its find 03331 d_simplifiedModelVars[var] = findThm; 03332 stack.push_back(findThm.getRHS()); 03333 TRACE("model", "collectBasicVars: simplified var: ", findThm.getExpr(), ""); 03334 continue; // Recycle to the beginning of the loop 03335 } 03336 lastSize = stack.size(); 03337 TRACE("model", "getModelTerm(", var, ") {"); 03338 getModelTerm(var, stack); 03339 TRACE("model", "getModelTerm => ", 03340 Expr(RAW_LIST, stack, getEM()), " }"); 03341 if(stack.size() == lastSize) { 03342 // Add a primitive variable 03343 TRACE("model", "collectBasicVars: adding primitive var: ", var, ""); 03344 d_basicModelVars.push_back(var); 03345 if(var.isTerm()) { 03346 Theory* t1 = theoryOf(var); 03347 Theory* t2 = theoryOf(getBaseType(var).getExpr().getKind()); 03348 if(t1 != t2) { 03349 TRACE("model", "collectBasicVars: adding shared var: ", var, ""); 03350 t1->addSharedTerm(var); 03351 t2->addSharedTerm(var); 03352 } 03353 } 03354 } else { // Record the descendants of var 03355 vector<Expr>& kids = d_varModelMap[var]; 03356 for(size_t i=lastSize; i<stack.size(); ++i) { 03357 DebugAssert(stack[i] != var, "Primitive var was pushed on " 03358 "the stack in computeModelTerm(): "+var.toString()); 03359 kids.push_back(stack[i]); 03360 } 03361 TRACE("model", "collectBasicVars: var="+var.toString() 03362 +" maps into vars=", Expr(RAW_LIST, kids, getEM()), ""); 03363 } 03364 } 03365 TRACE_MSG("model", "collectBasicVars() => }"); 03366 } 03367 03368 bool TheoryCore::buildModel(Theorem& thm) 03369 { 03370 size_t numTheories = getNumTheories(); 03371 // Use STL set to prune duplicate variables in theories 03372 vector<set<Expr> > theoryExprs(numTheories+1); 03373 03374 // Sort out model vars by theories 03375 for(size_t j = 0 ; j<d_basicModelVars.size() ; j++) { 03376 const Expr& var = d_basicModelVars[j]; 03377 Theorem findThm(find(var)); 03378 if(findThm.getRHS()!=var) { // Replace var with its find and skip it 03379 TRACE("model", "buildModel: replace var="+var.toString(), " with find(var)=", findThm.getRHS()); 03380 d_simplifiedModelVars[var] = findThm; 03381 continue; 03382 } 03383 03384 Theory *th = theoryOf(getBaseType(var).getExpr().getKind()); 03385 size_t i=0; 03386 for(; i<numTheories && d_theories[i] != th; ++i); 03387 DebugAssert(i<numTheories && d_theories[i] == th, "TheoryCore::buildModel: cannot find the theory [" +th->getName()+"] for the variable: " +var.toString()); 03388 theoryExprs[i].insert(var); 03389 TRACE("model", "buildModel: adding ", var, " to theory "+d_theories[i]->getName()); 03390 } 03391 03392 // Build a model for the basic-type variables 03393 for(int i=0; i<getNumTheories(); i++) { 03394 if(theoryExprs[i].size() > 0) { 03395 TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] {"); 03396 // Copy the corresponding variables into a vector 03397 vector<Expr> vars; 03398 vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end()); 03399 d_theories[i]->computeModelBasic(vars); 03400 TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] => }"); 03401 if(inconsistent()) { 03402 vector<Expr> assump; 03403 thm = inconsistentThm(); 03404 return false; 03405 } 03406 } 03407 } 03408 03409 return true; 03410 } 03411 03412 03413 void TheoryCore::buildModel(ExprMap<Expr>& m) 03414 { 03415 TRACE_MSG("model", "buildModel() {"); 03416 03417 size_t numTheories = getNumTheories(); 03418 // Use STL set to prune duplicate variables in theories 03419 vector<set<Expr> > theoryExprs(numTheories+1); 03420 // Sort out model vars by theories 03421 for(size_t j = 0 ; j<d_basicModelVars.size() ; j++) { 03422 const Expr& var = d_basicModelVars[j]; 03423 Theorem findThm(find(var)); 03424 if(findThm.getRHS()!=var) { // Replace var with its find and skip it 03425 TRACE("model", "buildModel: replace var="+var.toString(), 03426 " with find(var)=", findThm.getRHS()); 03427 d_simplifiedModelVars[var] = findThm; 03428 continue; 03429 } 03430 03431 Theory *th = theoryOf(getBaseType(var).getExpr().getKind()); 03432 size_t i=0; 03433 for(; i<numTheories && d_theories[i] != th; ++i); 03434 DebugAssert(i<numTheories && d_theories[i] == th, 03435 "TheoryCore::buildModel: cannot find the theory [" 03436 +th->getName()+"] for the variable: " 03437 +var.toString()); 03438 theoryExprs[i].insert(var); 03439 TRACE("model", "buildModel: adding ", var, 03440 " to theory "+d_theories[i]->getName()); 03441 } 03442 // Build a model for the basic-type variables 03443 for(int i=0; i<getNumTheories(); i++) { 03444 if(theoryExprs[i].size() > 0) { 03445 TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] {"); 03446 // Copy the corresponding variables into a vector 03447 vector<Expr> vars; 03448 vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end()); 03449 d_theories[i]->computeModelBasic(vars); 03450 TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] => }"); 03451 if(inconsistent()) { 03452 vector<Expr> assump; 03453 inconsistentThm().getLeafAssumptions(assump); 03454 Expr a = Expr(RAW_LIST, assump, d_em); 03455 throw EvalException 03456 ("Model Creation failed in Theory[" 03457 +d_theories[i]->getName() 03458 +"] due to the following assumptions:\n\n" 03459 +a.toString() 03460 +"\n\nYou might be using an incomplete logical fragment."); 03461 } 03462 } 03463 } 03464 // Recombine the values for the compound-type variables 03465 ExprHashMap<Theorem>::iterator k, kend=d_simplifiedModelVars.end(); 03466 for(CDList<Expr>::const_iterator i=d_vars.begin(), iend=d_vars.end(); i!=iend; ++i) { 03467 Expr var(*i); 03468 TRACE("model", "buildModel: recombining var=", var, ""); 03469 k=d_simplifiedModelVars.find(var); 03470 Theorem simp; // Null by default 03471 if(k!=kend) { // This var is simplified 03472 simp = k->second; 03473 TRACE("model", "buildModel: simplified var="+var.toString()+" to ", 03474 simp.getRHS(), ""); 03475 var = simp.getRHS(); 03476 } 03477 collectModelValues(var, m); 03478 if(d_varAssignments.count(var) > 0) { 03479 if(!simp.isNull()) { 03480 Theorem thm(transitivityRule(simp, d_varAssignments[var])); 03481 assignValue(thm); 03482 DebugAssert(thm.getLHS() == *i, ""); 03483 m[*i] = thm.getRHS(); 03484 } else 03485 m[*i] = d_varAssignments[var].getRHS(); 03486 } 03487 // else if(simp.isNull()) 03488 // m[*i] = *i; 03489 // else 03490 // m[*i] = simp.getRHS(); 03491 } 03492 TRACE_MSG("model", "buildModel => }"); 03493 } 03494 03495 03496 // Recursively build a compound-type variable assignment for e 03497 /*! Not all theories may implement aggregation of compound values. If 03498 * a compound variable is not assigned by a theory, add the more 03499 * primitive variable assignments to 'm'. 03500 * 03501 * Some variables may simplify to something else (simplifiedVars map). 03502 * INVARIANT: e is always simplified (it's not in simplifiedVars map). 03503 * Also, if v simplifies to e, and e is assigned, then v must be assigned. 03504 */ 03505 void TheoryCore::collectModelValues(const Expr& e, ExprMap<Expr>& m) 03506 { 03507 TRACE("model", "collectModelValues(", e, ") {"); 03508 if(d_varAssignments.count(e) > 0) { 03509 TRACE("model", "collectModelValues[cached] => ", 03510 d_varAssignments[e].getRHS(), " }"); 03511 return; // Got it already 03512 } 03513 ExprHashMap<Theorem>::iterator k, kend=d_simplifiedModelVars.end(); 03514 k=d_simplifiedModelVars.find(e); 03515 if(k!=kend) { 03516 const Theorem& findThm = k->second; 03517 const Expr& ee = findThm.getRHS(); 03518 collectModelValues(ee, m); 03519 if(d_varAssignments.count(ee) > 0) { 03520 Theorem thm = transitivityRule(findThm, d_varAssignments[ee]); 03521 assignValue(thm); 03522 } 03523 TRACE("model", "collectModelValues[simplified] => ", 03524 d_varAssignments[e].getRHS(), " }"); 03525 return; 03526 } 03527 if(d_varModelMap.count(e) == 0) { // Consider it a value of itself 03528 assignValue(reflexivityRule(e)); 03529 TRACE("model", "collectModelValues[e=e] => ", e, " }"); 03530 return; // Got it already 03531 } 03532 // Get the vector of more primitive vars 03533 const vector<Expr>& vars = d_varModelMap[e]; 03534 // Recurse 03535 bool gotAll(true); // Whether we got all the values 03536 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) { 03537 Expr var(*i); 03538 // k=d_simplifiedModelVars.find(var); 03539 // Theorem simp; // Null by default 03540 // if(k!=kend) { // This var is simplified 03541 // simp = k->second; 03542 // var = simp.getRHS(); 03543 // } 03544 collectModelValues(var, m); 03545 if(d_varAssignments.count(var) == 0) { 03546 gotAll = false; 03547 } 03548 // else if(!simp.isNull()) { 03549 // Theorem thm(transitivityRule(simp, d_varAssignments[var])); 03550 // DebugAssert(thm.getLHS() == *i, ""); 03551 // assignValue(thm); 03552 // } 03553 } 03554 IF_DEBUG(vector<Expr> res;) 03555 if(gotAll) { 03556 vector<Expr> assigned; // What DP actually assigns 03557 Theory* th = theoryOf(getBaseType(e).getExpr()); 03558 TRACE("model", "computeModel["+th->getName()+"](", e, ") {"); 03559 th->computeModel(e, assigned); 03560 TRACE("model", "computeModel["+th->getName()+"] => ", 03561 Expr(RAW_LIST, assigned, getEM()), " }"); 03562 // Check if the assigned vars are different from e 03563 if(!(assigned.size()==1 && assigned[0]==e)) { 03564 // if(d_varAssignments.count(e) == 0) { 03565 for(vector<Expr>::iterator i=assigned.begin(), iend=assigned.end(); 03566 i!=iend; ++i) { 03567 if(*i == e) continue; // Skip the original var 03568 m[*i] = getModelValue(*i).getRHS(); 03569 IF_DEBUG(res.push_back(getModelValue(*i).getExpr());) 03570 } 03571 } else { 03572 IF_DEBUG(res.push_back(getModelValue(e).getExpr());) 03573 } 03574 } 03575 TRACE("model", "collectModelValues => ", 03576 Expr(RAW_LIST, res, getEM()), " }"); 03577 } 03578 03579 03580 Theorem TheoryCore::rewriteLiteral(const Expr& e) { 03581 DebugAssert(e.isAbsLiteral(), "rewriteLiteral("+e.toString() 03582 +")\nExpected a literal."); 03583 Theorem res; 03584 //Theory* i = theoryOf(getBaseType(e).getExpr()); 03585 bool neg(e.isNot()); 03586 const Expr a = neg? e[0] : e; 03587 Theory * i; 03588 if(a.isEq()) 03589 i = theoryOf(getBaseType(a[0]).getExpr()); 03590 else if (a.arity() > 1) 03591 i = theoryOf(getBaseType(a[0]).getExpr()); 03592 else 03593 i = theoryOf(a); 03594 res = i->rewriteAtomic(a); 03595 if(neg) res = d_commonRules->iffContrapositive(res); 03596 return res; 03597 } 03598 03599 03600 03601 03602 03603 03604 void TheoryCore::setTimeLimit(unsigned limit) { 03605 initTimeLimit(); 03606 d_timeLimit = limit; 03607 } 03608 03609 void TheoryCore::initTimeLimit() { 03610 d_timeBase = clock() / (CLOCKS_PER_SEC / 10); 03611 } 03612 03613 bool TheoryCore::timeLimitReached() { 03614 if (d_timeLimit > 0 03615 && d_timeLimit < (unsigned)(clock() / (CLOCKS_PER_SEC / 10)) - d_timeBase) { 03616 setIncomplete("Exhausted user-specified time limit"); 03617 return true; 03618 } else { 03619 return false; 03620 } 03621 } 03622 03623 03624 03625 /*****************************************************************************/ 03626 /* 03627 * Methods provided for benefit of theories 03628 */ 03629 /*****************************************************************************/ 03630 03631 03632 /*! 03633 * Invariants: 03634 * - The input theorem e is either an equality or a conjunction of 03635 * equalities; 03636 * - In each equality e1=e2, the RHS e2 i-leaf-simplified; 03637 * - At the time of calling update(), all equalities in the queue are 03638 * processed by assertFormula() and the equivalence classes are merged 03639 * in the union-find database. 03640 * 03641 * In other words, the entire equality queue is processed "in parallel". 03642 */ 03643 03644 void TheoryCore::assertEqualities(const Theorem& e) 03645 { 03646 IF_DEBUG( 03647 string indentStr(getCM()->scopeLevel(), ' '); 03648 TRACE("facts", indentStr, "assertEqualities: ", e); 03649 if (!incomplete()) d_solver->checkAssertEqInvariant(e); 03650 ) 03651 TRACE("quant update", "equs in core ", e.getExpr(), ""); 03652 03653 // fast case 03654 if (e.isRewrite()) { 03655 const Expr& lhs = e.getLHS(); 03656 const Expr& rhs = e.getRHS(); 03657 DebugAssert(lhs.isTerm(), "term expected"); 03658 DebugAssert(findReduced(lhs) && 03659 findReduced(rhs), "should be find-reduced"); 03660 DebugAssert(lhs != rhs, "expected different lhs and rhs"); 03661 assertFormula(e); 03662 lhs.setFind(e); 03663 Theorem tmp = lhs.getEqNext(); 03664 lhs.setEqNext(transitivityRule(e, rhs.getEqNext())); 03665 rhs.setEqNext(transitivityRule(symmetryRule(e), tmp)); 03666 d_em->invalidateSimpCache(); 03667 NotifyList *L; 03668 L = lhs.getNotify(); 03669 if (L) processNotify(e, L); 03670 processNotify(e, &d_notifyEq); 03671 } 03672 else if (e.getExpr().isFalse()) { 03673 setInconsistent(e); 03674 } 03675 else { 03676 Expr conj = e.getExpr(); 03677 DebugAssert(conj.isAnd(), "Expected conjunction"); 03678 vector<Theorem> eqs; 03679 Theorem t; 03680 int index; 03681 03682 for (index = 0; index < conj.arity(); ++index) { 03683 t = d_commonRules->andElim(e, index); 03684 eqs.push_back(t); 03685 if (t.getExpr().isFalse()) { 03686 setInconsistent(t); 03687 return; 03688 } 03689 DebugAssert(t.isRewrite(), "Expected rewrite"); 03690 DebugAssert(t.getLHS().isTerm(), "term expected"); 03691 DebugAssert(findReduced(t.getLHS()) && 03692 findReduced(t.getRHS()), "should be find-reduced"); 03693 assertFormula(t); 03694 if (d_inconsistent) return; 03695 } 03696 03697 // Merge the equivalence classes 03698 vector<Theorem>::iterator i = eqs.begin(), iend = eqs.end(); 03699 for(; i!=iend; ++i) { 03700 const Theorem& thm = *i; 03701 const Expr& lhs = thm.getLHS(); 03702 const Expr& rhs = thm.getRHS(); 03703 DebugAssert(find(lhs).getRHS() == lhs, 03704 "find error: thm = "+thm.getExpr().toString() 03705 +"\n\n find(lhs) = " 03706 +find(lhs).getRHS().toString()); 03707 DebugAssert(find(rhs).getRHS() == rhs, 03708 "find error: thm = "+thm.getExpr().toString() 03709 +"\n\n find(rhs) = " 03710 +find(rhs).getRHS().toString()); 03711 lhs.setFind(thm); 03712 Theorem tmp = lhs.getEqNext(); 03713 lhs.setEqNext(transitivityRule(thm, rhs.getEqNext())); 03714 rhs.setEqNext(transitivityRule(symmetryRule(thm), tmp)); 03715 } 03716 03717 d_em->invalidateSimpCache(); 03718 03719 // Call the update() functions (process NotifyLists). 03720 03721 for(i=eqs.begin(); i!=iend && !d_inconsistent; ++i) { 03722 const Theorem& thm = *i; 03723 NotifyList *L = thm.getLHS().getNotify(); 03724 if (L) processNotify(thm, L); 03725 processNotify(thm, &d_notifyEq); 03726 } 03727 } 03728 } 03729 03730 03731 void TheoryCore::setIncomplete(const string& reason) 03732 { 03733 d_incomplete.insert(reason, true); 03734 } 03735 03736 03737 Theorem TheoryCore::typePred(const Expr& e) 03738 { 03739 return d_rules->typePred(e); 03740 } 03741 03742 03743 static bool hasBoundVarRec(const Expr& e) 03744 { 03745 if (e.getFlag()) return false; 03746 if (e.isQuantifier()) return false; 03747 if (e.getKind() == BOUND_VAR) return true; 03748 for (int i = 0, ar = e.arity(); i < ar; ++i) { 03749 if (hasBoundVarRec(e[i])) return true; 03750 } 03751 e.setFlag(); 03752 return false; 03753 } 03754 03755 IF_DEBUG( 03756 static bool hasBoundVar(const Expr& e) 03757 { 03758 e.getEM()->clearFlags(); 03759 return hasBoundVarRec(e); 03760 } 03761 ) 03762 03763 03764 void TheoryCore::enqueueFact(const Theorem& e) 03765 { 03766 // The theorem scope shouldn't be higher than current 03767 DebugAssert(e.getScope() <= d_cm->scopeLevel(), 03768 "\n e.getScope()="+int2string(e.getScope()) 03769 +"\n scopeLevel="+int2string(d_cm->scopeLevel()) 03770 +"\n e = "+e.getExpr().toString()); 03771 DebugAssert(okToEnqueue(), 03772 "enqueueFact() is called outside of addFact()" 03773 " or checkSATCore() or registerAtom() or preprocess"); 03774 DebugAssert((e.isRewrite() && !hasBoundVar(e.getLHS()) 03775 && !hasBoundVar(e.getRHS())) || 03776 (!e.isRewrite() && !hasBoundVar(e.getExpr())), 03777 "Bound vars shouldn't be free: " + e.toString()); 03778 03779 // No need to enqueue when already inconsistent or out of resources 03780 if (d_inconsistent || outOfResources()) return; 03781 03782 if (!e.isRewrite() && e.getExpr().isFalse()) { 03783 setInconsistent(e); 03784 } else { 03785 getResource(); 03786 d_queue.push(e); 03787 if (outOfResources()) { 03788 // No more resources: ignore all the remaining facts and fail 03789 // gracefully 03790 setIncomplete("Exhausted user-specified resource"); 03791 } 03792 } 03793 } 03794 03795 03796 void TheoryCore::setInconsistent(const Theorem& e) 03797 { 03798 DebugAssert(e.getExpr() == falseExpr(), "Expected proof of false"); 03799 d_inconsistent = true; d_incThm = e; 03800 // if(!d_queueSE.empty()){ 03801 // cout<<"before SAT 1"<<endl; 03802 // } 03803 d_queueSE.clear(); 03804 // Theory 0 is TheoryCore, skip it 03805 for(unsigned i=1; i < d_theories.size(); ++i) { 03806 d_theories[i]->notifyInconsistent(e); 03807 } 03808 } 03809 03810 03811 void TheoryCore::setupTerm(const Expr& t, Theory* i, const Theorem& thm) 03812 { 03813 int k; 03814 // Atomic formulas (non-terms) may have find pointers without the 03815 // subterms being setup. Recurse down to the terms before checking 03816 // for find pointers. 03817 if (!t.isTerm()) { 03818 if (!t.isStoredPredicate()) { 03819 DebugAssert(t.isAbsLiteral(), "Expected absliteral"); 03820 for (k = 0; k < t.arity(); ++k) { 03821 setupTerm(t[k], i, thm); 03822 } 03823 t.setStoredPredicate(); 03824 d_predicates.push_back(t); 03825 d_termTheorems[t] = thm; 03826 theoryOf(t)->setup(t); 03827 TRACE("quantlevel", "==========\npushed pred | ", t.getIndex(), "|" + t.toString()+"because : "+thm.toString() ); 03828 TRACE("quant","pushed pred ",t,thm); 03829 } 03830 return; 03831 } 03832 03833 // Even if t is already setup, it may become shared with another theory 03834 Theory* j = theoryOf(t); 03835 if(i != j) { 03836 j->addSharedTerm(t); 03837 i->addSharedTerm(t); 03838 } 03839 03840 // If already setup, nothing else to do 03841 if (t.hasFind()) return; 03842 03843 // Proceed with the setup 03844 03845 // Add the term into the set of all terms 03846 d_terms.push_back(t); 03847 d_termTheorems[t] = thm; 03848 TRACE("quantlevel","=========\npushed term ("+t.toString(), ") with quantlevel: ", thm.getQuantLevel()); 03849 03850 for (k = 0; k < t.arity(); ++k) { 03851 setupTerm(t[k], j, thm); 03852 } 03853 t.setFind(reflexivityRule(t)); 03854 t.setEqNext(reflexivityRule(t)); 03855 j->setup(t); 03856 03857 // Assert the subtyping predicate AFTER the setup is complete 03858 Theorem pred = d_rules->typePred(t); 03859 pred = iffMP(pred, simplify(pred.getExpr())); 03860 const Expr& predExpr = pred.getExpr(); 03861 if(predExpr.isFalse()) { 03862 IF_DEBUG(debugger.counter("conflicts from type predicate")++;) 03863 setInconsistent(pred); 03864 } 03865 else if(!predExpr.isTrue()) { 03866 Theory* k = theoryOf(t.getType().getExpr()); 03867 k->assertTypePred(t, pred); 03868 } 03869 }