CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory.cpp 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Thu Jan 30 15:11:55 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 00022 #include "theory_core.h" 00023 #include "common_proof_rules.h" 00024 #include "typecheck_exception.h" 00025 #include "theorem_manager.h" 00026 #include "command_line_flags.h" 00027 00028 00029 using namespace CVC3; 00030 using namespace std; 00031 00032 00033 Theory::Theory(void) : d_theoryCore(NULL) { } 00034 00035 00036 Theory::Theory(TheoryCore* theoryCore, const string& name) 00037 : d_em(theoryCore->getEM()), 00038 d_theoryCore(theoryCore), 00039 d_commonRules(theoryCore->getTM()->getRules()), 00040 d_name(name), d_theoryUsed(false) { 00041 } 00042 00043 00044 Theory::~Theory(void) { } 00045 00046 00047 void Theory::computeModelTerm(const Expr& e, vector<Expr>& v) { 00048 TRACE("model", "Theory::computeModelTerm(", e, "): is a variable"); 00049 // v.push_back(e); 00050 } 00051 00052 00053 Theorem Theory::simplifyOp(const Expr& e) { 00054 int ar = e.arity(); 00055 if (ar > 0) { 00056 if (ar == 1) { 00057 Theorem res = d_theoryCore->simplify(e[0]); 00058 if (!res.isRefl()) { 00059 return d_commonRules->substitutivityRule(e, res); 00060 } 00061 } 00062 else { 00063 vector<Theorem> newChildrenThm; 00064 vector<unsigned> changed; 00065 for(int k = 0; k < ar; ++k) { 00066 // Recursively simplify the kids 00067 Theorem thm = d_theoryCore->simplify(e[k]); 00068 if (!thm.isRefl()) { 00069 newChildrenThm.push_back(thm); 00070 changed.push_back(k); 00071 } 00072 } 00073 if(changed.size() > 0) 00074 return d_commonRules->substitutivityRule(e, changed, newChildrenThm); 00075 } 00076 } 00077 return reflexivityRule(e); 00078 } 00079 00080 00081 Expr Theory::computeTCC(const Expr& e) { 00082 vector<Expr> kids; 00083 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 00084 kids.push_back(getTCC(*i)); 00085 return (kids.size() == 0) ? trueExpr() : 00086 (kids.size() == 1) ? kids[0] : 00087 d_commonRules->rewriteAnd(andExpr(kids)).getRHS(); 00088 } 00089 00090 00091 void Theory::registerAtom(const Expr& e, const Theorem& thm) 00092 { 00093 d_theoryCore->registerAtom(e, thm); 00094 } 00095 00096 00097 bool Theory::inconsistent() 00098 { 00099 return d_theoryCore->inconsistent(); 00100 } 00101 00102 00103 void Theory::setInconsistent(const Theorem& e) 00104 { 00105 // TRACE("facts assertFact", ("setInconsistent[" + getName() + "->]("), e, ")"); 00106 // TRACE("conflict", ("setInconsistent[" + getName() + "->]("), e, ")"); 00107 IF_DEBUG(debugger.counter("conflicts from DPs")++;) 00108 d_theoryCore->setInconsistent(e); 00109 } 00110 00111 00112 void Theory::setIncomplete(const string& reason) 00113 { 00114 // TRACE("facts assertFact", "setIncomplete["+getName()+"](", reason, ")"); 00115 d_theoryCore->setIncomplete(reason); 00116 } 00117 00118 00119 Theorem Theory::simplify(const Expr& e) 00120 { 00121 // TRACE("simplify", ("simplify[" + getName() + "->]("), e, ") {"); 00122 Theorem res(d_theoryCore->simplify(e)); 00123 // TRACE("simplify", "simplify[" + getName() + "] => ", res, "}"); 00124 return res; 00125 } 00126 00127 00128 void Theory::enqueueFact(const Theorem& e) 00129 { 00130 // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")"); 00131 d_theoryCore->enqueueFact(e); 00132 } 00133 00134 void Theory::enqueueSE(const Theorem& e) 00135 { 00136 // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")"); 00137 d_theoryCore->enqueueSE(e); 00138 } 00139 00140 00141 00142 void Theory::assertEqualities(const Theorem& e) 00143 { 00144 d_theoryCore->assertEqualities(e); 00145 } 00146 00147 00148 void Theory::addSplitter(const Expr& e, int priority) { 00149 TRACE("facts assertFact", "addSplitter[" + getName() + "->](", e, 00150 ", pri="+int2string(priority)+")"); 00151 // DebugAssert(simplifyExpr(e) == e, "Expected splitter to be simplified"); 00152 DebugAssert(e.isAbsLiteral() && !e.isBoolConst(), "Expected literal"); 00153 d_theoryCore->d_coreSatAPI->addSplitter(e, priority); 00154 } 00155 00156 00157 void Theory::addGlobalLemma(const Theorem& thm, int priority) { 00158 d_theoryCore->d_coreSatAPI->addLemma(thm, priority, true); 00159 } 00160 00161 00162 void Theory::assignValue(const Expr& t, const Expr& val) { 00163 TRACE("facts assertFact", "assignValue["+getName()+"](", t, ", "+ 00164 val.toString()+") {"); 00165 d_theoryCore->assignValue(t, val); 00166 TRACE("facts assertFact", "assignValue[", getName(), "] => }"); 00167 } 00168 00169 00170 void Theory::assignValue(const Theorem& thm) { 00171 TRACE("facts assertFact", "assignValue["+getName()+"](", thm, ") {"); 00172 d_theoryCore->assignValue(thm); 00173 TRACE("facts assertFact", "assignValue[", getName(), "] => }"); 00174 } 00175 00176 00177 void Theory::registerKinds(Theory* theory, vector<int>& kinds) 00178 { 00179 vector<int>::const_iterator k; 00180 vector<int>::const_iterator kEnd; 00181 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) { 00182 DebugAssert(d_theoryCore->d_theoryMap.count(*k) == 0, 00183 "kind already registered: "+getEM()->getKindName(*k) 00184 +" = "+int2string(*k)); 00185 d_theoryCore->d_theoryMap[*k] = theory; 00186 } 00187 } 00188 00189 00190 void Theory::unregisterKinds(Theory* theory, vector<int>& kinds) 00191 { 00192 vector<int>::const_iterator k; 00193 vector<int>::const_iterator kEnd; 00194 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) { 00195 DebugAssert(d_theoryCore->d_theoryMap[*k] == theory, 00196 "kind not registered: "+getEM()->getKindName(*k) 00197 +" = "+int2string(*k)); 00198 d_theoryCore->d_theoryMap.erase(*k); 00199 } 00200 } 00201 00202 00203 void Theory::registerTheory(Theory* theory, vector<int>& kinds, 00204 bool hasSolver) 00205 { 00206 registerKinds(theory, kinds); 00207 unsigned i = 0; 00208 for (; i < d_theoryCore->d_theories.size(); ++i) { 00209 if (d_theoryCore->d_theories[i] == NULL) { 00210 d_theoryCore->d_theories[i] = theory; 00211 break; 00212 } 00213 } 00214 if (i == d_theoryCore->d_theories.size()) { 00215 d_theoryCore->d_theories.push_back(theory); 00216 } 00217 if (hasSolver) { 00218 DebugAssert(!d_theoryCore->d_solver,"Solver already registered"); 00219 d_theoryCore->d_solver = theory; 00220 } 00221 } 00222 00223 00224 void Theory::unregisterTheory(Theory* theory, vector<int>& kinds, 00225 bool hasSolver) 00226 { 00227 unregisterKinds(theory, kinds); 00228 unsigned i = 0; 00229 for (; i < d_theoryCore->d_theories.size(); ++i) { 00230 if (d_theoryCore->d_theories[i] == theory) { 00231 d_theoryCore->d_theories[i] = NULL; 00232 } 00233 } 00234 if (hasSolver) { 00235 DebugAssert(d_theoryCore->d_solver == theory, "Solver not registered"); 00236 d_theoryCore->d_solver = NULL; 00237 } 00238 } 00239 00240 00241 int Theory::getNumTheories() 00242 { 00243 return d_theoryCore->d_theories.size(); 00244 } 00245 00246 00247 bool Theory::hasTheory(int kind) { 00248 return (d_theoryCore->d_theoryMap.count(kind) > 0); 00249 } 00250 00251 00252 Theory* Theory::theoryOf(int kind) 00253 { 00254 DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0, 00255 "Unknown operator: " + getEM()->getKindName(kind)); 00256 return d_theoryCore->d_theoryMap[kind]; 00257 } 00258 00259 00260 Theory* Theory::theoryOf(const Type& e) 00261 { 00262 const Expr& typeExpr = getBaseType(e).getExpr(); 00263 DebugAssert(!typeExpr.isNull(),"Null type"); 00264 int kind = typeExpr.getOpKind(); 00265 DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0, 00266 "Unknown operator: " + getEM()->getKindName(kind)); 00267 return d_theoryCore->d_theoryMap[kind]; 00268 } 00269 00270 00271 Theory* Theory::theoryOf(const Expr& e) 00272 { 00273 Expr e2(e); 00274 while (e2.isNot() || e2.isEq()) { 00275 e2 = e2[0]; 00276 } 00277 if (e2.isApply()) { 00278 return d_theoryCore->d_theoryMap[e2.getOpKind()]; 00279 } 00280 if (!e2.isVar()) { 00281 return d_theoryCore->d_theoryMap[e2.getKind()]; 00282 } 00283 // Theory of a var is determined by its *base* type, since SUBTYPE 00284 // may have different base types, but SUBTYPE itself belongs to 00285 // TheoryCore. 00286 const Expr& typeExpr = getBaseType(e2).getExpr(); 00287 DebugAssert(!typeExpr.isNull(),"Null type"); 00288 int kind = typeExpr.getOpKind(); 00289 DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0, 00290 "Unknown operator: " + getEM()->getKindName(kind)); 00291 return d_theoryCore->d_theoryMap[kind]; 00292 } 00293 00294 00295 const Theorem& Theory::findRef(const Expr& e) 00296 { 00297 DebugAssert(e.hasFind(), "expected find"); 00298 const Theorem& thm1 = e.getFind(); 00299 if (thm1.isRefl()) return thm1; 00300 const Expr& e1 = thm1.getRHS(); 00301 if (!e1.hasFind() || e1.getFind().getRHS() == e1) return thm1; 00302 const Theorem& thm2 = findRef(e1); 00303 DebugAssert(thm2.getLHS()==e1,""); 00304 DebugAssert(thm2.getLHS() != thm2.getRHS(),""); 00305 e.setFind(transitivityRule(thm1,thm2)); 00306 return e.getFind(); 00307 } 00308 00309 00310 Theorem Theory::find(const Expr& e) 00311 { 00312 if (!e.hasFind()) return reflexivityRule(e); 00313 const Theorem& thm1 = e.getFind(); 00314 if (thm1.isRefl()) return thm1; 00315 const Expr& e1 = thm1.getRHS(); 00316 if (e1 == e || !e1.hasFind() || 00317 e1.getFind().getRHS() == e1) return thm1; 00318 Theorem thm2 = find(e1); 00319 DebugAssert(thm2.getLHS()==e1,""); 00320 DebugAssert(thm2.getLHS() != thm2.getRHS(),""); 00321 thm2 = transitivityRule(thm1,thm2); 00322 e.setFind(thm2); 00323 return thm2; 00324 } 00325 00326 00327 Theorem Theory::findReduce(const Expr& e) 00328 { 00329 if (e.hasFind()) return find(e); 00330 int ar = e.arity(); 00331 if (ar > 0) { 00332 if (ar == 1) { 00333 Theorem res = findReduce(e[0]); 00334 if (!res.isRefl()) { 00335 return d_commonRules->substitutivityRule(e, res); 00336 } 00337 } 00338 else { 00339 vector<Theorem> newChildrenThm; 00340 vector<unsigned> changed; 00341 for(int k = 0; k < ar; ++k) { 00342 // Recursively reduce the kids 00343 Theorem thm = findReduce(e[k]); 00344 if (!thm.isRefl()) { 00345 newChildrenThm.push_back(thm); 00346 changed.push_back(k); 00347 } 00348 } 00349 if(changed.size() > 0) 00350 return d_commonRules->substitutivityRule(e, changed, newChildrenThm); 00351 } 00352 } 00353 return reflexivityRule(e); 00354 } 00355 00356 00357 bool Theory::findReduced(const Expr& e) 00358 { 00359 if (e.hasFind()) 00360 return e.getFind().getRHS() == e; 00361 for (Expr::iterator i = e.begin(), iend = e.end(); i != iend; ++i) 00362 if (!findReduced(*i)) return false; 00363 return true; 00364 } 00365 00366 00367 Expr Theory::getTCC(const Expr& e) 00368 { 00369 if(e.isVar()) return trueExpr(); 00370 ExprMap<Expr>::iterator itccCache = d_theoryCore->d_tccCache.find(e); 00371 if (itccCache != d_theoryCore->d_tccCache.end()) { 00372 return (*itccCache).second; 00373 } 00374 Theory* i = theoryOf(e.getKind()); 00375 TRACE("tccs", "computeTCC["+i->getName()+"](", e, ") {"); 00376 Expr tcc = i->computeTCC(e); 00377 d_theoryCore->d_tccCache[e] = tcc; 00378 TRACE("tccs", "computeTCC["+i->getName()+"] => ", tcc, " }"); 00379 return tcc; 00380 } 00381 00382 00383 Type Theory::getBaseType(const Expr& e) 00384 { 00385 return getBaseType(e.getType()); 00386 } 00387 00388 00389 Type Theory::getBaseType(const Type& tp) 00390 { 00391 const Expr& e = tp.getExpr(); 00392 DebugAssert(!e.isNull(), "Theory::getBaseType(Type(Null))"); 00393 // See if we have it cached 00394 Type res(e.lookupType()); 00395 if(!res.isNull()) return res; 00396 00397 DebugAssert(theoryOf(e) != NULL, 00398 "Theory::getBaseType(): No theory for the type: " 00399 +tp.toString()); 00400 res= theoryOf(e)->computeBaseType(tp); 00401 e.setType(res); 00402 return res; 00403 } 00404 00405 00406 Expr Theory::getTypePred(const Type& t, const Expr& e) 00407 { 00408 Expr pred; 00409 Theory *i = theoryOf(t.getExpr().getKind()); 00410 // TRACE("typePred", "computeTypePred["+i->getName()+"]("+t.toString()+", ", e, ") {"); 00411 pred = i->computeTypePred(t, e); 00412 // TRACE("typePred", "computeTypePred["+i->getName()+"] => ", pred, " }"); 00413 return pred; 00414 } 00415 00416 00417 Theorem Theory::updateHelper(const Expr& e) 00418 { 00419 int ar = e.arity(); 00420 switch (ar) { 00421 case 0: 00422 break; 00423 case 1: { 00424 const Theorem& res = findRef(e[0]); 00425 if (res.getLHS() != res.getRHS()) { 00426 return d_commonRules->substitutivityRule(e, res); 00427 } 00428 break; 00429 } 00430 case 2: { 00431 const Theorem thm0 = findRef(e[0]); 00432 const Theorem thm1 = findRef(e[1]); 00433 if (thm0.getLHS() != thm0.getRHS() || 00434 thm1.getLHS() != thm1.getRHS()) { 00435 return d_commonRules->substitutivityRule(e, thm0, thm1); 00436 } 00437 break; 00438 } 00439 default: { 00440 vector<Theorem> newChildrenThm; 00441 vector<unsigned> changed; 00442 for (int k = 0; k < ar; ++k) { 00443 const Theorem& thm = findRef(e[k]); 00444 if (thm.getLHS() != thm.getRHS()) { 00445 newChildrenThm.push_back(thm); 00446 changed.push_back(k); 00447 } 00448 } 00449 if (changed.size() > 0) 00450 return d_commonRules->substitutivityRule(e, changed, newChildrenThm); 00451 break; 00452 } 00453 } 00454 return reflexivityRule(e); 00455 } 00456 00457 00458 //! Setup a term for congruence closure (must have sig and rep attributes) 00459 void Theory::setupCC(const Expr& e) { 00460 // TRACE("facts setup", "setupCC["+getName()+"](", e, ") {"); 00461 for (int k = 0; k < e.arity(); ++k) { 00462 e[k].addToNotify(this, e); 00463 } 00464 Theorem thm = reflexivityRule(e); 00465 e.setSig(thm); 00466 e.setRep(thm); 00467 e.setUsesCC(); 00468 // TRACE_MSG("facts setup", "setupCC["+getName()+"]() => }"); 00469 } 00470 00471 00472 //! Update a term w.r.t. congruence closure (must be setup with setupCC()) 00473 void Theory::updateCC(const Theorem& e, const Expr& d) { 00474 // TRACE("facts update", "updateCC["+getName()+"]("+e.getExpr().toString()+", ", 00475 // d, ") {"); 00476 int k, ar(d.arity()); 00477 const Theorem& dEQdsig = d.getSig(); 00478 if (!dEQdsig.isNull()) { 00479 const Expr& dsig = dEQdsig.getRHS(); 00480 Theorem thm = updateHelper(d); 00481 const Expr& sigNew = thm.getRHS(); 00482 if (sigNew == dsig) { 00483 // TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }"); 00484 return; 00485 } 00486 dsig.setRep(Theorem()); 00487 const Theorem& repEQsigNew = sigNew.getRep(); 00488 if (!repEQsigNew.isNull()) { 00489 d.setSig(Theorem()); 00490 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm))); 00491 } 00492 else if (d.getType().isBool()) { 00493 d.setSig(Theorem()); 00494 enqueueFact(thm); 00495 } 00496 else { 00497 for (k = 0; k < ar; ++k) { 00498 if (sigNew[k] != dsig[k]) { 00499 sigNew[k].addToNotify(this, d); 00500 } 00501 } 00502 d.setSig(thm); 00503 sigNew.setRep(thm); 00504 getEM()->invalidateSimpCache(); 00505 } 00506 } 00507 // TRACE_MSG("facts update", "updateCC["+getName()+"]() => }"); 00508 } 00509 00510 00511 //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC()) 00512 Theorem Theory::rewriteCC(const Expr& e) { 00513 const Theorem& rep = e.getRep(); 00514 if (rep.isNull()) return reflexivityRule(e); 00515 else return symmetryRule(rep); 00516 } 00517 00518 00519 Expr Theory::parseExpr(const Expr& e) { 00520 // TRACE("facts parseExpr", "parseExpr(", e, ") {"); 00521 Expr res(d_theoryCore->parseExpr(e)); 00522 // TRACE("facts parseExpr", "parseExpr => ", res, " }"); 00523 return res; 00524 } 00525 00526 00527 void Theory::getModelTerm(const Expr& e, vector<Expr>& v) 00528 { 00529 Theory *i = theoryOf(getBaseType(e).getExpr()); 00530 TRACE("model", "computeModelTerm["+i->getName()+"](", e, ") {"); 00531 IF_DEBUG(unsigned size = v.size();) 00532 i->computeModelTerm(e, v); 00533 TRACE("model", "computeModelTerm[", i->getName(), "] => }"); 00534 DebugAssert(v.size() <= size || v.back() != e, "Primitive var was pushed on " 00535 "the stack in computeModelTerm["+i->getName() 00536 +"]: "+e.toString()); 00537 00538 } 00539 00540 00541 Theorem Theory::getModelValue(const Expr& e) { 00542 return d_theoryCore->getModelValue(e); 00543 } 00544 00545 00546 bool Theory::isLeafIn(const Expr& e1, const Expr& e2) 00547 { 00548 DebugAssert(isLeaf(e1),"Expected leaf"); 00549 if (e1 == e2) return true; 00550 if (theoryOf(e2) != this) return false; 00551 for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i) 00552 if (isLeafIn(e1, *i)) return true; 00553 return false; 00554 } 00555 00556 00557 bool Theory::leavesAreSimp(const Expr& e) 00558 { 00559 if (isLeaf(e)) { 00560 return !e.hasFind() || e.getFind().getRHS() == e; 00561 } 00562 for (int k = 0; k < e.arity(); ++k) { 00563 if (!leavesAreSimp(e[k])) return false; 00564 } 00565 return true; 00566 } 00567 00568 00569 Expr Theory::newVar(const string& name, const Type& type) 00570 { 00571 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type"); 00572 Expr res = resolveID(name); 00573 Type t; 00574 // Expr res = lookupVar(name, &t); 00575 if (!res.isNull()) { 00576 t = res.getType(); 00577 if (t != type) { 00578 throw TypecheckException 00579 ("incompatible redefinition of variable "+name+":\n " 00580 "already defined with type: "+t.toString() 00581 +"\n the new type is: "+type.toString()); 00582 } 00583 return res; 00584 } 00585 // Replace TYPEDEF with its definition 00586 t = type; 00587 while(t.getExpr().getKind() == TYPEDEF) { 00588 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString()); 00589 t = t[1]; 00590 } 00591 if (type.isBool()) res = d_em->newSymbolExpr(name, UCONST); 00592 else res = getEM()->newVarExpr(name); 00593 00594 // Add the variable for constructing a concrete model 00595 d_theoryCore->addToVarDB(res); 00596 // Add the new global declaration 00597 installID(name, res); 00598 00599 DebugAssert(type.getExpr().getKind() != ARROW,""); 00600 DebugAssert(res.lookupType().isNull(), 00601 "newVarExpr: redefining a variable " 00602 + name); 00603 res.setType(type); 00604 return res; 00605 } 00606 00607 00608 Expr Theory::newVar(const string& name, const Type& type, const Expr& def) 00609 { 00610 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type"); 00611 Type t; 00612 Expr res = resolveID(name); 00613 if (!res.isNull()) { 00614 throw TypecheckException 00615 ("Redefinition of variable "+name+":\n " 00616 "This variable is already defined."); 00617 } 00618 Expr v; 00619 00620 // Replace TYPEDEF with its definition 00621 t = type; 00622 while(t.getExpr().getKind() == TYPEDEF) { 00623 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString()); 00624 t = t[1]; 00625 } 00626 00627 // Typecheck 00628 if(getBaseType(def) != getBaseType(t)) { 00629 throw TypecheckException("Type mismatch in constant definition:\n" 00630 "Constant "+name+ 00631 " is declared with type:\n " 00632 +t.toString() 00633 +"\nBut the type of definition is\n " 00634 +def.getType().toString()); 00635 } 00636 DebugAssert(t.getExpr().getKind() != ARROW,""); 00637 00638 // Add the new global declaration 00639 installID(name, def); 00640 00641 return def; 00642 } 00643 00644 00645 Op Theory::newFunction(const string& name, const Type& type, 00646 bool computeTransClosure) { 00647 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type"); 00648 Expr res = resolveID(name); 00649 Type t; 00650 if (!res.isNull()) { 00651 t = res.getType(); 00652 throw TypecheckException 00653 ("Redefinition of variable "+name+":\n " 00654 "already defined with type: "+t.toString() 00655 +"\n the new type is: "+type.toString()); 00656 } 00657 res = getEM()->newSymbolExpr(name, UFUNC); 00658 // Replace TYPEDEF with its definition 00659 t = type; 00660 while(t.getExpr().getKind() == TYPEDEF) { 00661 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString()); 00662 t = t[1]; 00663 } 00664 res.setType(t); 00665 // Add it to the database of variables for concrete model generation 00666 d_theoryCore->addToVarDB(res); 00667 // Add the new global declaration 00668 installID(name, res); 00669 if (computeTransClosure && 00670 t.isFunction() && t.arity() == 3 && t[2].isBool()) 00671 res.setComputeTransClosure(); 00672 return res.mkOp(); 00673 } 00674 00675 00676 Op Theory::newFunction(const string& name, const Type& type, 00677 const Expr& def) { 00678 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type"); 00679 Expr res = resolveID(name); 00680 Type t; 00681 if (!res.isNull()) { 00682 t = res.getType(); 00683 throw TypecheckException 00684 ("Redefinition of name "+name+":\n " 00685 "already defined with type: "+t.toString() 00686 +"\n the new type is: "+type.toString()); 00687 } 00688 00689 // Add the new global declaration 00690 installID(name, def); 00691 return def.mkOp(); 00692 } 00693 00694 00695 Op Theory::lookupFunction(const string& name, Type* type) 00696 { 00697 Expr e = getEM()->newSymbolExpr(name, UFUNC); 00698 *type = e.lookupType(); 00699 if ((*type).isNull()) return Op(); 00700 return e.mkOp(); 00701 } 00702 00703 00704 static int boundVarCount = 0; 00705 00706 00707 Expr Theory::addBoundVar(const string& name, const Type& type) { 00708 ostringstream ss; 00709 ss << boundVarCount++; 00710 Expr v(getEM()->newBoundVarExpr(name, ss.str(), type)); 00711 d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,v)); 00712 DebugAssert(v.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST"); 00713 hash_map<string, Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name); 00714 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) { 00715 (*iBoundVarMap).second = Expr(RAW_LIST, v, (*iBoundVarMap).second); 00716 } 00717 else d_theoryCore->d_boundVarMap[name] = v; 00718 d_theoryCore->d_parseCache.clear(); 00719 TRACE("vars", "addBoundVar("+name+", ", type, ") => "+v.toString()); 00720 return v; 00721 } 00722 00723 00724 Expr Theory::addBoundVar(const string& name, const Type& type, 00725 const Expr& def) { 00726 Expr res; 00727 // Without the type, just replace the bound variable with the definition 00728 if(type.isNull()) 00729 res = def; 00730 else { 00731 // When type is given, construct (LETDECL var, def) for the typechecker 00732 ostringstream ss; 00733 ss << boundVarCount++; 00734 res = Expr(LETDECL, 00735 getEM()->newBoundVarExpr(name, ss.str(), type), def); 00736 } 00737 d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,res)); 00738 DebugAssert(res.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST"); 00739 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name); 00740 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) { 00741 (*iBoundVarMap).second = Expr(RAW_LIST, res, (*iBoundVarMap).second); 00742 } 00743 else d_theoryCore->d_boundVarMap[name] = res; 00744 TRACE("vars", "addBoundVar("+name+", "+type.toString()+", ", def, 00745 ") => "+res.toString()); 00746 return res; 00747 } 00748 00749 00750 Expr Theory::lookupVar(const string& name, Type* type) 00751 { 00752 Expr e = getEM()->newVarExpr(name); 00753 *type = e.lookupType(); 00754 // if ((*type).isNull()) { 00755 // e = newApplyExpr(Op(UFUNC, e)); 00756 // *type = e.lookupType(); 00757 if ((*type).isNull()) return Expr(); 00758 // } 00759 return e; 00760 } 00761 00762 00763 // TODO: reconcile this with parser-driven new type expressions 00764 Type Theory::newTypeExpr(const string& name) 00765 { 00766 Expr res = resolveID(name); 00767 if (!res.isNull()) { 00768 throw TypecheckException 00769 ("Redefinition of type variable "+name+":\n " 00770 "This variable is already defined."); 00771 } 00772 res = Expr(TYPEDECL, getEM()->newStringExpr(name)); 00773 // Add the new global declaration 00774 installID(name, res); 00775 return Type(res); 00776 } 00777 00778 00779 Type Theory::lookupTypeExpr(const string& name) 00780 { 00781 Expr res = resolveID(name); 00782 if (res.isNull() || 00783 (res.getKind() != TYPEDECL && !res.isType())) { 00784 return Type(); 00785 } 00786 return Type(res); 00787 } 00788 00789 00790 Type Theory::newSubtypeExpr(const Expr& pred, const Expr& witness) 00791 { 00792 Type predTp(pred.getType()); 00793 if(!predTp.isFunction() || predTp.arity() != 2) 00794 throw TypecheckException 00795 ("Expected unary predicate in the predicate subtype:\n\n " 00796 +predTp.toString() 00797 +"\n\nThe predicate is:\n\n " 00798 +pred.toString()); 00799 if(!predTp[1].isBool()) 00800 throw TypecheckException 00801 ("Range is not BOOLEAN in the predicate subtype:\n\n " 00802 +predTp.toString() 00803 +"\n\nThe predicate is:\n\n " 00804 +pred.toString()); 00805 Expr p(simplifyExpr(pred)); 00806 // Make sure that the supplied predicate is total: construct 00807 // 00808 // FORALL (x: domType): getTCC(pred(x)) 00809 // 00810 // This only needs to be done for LAMBDA-expressions, since 00811 // uninterpreted predicates are defined for all the arguments 00812 // of correct (exact) types. 00813 if (pred.isLambda() && d_theoryCore->getFlags()["tcc"].getBool()) { 00814 Expr quant = d_em->newClosureExpr(FORALL, p.getVars(), 00815 d_theoryCore->getTCC(p.getBody())); 00816 if (!d_theoryCore->d_coreSatAPI->check(quant)) { 00817 throw TypecheckException 00818 ("Subtype predicate could not be proved total in the following type:\n\n " 00819 +Expr(SUBTYPE, p).toString() 00820 +"\n\nThe failed TCC is:\n\n " 00821 +quant.toString()); 00822 } 00823 } 00824 // We require that there exists an object of this type (otherwise there is an inherent inconsistency) 00825 Expr q; 00826 if (witness.isNull()) { 00827 vector<Expr> vec; 00828 vec.push_back(d_em->newBoundVarExpr(predTp[0])); 00829 q = d_em->newClosureExpr(EXISTS, vec, simplifyExpr(Expr(pred.mkOp(), vec.back()))); 00830 } 00831 else { 00832 q = Expr(pred.mkOp(), witness); 00833 } 00834 if (!d_theoryCore->d_coreSatAPI->check(q)) { 00835 throw TypecheckException 00836 ("Unable to prove witness for subtype:\n\n " 00837 +Expr(SUBTYPE, p).toString() 00838 +"\n\nThe failed condition is:\n\n " 00839 +q.toString()); 00840 } 00841 return Type(Expr(SUBTYPE, p)); 00842 } 00843 00844 00845 //! Create a new type abbreviation with the given name 00846 Type Theory::newTypeExpr(const string& name, const Type& def) 00847 { 00848 Expr res = resolveID(name); 00849 if (!res.isNull()) { 00850 throw TypecheckException 00851 ("Redefinition of type variable "+name+":\n " 00852 "This variable is already defined."); 00853 } 00854 res = def.getExpr(); 00855 // Add the new global declaration 00856 installID(name, res); 00857 return Type(res); 00858 } 00859 00860 00861 Expr Theory::resolveID(const string& name) { 00862 // TRACE("vars", "resolveID(", name, ") {"); 00863 Expr res; // Result is Null by default 00864 // First, look up the bound variable stack 00865 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name); 00866 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) { 00867 res = (*iBoundVarMap).second; 00868 if (res.getKind() == RAW_LIST) { 00869 res = res[0]; 00870 } 00871 } 00872 else { 00873 // Next, check in the globals 00874 map<string,Expr>::iterator i=d_theoryCore->d_globals.find(name), 00875 iend=d_theoryCore->d_globals.end(); 00876 if(i!=iend) 00877 res = i->second; 00878 } 00879 // TRACE("vars", "resolveID => ", res, " }"); 00880 return res; 00881 } 00882 00883 00884 void Theory::installID(const string& name, const Expr& e) 00885 { 00886 DebugAssert(resolveID(name).isNull(), 00887 "installID called on existing identifier"); 00888 d_theoryCore->d_globals[name] = e; 00889 } 00890 00891 00892 Theorem Theory::typePred(const Expr& e) { 00893 return d_theoryCore->typePred(e); 00894 } 00895 00896 00897 Theorem Theory::rewriteIte(const Expr& e) 00898 { 00899 if (e[0].isTrue()) 00900 return d_commonRules->rewriteIteTrue(e); 00901 if (e[0].isFalse()) 00902 return d_commonRules->rewriteIteFalse(e); 00903 if (e[1] == e[2]) 00904 return d_commonRules->rewriteIteSame(e); 00905 return reflexivityRule(e); 00906 } 00907 00908