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