CVC3

theory.cpp

Go to the documentation of this file.
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   if( type.isFunction() ) {
00600     throw Exception("newVar: expected non-function type");
00601   }
00602   if( !res.lookupType().isNull() ) {
00603     throw Exception("newVarExpr: redefining a variable " + name);
00604   }
00605   res.setType(type);
00606   return res;
00607 }
00608 
00609 
00610 Expr Theory::newVar(const string& name, const Type& type, const Expr& def)
00611 {
00612   DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00613   Type t;
00614   Expr res = resolveID(name);
00615   if (!res.isNull()) {
00616     throw TypecheckException
00617       ("Redefinition of variable "+name+":\n "
00618        "This variable is already defined.");
00619   }
00620   Expr v;
00621 
00622   // Replace TYPEDEF with its definition
00623   t = type;
00624   while(t.getExpr().getKind() == TYPEDEF) {
00625     DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
00626     t = t[1];
00627   }
00628 
00629   // Typecheck
00630   if(getBaseType(def) != getBaseType(t)) {
00631     throw TypecheckException("Type mismatch in constant definition:\n"
00632            "Constant "+name+
00633            " is declared with type:\n  "
00634            +t.toString()
00635            +"\nBut the type of definition is\n  "
00636            +def.getType().toString());
00637   }
00638   DebugAssert(t.getExpr().getKind() != ARROW,"");
00639 
00640   // Add the new global declaration
00641   installID(name, def);
00642   
00643   return def;
00644 }
00645 
00646 
00647 Op Theory::newFunction(const string& name, const Type& type,
00648                        bool computeTransClosure) {
00649   DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00650   Expr res = resolveID(name);
00651   Type t;
00652   if (!res.isNull()) {
00653     t = res.getType();
00654     throw TypecheckException
00655       ("Redefinition of variable "+name+":\n "
00656        "already defined with type: "+t.toString()
00657        +"\n the new type is: "+type.toString());
00658   }
00659   res = getEM()->newSymbolExpr(name, UFUNC);
00660   // Replace TYPEDEF with its definition
00661   t = type;
00662   while(t.getExpr().getKind() == TYPEDEF) {
00663     DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
00664     t = t[1];
00665   }
00666   res.setType(t);
00667   // Add it to the database of variables for concrete model generation
00668   d_theoryCore->addToVarDB(res);
00669   // Add the new global declaration
00670   installID(name, res);
00671   if (computeTransClosure &&
00672       t.isFunction() && t.arity() == 3 && t[2].isBool())
00673     res.setComputeTransClosure();
00674   return res.mkOp();
00675 }
00676 
00677 
00678 Op Theory::newFunction(const string& name, const Type& type,
00679                        const Expr& def) {
00680   DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
00681   Expr res = resolveID(name);
00682   Type t;
00683   if (!res.isNull()) {
00684     t = res.getType();
00685     throw TypecheckException
00686       ("Redefinition of name "+name+":\n "
00687        "already defined with type: "+t.toString()
00688        +"\n the new type is: "+type.toString());
00689   }
00690 
00691   // Add the new global declaration
00692   installID(name, def);
00693   return def.mkOp();
00694 }
00695 
00696 
00697 Op Theory::lookupFunction(const string& name, Type* type)
00698 {
00699   Expr e = getEM()->newSymbolExpr(name, UFUNC);
00700   *type = e.lookupType();
00701   if ((*type).isNull()) return Op();
00702   return e.mkOp();
00703 }
00704 
00705 
00706 static int boundVarCount = 0;
00707 
00708 
00709 Expr Theory::addBoundVar(const string& name, const Type& type) {
00710   ostringstream ss;
00711   ss << boundVarCount++;
00712   Expr v(getEM()->newBoundVarExpr(name, ss.str(), type));
00713   if (d_theoryCore->d_boundVarStack.size() == 0) {
00714     DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheTop,
00715                 "Parse cache invariant violated");
00716     d_theoryCore->d_parseCache = &d_theoryCore->d_parseCacheOther;
00717     DebugAssert(d_theoryCore->d_parseCache->empty(),
00718                 "Expected empty cache");
00719   }
00720   else {
00721     DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheOther,
00722                 "Parse cache invariant violated 2");
00723     d_theoryCore->d_parseCache->clear();
00724   }
00725   d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,v));
00726   DebugAssert(v.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
00727   hash_map<string, Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00728   if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00729     (*iBoundVarMap).second = Expr(RAW_LIST, v, (*iBoundVarMap).second);
00730   }
00731   else d_theoryCore->d_boundVarMap[name] = v;
00732   
00733   TRACE("vars", "addBoundVar("+name+", ", type, ") => "+v.toString());
00734   return v;
00735 }
00736 
00737 
00738 Expr Theory::addBoundVar(const string& name, const Type& type,
00739        const Expr& def) {
00740   Expr res;
00741   // Without the type, just replace the bound variable with the definition
00742   if(type.isNull())
00743     res = def;
00744   else {
00745     // When type is given, construct (LETDECL var, def) for the typechecker
00746     ostringstream ss;
00747     ss << boundVarCount++;
00748     res = Expr(LETDECL,
00749                getEM()->newBoundVarExpr(name, ss.str(), type), def);
00750   }
00751   if (d_theoryCore->d_boundVarStack.size() == 0) {
00752     DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheTop,
00753                 "Parse cache invariant violated");
00754     d_theoryCore->d_parseCache = &d_theoryCore->d_parseCacheOther;
00755     DebugAssert(d_theoryCore->d_parseCache->empty(),
00756                 "Expected empty cache");
00757   }
00758   else {
00759     DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheOther,
00760                 "Parse cache invariant violated 2");
00761     d_theoryCore->d_parseCache->clear();
00762   }
00763   d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,res));
00764   DebugAssert(res.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
00765   hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00766   if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00767     (*iBoundVarMap).second = Expr(RAW_LIST, res, (*iBoundVarMap).second);
00768   }
00769   else d_theoryCore->d_boundVarMap[name] = res;
00770   TRACE("vars", "addBoundVar("+name+", "+type.toString()+", ", def,
00771   ") => "+res.toString());
00772   return res;
00773 }
00774 
00775 
00776 Expr Theory::lookupVar(const string& name, Type* type)
00777 {
00778   Expr e = getEM()->newVarExpr(name);
00779   *type = e.lookupType();
00780 //   if ((*type).isNull()) {
00781 //     e = newApplyExpr(Op(UFUNC, e));
00782 //     *type = e.lookupType();
00783     if ((*type).isNull()) return Expr();
00784 //   }
00785   return e;
00786 }
00787 
00788 
00789 // TODO: reconcile this with parser-driven new type expressions
00790 Type Theory::newTypeExpr(const string& name)
00791 {
00792   Expr res = resolveID(name);
00793   if (!res.isNull()) {
00794     throw TypecheckException
00795       ("Redefinition of type variable "+name+":\n "
00796        "This variable is already defined.");
00797   }
00798   res = Expr(TYPEDECL, getEM()->newStringExpr(name));
00799   // Add the new global declaration
00800   installID(name, res);
00801   return Type(res);
00802 }
00803 
00804 
00805 Type Theory::lookupTypeExpr(const string& name)
00806 {
00807   Expr res = resolveID(name);
00808   if (res.isNull() ||
00809       (res.getKind() != TYPEDECL && !res.isType())) {
00810     return Type();
00811   }
00812   return Type(res);
00813 }
00814 
00815 
00816 Type Theory::newSubtypeExpr(const Expr& pred, const Expr& witness)
00817 {
00818   Type predTp(pred.getType());
00819   if(!predTp.isFunction() || predTp.arity() != 2)
00820     throw TypecheckException
00821       ("Expected unary predicate in the predicate subtype:\n\n  "
00822        +predTp.toString()
00823        +"\n\nThe predicate is:\n\n  "
00824        +pred.toString());
00825   if(!predTp[1].isBool())
00826     throw TypecheckException
00827       ("Range is not BOOLEAN in the predicate subtype:\n\n  "
00828        +predTp.toString()
00829        +"\n\nThe predicate is:\n\n  "
00830        +pred.toString());
00831   Expr p(simplifyExpr(pred));
00832   // Make sure that the supplied predicate is total: construct 
00833   // 
00834   //    FORALL (x: domType): getTCC(pred(x))
00835   //
00836   // This only needs to be done for LAMBDA-expressions, since
00837   // uninterpreted predicates are defined for all the arguments
00838   // of correct (exact) types.
00839   if (pred.isLambda() && d_theoryCore->getFlags()["tcc"].getBool()) {
00840     Expr quant = d_em->newClosureExpr(FORALL, p.getVars(),
00841                                       d_theoryCore->getTCC(p.getBody()));
00842     if (!d_theoryCore->d_coreSatAPI->check(quant)) {
00843       throw TypecheckException
00844         ("Subtype predicate could not be proved total in the following type:\n\n  "
00845          +Expr(SUBTYPE, p).toString()
00846          +"\n\nThe failed TCC is:\n\n  "
00847          +quant.toString());
00848     }
00849   }
00850   // We require that there exists an object of this type (otherwise there is an inherent inconsistency)
00851   Expr q;
00852   if (witness.isNull()) {
00853     vector<Expr> vec;
00854     vec.push_back(d_em->newBoundVarExpr(predTp[0]));
00855     q = d_em->newClosureExpr(EXISTS, vec, simplifyExpr(Expr(pred.mkOp(), vec.back())));
00856   }
00857   else {
00858     q = Expr(pred.mkOp(), witness);
00859   }
00860   if (!d_theoryCore->d_coreSatAPI->check(q)) {
00861     throw TypecheckException
00862       ("Unable to prove witness for subtype:\n\n  "
00863        +Expr(SUBTYPE, p).toString()
00864        +"\n\nThe failed condition is:\n\n  "
00865        +q.toString());
00866   }
00867   return Type(Expr(SUBTYPE, p));
00868 }
00869 
00870 
00871 //! Create a new type abbreviation with the given name 
00872 Type Theory::newTypeExpr(const string& name, const Type& def)
00873 {
00874   Expr res = resolveID(name);
00875   if (!res.isNull()) {
00876     throw TypecheckException
00877       ("Redefinition of type variable "+name+":\n "
00878        "This variable is already defined.");
00879   }
00880   res = def.getExpr();
00881   // Add the new global declaration
00882   installID(name, res);
00883   return Type(res);
00884 }
00885 
00886 
00887 Expr Theory::resolveID(const string& name) {
00888   //  TRACE("vars", "resolveID(", name, ") {");
00889   Expr res; // Result is Null by default
00890   // First, look up the bound variable stack
00891   hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
00892   if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
00893     res = (*iBoundVarMap).second;
00894     if (res.getKind() == RAW_LIST) {
00895       res = res[0];
00896     }
00897   }
00898   else {
00899     // Next, check in the globals
00900     map<string,Expr>::iterator i=d_theoryCore->d_globals.find(name),
00901       iend=d_theoryCore->d_globals.end();
00902     if(i!=iend)
00903       res = i->second;
00904   }
00905   //  TRACE("vars", "resolveID => ", res, " }");
00906   return res;
00907 }
00908 
00909 
00910 void Theory::installID(const string& name, const Expr& e)
00911 {
00912   DebugAssert(resolveID(name).isNull(),
00913               "installID called on existing identifier");
00914   d_theoryCore->d_globals[name] = e;
00915 }
00916 
00917 
00918 Theorem Theory::typePred(const Expr& e) {
00919   return d_theoryCore->typePred(e);
00920 }
00921 
00922 
00923 Theorem Theory::rewriteIte(const Expr& e)
00924 {
00925   if (e[0].isTrue())
00926     return d_commonRules->rewriteIteTrue(e);
00927   if (e[0].isFalse())
00928     return d_commonRules->rewriteIteFalse(e);
00929   if (e[1] == e[2])
00930     return d_commonRules->rewriteIteSame(e);
00931   return reflexivityRule(e);
00932 }
00933 
00934 
00935 Theorem Theory::renameExpr(const Expr& e) {
00936   Theorem thm = d_commonRules->varIntroSkolem(e);
00937   DebugAssert(thm.isRewrite() && thm.getRHS().isSkolem(),
00938               "thm = "+thm.toString());
00939   d_theoryCore->addToVarDB(thm.getRHS());
00940   return thm;
00941 }