CVC3

theory_core.cpp

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