00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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.getLHS() != res.getRHS()) {
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
00067 Theorem thm = d_theoryCore->simplify(e[k]);
00068 if (thm.getLHS() != thm.getRHS()) {
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) ?
00086 d_commonRules->rewriteAnd(andExpr(kids)).getRHS() : trueExpr();
00087 }
00088
00089
00090 bool Theory::inconsistent()
00091 {
00092 return d_theoryCore->inconsistent();
00093 }
00094
00095
00096 void Theory::setInconsistent(const Theorem& e)
00097 {
00098
00099
00100 IF_DEBUG(debugger.counter("conflicts from DPs")++);
00101 d_theoryCore->setInconsistent(e);
00102 }
00103
00104
00105 void Theory::setIncomplete(const string& reason)
00106 {
00107
00108 d_theoryCore->setIncomplete(reason);
00109 }
00110
00111
00112 Theorem Theory::simplify(const Expr& e)
00113 {
00114
00115 Theorem res(d_theoryCore->simplify(e));
00116
00117 return res;
00118 }
00119
00120
00121 void Theory::enqueueFact(const Theorem& e)
00122 {
00123
00124 d_theoryCore->enqueueFact(e);
00125 }
00126
00127
00128 void Theory::assertEqualities(const Theorem& e)
00129 {
00130 d_theoryCore->assertEqualities(e);
00131 }
00132
00133
00134 void Theory::addSplitter(const Expr& e, int priority) {
00135 TRACE("facts assertFact", "addSplitter[" + getName() + "->](", e,
00136 ", pri="+int2string(priority)+")");
00137
00138 DebugAssert(e.isAbsLiteral() && !e.isBoolConst(), "Expected literal");
00139 d_theoryCore->d_coreSatAPI->addSplitter(e, priority);
00140 }
00141
00142
00143 void Theory::assignValue(const Expr& t, const Expr& val) {
00144 TRACE("facts assertFact", "assignValue["+getName()+"](", t, ", "+
00145 val.toString()+") {");
00146 d_theoryCore->assignValue(t, val);
00147 TRACE("facts assertFact", "assignValue[", getName(), "] => }");
00148 }
00149
00150
00151 void Theory::assignValue(const Theorem& thm) {
00152 TRACE("facts assertFact", "assignValue["+getName()+"](", thm, ") {");
00153 d_theoryCore->assignValue(thm);
00154 TRACE("facts assertFact", "assignValue[", getName(), "] => }");
00155 }
00156
00157
00158 void Theory::registerKinds(Theory* theory, vector<int>& kinds)
00159 {
00160 vector<int>::const_iterator k;
00161 vector<int>::const_iterator kEnd;
00162 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
00163 DebugAssert(d_theoryCore->d_theoryMap.count(*k) == 0,
00164 "kind already registered: "+getEM()->getKindName(*k)
00165 +" = "+int2string(*k));
00166 d_theoryCore->d_theoryMap[*k] = theory;
00167 }
00168 }
00169
00170
00171 void Theory::registerTheory(Theory* theory, vector<int>& kinds,
00172 bool hasSolver)
00173 {
00174 registerKinds(theory, kinds);
00175 d_theoryCore->d_theories.push_back(theory);
00176 if (hasSolver) {
00177 DebugAssert(!d_theoryCore->d_solver,"Solver already registered");
00178 d_theoryCore->d_solver = theory;
00179 }
00180 }
00181
00182
00183 int Theory::getNumTheories()
00184 {
00185 return d_theoryCore->d_theories.size();
00186 }
00187
00188
00189 bool Theory::hasTheory(int kind) {
00190 return (d_theoryCore->d_theoryMap.count(kind) > 0);
00191 }
00192
00193
00194 Theory* Theory::theoryOf(int kind)
00195 {
00196 DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
00197 "Unknown operator: " + getEM()->getKindName(kind));
00198 return d_theoryCore->d_theoryMap[kind];
00199 }
00200
00201
00202 Theory* Theory::theoryOf(const Expr& e)
00203 {
00204 Expr e2(e);
00205 while (e2.isNot() || e2.isEq()) {
00206 e2 = e2[0];
00207 }
00208 if (e2.isApply()) {
00209 return d_theoryCore->d_theoryMap[e2.getOpKind()];
00210 }
00211 if (!e2.isVar()) {
00212 return d_theoryCore->d_theoryMap[e2.getKind()];
00213 }
00214
00215
00216
00217 const Expr& typeExpr = getBaseType(e2).getExpr();
00218 DebugAssert(!typeExpr.isNull(),"Null type");
00219 int kind = typeExpr.getKind();
00220 if (typeExpr.isApply()) kind = typeExpr.getOpKind();
00221 DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
00222 "Unknown operator: " + getEM()->getKindName(kind));
00223 return d_theoryCore->d_theoryMap[kind];
00224 }
00225
00226
00227 const Theorem& Theory::findRef(const Expr& e)
00228 {
00229 DebugAssert(e.hasFind(), "expected find");
00230 const Theorem& thm1 = e.getFind();
00231 if (thm1.isRefl()) return thm1;
00232 const Expr& e1 = thm1.getRHS();
00233 if (!e1.hasFind() || e1.getFind().getRHS() == e1) return thm1;
00234 const Theorem& thm2 = findRef(e1);
00235 DebugAssert(thm2.getLHS()==e1,"");
00236 DebugAssert(thm2.getLHS() != thm2.getRHS(),"");
00237 e.setFind(transitivityRule(thm1,thm2));
00238 return e.getFind();
00239 }
00240
00241
00242 Theorem Theory::find(const Expr& e)
00243 {
00244 if (!e.hasFind()) return reflexivityRule(e);
00245 const Theorem& thm1 = e.getFind();
00246 if (thm1.isRefl()) return thm1;
00247 const Expr& e1 = thm1.getRHS();
00248 if (e1 == e || !e1.hasFind() ||
00249 e1.getFind().getRHS() == e1) return thm1;
00250 Theorem thm2 = find(e1);
00251 DebugAssert(thm2.getLHS()==e1,"");
00252 DebugAssert(thm2.getLHS() != thm2.getRHS(),"");
00253 thm2 = transitivityRule(thm1,thm2);
00254 e.setFind(thm2);
00255 return thm2;
00256 }
00257
00258
00259 bool Theory::findReduced(const Expr& e)
00260 {
00261 if (e.hasFind())
00262 return e.getFind().getRHS() == e;
00263 for (Expr::iterator i = e.begin(), iend = e.end(); i != iend; ++i)
00264 if (!findReduced(*i)) return false;
00265 return true;
00266 }
00267
00268
00269 Expr Theory::getTCC(const Expr& e)
00270 {
00271 if(e.isVar()) return trueExpr();
00272 ExprMap<Expr>::iterator itccCache = d_theoryCore->d_tccCache.find(e);
00273 if (itccCache != d_theoryCore->d_tccCache.end()) {
00274 return (*itccCache).second;
00275 }
00276 Theory* i = theoryOf(e.getKind());
00277 TRACE("tccs", "computeTCC["+i->getName()+"](", e, ") {");
00278 Expr tcc = i->computeTCC(e);
00279 d_theoryCore->d_tccCache[e] = tcc;
00280 TRACE("tccs", "computeTCC["+i->getName()+"] => ", tcc, " }");
00281 return tcc;
00282 }
00283
00284
00285 Type Theory::getBaseType(const Expr& e)
00286 {
00287 return getBaseType(e.getType());
00288 }
00289
00290
00291 Type Theory::getBaseType(const Type& tp)
00292 {
00293 const Expr& e = tp.getExpr();
00294 DebugAssert(!e.isNull(), "Theory::getBaseType(Type(Null))");
00295
00296 Type res(e.lookupType());
00297 if(!res.isNull()) return res;
00298
00299 DebugAssert(theoryOf(e) != NULL,
00300 "Theory::getBaseType(): No theory for the type: "
00301 +tp.toString());
00302 res= theoryOf(e)->computeBaseType(tp);
00303 e.setType(res);
00304 return res;
00305 }
00306
00307
00308 Expr Theory::getTypePred(const Type& t, const Expr& e)
00309 {
00310 Expr pred;
00311 Theory *i = theoryOf(t.getExpr().getKind());
00312
00313 pred = i->computeTypePred(t, e);
00314
00315 return pred;
00316 }
00317
00318
00319 Theorem Theory::updateHelper(const Expr& e)
00320 {
00321 int ar = e.arity();
00322 switch (ar) {
00323 case 0:
00324 break;
00325 case 1: {
00326 const Theorem& res = findRef(e[0]);
00327 if (res.getLHS() != res.getRHS()) {
00328 return d_commonRules->substitutivityRule(e, res);
00329 }
00330 break;
00331 }
00332 case 2: {
00333 const Theorem thm0 = findRef(e[0]);
00334 const Theorem thm1 = findRef(e[1]);
00335 if (thm0.getLHS() != thm0.getRHS() ||
00336 thm1.getLHS() != thm1.getRHS()) {
00337 return d_commonRules->substitutivityRule(e, thm0, thm1);
00338 }
00339 break;
00340 }
00341 default: {
00342 vector<Theorem> newChildrenThm;
00343 vector<unsigned> changed;
00344 for (int k = 0; k < ar; ++k) {
00345 const Theorem& thm = findRef(e[k]);
00346 if (thm.getLHS() != thm.getRHS()) {
00347 newChildrenThm.push_back(thm);
00348 changed.push_back(k);
00349 }
00350 }
00351 if (changed.size() > 0)
00352 return d_commonRules->substitutivityRule(e, changed, newChildrenThm);
00353 break;
00354 }
00355 }
00356 return reflexivityRule(e);
00357 }
00358
00359
00360
00361 void Theory::setupCC(const Expr& e) {
00362
00363 for (int k = 0; k < e.arity(); ++k) {
00364 e[k].addToNotify(this, e);
00365 }
00366 Theorem thm = reflexivityRule(e);
00367 e.setSig(thm);
00368 e.setRep(thm);
00369
00370 }
00371
00372
00373
00374 void Theory::updateCC(const Theorem& e, const Expr& d) {
00375
00376
00377 int k, ar(d.arity());
00378 const Theorem& dEQdsig = d.getSig();
00379 if (!dEQdsig.isNull()) {
00380 const Expr& dsig = dEQdsig.getRHS();
00381 Theorem thm = updateHelper(d);
00382 const Expr& sigNew = thm.getRHS();
00383 if (sigNew == dsig) {
00384
00385 return;
00386 }
00387 dsig.setRep(Theorem());
00388 const Theorem& repEQsigNew = sigNew.getRep();
00389 if (!repEQsigNew.isNull()) {
00390 d.setSig(Theorem());
00391 enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
00392 }
00393 else if (d.getType().isBool()) {
00394 d.setSig(Theorem());
00395 enqueueFact(thm);
00396 }
00397 else {
00398 for (k = 0; k < ar; ++k) {
00399 if (sigNew[k] != dsig[k]) {
00400 sigNew[k].addToNotify(this, d);
00401 }
00402 }
00403 d.setSig(thm);
00404 sigNew.setRep(thm);
00405 }
00406 }
00407
00408 }
00409
00410
00411
00412 Theorem Theory::rewriteCC(const Expr& e) {
00413 const Theorem& rep = e.getRep();
00414 if (rep.isNull()) return reflexivityRule(e);
00415 else return symmetryRule(rep);
00416 }
00417
00418
00419 Expr Theory::parseExpr(const Expr& e) {
00420
00421 Expr res(d_theoryCore->parseExpr(e));
00422
00423 return res;
00424 }
00425
00426
00427 void Theory::getModelTerm(const Expr& e, vector<Expr>& v)
00428 {
00429 Theory *i = theoryOf(getBaseType(e).getExpr());
00430 TRACE("model", "computeModelTerm["+i->getName()+"](", e, ") {");
00431 IF_DEBUG(unsigned size = v.size();)
00432 i->computeModelTerm(e, v);
00433 TRACE("model", "computeModelTerm[", i->getName(), "] => }");
00434 DebugAssert(v.size() <= size || v.back() != e, "Primitive var was pushed on "
00435 "the stack in computeModelTerm["+i->getName()
00436 +"]: "+e.toString());
00437
00438 }
00439
00440
00441 Theorem Theory::getModelValue(const Expr& e) {
00442 return d_theoryCore->getModelValue(e);
00443 }
00444
00445
00446 bool Theory::isLeafIn(const Expr& e1, const Expr& e2)
00447 {
00448 DebugAssert(isLeaf(e1),"Expected leaf");
00449 if (e1 == e2) return true;
00450 if (theoryOf(e2) != this) return false;
00451 for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i)
00452 if (isLeafIn(e1, *i)) return true;
00453 return false;
00454 }
00455
00456
00457 bool Theory::leavesAreSimp(const Expr& e)
00458 {
00459 if (isLeaf(e)) {
00460 return !e.hasFind() || e.getFind().getRHS() == e;
00461 }
00462 for (int k = 0; k < e.arity(); ++k) {
00463 if (!leavesAreSimp(e[k])) return false;
00464 }
00465 return true;
00466 }
00467
00468
00469 Expr Theory::newVar(const string& name, const Type& type)
00470 {
00471 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00472 Expr res = resolveID(name);
00473 Type t;
00474
00475 if (!res.isNull()) {
00476 t = res.getType();
00477 if (t != type) {
00478 throw TypecheckException
00479 ("incompatible redefinition of variable "+name+":\n "
00480 "already defined with type: "+t.toString()
00481 +"\n the new type is: "+type.toString());
00482 }
00483 return res;
00484 }
00485
00486 t = type;
00487 while(t.getExpr().getKind() == TYPEDEF) {
00488 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
00489 t = t[1];
00490 }
00491 if (type.isBool()) res = d_em->newSymbolExpr(name, UCONST);
00492 else res = getEM()->newVarExpr(name);
00493
00494
00495 d_theoryCore->addToVarDB(res);
00496
00497 installID(name, res);
00498
00499 DebugAssert(type.getExpr().getKind() != ARROW,"");
00500 DebugAssert(res.lookupType().isNull(),
00501 "newVarExpr: redefining a variable "
00502 + name);
00503 res.setType(type);
00504 return res;
00505 }
00506
00507
00508 Expr Theory::newVar(const string& name, const Type& type, const Expr& def)
00509 {
00510 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00511 Type t;
00512 Expr res = resolveID(name);
00513 if (!res.isNull()) {
00514 throw TypecheckException
00515 ("Redefinition of variable "+name+":\n "
00516 "This variable is already defined.");
00517 }
00518 Expr v;
00519
00520
00521 t = type;
00522 while(t.getExpr().getKind() == TYPEDEF) {
00523 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
00524 t = t[1];
00525 }
00526
00527
00528 if(getBaseType(def) != getBaseType(t)) {
00529 throw TypecheckException("Type mismatch in constant definition:\n"
00530 "Constant "+name+
00531 " is declared with type:\n "
00532 +t.toString()
00533 +"\nBut the type of definition is\n "
00534 +def.getType().toString());
00535 }
00536 DebugAssert(t.getExpr().getKind() != ARROW,"");
00537
00538
00539 installID(name, def);
00540
00541 return def;
00542 }
00543
00544
00545 Op Theory::newFunction(const string& name, const Type& type,
00546 bool computeTransClosure) {
00547 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00548 Expr res = resolveID(name);
00549 Type t;
00550 if (!res.isNull()) {
00551 t = res.getType();
00552 throw TypecheckException
00553 ("Redefinition of variable "+name+":\n "
00554 "already defined with type: "+t.toString()
00555 +"\n the new type is: "+type.toString());
00556 }
00557 res = getEM()->newSymbolExpr(name, UFUNC);
00558
00559 t = type;
00560 while(t.getExpr().getKind() == TYPEDEF) {
00561 DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
00562 t = t[1];
00563 }
00564 res.setType(t);
00565
00566 d_theoryCore->addToVarDB(res);
00567
00568 installID(name, res);
00569 if (computeTransClosure &&
00570 t.isFunction() && t.arity() == 3 && t[2].isBool())
00571 res.setComputeTransClosure();
00572 return res.mkOp();
00573 }
00574
00575
00576 Op Theory::newFunction(const string& name, const Type& type,
00577 const Expr& def) {
00578 DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00579 Expr res = resolveID(name);
00580 Type t;
00581 if (!res.isNull()) {
00582 t = res.getType();
00583 throw TypecheckException
00584 ("Redefinition of name "+name+":\n "
00585 "already defined with type: "+t.toString()
00586 +"\n the new type is: "+type.toString());
00587 }
00588
00589
00590 installID(name, def);
00591 return def.mkOp();
00592 }
00593
00594
00595 static int boundVarCount = 0;
00596
00597
00598 Expr Theory::addBoundVar(const string& name, const Type& type) {
00599 ostringstream ss;
00600 ss << boundVarCount++;
00601 Expr v(getEM()->newBoundVarExpr(name, ss.str(), type));
00602 d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,v));
00603 DebugAssert(v.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
00604 hash_map<string, Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00605 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00606 (*iBoundVarMap).second = Expr(RAW_LIST, v, (*iBoundVarMap).second);
00607 }
00608 else d_theoryCore->d_boundVarMap[name] = v;
00609 d_theoryCore->d_parseCache.clear();
00610 TRACE("vars", "addBoundVar("+name+", ", type, ") => "+v.toString());
00611 return v;
00612 }
00613
00614
00615 Expr Theory::addBoundVar(const string& name, const Type& type,
00616 const Expr& def) {
00617 Expr res;
00618
00619 if(type.isNull())
00620 res = def;
00621 else {
00622
00623 ostringstream ss;
00624 ss << boundVarCount++;
00625 res = Expr(LETDECL,
00626 getEM()->newBoundVarExpr(name, ss.str(), type), def);
00627 }
00628 d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,res));
00629 DebugAssert(res.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
00630 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00631 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00632 (*iBoundVarMap).second = Expr(RAW_LIST, res, (*iBoundVarMap).second);
00633 }
00634 else d_theoryCore->d_boundVarMap[name] = res;
00635 TRACE("vars", "addBoundVar("+name+", "+type.toString()+", ", def,
00636 ") => "+res.toString());
00637 return res;
00638 }
00639
00640
00641 Expr Theory::lookupVar(const string& name, Type* type)
00642 {
00643 Expr e = getEM()->newVarExpr(name);
00644 *type = e.lookupType();
00645
00646
00647
00648 if ((*type).isNull()) return Expr();
00649
00650 return e;
00651 }
00652
00653
00654
00655 Type Theory::newTypeExpr(const string& name)
00656 {
00657 Expr res = resolveID(name);
00658 if (!res.isNull()) {
00659 throw TypecheckException
00660 ("Redefinition of type variable "+name+":\n "
00661 "This variable is already defined.");
00662 }
00663 res = Expr(TYPEDECL, getEM()->newStringExpr(name));
00664
00665 installID(name, res);
00666 return Type(res);
00667 }
00668
00669
00670 Type Theory::newSubtypeExpr(const Expr& pred, const Expr& witness)
00671 {
00672 Type predTp(pred.getType());
00673 if(!predTp.isFunction() || predTp.arity() != 2)
00674 throw TypecheckException
00675 ("Expected unary predicate in the predicate subtype:\n\n "
00676 +predTp.toString()
00677 +"\n\nThe predicate is:\n\n "
00678 +pred.toString());
00679 if(!predTp[1].isBool())
00680 throw TypecheckException
00681 ("Range is not BOOLEAN in the predicate subtype:\n\n "
00682 +predTp.toString()
00683 +"\n\nThe predicate is:\n\n "
00684 +pred.toString());
00685 Expr p(simplifyExpr(pred));
00686
00687
00688
00689
00690
00691
00692
00693 if (pred.isLambda() && d_theoryCore->getFlags()["tcc"].getBool()) {
00694 Expr quant = d_em->newClosureExpr(FORALL, p.getVars(),
00695 d_theoryCore->getTCC(p.getBody()));
00696 if (!d_theoryCore->d_coreSatAPI->check(quant)) {
00697 throw TypecheckException
00698 ("Subtype predicate could not be proved total in the following type:\n\n "
00699 +Expr(SUBTYPE, p).toString()
00700 +"\n\nThe failed TCC is:\n\n "
00701 +quant.toString());
00702 }
00703 }
00704
00705 Expr q;
00706 if (witness.isNull()) {
00707 vector<Expr> vec;
00708 vec.push_back(d_em->newBoundVarExpr(predTp[0]));
00709 q = d_em->newClosureExpr(EXISTS, vec, simplifyExpr(Expr(pred.mkOp(), vec.back())));
00710 }
00711 else {
00712 q = Expr(pred.mkOp(), witness);
00713 }
00714 if (!d_theoryCore->d_coreSatAPI->check(q)) {
00715 throw TypecheckException
00716 ("Unable to prove witness for subtype:\n\n "
00717 +Expr(SUBTYPE, p).toString()
00718 +"\n\nThe failed condition is:\n\n "
00719 +q.toString());
00720 }
00721 return Type(Expr(SUBTYPE, p));
00722 }
00723
00724
00725
00726 Type Theory::newTypeExpr(const string& name, const Type& def)
00727 {
00728 Expr res = resolveID(name);
00729 if (!res.isNull()) {
00730 throw TypecheckException
00731 ("Redefinition of type variable "+name+":\n "
00732 "This variable is already defined.");
00733 }
00734 res = def.getExpr();
00735
00736 installID(name, res);
00737 return Type(res);
00738 }
00739
00740
00741 Expr Theory::resolveID(const string& name) {
00742
00743 Expr res;
00744
00745 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00746 if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00747 res = (*iBoundVarMap).second;
00748 if (res.getKind() == RAW_LIST) {
00749 res = res[0];
00750 }
00751 }
00752 else {
00753
00754 map<string,Expr>::iterator i=d_theoryCore->d_globals.find(name),
00755 iend=d_theoryCore->d_globals.end();
00756 if(i!=iend)
00757 res = i->second;
00758 }
00759
00760 return res;
00761 }
00762
00763
00764 void Theory::installID(const string& name, const Expr& e)
00765 {
00766 DebugAssert(resolveID(name).isNull(),
00767 "installID called on existing identifier");
00768 d_theoryCore->d_globals[name] = e;
00769 }
00770
00771
00772 Theorem Theory::typePred(const Expr& e) {
00773 return d_theoryCore->typePred(e);
00774 }