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.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         // Recursively simplify the kids
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   //  TRACE("facts assertFact", ("setInconsistent[" + getName() + "->]("), e, ")");
00099   //  TRACE("conflict", ("setInconsistent[" + getName() + "->]("), e, ")");
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   //  TRACE("facts assertFact", "setIncomplete["+getName()+"](", reason, ")");
00108   d_theoryCore->setIncomplete(reason);
00109 }
00110 
00111 
00112 Theorem Theory::simplify(const Expr& e)
00113 {
00114   //  TRACE("simplify", ("simplify[" + getName() + "->]("), e, ") {");
00115   Theorem res(d_theoryCore->simplify(e));
00116   //  TRACE("simplify", "simplify[" + getName() + "] => ", res, "}");
00117   return res;
00118 }
00119 
00120 
00121 void Theory::enqueueFact(const Theorem& e)
00122 {
00123   //  TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
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   //  DebugAssert(simplifyExpr(e) == e, "Expected splitter to be simplified");
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   // Theory of a var is determined by its *base* type, since SUBTYPE
00215   // may have different base types, but SUBTYPE itself belongs to
00216   // TheoryCore.
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   // See if we have it cached
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   //  TRACE("typePred", "computeTypePred["+i->getName()+"]("+t.toString()+", ", e, ") {");
00313   pred = i->computeTypePred(t, e);
00314   //  TRACE("typePred", "computeTypePred["+i->getName()+"] => ", pred, " }");
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 //! Setup a term for congruence closure (must have sig and rep attributes)
00361 void Theory::setupCC(const Expr& e) {
00362   //  TRACE("facts setup", "setupCC["+getName()+"](", e, ") {");
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   //  TRACE_MSG("facts setup", "setupCC["+getName()+"]() => }");
00370 }
00371 
00372 
00373 //! Update a term w.r.t. congruence closure (must be setup with setupCC())
00374 void Theory::updateCC(const Theorem& e, const Expr& d) {
00375   //  TRACE("facts update", "updateCC["+getName()+"]("+e.getExpr().toString()+", ",
00376   //  d, ") {");
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       //      TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
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   //  TRACE_MSG("facts update", "updateCC["+getName()+"]() => }");
00408 }
00409 
00410 
00411 //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
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   //  TRACE("facts parseExpr", "parseExpr(", e, ") {");
00421   Expr res(d_theoryCore->parseExpr(e));
00422   //  TRACE("facts parseExpr", "parseExpr => ", res, " }");
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 //   Expr res = lookupVar(name, &t);
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   // Replace TYPEDEF with its definition
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   // Add the variable for constructing a concrete model
00495   d_theoryCore->addToVarDB(res);
00496   // Add the new global declaration
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   // Replace TYPEDEF with its definition
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   // Typecheck
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   // Add the new global declaration
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   // Replace TYPEDEF with its definition
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   // Add it to the database of variables for concrete model generation
00566   d_theoryCore->addToVarDB(res);
00567   // Add the new global declaration
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   // Add the new global declaration
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   // Without the type, just replace the bound variable with the definition
00619   if(type.isNull())
00620     res = def;
00621   else {
00622     // When type is given, construct (LETDECL var, def) for the typechecker
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 //   if ((*type).isNull()) {
00646 //     e = newApplyExpr(Op(UFUNC, e));
00647 //     *type = e.lookupType();
00648     if ((*type).isNull()) return Expr();
00649 //   }
00650   return e;
00651 }
00652 
00653 
00654 // TODO: reconcile this with parser-driven new type expressions
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   // Add the new global declaration
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   // Make sure that the supplied predicate is total: construct 
00687   // 
00688   //    FORALL (x: domType): getTCC(pred(x))
00689   //
00690   // This only needs to be done for LAMBDA-expressions, since
00691   // uninterpreted predicates are defined for all the arguments
00692   // of correct (exact) types.
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   // We require that there exists an object of this type (otherwise there is an inherent inconsistency)
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 //! Create a new type abbreviation with the given name 
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   // Add the new global declaration
00736   installID(name, res);
00737   return Type(res);
00738 }
00739 
00740 
00741 Expr Theory::resolveID(const string& name) {
00742   //  TRACE("vars", "resolveID(", name, ") {");
00743   Expr res; // Result is Null by default
00744   // First, look up the bound variable stack
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     // Next, check in the globals
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   //  TRACE("vars", "resolveID => ", res, " }");
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 }

Generated on Tue Jul 3 14:33:39 2007 for CVC3 by  doxygen 1.5.1