vcl.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file vcl.cpp
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Tue Dec 31 18:27:11 2002
00008  *
00009  * <hr>
00010  * License to use, copy, modify, sell and/or distribute this software
00011  * and its documentation for any purpose is hereby granted without
00012  * royalty, subject to the terms and conditions defined in the \ref
00013  * LICENSE file provided with this distribution.
00014  *
00015  * <hr>
00016  * 
00017  */
00018 /*****************************************************************************/
00019 
00020 
00021 #include <fstream>
00022 #include "os.h"
00023 #include "vcl.h"
00024 #include "parser.h"
00025 #include "vc_cmd.h"
00026 #include "search_simple.h"
00027 #include "search_fast.h"
00028 #include "search_sat.h"
00029 #include "theory_core.h"
00030 #include "theory_uf.h"
00031 #include "theory_arith_old.h"
00032 #include "theory_arith_new.h"
00033 #include "theory_bitvector.h"
00034 #include "theory_array.h"
00035 #include "theory_quant.h"
00036 #include "theory_records.h"
00037 #include "theory_simulate.h"
00038 #include "theory_datatype.h"
00039 #include "theory_datatype_lazy.h"
00040 #include "translator.h"
00041 #include "typecheck_exception.h"
00042 #include "eval_exception.h"
00043 #include "expr_transform.h"
00044 #include "theorem_manager.h"
00045 
00046 
00047 namespace CVC3{
00048   VCL* myvcl;
00049 }
00050 
00051 using namespace std;
00052 using namespace CVC3;
00053 
00054 
00055 ///////////////////////////////////////////////////////////////////////////////
00056 // Static ValidityChecker methods
00057 ///////////////////////////////////////////////////////////////////////////////
00058 
00059 
00060 
00061 ValidityChecker* ValidityChecker::create(const CLFlags& flags)
00062 {
00063   return new VCL(flags);
00064 }
00065 
00066 
00067 CLFlags ValidityChecker::createFlags() {
00068   CLFlags flags;
00069   // We expect the user to type cvc3 -h to get help, which will set
00070   // the "help" flag to false; that's why it's initially true.
00071 
00072   // Overall system control flags
00073   flags.addFlag("timeout", CLFlag(0, "Kill cvc3 process after given number of seconds (0==no limit)"));
00074   flags.addFlag("resource", CLFlag(0, "Set finite resource limit (0==no limit)"));
00075   flags.addFlag("mm", CLFlag("chunks", "Memory manager (chunks, malloc)"));
00076 
00077   // Information printing flags
00078   flags.addFlag("help",CLFlag(true, "print usage information and exit"));
00079   flags.addFlag("version",CLFlag(true, "print version information and exit"));
00080   flags.addFlag("interactive", CLFlag(false, "Interactive mode"));
00081   flags.addFlag("stats", CLFlag(false, "Print run-time statistics"));
00082   flags.addFlag("seed", CLFlag(1, "Set the seed for random sequence"));
00083   flags.addFlag("printResults", CLFlag(true, "Print results of interactive commands."));
00084   flags.addFlag("dump-log", CLFlag("", "Dump API call log in CVC3 input "
00085            "format to given file "
00086            "(off when file name is \"\")"));
00087 
00088   //Translation related flags
00089   flags.addFlag("expResult", CLFlag("", "For smtlib translation.  Give the expected result"));
00090   flags.addFlag("category", CLFlag("unknown", "For smtlib translation.  Give the category"));
00091   flags.addFlag("translate", CLFlag(false, "Produce a complete translation from "
00092                                            "the input language to output language.  "));
00093   flags.addFlag("real2int", CLFlag(false, "When translating, convert reals to integers."));
00094   flags.addFlag("convertArith", CLFlag(false, "When translating, try to rewrite arith terms into smt-lib subset"));
00095   flags.addFlag("convert2diff", CLFlag("", "When translating, try to force into difference logic.  Legal values are int and real."));
00096   flags.addFlag("iteLiftArith", CLFlag(false, "For translation.  If true, ite's are lifted out of arith exprs."));
00097   flags.addFlag("convertArray", CLFlag(false, "For translation.  If true, arrays are converted to uninterpreted functions if possible."));
00098   flags.addFlag("combineAssump", CLFlag(false, "For translation.  If true, assumptions are combined into the query."));
00099 
00100   // Parser related flags
00101   flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax"));
00102 
00103   // Pretty-printing related flags
00104   flags.addFlag("dagify-exprs",
00105     CLFlag(true, "Print expressions with sharing as DAGs"));
00106   flags.addFlag("lang", CLFlag("presentation", "Input language "
00107              "(presentation, smtlib, internal)"));
00108   flags.addFlag("output-lang", CLFlag("", "Output language "
00109               "(presentation, smtlib, simplify, internal, lisp)"));
00110   flags.addFlag("indent", CLFlag(false, "Print expressions with indentation"));
00111   flags.addFlag("width", CLFlag(80, "Suggested line width for printing"));
00112   flags.addFlag("print-depth", CLFlag(-1, "Max. depth to print expressions "));
00113   flags.addFlag("print-assump", CLFlag(false, "Print assumptions in Theorems "));
00114 
00115   // Search Engine (SAT) related flags
00116   flags.addFlag("sat",CLFlag("minisat", "choose a SAT solver to use "
00117            "(fast, simple, sat, minisat)"));
00118   flags.addFlag("de",CLFlag("dfs", "choose a decision engine to use "
00119           "(dfs, sat)"));
00120 
00121   // Proofs and Assumptions
00122   flags.addFlag("proofs", CLFlag(false, "Produce proofs"));
00123   flags.addFlag("check-proofs",
00124     CLFlag(IF_DEBUG(true ||) false, "Check proofs on-the-fly"));
00125   flags.addFlag("minimizeClauses", CLFlag(false, "Use brute-force minimization of clauses"));
00126 
00127   // Core framework switches
00128   flags.addFlag("tcc", CLFlag(false, "Check TCCs for each ASSERT and QUERY"));
00129   flags.addFlag("cnf", CLFlag(true, "Convert top-level Boolean formulas to CNF"));
00130   flags.addFlag("ignore-cnf-vars", CLFlag(false, "Do not split on aux. CNF vars (with +cnf)"));
00131   flags.addFlag("orig-formula", CLFlag(false, "Preserve the original formula with +cnf (for splitter heuristics)"));
00132   flags.addFlag("iflift", CLFlag(false, "Translate if-then-else terms to CNF (with +cnf)"));
00133   flags.addFlag("circuit", CLFlag(false, "With +cnf, use circuit propagation"));
00134   flags.addFlag("un-ite-ify", CLFlag(false, "Unconvert ITE expressions"));
00135   flags.addFlag("ite-cond-simp",
00136     CLFlag(false, "Replace ITE condition by TRUE/FALSE in subexprs"));
00137   flags.addFlag("pp-pushneg", CLFlag(false, "Push negation in preprocessor"));
00138   flags.addFlag("pushneg", CLFlag(true, "Push negation while simplifying"));
00139   flags.addFlag("simp-and", CLFlag(false, "Rewrite x&y to x&y[x/true]"));
00140   flags.addFlag("simp-or", CLFlag(false, "Rewrite x|y to x|y[x/false]"));
00141   // Concrete model generation (counterexamples) flags
00142   flags.addFlag("applications", CLFlag(true, "Add relevant function applications and array accesses to the concrete countermodel"));
00143   // Debugging flags (only for the debug build)
00144   // #ifdef DEBUG
00145   vector<pair<string,bool> > sv;
00146   flags.addFlag("trace", CLFlag(sv, "Tracing.  Multiple flags add up."));
00147   flags.addFlag("dump-trace", CLFlag("", "Dump debugging trace to "
00148            "given file (off when file name is \"\")"));
00149   // #endif
00150   // DP-specific flags
00151 
00152   // Arithmetic
00153   flags.addFlag("arith-new",CLFlag(false, "Use new arithmetic dp"));
00154   flags.addFlag("var-order",
00155     CLFlag(false, "Use simple variable order in arith"));
00156   flags.addFlag("ineq-delay", CLFlag(10, "Accumulate this many inequalities "
00157              "before processing"));
00158 
00159   // Arrays
00160   flags.addFlag("liftReadIte", CLFlag(true, "Lift read of ite"));
00161 
00162   // Quantifiers
00163   flags.addFlag("max-quant-inst", CLFlag(200, "The maximum number of"
00164               " naive instantiations"));
00165 
00166   flags.addFlag("quant-new",
00167      CLFlag(true, "Use new quantifier instantiation algorithm"));
00168 
00169   flags.addFlag("quant-lazy", CLFlag(false, "Instantiate lazily"));
00170 
00171   flags.addFlag("quant-sem-match",
00172                 CLFlag(false, "Attempt to match semantically when instantiating"));
00173 
00174   flags.addFlag("quant-const-match",
00175                 CLFlag(true, "When matching semantically, only match with constants"));
00176 
00177   flags.addFlag("quant-match-old",
00178     CLFlag(false, "Use the old match algorithm"));
00179 
00180   flags.addFlag("quant-inst-part", 
00181                 CLFlag(false, "Use partial instantiation"));
00182 
00183   flags.addFlag("quant-inst-mult", 
00184                 CLFlag(true, "Use multi-triggers in instantiation"));
00185 
00186   flags.addFlag("quant-trig-new", 
00187     CLFlag(true, "Use new trig algorithms"));
00188 
00189   flags.addFlag("quant-max-inst", 
00190     CLFlag(600, "The maximum number of instantiations"));
00191 
00192   flags.addFlag("quant-inst-end", 
00193     CLFlag(true, "Use end heuristic"));
00194 
00195   flags.addFlag("quant-inst-lcache", 
00196                 CLFlag(true, "Cache instantiations"));
00197 
00198   flags.addFlag("quant-inst-gcache", 
00199                 CLFlag(false, "Cache instantiations"));
00200 
00201   flags.addFlag("quant-inst-true", 
00202                 CLFlag(true, "Ignore true instantiations"));
00203 
00204   flags.addFlag("quant-pullvar", 
00205                 CLFlag(false, "Pull out vars"));
00206 
00207   flags.addFlag("quant-trig-loop", 
00208                 CLFlag(0, "Trigger loop prevention method, 0, 1, 2"));
00209 
00210   flags.addFlag("quant-score", 
00211                 CLFlag(true, "Use instantiation level"));
00212 
00213   flags.addFlag("quant-polarity", 
00214                 CLFlag(true, "Use polarity "));
00215 
00216   flags.addFlag("quant-equ", 
00217                 CLFlag(true, "Use equality matching"));
00218 
00219   flags.addFlag("quant-max-score", 
00220                 CLFlag(0, "Maximum initial dynamic score"));
00221 
00222   flags.addFlag("quant-inst-all", 
00223                 CLFlag(false, "try all possible instantiation eagerly"));
00224 
00225   flags.addFlag("quant-trans3", 
00226                 CLFlag(true, "Use trans heuristic"));
00227 
00228   flags.addFlag("quant-trans2", 
00229                 CLFlag(true, "Use trans2 heuristic"));
00230 
00231   flags.addFlag("quant-naive-num", 
00232                 CLFlag(100, "Maximum number to call niave instantiation"));
00233 
00234   
00235   //Bitvectors
00236   flags.addFlag("bv32-flag",
00237     CLFlag(false, "assume that all bitvectors are 32bits with no overflow"));
00238   flags.addFlag("bv-rewrite",
00239     CLFlag(true, "Rewrite bitvector expressions"));
00240   flags.addFlag("bv-concatnormal-rewrite",
00241     CLFlag(true, "Concat Normal Form rewrites"));
00242   flags.addFlag("bv-plusnormal-rewrite",
00243     CLFlag(true, "Bvplus Normal Form rewrites"));
00244   flags.addFlag("bv-rw-bitblast",
00245     CLFlag(false, "Rewrite while bit-blasting"));
00246   flags.addFlag("bv-cnf-bitblast", 
00247     CLFlag(true,"Bitblast equalities in CNFconverter with +cnf"));
00248   flags.addFlag("bv-lhs-minus-rhs", 
00249     CLFlag(false,"Do lhs-rhs=0 if both lhs/rhs are BVPLUS"));
00250   flags.addFlag("bv-pushnegation", 
00251     CLFlag(true,"pushnegation to the leaves"));
00252 
00253   // Uninterpreted Functions
00254   flags.addFlag("trans-closure",
00255     CLFlag(false,"enables transitive closure of binary relations"));
00256 
00257   // Datatypes
00258   flags.addFlag("dt-smartsplits",
00259                 CLFlag(true, "enables smart splitting in datatype theory"));
00260   flags.addFlag("dt-lazy",
00261                 CLFlag(false, "lazy splitting on datatypes"));
00262 
00263   return flags;
00264 }
00265 
00266 
00267 ValidityChecker* ValidityChecker::create()
00268 {
00269   return new VCL(createFlags());
00270 }
00271 
00272 
00273 ///////////////////////////////////////////////////////////////////////////////
00274 // VCL private methods
00275 ///////////////////////////////////////////////////////////////////////////////
00276 
00277 
00278 Theorem3 VCL::deriveClosure(const Theorem3& thm) {
00279   vector<Expr> assump;
00280   set<UserAssertion> assumpSet;
00281   // Compute the vector of assumptions for thm, and iteratively move
00282   // the assumptions to the RHS until done.  Each closure step may
00283   // introduce new assumptions from the proofs of TCCs, so those need
00284   // to be dealt with in the same way, until no assumptions remain.
00285   Theorem3 res = thm;
00286   vector<Theorem> tccs;
00287   while(true) {
00288     {
00289       const Assumptions& a(res.getAssumptionsRef());
00290       if (a.empty()) break;
00291       assump.clear();
00292       assumpSet.clear();
00293       Assumptions::iterator i=a.begin(), iend=a.end();
00294       if(i!=iend) i->clearAllFlags();
00295       // Collect the assumptions of 'res' *without* TCCs
00296       for(; i!=iend; ++i)
00297         getAssumptionsRec(*i, assumpSet, false);
00298 
00299       // Build the vectors of assumptions and TCCs
00300       if(getFlags()["tcc"].getBool()) {
00301         tccs.clear();
00302         for(set<UserAssertion>::iterator i=assumpSet.begin(),
00303               iend=assumpSet.end(); i!=iend; ++i) {
00304           assump.push_back(i->thm().getExpr());
00305           tccs.push_back(i->tcc());
00306         }
00307       }
00308     }
00309     // Derive the closure
00310     res = d_se->getCommonRules()->implIntro3(res, assump, tccs);
00311   }
00312   return res;
00313 }
00314 
00315 
00316 //! Recursive assumption graph traversal to find user assumptions
00317 /*!
00318  *  If an assumption has a TCC, traverse the proof of TCC and add its
00319  *  assumptions to the set recursively.
00320  */
00321 void VCL::getAssumptionsRec(const Theorem& thm,
00322           set<UserAssertion>& assumptions,
00323           bool addTCCs) {
00324   if(thm.isNull() || thm.isRefl() || thm.isFlagged()) return;
00325   thm.setFlag();
00326   if(thm.isAssump()) {
00327     if(d_userAssertions->count(thm.getExpr())>0) {
00328       const UserAssertion& a = (*d_userAssertions)[thm.getExpr()];
00329       assumptions.insert(a);
00330       if(addTCCs) {
00331   DebugAssert(!a.tcc().isNull(), "getAssumptionsRec(a="
00332         +a.thm().toString()+", thm = "+thm.toString()+")");
00333   getAssumptionsRec(a.tcc(), assumptions, true);
00334       }
00335     } else { // it's a splitter
00336       UserAssertion a(thm, Theorem(), d_nextIdx++);
00337       assumptions.insert(a);
00338     }
00339   }
00340   else {
00341     const Assumptions& a(thm.getAssumptionsRef());
00342     for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
00343       getAssumptionsRec(*i, assumptions, addTCCs);
00344   }
00345 }
00346 
00347 
00348 void VCL::getAssumptions(const Assumptions& a, vector<Expr>& assumptions)
00349 {
00350   set<UserAssertion> assumpSet;
00351   if(a.empty()) return;
00352   Assumptions::iterator i=a.begin(), iend=a.end();
00353   if(i!=iend) i->clearAllFlags();
00354   for(; i!=iend; ++i)
00355     getAssumptionsRec(*i, assumpSet, getFlags()["tcc"].getBool());
00356   // Order assumptions by their creation time
00357   for(set<UserAssertion>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00358       i!=iend; ++i)
00359     assumptions.push_back(i->thm().getExpr());
00360 }
00361 
00362 
00363 IF_DEBUG(
00364 void VCL::dumpTrace(int scope) {
00365   vector<StrPair> fields;
00366   fields.push_back(strPair("scope", int2string(scope)));
00367   debugger.dumpTrace("scope", fields);
00368 }
00369 )
00370 
00371 
00372 ///////////////////////////////////////////////////////////////////////////////
00373 // Public VCL methods
00374 ///////////////////////////////////////////////////////////////////////////////
00375 
00376 
00377 VCL::VCL(const CLFlags& flags)
00378   : d_flags(new CLFlags(flags)), d_nextIdx(0)
00379 {
00380   // Set the dependent flags so that they are consistent
00381 
00382   if ((*d_flags)["translate"].getBool())
00383     d_flags->setFlag("printResults", false);
00384 
00385   IF_DEBUG( // Initialize the global debugger
00386      CVC3::debugger.init(&((*d_flags)["trace"].getStrVec()),
00387                                &((*d_flags)["dump-trace"].getString()))
00388   );
00389 
00390   d_cm = new ContextManager();
00391 
00392   // Initialize the database of user assertions.  It has to be
00393   // initialized after d_cm.
00394   d_userAssertions = new(true) CDMap<Expr,UserAssertion>(getCurrentContext());
00395 
00396   d_em = new ExprManager(d_cm, *d_flags);
00397 
00398   d_tm = new TheoremManager(d_cm, d_em, *d_flags);
00399   d_em->setTM(d_tm);
00400 
00401   d_translator = new Translator(d_em,
00402                                 (*d_flags)["translate"].getBool(),
00403                                 (*d_flags)["real2int"].getBool(),
00404                                 (*d_flags)["convertArith"].getBool(),
00405                                 (*d_flags)["convert2diff"].getString(),
00406                                 (*d_flags)["iteLiftArith"].getBool(),
00407                                 (*d_flags)["expResult"].getString(),
00408                                 (*d_flags)["category"].getString(),
00409                                 (*d_flags)["convertArray"].getBool(),
00410                                 (*d_flags)["combineAssump"].getBool());
00411 
00412   d_dump = d_translator->start((*d_flags)["dump-log"].getString());
00413 
00414   d_theoryCore = new TheoryCore(d_cm, d_em, d_tm, d_translator, *d_flags, d_statistics);
00415   d_theories.push_back(d_theoryCore);
00416 
00417   // Fast rewriting of literals is done by setting their find to true or false.
00418   falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr()));
00419   trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr()));
00420 
00421   d_theories.push_back(d_theoryUF = new TheoryUF(d_theoryCore));
00422 
00423   if ((*d_flags)["arith-new"].getBool()) {
00424     d_theories.push_back(d_theoryArith = new TheoryArithNew(d_theoryCore));
00425   }
00426   else {
00427     d_theories.push_back(d_theoryArith = new TheoryArithOld(d_theoryCore));
00428   }
00429   d_theories.push_back(d_theoryArray = new TheoryArray(d_theoryCore));
00430   d_theories.push_back(d_theoryRecords = new TheoryRecords(d_theoryCore));
00431   d_theories.push_back(d_theorySimulate = new TheorySimulate(d_theoryCore));
00432   d_theories.push_back(d_theoryBitvector = new TheoryBitvector(d_theoryCore));
00433   if ((*d_flags)["dt-lazy"].getBool()) {
00434     d_theories.push_back(d_theoryDatatype = new TheoryDatatypeLazy(d_theoryCore));
00435   }
00436   else {
00437     d_theories.push_back(d_theoryDatatype = new TheoryDatatype(d_theoryCore));
00438   }
00439   d_theories.push_back(d_theoryQuant = new TheoryQuant(d_theoryCore));
00440 
00441   d_translator->setTheoryCore(d_theoryCore);
00442   d_translator->setTheoryUF(d_theoryUF);
00443   d_translator->setTheoryArith(d_theoryArith);
00444   d_translator->setTheoryArray(d_theoryArray);
00445   d_translator->setTheoryQuant(d_theoryQuant);
00446   d_translator->setTheoryRecords(d_theoryRecords);
00447   d_translator->setTheorySimulate(d_theorySimulate);
00448   d_translator->setTheoryBitvector(d_theoryBitvector);
00449   d_translator->setTheoryDatatype(d_theoryDatatype);
00450 
00451   // Must be created after TheoryCore, since it needs it.
00452   // When we have more than one search engine, select one to create
00453   // based on flags
00454   const string& satEngine = (*d_flags)["sat"].getString();
00455   if (satEngine == "simple")
00456     d_se = new SearchSimple(d_theoryCore); 
00457   else if (satEngine == "fast")
00458     d_se = new SearchEngineFast(d_theoryCore);
00459   else if (satEngine == "sat" || satEngine == "minisat")
00460     d_se = new SearchSat(d_theoryCore, satEngine);
00461   else
00462     throw CLException("Unrecognized SAT solver name: "
00463                       +(*d_flags)["sat"].getString());
00464 
00465   // Initial scope level should be 1
00466   d_cm->push();
00467 
00468   d_stackLevel = new(true) CDO<int>(d_cm->getCurrentContext(), 0);
00469 
00470   d_theoryCore->setResourceLimit((unsigned)((*d_flags)["resource"].getInt()));
00471 
00472   myvcl = this;
00473 }
00474 
00475 
00476 VCL::~VCL()
00477 {
00478   popto(0);
00479   d_cm->popto(0);
00480   delete d_stackLevel;
00481   free(d_stackLevel);
00482   d_translator->finish();
00483   delete d_translator;
00484 
00485   TRACE_MSG("delete", "Deleting SearchEngine {");
00486   delete d_se;
00487   TRACE_MSG("delete", "Finished deleting SearchEngine }");
00488   // This map contains expressions and theorems; delete it before
00489   // d_em, d_tm, and d_cm.
00490   TRACE_MSG("delete", "Deleting d_userAssertions {");
00491   delete d_userAssertions;
00492   free(d_userAssertions);
00493   TRACE_MSG("delete", "Finished deleting d_userAssertions }");
00494   // and set these to null so their destructors don't blow up
00495   d_lastQuery = Theorem3();
00496   d_lastQueryTCC = Theorem();
00497   d_lastClosure = Theorem3();
00498   // Delete ExprManager BEFORE TheoremManager, since Exprs use Theorems
00499   TRACE_MSG("delete", "Clearing d_em {");
00500   d_em->clear();
00501   d_tm->clear();
00502   TRACE_MSG("delete", "Finished clearing d_em }");
00503   TRACE_MSG("delete", "Deleting d_cm {");
00504   delete d_cm;
00505   TRACE_MSG("delete", "Finished deleting d_cm }");
00506 
00507   for(size_t i=0; i<d_theories.size(); ++i) {
00508     string name(d_theories[i]->getName());
00509     TRACE("delete", "Deleting Theory[", name, "] {");
00510     delete d_theories[i];
00511     TRACE("delete", "Finished deleting Theory[", name, "] }");
00512   }
00513   // TheoremManager does not call ~Theorem() destructors, and only
00514   // releases memory.  At worst, we'll lose some Assumptions.
00515   TRACE_MSG("delete", "Deleting d_tm {");
00516   delete d_tm;
00517   TRACE_MSG("delete", "Finished deleting d_tm }");
00518 
00519   TRACE_MSG("delete", "Deleting d_em {");
00520   delete d_em;
00521   TRACE_MSG("delete", "Finished deleting d_em }");
00522 
00523   TRACE_MSG("delete", "Deleting d_flags [end of ~VCL()]");
00524   delete d_flags;
00525   // No more TRACE-ing after this point (it needs d_flags)
00526 }
00527 
00528 
00529 void VCL::reprocessFlags() {
00530   if (d_se->getName() != (*d_flags)["sat"].getString()) {
00531     delete d_se;
00532     const string& satEngine = (*d_flags)["sat"].getString();
00533     if (satEngine == "simple")
00534       d_se = new SearchSimple(d_theoryCore); 
00535     else if (satEngine == "fast")
00536       d_se = new SearchEngineFast(d_theoryCore);
00537     else if (satEngine == "sat" || satEngine == "minisat")
00538       d_se = new SearchSat(d_theoryCore, satEngine);
00539     else
00540       throw CLException("Unrecognized SAT solver name: "
00541                         +(*d_flags)["sat"].getString());
00542   }
00543 
00544   if (d_theoryArith->getName() == "ArithmeticOld" &&
00545       (*d_flags)["arith-new"].getBool()) {
00546     delete d_theoryArith;
00547     d_theoryArith = new TheoryArithNew(d_theoryCore);
00548     d_theories[2] = d_theoryArith;
00549     d_translator->setTheoryArith(d_theoryArith);
00550   }
00551   else if (d_theoryArith->getName() == "ArithmeticNew" &&
00552            !(*d_flags)["arith-new"].getBool()) {
00553     delete d_theoryArith;
00554     d_theoryArith = new TheoryArithOld(d_theoryCore);
00555     d_theories[2] = d_theoryArith;
00556     d_translator->setTheoryArith(d_theoryArith);
00557   }
00558 
00559   //TODO: handle more flags
00560 }
00561 
00562 TheoryCore* VCL::core(){
00563   return d_theoryCore;
00564 }
00565 
00566 Type VCL::boolType(){
00567   return d_theoryCore->boolType();
00568 }
00569 
00570 
00571 Type VCL::realType()
00572 {
00573   return d_theoryArith->realType();
00574 }
00575 
00576 
00577 Type VCL::intType() {
00578   return d_theoryArith->intType();
00579 }
00580 
00581 
00582 Type VCL::subrangeType(const Expr& l, const Expr& r) {
00583   return d_theoryArith->subrangeType(l, r);
00584 }
00585 
00586 
00587 Type VCL::subtypeType(const Expr& pred, const Expr& witness)
00588 {
00589   return d_theoryCore->newSubtypeExpr(pred, witness);
00590 }
00591 
00592 
00593 Type VCL::tupleType(const Type& type0, const Type& type1)
00594 {
00595   vector<Type> types;
00596   types.push_back(type0);
00597   types.push_back(type1);
00598   return d_theoryRecords->tupleType(types);
00599 }
00600 
00601 
00602 Type VCL::tupleType(const Type& type0, const Type& type1, const Type& type2)
00603 {
00604   vector<Type> types;
00605   types.push_back(type0);
00606   types.push_back(type1);
00607   types.push_back(type2);
00608   return d_theoryRecords->tupleType(types);
00609 }
00610 
00611 
00612 Type VCL::tupleType(const vector<Type>& types)
00613 {
00614   return d_theoryRecords->tupleType(types);
00615 }
00616 
00617 
00618 Type VCL::recordType(const string& field, const Type& type)
00619 {
00620   vector<string> fields;
00621   vector<Type> kids;
00622   fields.push_back(field);
00623   kids.push_back(type);
00624   return Type(d_theoryRecords->recordType(fields, kids));
00625 }
00626 
00627 
00628 Type VCL::recordType(const string& field0, const Type& type0,
00629          const string& field1, const Type& type1) {
00630   vector<string> fields;
00631   vector<Type> kids;
00632   fields.push_back(field0);
00633   fields.push_back(field1);
00634   kids.push_back(type0);
00635   kids.push_back(type1);
00636   sort2(fields, kids);
00637   return Type(d_theoryRecords->recordType(fields, kids));
00638 }
00639 
00640 
00641 Type VCL::recordType(const string& field0, const Type& type0,
00642          const string& field1, const Type& type1,
00643          const string& field2, const Type& type2)
00644 {
00645   vector<string> fields;
00646   vector<Type> kids;
00647   fields.push_back(field0);
00648   fields.push_back(field1);
00649   fields.push_back(field2);
00650   kids.push_back(type0);
00651   kids.push_back(type1);
00652   kids.push_back(type2);
00653   sort2(fields, kids);
00654   return Type(d_theoryRecords->recordType(fields, kids));
00655 }
00656 
00657 
00658 Type VCL::recordType(const vector<string>& fields,
00659          const vector<Type>& types)
00660 {
00661   DebugAssert(fields.size() == types.size(),
00662         "VCL::recordType: number of fields is different \n"
00663         "from the number of types");
00664   // Create copies of the vectors to sort them
00665   vector<string> fs(fields);
00666   vector<Type> ts(types);
00667   sort2(fs, ts);
00668   return Type(d_theoryRecords->recordType(fs, ts));
00669 }
00670 
00671 
00672 Type VCL::dataType(const string& name,
00673                    const string& constructor,
00674                    const vector<string>& selectors, const vector<Expr>& types)
00675 {
00676   vector<string> constructors;
00677   constructors.push_back(constructor);
00678 
00679   vector<vector<string> > selectorsVec;
00680   selectorsVec.push_back(selectors);
00681 
00682   vector<vector<Expr> > typesVec;
00683   typesVec.push_back(types);
00684 
00685   return dataType(name, constructors, selectorsVec, typesVec);
00686 }
00687 
00688 
00689 Type VCL::dataType(const string& name,
00690                    const vector<string>& constructors,
00691                    const vector<vector<string> >& selectors,
00692                    const vector<vector<Expr> >& types)
00693 {
00694   return d_theoryDatatype->dataType(name, constructors, selectors, types);
00695 }
00696 
00697 
00698 void VCL::dataType(const vector<string>& names,
00699                    const vector<vector<string> >& constructors,
00700                    const vector<vector<vector<string> > >& selectors,
00701                    const vector<vector<vector<Expr> > >& types,
00702                    vector<Type>& returnTypes)
00703 {
00704   d_theoryDatatype->dataType(names, constructors, selectors, types, returnTypes);
00705 }
00706 
00707 
00708 Type VCL::arrayType(const Type& typeIndex, const Type& typeData)
00709 {
00710   return ::arrayType(typeIndex, typeData);
00711 }
00712 
00713 
00714 Type VCL::bitvecType(int n)
00715 {
00716   return d_theoryBitvector->newBitvectorType(n);
00717 }
00718 
00719 
00720 Type VCL::funType(const Type& typeDom, const Type& typeRan)
00721 {
00722   return typeDom.funType(typeRan);
00723 }
00724 
00725 
00726 Type VCL::funType(const vector<Type>& typeDom, const Type& typeRan) {
00727   DebugAssert(typeDom.size() >= 1, "VCL::funType: missing domain types");
00728   return Type::funType(typeDom, typeRan);
00729 }
00730 
00731 
00732 Type VCL::createType(const string& typeName)
00733 {
00734   if(d_dump) {
00735     d_translator->dump(Expr(TYPE, listExpr(idExpr(typeName))));
00736   }
00737   return d_theoryCore->newTypeExpr(typeName);
00738 }
00739 
00740 
00741 Type VCL::createType(const string& typeName, const Type& def)
00742 {
00743   if (d_dump) {
00744     d_translator->dump(Expr(TYPE, idExpr(typeName), def.getExpr()), true);
00745   }
00746   return d_theoryCore->newTypeExpr(typeName, def);
00747 }
00748 
00749 
00750 Type VCL::lookupType(const string& typeName)
00751 {
00752   // TODO: check if it already exists
00753   return d_theoryCore->newTypeExpr(typeName);
00754 }
00755 
00756 
00757 Expr VCL::varExpr(const string& name, const Type& type)
00758 {
00759   // Check if the ofstream is open (as opposed to the command line flag)
00760   if(d_dump) {
00761     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
00762   }
00763   return d_theoryCore->newVar(name, type);
00764 }
00765 
00766 
00767 Expr VCL::varExpr(const string& name, const Type& type, const Expr& def)
00768 {
00769   // Check if the ofstream is open (as opposed to the command line flag)
00770   if(d_dump) {
00771     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
00772   }
00773   // Prove the TCCs of the definition
00774   if(getFlags()["tcc"].getBool()) {
00775     Type tpDef(def.getType()), tpVar(type);
00776     // Make sure that def is in the subtype of tpVar; that is, prove
00777     // FORALL (x: tpDef): x = def => typePred(tpVar)(x)
00778     if(tpDef != tpVar) {
00779       // Typecheck the base types
00780       if(getBaseType(tpDef) != getBaseType(type)) {
00781   throw TypecheckException("Type mismatch in constant definition:\n"
00782          "Constant "+name+
00783          " is declared with type:\n  "
00784          +type.toString()
00785          +"\nBut the type of definition is\n  "
00786          +tpDef.toString());
00787       }
00788       TRACE("tccs", "CONST def: "+name+" : "+tpVar.toString()
00789       +" := <value> : ", tpDef, ";");
00790       vector<Expr> boundVars;
00791       boundVars.push_back(boundVarExpr(name, "tcc", tpDef));
00792       Expr body(boundVars[0].eqExpr(def).impExpr(getTypePred(tpVar, boundVars[0])));
00793       Expr quant(forallExpr(boundVars, body));
00794       try {
00795         checkTCC(quant);
00796       } catch(TypecheckException&) {
00797   throw TypecheckException
00798     ("Type mismatch in constant definition:\n"
00799      "Constant "+name+
00800      " is declared with type:\n  "
00801      +type.toString()
00802      +"\nBut the type of definition is\n  "
00803      +def.getType().toString()
00804      +"\n\n which is not a subtype of the constant");
00805       }
00806     }
00807   }
00808   return d_theoryCore->newVar(name, type, def);
00809 }
00810 
00811 
00812 Expr VCL::boundVarExpr(const string& name, const string& uid, 
00813            const Type& type) {
00814   return d_em->newBoundVarExpr(name, uid, type);
00815 }
00816 
00817 
00818 Expr VCL::lookupVar(const string& name, Type* type)
00819 {
00820   return d_theoryCore->lookupVar(name, type);
00821 }
00822 
00823 
00824 Type VCL::getType(const Expr& e)
00825 {
00826   return e.getType();
00827 }
00828 
00829 
00830 Type VCL::getBaseType(const Expr& e)
00831 {
00832   return d_theoryCore->getBaseType(e);
00833 }
00834 
00835 
00836 Type VCL::getBaseType(const Type& t)
00837 {
00838   return d_theoryCore->getBaseType(t);
00839 }
00840 
00841 
00842 Expr VCL::getTypePred(const Type&t, const Expr& e)
00843 {
00844   return d_theoryCore->getTypePred(t, e);
00845 }
00846 
00847 
00848 Expr VCL::stringExpr(const string& str) {
00849   return getEM()->newStringExpr(str);
00850 }
00851 
00852 
00853 Expr VCL::idExpr(const string& name) {
00854   return Expr(ID, stringExpr(name));
00855 }
00856 
00857 
00858 Expr VCL::listExpr(const vector<Expr>& kids) {
00859   return Expr(RAW_LIST, kids, getEM());
00860 }
00861 
00862 
00863 Expr VCL::listExpr(const Expr& e1) {
00864   return Expr(RAW_LIST, e1);
00865 }
00866 
00867 
00868 Expr VCL::listExpr(const Expr& e1, const Expr& e2) {
00869   return Expr(RAW_LIST, e1, e2);
00870 }
00871 
00872 
00873 Expr VCL::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
00874   return Expr(RAW_LIST, e1, e2, e3);
00875 }
00876 
00877 
00878 Expr VCL::listExpr(const string& op, const vector<Expr>& kids) {
00879   vector<Expr> newKids;
00880   newKids.push_back(idExpr(op));
00881   newKids.insert(newKids.end(), kids.begin(), kids.end());
00882   return listExpr(newKids);
00883 }
00884 
00885 
00886 Expr VCL::listExpr(const string& op, const Expr& e1) {
00887   return Expr(RAW_LIST, idExpr(op), e1);
00888 }
00889 
00890 
00891 Expr VCL::listExpr(const string& op, const Expr& e1,
00892        const Expr& e2) {
00893   return Expr(RAW_LIST, idExpr(op), e1, e2);
00894 }
00895 
00896 
00897 Expr VCL::listExpr(const string& op, const Expr& e1,
00898        const Expr& e2, const Expr& e3) {
00899   vector<Expr> kids;
00900   kids.push_back(idExpr(op));
00901   kids.push_back(e1);
00902   kids.push_back(e2);
00903   kids.push_back(e3);
00904   return listExpr(kids);
00905 }
00906 
00907 
00908 void VCL::printExpr(const Expr& e) {
00909   printExpr(e, cout);
00910 }
00911 
00912 
00913 void VCL::printExpr(const Expr& e, ostream& os) {
00914   os << e << endl;
00915 }
00916 
00917 
00918 Expr VCL::parseExpr(const Expr& e) {
00919   return d_theoryCore->parseExprTop(e);
00920 }
00921 
00922 
00923 Type VCL::parseType(const Expr& e) {
00924   return Type(d_theoryCore->parseExpr(e));
00925 }
00926 
00927 
00928 Expr VCL::importExpr(const Expr& e)
00929 {
00930   return d_em->rebuild(e);
00931 }
00932 
00933 
00934 Type VCL::importType(const Type& t)
00935 {
00936   return Type(d_em->rebuild(t.getExpr()));
00937 }
00938 
00939 
00940 Expr VCL::trueExpr()
00941 {
00942   return d_em->trueExpr();
00943 }
00944 
00945 
00946 Expr VCL::falseExpr()
00947 {
00948   return d_em->falseExpr();
00949 }
00950 
00951 
00952 Expr VCL::notExpr(const Expr& child)
00953 {
00954   return !child;
00955 }
00956 
00957 
00958 Expr VCL::andExpr(const Expr& left, const Expr& right)
00959 {
00960   return left && right;
00961 }
00962 
00963 
00964 Expr VCL::andExpr(const vector<Expr>& children)
00965 {
00966   if (children.size() == 0)
00967     throw Exception("andExpr requires at least one child");
00968   return Expr(AND, children);
00969 }
00970 
00971 
00972 Expr VCL::orExpr(const Expr& left, const Expr& right)
00973 {
00974   return left || right;
00975 }
00976 
00977 
00978 Expr VCL::orExpr(const vector<Expr>& children)
00979 {
00980   if (children.size() == 0)
00981     throw Exception("orExpr requires at least one child");
00982   return Expr(OR, children);
00983 }
00984 
00985 
00986 Expr VCL::impliesExpr(const Expr& hyp, const Expr& conc)
00987 {
00988   return hyp.impExpr(conc);
00989 }
00990 
00991 
00992 Expr VCL::iffExpr(const Expr& left, const Expr& right)
00993 {
00994   return left.iffExpr(right);
00995 }
00996 
00997 
00998 Expr VCL::eqExpr(const Expr& child0, const Expr& child1)
00999 {
01000   return child0.eqExpr(child1);
01001 }
01002 
01003 
01004 Expr VCL::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart)
01005 {
01006   return ifpart.iteExpr(thenpart, elsepart);
01007 }
01008 
01009 
01010 Op VCL::createOp(const string& name, const Type& type)
01011 {
01012   if (!type.isFunction())
01013     throw Exception("createOp: expected function type");
01014   if(d_dump) {
01015     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
01016   }
01017   return d_theoryCore->newFunction(name, type,
01018                                    getFlags()["trans-closure"].getBool());
01019 }
01020 
01021 
01022 Op VCL::createOp(const string& name, const Type& type, const Expr& def)
01023 {
01024   if (!type.isFunction())
01025     throw TypecheckException
01026     ("Type error in createOp:\n"
01027      "Constant "+name+
01028      " is declared with type:\n  "
01029      +type.toString()
01030      +"\n which is not a function type");
01031   if (getBaseType(type) != getBaseType(def.getType()))
01032     throw TypecheckException
01033     ("Type mismatch in createOp:\n"
01034      "Function "+name+
01035      " is declared with type:\n  "
01036      +type.toString()
01037      +"\nBut the type of definition is\n  "
01038      +def.getType().toString()
01039      +"\n\n which does not match");
01040   if(d_dump) {
01041     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
01042   }
01043   // Prove the TCCs of the definition
01044   if(getFlags()["tcc"].getBool()) {
01045     Type tpDef(def.getType());
01046     // Make sure that def is within the subtype; that is, prove
01047     // FORALL (xs: argType): typePred_{return_type}(def(xs))
01048     if(tpDef != type) {
01049       vector<Expr> boundVars;
01050       for (int i = 0; i < type.arity()-1; ++i) {
01051         boundVars.push_back(d_em->newBoundVarExpr(type[i]));
01052       }
01053       Expr app = Expr(def.mkOp(), boundVars);
01054       Expr body(getTypePred(type[type.arity()-1], app));
01055       Expr quant(forallExpr(boundVars, body));
01056       Expr tcc = quant.andExpr(d_theoryCore->getTCC(quant));
01057       // Query the subtyping formula
01058       bool typesMatch = true;
01059       try {
01060         checkTCC(tcc);
01061       } catch (TypecheckException&) {
01062         typesMatch = false;
01063       }
01064       if(!typesMatch) {
01065   throw TypecheckException
01066     ("Type mismatch in createOp:\n"
01067      "Function "+name+
01068      " is declared with type:\n  "
01069      +type.toString()
01070      +"\nBut the definition is\n  "
01071      +def.toString()
01072      +"\n\nwhose type could not be proved to be a subtype");
01073       }
01074     }
01075   }
01076   return d_theoryCore->newFunction(name, type, def);
01077 }
01078 
01079 
01080 Expr VCL::funExpr(const Op& op, const Expr& child)
01081 {
01082   return Expr(op, child);
01083 }
01084 
01085 
01086 Expr VCL::funExpr(const Op& op, const Expr& left, const Expr& right)
01087 {
01088   return Expr(op, left, right);
01089 }
01090 
01091 
01092 Expr VCL::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2)
01093 {
01094   return Expr(op, child0, child1, child2);
01095 }
01096 
01097 
01098 Expr VCL::funExpr(const Op& op, const vector<Expr>& children)
01099 {
01100   return Expr(op, children);
01101 }
01102 
01103 
01104 Expr VCL::ratExpr(int n, int d)
01105 {
01106   DebugAssert(d != 0,"denominator cannot be 0");
01107   return d_em->newRatExpr(Rational(n,d));
01108 }
01109 
01110 
01111 Expr VCL::ratExpr(const string& n, const string& d, int base)
01112 {
01113   return d_em->newRatExpr(Rational(n.c_str(), d.c_str(), base));
01114 }
01115 
01116 
01117 Expr VCL::ratExpr(const string& n, int base)
01118 {
01119   string::size_type pos = n.rfind(".");
01120   if (pos == string::npos) {
01121     return d_em->newRatExpr(Rational(n.c_str(), base));
01122   }
01123   string afterdec = n.substr(pos+1);
01124   string beforedec = n.substr(0, pos);
01125   if (afterdec.size() == 0 || beforedec.size() == 0) {
01126     throw Exception("Cannot convert string to rational: "+n);
01127   }
01128   pos = beforedec.rfind(".");
01129   if (pos != string::npos) {
01130     throw Exception("Cannot convert string to rational: "+n);
01131   }
01132   Rational r = Rational(beforedec.c_str(), base);
01133   Rational fracPart = Rational(afterdec.c_str(), base);
01134   r = r + (fracPart / pow(afterdec.size(), base));
01135   return d_em->newRatExpr(r);
01136 }
01137 
01138 
01139 Expr VCL::uminusExpr(const Expr& child)
01140 {
01141   return -child;
01142 }
01143 
01144 
01145 Expr VCL::plusExpr(const Expr& left, const Expr& right)
01146 {
01147   return left + right;
01148 }
01149 
01150 
01151 Expr VCL::minusExpr(const Expr& left, const Expr& right)
01152 {
01153   return left - right;
01154 }
01155 
01156 
01157 Expr VCL::multExpr(const Expr& left, const Expr& right)
01158 {
01159   return left * right;
01160 }
01161 
01162 
01163 Expr VCL::powExpr(const Expr& x, const Expr& n)
01164 {
01165   return ::powExpr(n, x);
01166 }
01167 
01168 
01169 Expr VCL::divideExpr(const Expr& num, const Expr& denom)
01170 {
01171   return ::divideExpr(num,denom);
01172 }
01173 
01174 
01175 Expr VCL::ltExpr(const Expr& left, const Expr& right)
01176 {
01177   return ::ltExpr(left, right);
01178 }
01179 
01180 
01181 Expr VCL::leExpr(const Expr& left, const Expr& right)
01182 {
01183   return ::leExpr(left, right);
01184 }
01185 
01186 
01187 Expr VCL::gtExpr(const Expr& left, const Expr& right)
01188 {
01189   return ::gtExpr(left, right);
01190 }
01191 
01192 
01193 Expr VCL::geExpr(const Expr& left, const Expr& right)
01194 {
01195   return ::geExpr(left, right);
01196 }
01197 
01198 
01199 Expr VCL::recordExpr(const string& field, const Expr& expr)
01200 {
01201   vector<string> fields;
01202   vector<Expr> kids;
01203   kids.push_back(expr);
01204   fields.push_back(field);
01205   return d_theoryRecords->recordExpr(fields, kids);
01206 }
01207 
01208 
01209 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01210          const string& field1, const Expr& expr1)
01211 {
01212   vector<string> fields;
01213   vector<Expr> kids;
01214   fields.push_back(field0);
01215   fields.push_back(field1);
01216   kids.push_back(expr0);
01217   kids.push_back(expr1);
01218   sort2(fields, kids);
01219   return d_theoryRecords->recordExpr(fields, kids);
01220 }
01221 
01222 
01223 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01224          const string& field1, const Expr& expr1,
01225          const string& field2, const Expr& expr2)
01226 {
01227   vector<string> fields;
01228   vector<Expr> kids;
01229   fields.push_back(field0);
01230   fields.push_back(field1);
01231   fields.push_back(field2);
01232   kids.push_back(expr0);
01233   kids.push_back(expr1);
01234   kids.push_back(expr2);
01235   sort2(fields, kids);
01236   return d_theoryRecords->recordExpr(fields, kids);
01237 }
01238 
01239 
01240 Expr VCL::recordExpr(const vector<string>& fields,
01241          const vector<Expr>& exprs)
01242 {
01243   DebugAssert(fields.size() > 0, "VCL::recordExpr()");
01244   DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
01245   // Create copies of the vectors to sort them
01246   vector<string> fs(fields);
01247   vector<Expr> es(exprs);
01248   sort2(fs, es);
01249   return d_theoryRecords->recordExpr(fs, es);
01250 }
01251 
01252 
01253 Expr VCL::recSelectExpr(const Expr& record, const string& field)
01254 {
01255   return d_theoryRecords->recordSelect(record, field);
01256 }
01257 
01258 
01259 Expr VCL::recUpdateExpr(const Expr& record, const string& field,
01260       const Expr& newValue)
01261 {
01262   return d_theoryRecords->recordUpdate(record, field, newValue);
01263 }
01264 
01265 
01266 Expr VCL::readExpr(const Expr& array, const Expr& index)
01267 {
01268   return Expr(READ, array, index);
01269 }
01270 
01271 
01272 Expr VCL::writeExpr(const Expr& array, const Expr& index, const Expr& newValue)
01273 {
01274   return Expr(WRITE, array, index, newValue);
01275 }
01276 
01277 
01278 Expr VCL::newBVConstExpr(const std::string& s, int base)
01279 {
01280   return d_theoryBitvector->newBVConstExpr(s, base);
01281 }
01282 
01283 
01284 Expr VCL::newBVConstExpr(const std::vector<bool>& bits)
01285 {
01286   return d_theoryBitvector->newBVConstExpr(bits);
01287 }
01288 
01289 
01290 Expr VCL::newBVConstExpr(const Rational& r, int len)
01291 {
01292   return d_theoryBitvector->newBVConstExpr(r, len);
01293 }
01294 
01295 
01296 Expr VCL::newConcatExpr(const Expr& t1, const Expr& t2)
01297 {
01298   return d_theoryBitvector->newConcatExpr(t1, t2);
01299 }
01300 
01301 
01302 Expr VCL::newConcatExpr(const std::vector<Expr>& kids)
01303 {
01304   return d_theoryBitvector->newConcatExpr(kids);
01305 }
01306 
01307 
01308 Expr VCL::newBVExtractExpr(const Expr& e, int hi, int low)
01309 {
01310   return d_theoryBitvector->newBVExtractExpr(e, hi, low);
01311 }
01312 
01313 
01314 Expr VCL::newBVNegExpr(const Expr& t1)
01315 {
01316   return d_theoryBitvector->newBVNegExpr(t1);
01317 }
01318 
01319 
01320 Expr VCL::newBVAndExpr(const Expr& t1, const Expr& t2)
01321 {
01322   return d_theoryBitvector->newBVAndExpr(t1, t2);
01323 }
01324 
01325 
01326 Expr VCL::newBVAndExpr(const std::vector<Expr>& kids)
01327 {
01328   return d_theoryBitvector->newBVAndExpr(kids);
01329 }
01330 
01331 
01332 Expr VCL::newBVOrExpr(const Expr& t1, const Expr& t2)
01333 {
01334   return d_theoryBitvector->newBVOrExpr(t1, t2);
01335 }
01336 
01337 
01338 Expr VCL::newBVOrExpr(const std::vector<Expr>& kids)
01339 {
01340   return d_theoryBitvector->newBVOrExpr(kids);
01341 }
01342 
01343 
01344 Expr VCL::newBVXorExpr(const Expr& t1, const Expr& t2)
01345 {
01346   return d_theoryBitvector->newBVXorExpr(t1, t2);
01347 }
01348 
01349 
01350 Expr VCL::newBVXorExpr(const std::vector<Expr>& kids)
01351 {
01352   return d_theoryBitvector->newBVXorExpr(kids);
01353 }
01354 
01355 
01356 Expr VCL::newBVXnorExpr(const Expr& t1, const Expr& t2)
01357 {
01358   return d_theoryBitvector->newBVXnorExpr(t1, t2);
01359 }
01360 
01361 
01362 Expr VCL::newBVXnorExpr(const std::vector<Expr>& kids)
01363 {
01364   return d_theoryBitvector->newBVXnorExpr(kids);
01365 }
01366 
01367 
01368 Expr VCL::newBVNandExpr(const Expr& t1, const Expr& t2)
01369 {
01370   return d_theoryBitvector->newBVNandExpr(t1, t2);
01371 }
01372 
01373 
01374 Expr VCL::newBVNorExpr(const Expr& t1, const Expr& t2)
01375 {
01376   return d_theoryBitvector->newBVNorExpr(t1, t2);
01377 }
01378 
01379 
01380 Expr VCL::newBVLTExpr(const Expr& t1, const Expr& t2)
01381 {
01382   return d_theoryBitvector->newBVLTExpr(t1, t2);
01383 }
01384 
01385 
01386 Expr VCL::newBVLEExpr(const Expr& t1, const Expr& t2)
01387 {
01388   return d_theoryBitvector->newBVLEExpr(t1, t2);
01389 }
01390 
01391 
01392 Expr VCL::newBVSLTExpr(const Expr& t1, const Expr& t2)
01393 {
01394   return d_theoryBitvector->newBVSLTExpr(t1, t2);
01395 }
01396 
01397 
01398 Expr VCL::newBVSLEExpr(const Expr& t1, const Expr& t2)
01399 {
01400   return d_theoryBitvector->newBVSLEExpr(t1, t2);
01401 }
01402 
01403 
01404 Expr VCL::newSXExpr(const Expr& t1, int len)
01405 {
01406   return d_theoryBitvector->newSXExpr(t1, len);
01407 }
01408 
01409 
01410 Expr VCL::newBVUminusExpr(const Expr& t1)
01411 {
01412   return d_theoryBitvector->newBVUminusExpr(t1);
01413 }
01414 
01415 
01416 Expr VCL::newBVSubExpr(const Expr& t1, const Expr& t2)
01417 {
01418   return d_theoryBitvector->newBVSubExpr(t1, t2);
01419 }
01420 
01421 
01422 Expr VCL::newBVPlusExpr(int numbits, const std::vector<Expr>& k)
01423 {
01424   return d_theoryBitvector->newBVPlusExpr(numbits, k);
01425 }
01426 
01427 
01428 Expr VCL::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2)
01429 {
01430   return d_theoryBitvector->newBVMultExpr(numbits, t1, t2);
01431 }
01432 
01433 
01434 Expr VCL::newFixedLeftShiftExpr(const Expr& t1, int r)
01435 {
01436   return d_theoryBitvector->newFixedLeftShiftExpr(t1, r);
01437 }
01438 
01439 
01440 Expr VCL::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r)
01441 {
01442   return d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t1, r);
01443 }
01444 
01445 
01446 Expr VCL::newFixedRightShiftExpr(const Expr& t1, int r)
01447 {
01448   return d_theoryBitvector->newFixedRightShiftExpr(t1, r);
01449 }
01450 
01451 
01452 Expr VCL::tupleExpr(const vector<Expr>& exprs) {
01453   DebugAssert(exprs.size() > 0, "VCL::tupleExpr()");
01454   return d_theoryRecords->tupleExpr(exprs);
01455 }
01456 
01457 
01458 Expr VCL::tupleSelectExpr(const Expr& tuple, int index)
01459 {
01460   return d_theoryRecords->tupleSelect(tuple, index);
01461 }
01462 
01463 
01464 Expr VCL::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue)
01465 {
01466   return d_theoryRecords->tupleUpdate(tuple, index, newValue);
01467 }
01468 
01469 
01470 Expr VCL::datatypeConsExpr(const string& constructor, const vector<Expr>& args)
01471 {
01472   return d_theoryDatatype->datatypeConsExpr(constructor, args);
01473 }
01474 
01475 
01476 Expr VCL::datatypeSelExpr(const string& selector, const Expr& arg)
01477 {
01478   return d_theoryDatatype->datatypeSelExpr(selector, arg);
01479 }
01480 
01481 
01482 Expr VCL::datatypeTestExpr(const string& constructor, const Expr& arg)
01483 {
01484   return d_theoryDatatype->datatypeTestExpr(constructor, arg);
01485 }
01486 
01487 
01488 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body) {
01489   DebugAssert(vars.size() > 0, "VCL::andExpr()");
01490   return d_em->newClosureExpr(FORALL, vars, body);
01491 }
01492 
01493 
01494 Expr VCL::existsExpr(const vector<Expr>& vars, const Expr& body) {
01495   return d_em->newClosureExpr(EXISTS, vars, body);
01496 }
01497 
01498 
01499 Op VCL::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
01500   return d_em->newClosureExpr(LAMBDA, vars, body).mkOp();
01501 }
01502 
01503 
01504 Expr VCL::simulateExpr(const Expr& f, const Expr& s0,
01505            const vector<Expr>& inputs, const Expr& n) {
01506   vector<Expr> kids;
01507   kids.push_back(f);
01508   kids.push_back(s0);
01509   kids.insert(kids.end(), inputs.begin(), inputs.end());
01510   kids.push_back(n);
01511   return Expr(SIMULATE, kids);
01512 }
01513 
01514 
01515 void VCL::setResourceLimit(unsigned limit)
01516 {
01517   d_theoryCore->setResourceLimit(limit);
01518 }
01519 
01520 
01521 Theorem VCL::checkTCC(const Expr& tcc)
01522 {
01523   Theorem tccThm;
01524   d_se->push();
01525   QueryResult res = d_se->checkValid(tcc, tccThm);
01526   switch (res) {
01527     case VALID:
01528       d_lastQueryTCC = tccThm;
01529       d_se->pop();
01530       break;
01531     case INVALID:
01532       throw TypecheckException("Failed TCC:\n\n  "
01533                                +tcc.toString()
01534                                +"\n\nWhich simplified to:\n\n  "
01535                                +simplify(tcc).toString()
01536                                +"\n\nAnd the last formula is not valid "
01537                                "in the current context.");
01538     case ABORT:
01539       throw TypecheckException("Budget exceeded:\n\n  "
01540                                "Unable to verify TCC:\n\n  "                               
01541                                +tcc.toString()
01542                                +"\n\nWhich simplified to:\n\n  "
01543                                +simplify(tcc).toString());
01544     case UNKNOWN:
01545       throw TypecheckException("Result unknown:\n\n  "
01546                                "Unable to verify TCC:\n\n  "
01547                                +tcc.toString()
01548                                +"\n\nWhich simplified to:\n\n  "
01549                                +simplify(tcc).toString()
01550                                +"\n\nAnd the last formula is unknown "
01551                                "in the current context.");
01552     default:
01553       FatalAssert(false, "Unexpected case");
01554   }
01555   return tccThm;
01556 }
01557 
01558 
01559 void VCL::assertFormula(const Expr& e)
01560 {
01561   // Typecheck the user input
01562   if(!e.getType().isBool()) {
01563     throw TypecheckException("Non-BOOLEAN formula in ASSERT:\n  "
01564            +Expr(ASSERT, e).toString()
01565            +"\nDerived type of the formula:\n  "
01566            +e.getType().toString());
01567   }
01568 
01569   // Check if the ofstream is open (as opposed to the command line flag)
01570   if(d_dump) {
01571     if (d_translator->dumpAssertion(e)) return;
01572   }
01573 
01574   TRACE("assetFormula", "VCL::assertFormula(", e, ") {");
01575   // See if e was already asserted before
01576   if(d_userAssertions->count(e) > 0) {
01577     TRACE_MSG("assertFormula", "VCL::assertFormula[repeated assertion] => }");
01578     return;
01579   }
01580   // Check the validity of the TCC
01581   Theorem tccThm;
01582   if(getFlags()["tcc"].getBool()) {
01583     Expr tcc(d_theoryCore->getTCC(e));
01584     tccThm = checkTCC(tcc);
01585   }
01586 
01587   Theorem thm = d_se->newUserAssumption(e);
01588   (*d_userAssertions)[e] = UserAssertion(thm, tccThm, d_nextIdx++);
01589   TRACE_MSG("assertFormula", "VCL::assertFormula => }");
01590 }
01591 
01592 
01593 void VCL::registerAtom(const Expr& e)
01594 {
01595   //TODO: add to interactive interface
01596   d_se->registerAtom(e);
01597 }
01598 
01599 
01600 Expr VCL::getImpliedLiteral()
01601 {
01602   //TODO: add to interactive interface
01603   Theorem thm = d_se->getImpliedLiteral();
01604   if (thm.isNull()) return Expr();
01605   return thm.getExpr();
01606 }
01607 
01608 
01609 Expr VCL::simplify(const Expr& e) {
01610   //TODO: add to interactive interface
01611   return simplifyThm(e).getRHS();
01612 }
01613 
01614 
01615 Theorem VCL::simplifyThm(const Expr& e)
01616 {
01617   e.getType();
01618   Theorem res = d_theoryCore->getExprTrans()->preprocess(e);
01619   Theorem simpThm =  d_theoryCore->simplify(res.getRHS());
01620   res = d_theoryCore->transitivityRule(res, simpThm);
01621   return res;
01622 }
01623 
01624 
01625 QueryResult VCL::query(const Expr& e)
01626 {
01627   TRACE("query", "VCL::query(", e,") {");
01628   // Typecheck the user input
01629   if(!e.getType().isBool()) {
01630     throw TypecheckException("Non-BOOLEAN formula in QUERY:\n  "
01631            +Expr(QUERY, e).toString()
01632            +"\nDerived type of the formula:\n  "
01633            +e.getType().toString());
01634   }
01635 
01636   if(d_dump) {
01637     if (d_translator->dumpQuery(e)) return UNKNOWN;
01638   }
01639 
01640   // Check the validity of the TCC
01641   Theorem tccThm = d_se->getCommonRules()->trueTheorem();
01642   if(getFlags()["tcc"].getBool()) {
01643     Expr tcc(d_theoryCore->getTCC(e));
01644     // FIXME: we have to guarantee that the TCC of 'tcc' is always valid
01645     tccThm = checkTCC(tcc);
01646   }
01647   Theorem res;
01648   QueryResult qres = d_se->checkValid(e, res);
01649   switch (qres) {
01650     case VALID:
01651       d_lastQuery = d_se->getCommonRules()->queryTCC(res, tccThm);
01652       break;
01653     default:
01654       d_lastQueryTCC = Theorem();
01655       d_lastQuery = Theorem3();
01656       d_lastClosure = Theorem3();
01657   }
01658   TRACE("query", "VCL::query => ", 
01659         qres == VALID ? "VALID" :
01660         qres == INVALID ? "INVALID" :
01661         qres == ABORT ? "ABORT" : "UNKNOWN", " }");
01662 
01663   if (d_dump) d_translator->dumpQueryResult(qres);
01664 
01665   return qres;
01666 }
01667 
01668 
01669 QueryResult VCL::checkUnsat(const Expr& e)
01670 {
01671   return query(e.negate());
01672 }
01673 
01674 
01675 QueryResult VCL::checkContinue()
01676 {
01677   if(d_dump) {
01678     d_translator->dump(d_em->newLeafExpr(CONTINUE), true);
01679   }
01680   vector<Expr> assertions;
01681   d_se->getCounterExample(assertions);
01682   Theorem thm;
01683   if (assertions.size() == 0) {
01684     return d_se->restart(falseExpr(), thm);
01685   }
01686   Expr eAnd = assertions.size() == 1 ? assertions[0] : andExpr(assertions);
01687   return d_se->restart(!eAnd, thm);
01688 }
01689 
01690 
01691 QueryResult VCL::restart(const Expr& e)
01692 {
01693   if (d_dump) {
01694     d_translator->dump(Expr(RESTART, e), true);
01695   }
01696   Theorem thm;
01697   return d_se->restart(e, thm);
01698 }
01699 
01700 
01701 void VCL::returnFromCheck()
01702 {
01703   //TODO: add to interactive interface
01704   d_se->returnFromCheck();
01705 }
01706 
01707 
01708 void VCL::getUserAssumptions(vector<Expr>& assumptions)
01709 {
01710   // TODO: add to interactive interface
01711   d_se->getUserAssumptions(assumptions);
01712 }
01713 
01714 
01715 void VCL::getInternalAssumptions(vector<Expr>& assumptions)
01716 {
01717   // TODO: add to interactive interface
01718   d_se->getInternalAssumptions(assumptions);
01719 }
01720 
01721 
01722 void VCL::getAssumptions(vector<Expr>& assumptions)
01723 {
01724   if(d_dump) {
01725     d_translator->dump(d_em->newLeafExpr(ASSUMPTIONS), true);
01726   }
01727   d_se->getAssumptions(assumptions);
01728 }
01729 
01730 
01731 void VCL::getAssumptionsUsed(vector<Expr>& assumptions)
01732 {
01733   if(d_dump) {
01734     d_translator->dump(d_em->newLeafExpr(DUMP_ASSUMPTIONS), true);
01735   }
01736   Theorem thm = d_se->lastThm();
01737   if (thm.isNull()) return;
01738   thm.getLeafAssumptions(assumptions);
01739 }
01740 
01741 
01742 void VCL::getCounterExample(vector<Expr>& assertions, bool inOrder)
01743 {
01744   if(d_dump) {
01745     d_translator->dump(d_em->newLeafExpr(COUNTEREXAMPLE), true);
01746   }
01747   if (!(*d_flags)["translate"].getBool())
01748     d_se->getCounterExample(assertions, inOrder);
01749 }
01750 
01751 
01752 void VCL::getConcreteModel(ExprMap<Expr> & m)
01753 {
01754   if(d_dump) {
01755     d_translator->dump(d_em->newLeafExpr(COUNTERMODEL), true);
01756   }
01757   if (!(*d_flags)["translate"].getBool())
01758     d_se->getConcreteModel(m);
01759 }
01760 
01761 
01762 bool VCL::inconsistent(vector<Expr>& assumptions)
01763 {
01764   // TODO: add to interactive interface
01765   if (d_theoryCore->inconsistent()) {
01766     // TODO: do we need local getAssumptions?
01767     getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
01768        assumptions);
01769     return true;
01770   }
01771   return false;
01772 }
01773 
01774 
01775 bool VCL::incomplete() {
01776   // TODO: add to interactive interface
01777   // Return true only after a failed query
01778   return (d_lastQuery.isNull() && d_theoryCore->incomplete());
01779 }
01780 
01781 
01782 bool VCL::incomplete(vector<string>& reasons) {
01783   // TODO: add to interactive interface
01784   // Return true only after a failed query
01785   return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
01786 }
01787 
01788 
01789 Proof VCL::getProof()
01790 {
01791   if(d_dump) {
01792     d_translator->dump(d_em->newLeafExpr(DUMP_PROOF), true);
01793   }
01794 
01795   if(d_lastQuery.isNull())
01796     throw EvalException
01797       ("Method getProof() (or command DUMP_PROOF)\n"
01798        " must be called only after a Valid QUERY");
01799   return d_se->getProof();
01800 }
01801 
01802 
01803 Expr VCL::getTCC(){
01804   static Expr null;
01805   if(d_dump) {
01806     d_translator->dump(d_em->newLeafExpr(DUMP_TCC), true);
01807   }
01808   if(d_lastQueryTCC.isNull()) return null;
01809   else return d_lastQueryTCC.getExpr();
01810 }
01811 
01812 
01813 void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
01814 {
01815   if(d_dump) {
01816     d_translator->dump(d_em->newLeafExpr(DUMP_TCC_ASSUMPTIONS), true);
01817   }
01818   if(d_lastQuery.isNull())
01819     throw EvalException
01820       ("Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
01821        " must be called only after a Valid QUERY");
01822   getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
01823 }
01824 
01825 
01826 Proof VCL::getProofTCC() {
01827   static Proof null;
01828   if(d_dump) {
01829     d_translator->dump(d_em->newLeafExpr(DUMP_TCC_PROOF), true);
01830   }
01831   if(d_lastQueryTCC.isNull()) return null;
01832   else return d_lastQueryTCC.getProof();
01833 }
01834 
01835 
01836 Expr VCL::getClosure() {
01837   static Expr null;
01838   if(d_dump) {
01839     d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE), true);
01840   }
01841   if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
01842     // Construct the proof of closure and cache it in d_lastClosure
01843     d_lastClosure = deriveClosure(d_lastQuery);
01844   }
01845   if(d_lastClosure.isNull()) return null;
01846   else return d_lastClosure.getExpr();
01847 }
01848 
01849 
01850 Proof VCL::getProofClosure() {
01851   static Proof null;
01852   if(d_dump) {
01853     d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE_PROOF), true);
01854   }
01855   if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
01856     // Construct the proof of closure and cache it in d_lastClosure
01857     d_lastClosure = deriveClosure(d_lastQuery);
01858   }
01859   if(d_lastClosure.isNull()) return null;
01860   else return d_lastClosure.getProof();
01861 }
01862 
01863 
01864 int VCL::stackLevel()
01865 {
01866   return d_stackLevel->get();
01867 }
01868 
01869 
01870 void VCL::push()
01871 {
01872   if(d_dump) {
01873     d_translator->dump(d_em->newLeafExpr(PUSH), true);
01874   }
01875   d_se->push();
01876   d_stackLevel->set(stackLevel()+1);
01877 }
01878 
01879 
01880 void VCL::pop()
01881 {
01882   if(d_dump) {
01883     d_translator->dump(d_em->newLeafExpr(POP), true);
01884   }
01885   if (stackLevel() == 0) {
01886     throw EvalException
01887       ("POP called with no previous call to PUSH");
01888   }
01889   int level = stackLevel();
01890   while (level == stackLevel())
01891     d_se->pop();
01892 }
01893 
01894 
01895 void VCL::popto(int toLevel)
01896 {
01897   // Check if the ofstream is open (as opposed to the command line flag)
01898   if(d_dump) {
01899     d_translator->dump(Expr(POPTO, ratExpr(toLevel, 1)), true);
01900   }
01901   if (toLevel < 0) toLevel = 0;
01902   while (stackLevel() > toLevel) {
01903     d_se->pop();
01904   }
01905 }
01906 
01907 
01908 int VCL::scopeLevel()
01909 {
01910   return d_cm->scopeLevel();
01911 }
01912 
01913 
01914 void VCL::pushScope()
01915 {
01916   throw EvalException ("Scope-level push/pop is no longer supported");
01917   d_cm->push();
01918   if(d_dump) {
01919     d_translator->dump(d_em->newLeafExpr(PUSH_SCOPE), true);
01920   }
01921   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
01922      dumpTrace(scopeLevel()));
01923 }
01924 
01925 
01926 void VCL::popScope()
01927 {
01928   throw EvalException ("Scope-level push/pop is no longer supported");
01929   if(d_dump) {
01930     d_translator->dump(d_em->newLeafExpr(POP_SCOPE), true);
01931   }
01932   if (scopeLevel() == 1) {
01933     cout << "Cannot POP from scope level 1" << endl;
01934   }
01935   else d_cm->pop();
01936   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
01937      dumpTrace(scopeLevel()));
01938 }
01939 
01940 
01941 void VCL::poptoScope(int toLevel)
01942 {
01943   throw EvalException ("Scope-level push/pop is no longer supported");
01944   if(d_dump) {
01945     d_translator->dump(Expr(POPTO_SCOPE, ratExpr(toLevel, 1)), true);
01946   }
01947   if (toLevel < 1) {
01948     d_cm->popto(0);
01949     d_cm->push();
01950   }
01951   else d_cm->popto(toLevel);
01952   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
01953      dumpTrace(scopeLevel()));
01954 }
01955 
01956 
01957 Context* VCL::getCurrentContext()
01958 {
01959   return d_cm->getCurrentContext();
01960 }
01961 
01962 
01963 void VCL::loadFile(const string& fileName, InputLanguage lang,
01964        bool interactive) {
01965   // TODO: move these?
01966   Parser parser(this, lang, interactive, fileName);
01967   VCCmd cmd(this, &parser);
01968   cmd.processCommands();
01969 }
01970 
01971 
01972 void VCL::loadFile(istream& is, InputLanguage lang,
01973        bool interactive) {
01974   // TODO: move these?
01975   Parser parser(this, lang, is, interactive);
01976   VCCmd cmd(this, &parser);
01977   cmd.processCommands();
01978 }
01979 
01980 
01981 unsigned long VCL::printMemory()
01982 {
01983   cout << "VCL: " <<
01984     sizeof(VCL) + d_theories.size() * sizeof(Theory*)
01985        << endl;
01986 
01987   cout << "Context: " << d_cm->getMemory() << endl;
01988   return 0;
01989 //   d_em->printMemory();
01990 //   d_tm->printMemory();
01991 //   d_translator->printMemory();
01992 //   d_se->printMemory();
01993 
01994 //   d_theoryCore->printMemory();
01995   
01996 }

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