CVC3

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_arith3.h"
00034 #include "theory_bitvector.h"
00035 #include "theory_array.h"
00036 #include "theory_quant.h"
00037 #include "theory_records.h"
00038 #include "theory_simulate.h"
00039 #include "theory_datatype.h"
00040 #include "theory_datatype_lazy.h"
00041 #include "translator.h"
00042 #include "typecheck_exception.h"
00043 #include "eval_exception.h"
00044 #include "expr_transform.h"
00045 #include "theorem_manager.h"
00046 #include "assumptions.h"
00047 #include "parser_exception.h"
00048 
00049 
00050 using namespace std;
00051 using namespace CVC3;
00052 
00053 //namespace CVC3{
00054 //  VCL* myvcl;
00055 //}
00056 
00057 ///////////////////////////////////////////////////////////////////////////////
00058 // Static ValidityChecker methods
00059 ///////////////////////////////////////////////////////////////////////////////
00060 
00061 
00062 
00063 ValidityChecker* ValidityChecker::create(const CLFlags& flags)
00064 {
00065   return new VCL(flags);
00066 }
00067 
00068 
00069 CLFlags ValidityChecker::createFlags() {
00070   CLFlags flags;
00071   // We expect the user to type cvc3 -h to get help, which will set
00072   // the "help" flag to false; that's why it's initially true.
00073 
00074   // Overall system control flags
00075   flags.addFlag("timeout", CLFlag(0, "Kill cvc3 process after given number of seconds (0==no limit)"));
00076   flags.addFlag("stimeout", CLFlag(0, "Set time resource limit in tenths of seconds for a query(0==no limit)"));
00077   flags.addFlag("resource", CLFlag(0, "Set finite resource limit (0==no limit)"));
00078   flags.addFlag("mm", CLFlag("chunks", "Memory manager (chunks, malloc)"));
00079 
00080   // Information printing flags
00081   flags.addFlag("help",CLFlag(true, "print usage information and exit"));
00082   flags.addFlag("unsupported",CLFlag(true, "print usage for old/unsupported/experimental options"));
00083   flags.addFlag("version",CLFlag(true, "print version information and exit"));
00084   flags.addFlag("interactive", CLFlag(false, "Interactive mode"));
00085   flags.addFlag("stats", CLFlag(false, "Print run-time statistics"));
00086   flags.addFlag("seed", CLFlag(1, "Set the seed for random sequence"));
00087   flags.addFlag("printResults", CLFlag(true, "Print results of interactive commands."));
00088   flags.addFlag("dump-log", CLFlag("", "Dump API call log in CVC3 input "
00089            "format to given file "
00090            "(off when file name is \"\")"));
00091   flags.addFlag("parse-only", CLFlag(false,"Parse the input, then exit."));
00092 
00093   //Translation related flags
00094   flags.addFlag("expResult", CLFlag("", "For smtlib translation.  Give the expected result", false));
00095   flags.addFlag("category", CLFlag("unknown", "For smtlib translation.  Give the category", false));
00096   flags.addFlag("translate", CLFlag(false, "Produce a complete translation from "
00097                                     "the input language to output language.  "));
00098   flags.addFlag("real2int", CLFlag(false, "When translating, convert reals to integers.", false));
00099   flags.addFlag("convertArith", CLFlag(false, "When translating, try to rewrite arith terms into smt-lib subset", false));
00100   flags.addFlag("convert2diff", CLFlag("", "When translating, try to force into difference logic.  Legal values are int and real.", false));
00101   flags.addFlag("iteLiftArith", CLFlag(false, "For translation.  If true, ite's are lifted out of arith exprs.", false));
00102   flags.addFlag("convertArray", CLFlag(false, "For translation.  If true, arrays are converted to uninterpreted functions if possible.", false));
00103   flags.addFlag("combineAssump", CLFlag(false, "For translation.  If true, assumptions are combined into the query.", false));
00104   flags.addFlag("convert2array", CLFlag(false, "For translation. If true, try to convert to array-only theory", false));
00105   flags.addFlag("convertToBV",CLFlag(0, "For translation.  Set to nonzero to convert ints to bv's of that length", false));
00106   flags.addFlag("convert-eq-iff",CLFlag(false, "Convert equality on Boolean expressions to iff.", false));
00107   flags.addFlag("preSimplify",CLFlag(false, "Simplify each assertion or query before translating it", false));
00108   flags.addFlag("dump-tcc", CLFlag(false, "Compute and dump TCC only"));
00109   flags.addFlag("trans-skip-pp", CLFlag(false, "Skip preprocess step in translation module", false));
00110   flags.addFlag("trans-skip-difficulty", CLFlag(false, "Leave out difficulty attribute during translation to SMT v2.0", false));
00111   flags.addFlag("promote", CLFlag(true, "Promote undefined logic combinations to defined logic combinations during translation to SMT", false));
00112 
00113   // Parser related flags
00114   flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax", false));
00115 
00116   // Pretty-printing related flags
00117   flags.addFlag("dagify-exprs",
00118     CLFlag(true, "Print expressions with sharing as DAGs"));
00119   flags.addFlag("lang", CLFlag("presentation", "Input language "
00120              "(presentation, smt, smt2, internal)"));
00121   flags.addFlag("output-lang", CLFlag("", "Output language "
00122               "(presentation, smtlib, simplify, internal, lisp, tptp, spass)"));
00123   flags.addFlag("indent", CLFlag(false, "Print expressions with indentation"));
00124   flags.addFlag("width", CLFlag(80, "Suggested line width for printing"));
00125   flags.addFlag("print-depth", CLFlag(-1, "Max. depth to print expressions "));
00126   flags.addFlag("print-assump", CLFlag(false, "Print assumptions in Theorems "));
00127 
00128   // Search Engine (SAT) related flags
00129   flags.addFlag("sat",CLFlag("minisat", "choose a SAT solver to use "
00130            "(sat, minisat)"));
00131   flags.addFlag("de",CLFlag("dfs", "choose a decision engine to use "
00132           "(dfs, sat)"));
00133 
00134   // Proofs and Assumptions
00135   flags.addFlag("proofs", CLFlag(false, "Produce proofs"));
00136   flags.addFlag("check-proofs",
00137     CLFlag(IF_DEBUG(true ||) false, "Check proofs on-the-fly"));
00138   flags.addFlag("minimizeClauses", CLFlag(false, "Use brute-force minimization of clauses", false));
00139   flags.addFlag("dynack", CLFlag(false, "Use dynamic Ackermannization", false));
00140   flags.addFlag("smart-clauses", CLFlag(true, "Learn multiple clauses per conflict"));
00141 
00142 
00143   // Core framework switches
00144   flags.addFlag("tcc", CLFlag(false, "Check TCCs for each ASSERT and QUERY"));
00145   flags.addFlag("cnf", CLFlag(true, "Convert top-level Boolean formulas to CNF", false));
00146   flags.addFlag("ignore-cnf-vars", CLFlag(false, "Do not split on aux. CNF vars (with +cnf)", false));
00147   flags.addFlag("orig-formula", CLFlag(false, "Preserve the original formula with +cnf (for splitter heuristics)", false));
00148   flags.addFlag("liftITE", CLFlag(false, "Eagerly lift all ITE exprs"));
00149   flags.addFlag("iflift", CLFlag(false, "Translate if-then-else terms to CNF (with +cnf)", false));
00150   flags.addFlag("circuit", CLFlag(false, "With +cnf, use circuit propagation", false));
00151   flags.addFlag("un-ite-ify", CLFlag(false, "Unconvert ITE expressions", false));
00152   flags.addFlag("ite-cond-simp",
00153     CLFlag(false, "Replace ITE condition by TRUE/FALSE in subexprs", false));
00154   flags.addFlag("preprocess", CLFlag(true, "Preprocess queries"));
00155   flags.addFlag("pp-pushneg", CLFlag(false, "Push negation in preprocessor"));
00156   flags.addFlag("pp-bryant", CLFlag(false, "Enable Bryant algorithm for UF", false));
00157   flags.addFlag("pp-budget", CLFlag(0, "Budget for new preprocessing step", false));
00158   flags.addFlag("pp-care", CLFlag(true, "Enable care-set preprocessing step", false));
00159   flags.addFlag("simp-and", CLFlag(false, "Rewrite x&y to x&y[x/true]", false));
00160   flags.addFlag("simp-or", CLFlag(false, "Rewrite x|y to x|y[x/false]", false));
00161   flags.addFlag("pp-batch", CLFlag(false, "Ignore assumptions until query, then process all at once"));
00162 
00163   // Negate the query when translate into tptp
00164   flags.addFlag("negate-query", CLFlag(true, "Negate the query when translate into TPTP format"));;
00165 
00166   // Concrete model generation (counterexamples) flags
00167   flags.addFlag("counterexample", CLFlag(false, "Dump counterexample if formula is invalid or satisfiable"));
00168   flags.addFlag("model", CLFlag(false, "Dump model if formula is invalid or satisfiable"));
00169   flags.addFlag("unknown-check-model", CLFlag(false, "Try to generate model if formula is unknown"));
00170   flags.addFlag("applications", CLFlag(true, "Add relevant function applications and array accesses to the concrete countermodel"));
00171   // Debugging flags (only for the debug build)
00172   // #ifdef _CVC3_DEBUG_MODE
00173   vector<pair<string,bool> > sv;
00174   flags.addFlag("trace", CLFlag(sv, "Tracing.  Multiple flags add up."));
00175   flags.addFlag("dump-trace", CLFlag("", "Dump debugging trace to "
00176            "given file (off when file name is \"\")"));
00177   // #endif
00178   // DP-specific flags
00179 
00180   // Arithmetic
00181   flags.addFlag("arith-new",CLFlag(false, "Use new arithmetic dp", false));
00182   flags.addFlag("arith3",CLFlag(false, "Use old arithmetic dp that works well with combined theories", false));
00183   flags.addFlag("var-order",
00184     CLFlag(false, "Use simple variable order in arith", false));
00185   flags.addFlag("ineq-delay", CLFlag(0, "Accumulate this many inequalities before processing (-1 for don't process until necessary)"));
00186 
00187   flags.addFlag("nonlinear-sign-split", CLFlag(true, "Whether to split on the signs of nontrivial nonlinear terms"));
00188 
00189   flags.addFlag("grayshadow-threshold", CLFlag(-1, "Ignore gray shadows bigger than this (makes solver incomplete)"));
00190   flags.addFlag("pathlength-threshold", CLFlag(-1, "Ignore gray shadows bigger than this (makes solver incomplete)"));
00191 
00192   // Arrays
00193   flags.addFlag("liftReadIte", CLFlag(true, "Lift read of ite"));
00194 
00195   //for LFSC stuff, disable Tseitin CNF conversion, by Yeting
00196   flags.addFlag("cnf-formula", CLFlag(false, "The input must be in CNF. This option automatically enables '-de sat' and disable preprocess"));
00197 
00198   //for LFSC print out, by Yeting
00199   //flags.addFlag("lfsc", CLFlag(false, "the input is already in CNF. This option automatically enables -de sat and disable -preprocess"));
00200 
00201   // for LFSC print, allows different modes by Liana
00202   flags.addFlag("lfsc-mode",
00203                   CLFlag(0, "lfsc mode 0: off, 1:normal, 2:cvc3-mimic etc."));
00204 
00205 
00206   // Quantifiers
00207   flags.addFlag("max-quant-inst", CLFlag(200, "The maximum number of"
00208               " naive instantiations"));
00209 
00210   flags.addFlag("quant-new",
00211      CLFlag(true, "If this option is false, only naive instantiation is called"));
00212 
00213   flags.addFlag("quant-lazy", CLFlag(false, "Instantiate lazily", false));
00214 
00215   flags.addFlag("quant-sem-match",
00216     CLFlag(false, "Attempt to match semantically when instantiating", false));
00217 
00218 //   flags.addFlag("quant-const-match",
00219 //                 CLFlag(true, "When matching semantically, only match with constants", false));
00220 
00221   flags.addFlag("quant-complete-inst",
00222     CLFlag(false, "Try complete instantiation heuristic.  +pp-batch will be automatically enabled"));
00223 
00224   flags.addFlag("quant-max-IL",
00225     CLFlag(100, "The maximum Instantiation Level allowed"));
00226 
00227   flags.addFlag("quant-inst-lcache",
00228                 CLFlag(true, "Cache instantiations"));
00229 
00230   flags.addFlag("quant-inst-gcache",
00231                 CLFlag(false, "Cache instantiations", false));
00232 
00233   flags.addFlag("quant-inst-tcache",
00234                 CLFlag(false, "Cache instantiations", false));
00235 
00236 
00237   flags.addFlag("quant-inst-true",
00238                 CLFlag(true, "Ignore true instantiations"));
00239 
00240   flags.addFlag("quant-pullvar",
00241                 CLFlag(false, "Pull out vars", false));
00242 
00243   flags.addFlag("quant-score",
00244                 CLFlag(true, "Use instantiation level"));
00245 
00246   flags.addFlag("quant-polarity",
00247                 CLFlag(false, "Use polarity ", false));
00248 
00249   flags.addFlag("quant-eqnew",
00250                 CLFlag(true, "Use new equality matching"));
00251 
00252   flags.addFlag("quant-max-score",
00253                 CLFlag(0, "Maximum initial dynamic score"));
00254 
00255   flags.addFlag("quant-trans3",
00256                 CLFlag(true, "Use trans heuristic"));
00257 
00258   flags.addFlag("quant-trans2",
00259                 CLFlag(true, "Use trans2 heuristic"));
00260 
00261   flags.addFlag("quant-naive-num",
00262                 CLFlag(1000, "Maximum number to call naive instantiation"));
00263 
00264   flags.addFlag("quant-naive-inst",
00265                 CLFlag(true, "Use naive instantiation"));
00266 
00267   flags.addFlag("quant-man-trig",
00268                 CLFlag(true, "Use manual triggers"));
00269 
00270   flags.addFlag("quant-gfact",
00271                 CLFlag(false, "Send facts to core directly", false));
00272 
00273   flags.addFlag("quant-glimit",
00274                 CLFlag(1000, "Limit for gfacts", false));
00275 
00276   flags.addFlag("print-var-type", //by yeting, as requested by Sascha Boehme for proofs
00277                 CLFlag(false, "Print types for bound variables"));
00278 
00279   //Bitvectors
00280   flags.addFlag("bv32-flag",
00281     CLFlag(false, "assume that all bitvectors are 32bits with no overflow", false));
00282 
00283   // Uninterpreted Functions
00284   flags.addFlag("trans-closure",
00285     CLFlag(false,"enables transitive closure of binary relations", false));
00286 
00287   // Datatypes
00288   flags.addFlag("dt-smartsplits",
00289                 CLFlag(true, "enables smart splitting in datatype theory", false));
00290   flags.addFlag("dt-lazy",
00291                 CLFlag(false, "lazy splitting on datatypes", false));
00292 
00293 
00294   return flags;
00295 }
00296 
00297 
00298 ValidityChecker* ValidityChecker::create()
00299 {
00300   return new VCL(createFlags());
00301 }
00302 
00303 
00304 ///////////////////////////////////////////////////////////////////////////////
00305 // VCL private methods
00306 ///////////////////////////////////////////////////////////////////////////////
00307 
00308 
00309 Theorem3 VCL::deriveClosure(const Theorem3& thm) {
00310   vector<Expr> assump;
00311   set<UserAssertion> assumpSet;
00312   // Compute the vector of assumptions for thm, and iteratively move
00313   // the assumptions to the RHS until done.  Each closure step may
00314   // introduce new assumptions from the proofs of TCCs, so those need
00315   // to be dealt with in the same way, until no assumptions remain.
00316   Theorem3 res = thm;
00317   vector<Theorem> tccs;
00318   while(true) {
00319     {
00320       const Assumptions& a(res.getAssumptionsRef());
00321       if (a.empty()) break;
00322       assump.clear();
00323       assumpSet.clear();
00324       Assumptions::iterator i=a.begin(), iend=a.end();
00325       if(i!=iend) i->clearAllFlags();
00326       // Collect the assumptions of 'res' *without* TCCs
00327       for(; i!=iend; ++i)
00328         getAssumptionsRec(*i, assumpSet, false);
00329 
00330       // Build the vectors of assumptions and TCCs
00331       if(getFlags()["tcc"].getBool()) {
00332         tccs.clear();
00333         for(set<UserAssertion>::iterator i=assumpSet.begin(),
00334               iend=assumpSet.end(); i!=iend; ++i) {
00335           assump.push_back(i->thm().getExpr());
00336           tccs.push_back(i->tcc());
00337         }
00338       }
00339     }
00340     // Derive the closure
00341     res = d_se->getCommonRules()->implIntro3(res, assump, tccs);
00342   }
00343   return res;
00344 }
00345 
00346 
00347 //! Recursive assumption graph traversal to find user assumptions
00348 /*!
00349  *  If an assumption has a TCC, traverse the proof of TCC and add its
00350  *  assumptions to the set recursively.
00351  */
00352 void VCL::getAssumptionsRec(const Theorem& thm,
00353           set<UserAssertion>& assumptions,
00354           bool addTCCs) {
00355   if(thm.isNull() || thm.isRefl() || thm.isFlagged()) return;
00356   thm.setFlag();
00357   if(thm.isAssump()) {
00358     if(d_userAssertions->count(thm.getExpr())>0) {
00359       const UserAssertion& a = (*d_userAssertions)[thm.getExpr()];
00360       assumptions.insert(a);
00361       if(addTCCs) {
00362   DebugAssert(!a.tcc().isNull(), "getAssumptionsRec(a="
00363         +a.thm().toString()+", thm = "+thm.toString()+")");
00364   getAssumptionsRec(a.tcc(), assumptions, true);
00365       }
00366     } else { // it's a splitter
00367       UserAssertion a(thm, Theorem(), d_nextIdx++);
00368       assumptions.insert(a);
00369     }
00370   }
00371   else {
00372     const Assumptions& a(thm.getAssumptionsRef());
00373     for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
00374       getAssumptionsRec(*i, assumptions, addTCCs);
00375   }
00376 }
00377 
00378 
00379 void VCL::getAssumptions(const Assumptions& a, vector<Expr>& assumptions)
00380 {
00381   set<UserAssertion> assumpSet;
00382   if(a.empty()) return;
00383   Assumptions::iterator i=a.begin(), iend=a.end();
00384   if(i!=iend) i->clearAllFlags();
00385   for(; i!=iend; ++i)
00386     getAssumptionsRec(*i, assumpSet, getFlags()["tcc"].getBool());
00387   // Order assumptions by their creation time
00388   for(set<UserAssertion>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00389       i!=iend; ++i)
00390     assumptions.push_back(i->thm().getExpr());
00391 }
00392 
00393 
00394 IF_DEBUG(
00395 void VCL::dumpTrace(int scope) {
00396   vector<StrPair> fields;
00397   fields.push_back(strPair("scope", int2string(scope)));
00398   debugger.dumpTrace("scope", fields);
00399 }
00400 )
00401 
00402 
00403 ///////////////////////////////////////////////////////////////////////////////
00404 // Public VCL methods
00405 ///////////////////////////////////////////////////////////////////////////////
00406 
00407 
00408 VCL::VCL(const CLFlags& flags)
00409   : d_flags(new CLFlags(flags))
00410 {
00411   // Set the dependent flags so that they are consistent
00412 
00413   if ((*d_flags)["dump-tcc"].getBool()) {
00414     d_flags->setFlag("translate", true);
00415     d_flags->setFlag("pp-batch", true);
00416     d_flags->setFlag("tcc", true);
00417   }
00418 
00419   if ((*d_flags)["translate"].getBool()) {
00420     d_flags->setFlag("printResults", false);
00421   }
00422 
00423   if ((*d_flags)["pp-bryant"].getBool()) {
00424     d_flags->setFlag("pp-batch", true);
00425   }
00426 
00427   //added by Yeting
00428   if ((*d_flags)["quant-complete-inst"].getBool() && !(*d_flags)["translate"].getBool()) {
00429     d_flags->setFlag("pp-batch", true);
00430   }
00431 
00432   //added by Yeting
00433   if ((*d_flags)["cnf-formula"].getBool()) {
00434     d_flags->setFlag("de", "sat");
00435     d_flags->setFlag("preprocess", false);
00436   }
00437 
00438 
00439   IF_DEBUG( // Initialize the global debugger
00440      CVC3::debugger.init(&((*d_flags)["trace"].getStrVec()),
00441                                &((*d_flags)["dump-trace"].getString()));
00442   )
00443   init();
00444 }
00445 
00446 
00447 void VCL::init()
00448 {
00449   d_nextIdx = 0;
00450 
00451   d_statistics = new Statistics();
00452 
00453   d_cm = new ContextManager();
00454 
00455   // Initialize the database of user assertions.  It has to be
00456   // initialized after d_cm.
00457   d_userAssertions = new(true) CDMap<Expr,UserAssertion>(getCurrentContext());
00458   d_batchedAssertions = new(true) CDList<Expr>(getCurrentContext());
00459   d_batchedAssertionsIdx = new(true) CDO<unsigned>(getCurrentContext(), 0);
00460 
00461   d_em = new ExprManager(d_cm, *d_flags);
00462 
00463   d_tm = new TheoremManager(d_cm, d_em, *d_flags);
00464   d_em->setTM(d_tm);
00465 
00466   d_translator = new Translator(d_em,
00467                                 (*d_flags)["translate"].getBool(),
00468                                 (*d_flags)["real2int"].getBool(),
00469                                 (*d_flags)["convertArith"].getBool(),
00470                                 (*d_flags)["convert2diff"].getString(),
00471                                 (*d_flags)["iteLiftArith"].getBool(),
00472                                 (*d_flags)["expResult"].getString(),
00473                                 (*d_flags)["category"].getString(),
00474                                 (*d_flags)["convertArray"].getBool(),
00475                                 (*d_flags)["combineAssump"].getBool(),
00476                                 (*d_flags)["convertToBV"].getInt());
00477 
00478   d_dump = d_translator->start((*d_flags)["dump-log"].getString());
00479 
00480   d_theoryCore = new TheoryCore(d_cm, d_em, d_tm, d_translator, *d_flags, *d_statistics);
00481 
00482   DebugAssert(d_theories.size() == 0, "Expected empty theories array");
00483   d_theories.push_back(d_theoryCore);
00484 
00485   // Fast rewriting of literals is done by setting their find to true or false.
00486   falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr()));
00487   trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr()));
00488 
00489   d_theories.push_back(d_theoryUF = new TheoryUF(d_theoryCore));
00490 
00491   if ((*d_flags)["arith-new"].getBool()) {
00492     d_theories.push_back(d_theoryArith = new TheoryArithNew(d_theoryCore));
00493   }
00494   else if ((*d_flags)["arith3"].getBool()) {
00495     d_theories.push_back(d_theoryArith = new TheoryArith3(d_theoryCore));
00496   }
00497   else {
00498     d_theories.push_back(d_theoryArith = new TheoryArithOld(d_theoryCore));
00499   }
00500   d_theoryCore->getExprTrans()->setTheoryArith(d_theoryArith);
00501   d_theories.push_back(d_theoryArray = new TheoryArray(d_theoryCore));
00502   d_theories.push_back(d_theoryRecords = new TheoryRecords(d_theoryCore));
00503   d_theories.push_back(d_theorySimulate = new TheorySimulate(d_theoryCore));
00504   d_theories.push_back(d_theoryBitvector = new TheoryBitvector(d_theoryCore));
00505   if ((*d_flags)["dt-lazy"].getBool()) {
00506     d_theories.push_back(d_theoryDatatype = new TheoryDatatypeLazy(d_theoryCore));
00507   }
00508   else {
00509     d_theories.push_back(d_theoryDatatype = new TheoryDatatype(d_theoryCore));
00510   }
00511   d_theories.push_back(d_theoryQuant = new TheoryQuant(d_theoryCore));
00512 
00513   d_translator->setTheoryCore(d_theoryCore);
00514   d_translator->setTheoryUF(d_theoryUF);
00515   d_translator->setTheoryArith(d_theoryArith);
00516   d_translator->setTheoryArray(d_theoryArray);
00517   d_translator->setTheoryQuant(d_theoryQuant);
00518   d_translator->setTheoryRecords(d_theoryRecords);
00519   d_translator->setTheorySimulate(d_theorySimulate);
00520   d_translator->setTheoryBitvector(d_theoryBitvector);
00521   d_translator->setTheoryDatatype(d_theoryDatatype);
00522 
00523   // Must be created after TheoryCore, since it needs it.
00524   // When we have more than one search engine, select one to create
00525   // based on flags
00526   const string& satEngine = (*d_flags)["sat"].getString();
00527   if (satEngine == "simple")
00528     d_se = new SearchSimple(d_theoryCore);
00529   else if (satEngine == "fast")
00530     d_se = new SearchEngineFast(d_theoryCore);
00531   else if (satEngine == "sat" || satEngine == "minisat")
00532     d_se = new SearchSat(d_theoryCore, satEngine);
00533   else
00534     throw CLException("Unrecognized SAT solver name: "
00535                       +(*d_flags)["sat"].getString());
00536 
00537   // Initial scope level should be 1
00538   d_cm->push();
00539 
00540   d_stackLevel = new(true) CDO<int>(d_cm->getCurrentContext(), 0);
00541 
00542   d_theoryCore->setResourceLimit((unsigned)((*d_flags)["resource"].getInt()));
00543   d_theoryCore->setTimeLimit((unsigned)((*d_flags)["stimeout"].getInt()));
00544 
00545   //  myvcl = this;
00546 }
00547 
00548 
00549 void VCL::destroy()
00550 {
00551   popto(0);
00552   d_cm->popto(0);
00553   delete d_stackLevel;
00554   free(d_stackLevel);
00555   d_translator->finish();
00556   delete d_translator;
00557 
00558   TRACE_MSG("delete", "Deleting SearchEngine {");
00559   delete d_se;
00560   TRACE_MSG("delete", "Finished deleting SearchEngine }");
00561   // This map contains expressions and theorems; delete it before
00562   // d_em, d_tm, and d_cm.
00563   TRACE_MSG("delete", "Deleting d_userAssertions {");
00564   delete d_batchedAssertionsIdx;
00565   free(d_batchedAssertionsIdx);
00566   delete d_batchedAssertions;
00567   free(d_batchedAssertions);
00568   delete d_userAssertions;
00569   free(d_userAssertions);
00570   TRACE_MSG("delete", "Finished deleting d_userAssertions }");
00571   // and set these to null so their destructors don't blow up
00572   d_lastQuery = Theorem3();
00573   d_lastQueryTCC = Theorem();
00574   d_lastClosure = Theorem3();
00575   // Delete ExprManager BEFORE TheoremManager, since Exprs use Theorems
00576   TRACE_MSG("delete", "Clearing d_em {");
00577   d_em->clear();
00578   d_tm->clear();
00579   TRACE_MSG("delete", "Finished clearing d_em }");
00580 
00581   for(size_t i=d_theories.size(); i!= 0; ) {
00582     --i;
00583     string name(d_theories[i]->getName());
00584     TRACE("delete", "Deleting Theory[", name, "] {");
00585     delete d_theories[i];
00586     TRACE("delete", "Finished deleting Theory[", name, "] }");
00587   }
00588   d_theories.clear();
00589 
00590   // TheoremManager does not call ~Theorem() destructors, and only
00591   // releases memory.  At worst, we'll lose some Assumptions.
00592   TRACE_MSG("delete", "Deleting d_tm {");
00593   delete d_tm;
00594   TRACE_MSG("delete", "Finished deleting d_tm }");
00595 
00596   TRACE_MSG("delete", "Deleting d_em {");
00597   delete d_em;
00598   TRACE_MSG("delete", "Finished deleting d_em }");
00599 
00600   TRACE_MSG("delete", "Deleting d_cm {");
00601   delete d_cm;
00602   TRACE_MSG("delete", "Finished deleting d_cm }");
00603   delete d_statistics;
00604   TRACE_MSG("delete", "Finished deleting d_statistics }");
00605 }
00606 
00607 
00608 VCL::~VCL()
00609 {
00610   destroy();
00611   TRACE_MSG("delete", "Deleting d_flags [end of ~VCL()]");
00612   delete d_flags;
00613   // No more TRACE-ing after this point (it needs d_flags)
00614   // Finalize the global debugger,
00615   // otherwise applications with more than one instance of VCL
00616   // may use refer to deallocated flags (e.g. test6 uses 2 VLCs)
00617   IF_DEBUG(
00618      CVC3::debugger.finalize();
00619   )
00620 }
00621 
00622 
00623 void VCL::reprocessFlags() {
00624   if (d_se->getName() != (*d_flags)["sat"].getString()) {
00625     delete d_se;
00626     const string& satEngine = (*d_flags)["sat"].getString();
00627     if (satEngine == "simple")
00628       d_se = new SearchSimple(d_theoryCore);
00629     else if (satEngine == "fast")
00630       d_se = new SearchEngineFast(d_theoryCore);
00631     else if (satEngine == "sat" || satEngine == "minisat")
00632       d_se = new SearchSat(d_theoryCore, satEngine);
00633     else
00634       throw CLException("Unrecognized SAT solver name: "
00635                         +(*d_flags)["sat"].getString());
00636   }
00637 
00638   int arithCur;
00639   if (d_theoryArith->getName() == "ArithmeticOld") arithCur = 1;
00640   else if (d_theoryArith->getName() == "ArithmeticNew") arithCur = 2;
00641   else {
00642     DebugAssert(d_theoryArith->getName() == "Arithmetic3", "unexpected name");
00643     arithCur = 3;
00644   }
00645 
00646   int arithNext;
00647   if ((*d_flags)["arith-new"].getBool()) arithNext = 2;
00648   else if ((*d_flags)["arith3"].getBool()) arithNext = 3;
00649   else arithNext = 1;
00650 
00651   if (arithCur != arithNext) {
00652     delete d_theoryArith;
00653     switch (arithNext) {
00654       case 1:
00655         d_theoryArith = new TheoryArithOld(d_theoryCore);
00656         break;
00657       case 2:
00658         d_theoryArith = new TheoryArithNew(d_theoryCore);
00659         break;
00660       case 3:
00661         d_theoryArith = new TheoryArith3(d_theoryCore);
00662         break;
00663     }
00664     d_theories[2] = d_theoryArith;
00665     d_translator->setTheoryArith(d_theoryArith);
00666   }
00667 
00668   if ((*d_flags)["dump-tcc"].getBool()) {
00669     d_flags->setFlag("translate", true);
00670     d_flags->setFlag("pp-batch", true);
00671     d_flags->setFlag("tcc", true);
00672   }
00673 
00674   if ((*d_flags)["translate"].getBool()) {
00675     d_flags->setFlag("printResults", false);
00676   }
00677 
00678   if ((*d_flags)["pp-bryant"].getBool()) {
00679     d_flags->setFlag("pp-batch", true);
00680   }
00681 
00682   //added by Yeting
00683   if ((*d_flags)["quant-complete-inst"].getBool() && !(*d_flags)["translate"].getBool()) {
00684     d_flags->setFlag("pp-batch", true);
00685   }
00686 
00687   if ((*d_flags)["cnf-formula"].getBool()) {
00688     d_flags->setFlag("de", "sat");
00689     d_flags->setFlag("preprocess", false);
00690   }
00691 
00692 
00693   //TODO: handle more flags
00694 }
00695 
00696 TheoryCore* VCL::core(){
00697   return d_theoryCore;
00698 }
00699 
00700 Type VCL::boolType(){
00701   return d_theoryCore->boolType();
00702 }
00703 
00704 
00705 Type VCL::realType()
00706 {
00707   return d_theoryArith->realType();
00708 }
00709 
00710 
00711 Type VCL::intType() {
00712   return d_theoryArith->intType();
00713 }
00714 
00715 
00716 Type VCL::subrangeType(const Expr& l, const Expr& r) {
00717   return d_theoryArith->subrangeType(l, r);
00718 }
00719 
00720 
00721 Type VCL::subtypeType(const Expr& pred, const Expr& witness)
00722 {
00723   return d_theoryCore->newSubtypeExpr(pred, witness);
00724 }
00725 
00726 
00727 Type VCL::tupleType(const Type& type0, const Type& type1)
00728 {
00729   vector<Type> types;
00730   types.push_back(type0);
00731   types.push_back(type1);
00732   return d_theoryRecords->tupleType(types);
00733 }
00734 
00735 
00736 Type VCL::tupleType(const Type& type0, const Type& type1, const Type& type2)
00737 {
00738   vector<Type> types;
00739   types.push_back(type0);
00740   types.push_back(type1);
00741   types.push_back(type2);
00742   return d_theoryRecords->tupleType(types);
00743 }
00744 
00745 
00746 Type VCL::tupleType(const vector<Type>& types)
00747 {
00748   return d_theoryRecords->tupleType(types);
00749 }
00750 
00751 
00752 Type VCL::recordType(const string& field, const Type& type)
00753 {
00754   vector<string> fields;
00755   vector<Type> kids;
00756   fields.push_back(field);
00757   kids.push_back(type);
00758   return Type(d_theoryRecords->recordType(fields, kids));
00759 }
00760 
00761 
00762 Type VCL::recordType(const string& field0, const Type& type0,
00763          const string& field1, const Type& type1) {
00764   vector<string> fields;
00765   vector<Type> kids;
00766   fields.push_back(field0);
00767   fields.push_back(field1);
00768   kids.push_back(type0);
00769   kids.push_back(type1);
00770   sort2(fields, kids);
00771   return Type(d_theoryRecords->recordType(fields, kids));
00772 }
00773 
00774 
00775 Type VCL::recordType(const string& field0, const Type& type0,
00776          const string& field1, const Type& type1,
00777          const string& field2, const Type& type2)
00778 {
00779   vector<string> fields;
00780   vector<Type> kids;
00781   fields.push_back(field0);
00782   fields.push_back(field1);
00783   fields.push_back(field2);
00784   kids.push_back(type0);
00785   kids.push_back(type1);
00786   kids.push_back(type2);
00787   sort2(fields, kids);
00788   return Type(d_theoryRecords->recordType(fields, kids));
00789 }
00790 
00791 
00792 Type VCL::recordType(const vector<string>& fields,
00793          const vector<Type>& types)
00794 {
00795   DebugAssert(fields.size() == types.size(),
00796         "VCL::recordType: number of fields is different \n"
00797         "from the number of types");
00798   // Create copies of the vectors to sort them
00799   vector<string> fs(fields);
00800   vector<Type> ts(types);
00801   sort2(fs, ts);
00802   return Type(d_theoryRecords->recordType(fs, ts));
00803 }
00804 
00805 
00806 Type VCL::dataType(const string& name,
00807                    const string& constructor,
00808                    const vector<string>& selectors, const vector<Expr>& types)
00809 {
00810   vector<string> constructors;
00811   constructors.push_back(constructor);
00812 
00813   vector<vector<string> > selectorsVec;
00814   selectorsVec.push_back(selectors);
00815 
00816   vector<vector<Expr> > typesVec;
00817   typesVec.push_back(types);
00818 
00819   return dataType(name, constructors, selectorsVec, typesVec);
00820 }
00821 
00822 
00823 Type VCL::dataType(const string& name,
00824                    const vector<string>& constructors,
00825                    const vector<vector<string> >& selectors,
00826                    const vector<vector<Expr> >& types)
00827 {
00828   Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
00829   if(d_dump) {
00830     d_translator->dump(res);
00831   }
00832   return Type(res[0]);
00833 }
00834 
00835 
00836 void VCL::dataType(const vector<string>& names,
00837                    const vector<vector<string> >& constructors,
00838                    const vector<vector<vector<string> > >& selectors,
00839                    const vector<vector<vector<Expr> > >& types,
00840                    vector<Type>& returnTypes)
00841 {
00842   Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
00843   if(d_dump) {
00844     d_translator->dump(res);
00845   }
00846   for (int i = 0; i < res.arity(); ++i) {
00847     returnTypes.push_back(Type(res[i]));
00848   }
00849 }
00850 
00851 
00852 Type VCL::arrayType(const Type& typeIndex, const Type& typeData)
00853 {
00854   return ::arrayType(typeIndex, typeData);
00855 }
00856 
00857 
00858 Type VCL::bitvecType(int n)
00859 {
00860   return d_theoryBitvector->newBitvectorType(n);
00861 }
00862 
00863 
00864 Type VCL::funType(const Type& typeDom, const Type& typeRan)
00865 {
00866   return typeDom.funType(typeRan);
00867 }
00868 
00869 
00870 Type VCL::funType(const vector<Type>& typeDom, const Type& typeRan) {
00871   DebugAssert(typeDom.size() >= 1, "VCL::funType: missing domain types");
00872   return Type::funType(typeDom, typeRan);
00873 }
00874 
00875 
00876 Type VCL::createType(const string& typeName)
00877 {
00878   if(d_dump) {
00879     d_translator->dump(Expr(TYPE, listExpr(idExpr(typeName))));
00880   }
00881   return d_theoryCore->newTypeExpr(typeName);
00882 }
00883 
00884 
00885 Type VCL::createType(const string& typeName, const Type& def)
00886 {
00887   if (d_dump) {
00888     d_translator->dump(Expr(TYPE, idExpr(typeName), def.getExpr()), true);
00889   }
00890   return d_theoryCore->newTypeExpr(typeName, def);
00891 }
00892 
00893 
00894 Type VCL::lookupType(const string& typeName)
00895 {
00896   return d_theoryCore->lookupTypeExpr(typeName);
00897 }
00898 
00899 
00900 Expr VCL::varExpr(const string& name, const Type& type)
00901 {
00902   // Check if the ofstream is open (as opposed to the command line flag)
00903   if(d_dump) {
00904     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
00905   }
00906   return d_theoryCore->newVar(name, type);
00907 }
00908 
00909 
00910 Expr VCL::varExpr(const string& name, const Type& type, const Expr& def)
00911 {
00912   // Check if the ofstream is open (as opposed to the command line flag)
00913   if(d_dump) {
00914     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
00915   }
00916   // Prove the TCCs of the definition
00917   if(getFlags()["tcc"].getBool()) {
00918     Type tpDef(def.getType()), tpVar(type);
00919     // Make sure that def is in the subtype of tpVar; that is, prove
00920     // FORALL (x: tpDef): x = def => typePred(tpVar)(x)
00921     if(tpDef != tpVar) {
00922       // Typecheck the base types
00923       if(getBaseType(tpDef) != getBaseType(type)) {
00924   throw TypecheckException("Type mismatch in constant definition:\n"
00925          "Constant "+name+
00926          " is declared with type:\n  "
00927          +type.toString()
00928          +"\nBut the type of definition is\n  "
00929          +tpDef.toString());
00930       }
00931       TRACE("tccs", "CONST def: "+name+" : "+tpVar.toString()
00932       +" := <value> : ", tpDef, ";");
00933       vector<Expr> boundVars;
00934       boundVars.push_back(boundVarExpr(name, "tcc", tpDef));
00935       Expr body(boundVars[0].eqExpr(def).impExpr(getTypePred(tpVar, boundVars[0])));
00936       Expr quant(forallExpr(boundVars, body));
00937       try {
00938         checkTCC(quant);
00939       } catch(TypecheckException&) {
00940   throw TypecheckException
00941     ("Type mismatch in constant definition:\n"
00942      "Constant "+name+
00943      " is declared with type:\n  "
00944      +type.toString()
00945      +"\nBut the type of definition is\n  "
00946      +def.getType().toString()
00947      +"\n\n which is not a subtype of the constant");
00948       }
00949     }
00950   }
00951   return d_theoryCore->newVar(name, type, def);
00952 }
00953 
00954 
00955 Expr VCL::lookupVar(const string& name, Type* type)
00956 {
00957   return d_theoryCore->lookupVar(name, type);
00958 }
00959 
00960 
00961 Type VCL::getType(const Expr& e)
00962 {
00963   return e.getType();
00964 }
00965 
00966 
00967 Type VCL::getBaseType(const Expr& e)
00968 {
00969   return d_theoryCore->getBaseType(e);
00970 }
00971 
00972 
00973 Type VCL::getBaseType(const Type& t)
00974 {
00975   return d_theoryCore->getBaseType(t);
00976 }
00977 
00978 
00979 Expr VCL::getTypePred(const Type&t, const Expr& e)
00980 {
00981   return d_theoryCore->getTypePred(t, e);
00982 }
00983 
00984 
00985 Expr VCL::stringExpr(const string& str) {
00986   return getEM()->newStringExpr(str);
00987 }
00988 
00989 
00990 Expr VCL::idExpr(const string& name) {
00991   return Expr(ID, stringExpr(name));
00992 }
00993 
00994 
00995 Expr VCL::listExpr(const vector<Expr>& kids) {
00996   return Expr(RAW_LIST, kids, getEM());
00997 }
00998 
00999 
01000 Expr VCL::listExpr(const Expr& e1) {
01001   return Expr(RAW_LIST, e1);
01002 }
01003 
01004 
01005 Expr VCL::listExpr(const Expr& e1, const Expr& e2) {
01006   return Expr(RAW_LIST, e1, e2);
01007 }
01008 
01009 
01010 Expr VCL::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
01011   return Expr(RAW_LIST, e1, e2, e3);
01012 }
01013 
01014 
01015 Expr VCL::listExpr(const string& op, const vector<Expr>& kids) {
01016   vector<Expr> newKids;
01017   newKids.push_back(idExpr(op));
01018   newKids.insert(newKids.end(), kids.begin(), kids.end());
01019   return listExpr(newKids);
01020 }
01021 
01022 
01023 Expr VCL::listExpr(const string& op, const Expr& e1) {
01024   return Expr(RAW_LIST, idExpr(op), e1);
01025 }
01026 
01027 
01028 Expr VCL::listExpr(const string& op, const Expr& e1,
01029        const Expr& e2) {
01030   return Expr(RAW_LIST, idExpr(op), e1, e2);
01031 }
01032 
01033 
01034 Expr VCL::listExpr(const string& op, const Expr& e1,
01035        const Expr& e2, const Expr& e3) {
01036   vector<Expr> kids;
01037   kids.push_back(idExpr(op));
01038   kids.push_back(e1);
01039   kids.push_back(e2);
01040   kids.push_back(e3);
01041   return listExpr(kids);
01042 }
01043 
01044 
01045 void VCL::printExpr(const Expr& e) {
01046   printExpr(e, cout);
01047 }
01048 
01049 
01050 void VCL::printExpr(const Expr& e, ostream& os) {
01051   os << e << endl;
01052 }
01053 
01054 
01055 Expr VCL::parseExpr(const Expr& e) {
01056   return d_theoryCore->parseExprTop(e);
01057 }
01058 
01059 
01060 Type VCL::parseType(const Expr& e) {
01061   return Type(d_theoryCore->parseExpr(e));
01062 }
01063 
01064 
01065 Expr VCL::importExpr(const Expr& e)
01066 {
01067   return d_em->rebuild(e);
01068 }
01069 
01070 
01071 Type VCL::importType(const Type& t)
01072 {
01073   return Type(d_em->rebuild(t.getExpr()));
01074 }
01075 
01076 void VCL::cmdsFromString(const std::string& s, InputLanguage lang=PRESENTATION_LANG)
01077 {
01078   stringstream ss(s,stringstream::in);
01079   return loadFile(ss,lang,false);
01080 }
01081 
01082 Expr VCL::exprFromString(const std::string& s)
01083 {
01084   stringstream ss("PRINT " + s + ";",stringstream::in);
01085   Parser p(this,d_translator,PRESENTATION_LANG,ss);
01086   Expr e = p.next();
01087   if( e.isNull() ) {
01088     throw ParserException("Parser result is null: '" + s + "'");
01089   }
01090   DebugAssert(e.getKind() == RAW_LIST, "Expected list expression");
01091   DebugAssert(e.arity() == 2, "Expected two children");
01092   return parseExpr(e[1]);
01093 }
01094 
01095 Expr VCL::trueExpr()
01096 {
01097   return d_em->trueExpr();
01098 }
01099 
01100 
01101 Expr VCL::falseExpr()
01102 {
01103   return d_em->falseExpr();
01104 }
01105 
01106 
01107 Expr VCL::notExpr(const Expr& child)
01108 {
01109   return !child;
01110 }
01111 
01112 
01113 Expr VCL::andExpr(const Expr& left, const Expr& right)
01114 {
01115   return left && right;
01116 }
01117 
01118 
01119 Expr VCL::andExpr(const vector<Expr>& children)
01120 {
01121   if (children.size() == 0)
01122     throw Exception("andExpr requires at least one child");
01123   return Expr(AND, children);
01124 }
01125 
01126 
01127 Expr VCL::orExpr(const Expr& left, const Expr& right)
01128 {
01129   return left || right;
01130 }
01131 
01132 
01133 Expr VCL::orExpr(const vector<Expr>& children)
01134 {
01135   if (children.size() == 0)
01136     throw Exception("orExpr requires at least one child");
01137   return Expr(OR, children);
01138 }
01139 
01140 
01141 Expr VCL::impliesExpr(const Expr& hyp, const Expr& conc)
01142 {
01143   return hyp.impExpr(conc);
01144 }
01145 
01146 
01147 Expr VCL::iffExpr(const Expr& left, const Expr& right)
01148 {
01149   return left.iffExpr(right);
01150 }
01151 
01152 
01153 Expr VCL::eqExpr(const Expr& child0, const Expr& child1)
01154 {
01155   return child0.eqExpr(child1);
01156 }
01157 
01158 Expr VCL::distinctExpr(const std::vector<Expr>& children)
01159 {
01160   return Expr(DISTINCT, children);
01161 }
01162 
01163 Expr VCL::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart)
01164 {
01165   return ifpart.iteExpr(thenpart, elsepart);
01166 }
01167 
01168 
01169 Op VCL::createOp(const string& name, const Type& type)
01170 {
01171   if (!type.isFunction())
01172     throw Exception("createOp: expected function type");
01173   if(d_dump) {
01174     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
01175   }
01176   return d_theoryCore->newFunction(name, type,
01177                                    getFlags()["trans-closure"].getBool());
01178 }
01179 
01180 
01181 Op VCL::createOp(const string& name, const Type& type, const Expr& def)
01182 {
01183   if (!type.isFunction())
01184     throw TypecheckException
01185     ("Type error in createOp:\n"
01186      "Constant "+name+
01187      " is declared with type:\n  "
01188      +type.toString()
01189      +"\n which is not a function type");
01190   if (getBaseType(type) != getBaseType(def.getType()))
01191     throw TypecheckException
01192     ("Type mismatch in createOp:\n"
01193      "Function "+name+
01194      " is declared with type:\n  "
01195      +type.toString()
01196      +"\nBut the type of definition is\n  "
01197      +def.getType().toString()
01198      +"\n\n which does not match");
01199   if(d_dump) {
01200     d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
01201   }
01202   // Prove the TCCs of the definition
01203   if(getFlags()["tcc"].getBool()) {
01204     Type tpDef(def.getType());
01205     // Make sure that def is within the subtype; that is, prove
01206     // FORALL (xs: argType): typePred_{return_type}(def(xs))
01207     if(tpDef != type) {
01208       vector<Expr> boundVars;
01209       for (int i = 0; i < type.arity()-1; ++i) {
01210         boundVars.push_back(d_em->newBoundVarExpr(type[i]));
01211       }
01212       Expr app = Expr(def.mkOp(), boundVars);
01213       Expr body(getTypePred(type[type.arity()-1], app));
01214       Expr quant(forallExpr(boundVars, body));
01215       Expr tcc = quant.andExpr(d_theoryCore->getTCC(quant));
01216       // Query the subtyping formula
01217       bool typesMatch = true;
01218       try {
01219         checkTCC(tcc);
01220       } catch (TypecheckException&) {
01221         typesMatch = false;
01222       }
01223       if(!typesMatch) {
01224   throw TypecheckException
01225     ("Type mismatch in createOp:\n"
01226      "Function "+name+
01227      " is declared with type:\n  "
01228      +type.toString()
01229      +"\nBut the definition is\n  "
01230      +def.toString()
01231      +"\n\nwhose type could not be proved to be a subtype");
01232       }
01233     }
01234   }
01235   return d_theoryCore->newFunction(name, type, def);
01236 }
01237 
01238 
01239 Op VCL::lookupOp(const string& name, Type* type)
01240 {
01241   return d_theoryCore->lookupFunction(name, type);
01242 }
01243 
01244 
01245 Expr VCL::funExpr(const Op& op, const Expr& child)
01246 {
01247   return Expr(op, child);
01248 }
01249 
01250 
01251 Expr VCL::funExpr(const Op& op, const Expr& left, const Expr& right)
01252 {
01253   return Expr(op, left, right);
01254 }
01255 
01256 
01257 Expr VCL::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2)
01258 {
01259   return Expr(op, child0, child1, child2);
01260 }
01261 
01262 
01263 Expr VCL::funExpr(const Op& op, const vector<Expr>& children)
01264 {
01265   return Expr(op, children);
01266 }
01267 
01268 bool VCL::addPairToArithOrder(const Expr& smaller, const Expr& bigger)
01269 {
01270   if (d_dump) {
01271     d_translator->dump(Expr(ARITH_VAR_ORDER, smaller, bigger), true);
01272   }
01273   return d_theoryArith->addPairToArithOrder(smaller, bigger);
01274 }
01275 
01276 Expr VCL::ratExpr(int n, int d)
01277 {
01278   DebugAssert(d != 0,"denominator cannot be 0");
01279   return d_em->newRatExpr(Rational(n,d));
01280 }
01281 
01282 
01283 Expr VCL::ratExpr(const string& n, const string& d, int base)
01284 {
01285   return d_em->newRatExpr(Rational(n.c_str(), d.c_str(), base));
01286 }
01287 
01288 
01289 Expr VCL::ratExpr(const string& n, int base)
01290 {
01291   string::size_type pos = n.rfind(".");
01292   if (pos == string::npos) {
01293     return d_em->newRatExpr(Rational(n.c_str(), base));
01294   }
01295   string afterdec = n.substr(pos+1);
01296   string beforedec = n.substr(0, pos);
01297   if (afterdec.size() == 0 || beforedec.size() == 0) {
01298     throw Exception("Cannot convert string to rational: "+n);
01299   }
01300   pos = beforedec.rfind(".");
01301   if (pos != string::npos) {
01302     throw Exception("Cannot convert string to rational: "+n);
01303   }
01304   Rational r = Rational(beforedec.c_str(), base);
01305   Rational fracPart = Rational(afterdec.c_str(), base);
01306   if( r < 0 || ((r == 0) && (beforedec.rfind("-") != string::npos)) ) {
01307     r = r - (fracPart / pow(afterdec.size(), (Rational)base));
01308   }
01309   else {
01310     r = r + (fracPart / pow(afterdec.size(), (Rational)base));
01311   }
01312   return d_em->newRatExpr(r);
01313 }
01314 
01315 
01316 Expr VCL::uminusExpr(const Expr& child)
01317 {
01318   return -child;
01319 }
01320 
01321 
01322 Expr VCL::plusExpr(const Expr& left, const Expr& right)
01323 {
01324   return left + right;
01325 }
01326 
01327 Expr VCL::plusExpr(const std::vector<Expr>& children)
01328 {
01329   return Expr(PLUS, children);
01330 }
01331 
01332 
01333 Expr VCL::minusExpr(const Expr& left, const Expr& right)
01334 {
01335   return left - right;
01336 }
01337 
01338 
01339 Expr VCL::multExpr(const Expr& left, const Expr& right)
01340 {
01341   return left * right;
01342 }
01343 
01344 
01345 Expr VCL::powExpr(const Expr& x, const Expr& n)
01346 {
01347   return ::powExpr(n, x);
01348 }
01349 
01350 
01351 Expr VCL::divideExpr(const Expr& num, const Expr& denom)
01352 {
01353   return ::divideExpr(num,denom);
01354 }
01355 
01356 
01357 Expr VCL::ltExpr(const Expr& left, const Expr& right)
01358 {
01359   return ::ltExpr(left, right);
01360 }
01361 
01362 
01363 Expr VCL::leExpr(const Expr& left, const Expr& right)
01364 {
01365   return ::leExpr(left, right);
01366 }
01367 
01368 
01369 Expr VCL::gtExpr(const Expr& left, const Expr& right)
01370 {
01371   return ::gtExpr(left, right);
01372 }
01373 
01374 
01375 Expr VCL::geExpr(const Expr& left, const Expr& right)
01376 {
01377   return ::geExpr(left, right);
01378 }
01379 
01380 
01381 Expr VCL::recordExpr(const string& field, const Expr& expr)
01382 {
01383   vector<string> fields;
01384   vector<Expr> kids;
01385   kids.push_back(expr);
01386   fields.push_back(field);
01387   return d_theoryRecords->recordExpr(fields, kids);
01388 }
01389 
01390 
01391 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01392          const string& field1, const Expr& expr1)
01393 {
01394   vector<string> fields;
01395   vector<Expr> kids;
01396   fields.push_back(field0);
01397   fields.push_back(field1);
01398   kids.push_back(expr0);
01399   kids.push_back(expr1);
01400   sort2(fields, kids);
01401   return d_theoryRecords->recordExpr(fields, kids);
01402 }
01403 
01404 
01405 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01406          const string& field1, const Expr& expr1,
01407          const string& field2, const Expr& expr2)
01408 {
01409   vector<string> fields;
01410   vector<Expr> kids;
01411   fields.push_back(field0);
01412   fields.push_back(field1);
01413   fields.push_back(field2);
01414   kids.push_back(expr0);
01415   kids.push_back(expr1);
01416   kids.push_back(expr2);
01417   sort2(fields, kids);
01418   return d_theoryRecords->recordExpr(fields, kids);
01419 }
01420 
01421 
01422 Expr VCL::recordExpr(const vector<string>& fields,
01423          const vector<Expr>& exprs)
01424 {
01425   DebugAssert(fields.size() > 0, "VCL::recordExpr()");
01426   DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
01427   // Create copies of the vectors to sort them
01428   vector<string> fs(fields);
01429   vector<Expr> es(exprs);
01430   sort2(fs, es);
01431   return d_theoryRecords->recordExpr(fs, es);
01432 }
01433 
01434 
01435 Expr VCL::recSelectExpr(const Expr& record, const string& field)
01436 {
01437   return d_theoryRecords->recordSelect(record, field);
01438 }
01439 
01440 
01441 Expr VCL::recUpdateExpr(const Expr& record, const string& field,
01442       const Expr& newValue)
01443 {
01444   return d_theoryRecords->recordUpdate(record, field, newValue);
01445 }
01446 
01447 
01448 Expr VCL::readExpr(const Expr& array, const Expr& index)
01449 {
01450   return Expr(READ, array, index);
01451 }
01452 
01453 
01454 Expr VCL::writeExpr(const Expr& array, const Expr& index, const Expr& newValue)
01455 {
01456   return Expr(WRITE, array, index, newValue);
01457 }
01458 
01459 
01460 Expr VCL::newBVConstExpr(const std::string& s, int base)
01461 {
01462   return d_theoryBitvector->newBVConstExpr(s, base);
01463 }
01464 
01465 
01466 Expr VCL::newBVConstExpr(const std::vector<bool>& bits)
01467 {
01468   return d_theoryBitvector->newBVConstExpr(bits);
01469 }
01470 
01471 
01472 Expr VCL::newBVConstExpr(const Rational& r, int len)
01473 {
01474   return d_theoryBitvector->newBVConstExpr(r, len);
01475 }
01476 
01477 
01478 Expr VCL::newConcatExpr(const Expr& t1, const Expr& t2)
01479 {
01480   return d_theoryBitvector->newConcatExpr(t1, t2);
01481 }
01482 
01483 
01484 Expr VCL::newConcatExpr(const std::vector<Expr>& kids)
01485 {
01486   return d_theoryBitvector->newConcatExpr(kids);
01487 }
01488 
01489 
01490 Expr VCL::newBVExtractExpr(const Expr& e, int hi, int low)
01491 {
01492   return d_theoryBitvector->newBVExtractExpr(e, hi, low);
01493 }
01494 
01495 
01496 Expr VCL::newBVNegExpr(const Expr& t1)
01497 {
01498   return d_theoryBitvector->newBVNegExpr(t1);
01499 }
01500 
01501 
01502 Expr VCL::newBVAndExpr(const Expr& t1, const Expr& t2)
01503 {
01504   return d_theoryBitvector->newBVAndExpr(t1, t2);
01505 }
01506 
01507 
01508 Expr VCL::newBVAndExpr(const std::vector<Expr>& kids)
01509 {
01510   return d_theoryBitvector->newBVAndExpr(kids);
01511 }
01512 
01513 
01514 Expr VCL::newBVOrExpr(const Expr& t1, const Expr& t2)
01515 {
01516   return d_theoryBitvector->newBVOrExpr(t1, t2);
01517 }
01518 
01519 
01520 Expr VCL::newBVOrExpr(const std::vector<Expr>& kids)
01521 {
01522   return d_theoryBitvector->newBVOrExpr(kids);
01523 }
01524 
01525 
01526 Expr VCL::newBVXorExpr(const Expr& t1, const Expr& t2)
01527 {
01528   return d_theoryBitvector->newBVXorExpr(t1, t2);
01529 }
01530 
01531 
01532 Expr VCL::newBVXorExpr(const std::vector<Expr>& kids)
01533 {
01534   return d_theoryBitvector->newBVXorExpr(kids);
01535 }
01536 
01537 
01538 Expr VCL::newBVXnorExpr(const Expr& t1, const Expr& t2)
01539 {
01540   return d_theoryBitvector->newBVXnorExpr(t1, t2);
01541 }
01542 
01543 
01544 Expr VCL::newBVXnorExpr(const std::vector<Expr>& kids)
01545 {
01546   return d_theoryBitvector->newBVXnorExpr(kids);
01547 }
01548 
01549 
01550 Expr VCL::newBVNandExpr(const Expr& t1, const Expr& t2)
01551 {
01552   return d_theoryBitvector->newBVNandExpr(t1, t2);
01553 }
01554 
01555 
01556 Expr VCL::newBVNorExpr(const Expr& t1, const Expr& t2)
01557 {
01558   return d_theoryBitvector->newBVNorExpr(t1, t2);
01559 }
01560 
01561 
01562 Expr VCL::newBVCompExpr(const Expr& t1, const Expr& t2)
01563 {
01564   return d_theoryBitvector->newBVCompExpr(t1, t2);
01565 }
01566 
01567 
01568 Expr VCL::newBVLTExpr(const Expr& t1, const Expr& t2)
01569 {
01570   return d_theoryBitvector->newBVLTExpr(t1, t2);
01571 }
01572 
01573 
01574 Expr VCL::newBVLEExpr(const Expr& t1, const Expr& t2)
01575 {
01576   return d_theoryBitvector->newBVLEExpr(t1, t2);
01577 }
01578 
01579 
01580 Expr VCL::newBVSLTExpr(const Expr& t1, const Expr& t2)
01581 {
01582   return d_theoryBitvector->newBVSLTExpr(t1, t2);
01583 }
01584 
01585 
01586 Expr VCL::newBVSLEExpr(const Expr& t1, const Expr& t2)
01587 {
01588   return d_theoryBitvector->newBVSLEExpr(t1, t2);
01589 }
01590 
01591 
01592 Expr VCL::newSXExpr(const Expr& t1, int len)
01593 {
01594   return d_theoryBitvector->newSXExpr(t1, len);
01595 }
01596 
01597 
01598 Expr VCL::newBVUminusExpr(const Expr& t1)
01599 {
01600   return d_theoryBitvector->newBVUminusExpr(t1);
01601 }
01602 
01603 
01604 Expr VCL::newBVSubExpr(const Expr& t1, const Expr& t2)
01605 {
01606   return d_theoryBitvector->newBVSubExpr(t1, t2);
01607 }
01608 
01609 
01610 Expr VCL::newBVPlusExpr(int numbits, const std::vector<Expr>& k)
01611 {
01612   return d_theoryBitvector->newBVPlusPadExpr(numbits, k);
01613 }
01614 
01615 Expr VCL::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2)
01616 {
01617   std::vector<Expr> k;
01618   k.push_back(t1);
01619   k.push_back(t2);
01620   return newBVPlusExpr(numbits, k);
01621 }
01622 
01623 
01624 Expr VCL::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2)
01625 {
01626   return d_theoryBitvector->newBVMultPadExpr(numbits, t1, t2);
01627 }
01628 
01629 Expr VCL::newBVUDivExpr(const Expr& t1, const Expr& t2)
01630 {
01631   return d_theoryBitvector->newBVUDivExpr(t1, t2);
01632 }
01633 
01634 Expr VCL::newBVURemExpr(const Expr& t1, const Expr& t2)
01635 {
01636   return d_theoryBitvector->newBVURemExpr(t1, t2);
01637 }
01638 
01639 Expr VCL::newBVSDivExpr(const Expr& t1, const Expr& t2)
01640 {
01641   return d_theoryBitvector->newBVSDivExpr(t1, t2);
01642 }
01643 
01644 Expr VCL::newBVSRemExpr(const Expr& t1, const Expr& t2)
01645 {
01646   return d_theoryBitvector->newBVSRemExpr(t1, t2);
01647 }
01648 
01649 Expr VCL::newBVSModExpr(const Expr& t1, const Expr& t2)
01650 {
01651   return d_theoryBitvector->newBVSModExpr(t1, t2);
01652 }
01653 
01654 
01655 Expr VCL::newFixedLeftShiftExpr(const Expr& t1, int r)
01656 {
01657   return d_theoryBitvector->newFixedLeftShiftExpr(t1, r);
01658 }
01659 
01660 
01661 Expr VCL::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r)
01662 {
01663   return d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t1, r);
01664 }
01665 
01666 
01667 Expr VCL::newFixedRightShiftExpr(const Expr& t1, int r)
01668 {
01669   return d_theoryBitvector->newFixedRightShiftExpr(t1, r);
01670 }
01671 
01672 
01673 Expr VCL::newBVSHL(const Expr& t1, const Expr& t2)
01674 {
01675   return Expr(BVSHL, t1, t2);
01676 }
01677 
01678 
01679 Expr VCL::newBVLSHR(const Expr& t1, const Expr& t2)
01680 {
01681   return Expr(BVLSHR, t1, t2);
01682 }
01683 
01684 
01685 Expr VCL::newBVASHR(const Expr& t1, const Expr& t2)
01686 {
01687   return Expr(BVASHR, t1, t2);
01688 }
01689 
01690 
01691 Rational VCL::computeBVConst(const Expr& e)
01692 {
01693   return d_theoryBitvector->computeBVConst(e);
01694 }
01695 
01696 
01697 Expr VCL::tupleExpr(const vector<Expr>& exprs) {
01698   DebugAssert(exprs.size() > 0, "VCL::tupleExpr()");
01699   return d_theoryRecords->tupleExpr(exprs);
01700 }
01701 
01702 
01703 Expr VCL::tupleSelectExpr(const Expr& tuple, int index)
01704 {
01705   return d_theoryRecords->tupleSelect(tuple, index);
01706 }
01707 
01708 
01709 Expr VCL::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue)
01710 {
01711   return d_theoryRecords->tupleUpdate(tuple, index, newValue);
01712 }
01713 
01714 
01715 Expr VCL::datatypeConsExpr(const string& constructor, const vector<Expr>& args)
01716 {
01717   return d_theoryDatatype->datatypeConsExpr(constructor, args);
01718 }
01719 
01720 
01721 Expr VCL::datatypeSelExpr(const string& selector, const Expr& arg)
01722 {
01723   return d_theoryDatatype->datatypeSelExpr(selector, arg);
01724 }
01725 
01726 
01727 Expr VCL::datatypeTestExpr(const string& constructor, const Expr& arg)
01728 {
01729   return d_theoryDatatype->datatypeTestExpr(constructor, arg);
01730 }
01731 
01732 
01733 Expr VCL::boundVarExpr(const string& name, const string& uid,
01734            const Type& type) {
01735   return d_em->newBoundVarExpr(name, uid, type);
01736 }
01737 
01738 
01739 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body) {
01740   DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01741   return d_em->newClosureExpr(FORALL, vars, body);
01742 }
01743 
01744 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body,
01745                      const Expr& trigger) {
01746   DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01747   return d_em->newClosureExpr(FORALL, vars, body, trigger);
01748 }
01749 
01750 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body,
01751                      const vector<Expr>& triggers) {
01752   DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01753   return d_em->newClosureExpr(FORALL, vars, body, triggers);
01754 }
01755 
01756 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body,
01757          const vector<vector<Expr> >& triggers) {
01758   DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01759   return d_em->newClosureExpr(FORALL, vars, body, triggers);
01760 }
01761 
01762 void VCL::setTriggers(const Expr& e, const vector< vector<Expr> >& triggers) {
01763   e.setTriggers(triggers);
01764 }
01765 
01766 void VCL::setTriggers(const Expr& e, const vector<Expr>& triggers) {
01767   e.setTriggers(triggers);
01768 }
01769 
01770 void VCL::setTrigger(const Expr& e, const Expr& trigger) {
01771   e.setTrigger(trigger);
01772 }
01773 
01774 void VCL::setMultiTrigger(const Expr& e, const vector<Expr>& multiTrigger) {
01775   e.setMultiTrigger(multiTrigger);
01776 }
01777 
01778 Expr VCL::existsExpr(const vector<Expr>& vars, const Expr& body) {
01779   return d_em->newClosureExpr(EXISTS, vars, body);
01780 }
01781 
01782 
01783 Op VCL::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
01784   return d_em->newClosureExpr(LAMBDA, vars, body).mkOp();
01785 }
01786 
01787 Op VCL::transClosure(const Op& op) {
01788   const string& name = op.getExpr().getName();
01789   return d_em->newSymbolExpr(name, TRANS_CLOSURE).mkOp();
01790 }
01791 
01792 
01793 Expr VCL::simulateExpr(const Expr& f, const Expr& s0,
01794            const vector<Expr>& inputs, const Expr& n) {
01795   vector<Expr> kids;
01796   kids.push_back(f);
01797   kids.push_back(s0);
01798   kids.insert(kids.end(), inputs.begin(), inputs.end());
01799   kids.push_back(n);
01800   return Expr(SIMULATE, kids);
01801 }
01802 
01803 
01804 void VCL::setResourceLimit(unsigned limit)
01805 {
01806   d_theoryCore->setResourceLimit(limit);
01807 }
01808 
01809 
01810 Theorem VCL::checkTCC(const Expr& tcc)
01811 {
01812   Theorem tccThm;
01813   d_se->push();
01814   QueryResult res = d_se->checkValid(tcc, tccThm);
01815   switch (res) {
01816     case VALID:
01817       d_lastQueryTCC = tccThm;
01818       d_se->pop();
01819       break;
01820     case INVALID:
01821       throw TypecheckException("Failed TCC:\n\n  "
01822                                +tcc.toString()
01823                                +"\n\nWhich simplified to:\n\n  "
01824                                +simplify(tcc).toString()
01825                                +"\n\nAnd the last formula is not valid "
01826                                "in the current context.");
01827     case ABORT:
01828       throw TypecheckException("Budget exceeded:\n\n  "
01829                                "Unable to verify TCC:\n\n  "
01830                                +tcc.toString()
01831                                +"\n\nWhich simplified to:\n\n  "
01832                                +simplify(tcc).toString());
01833     case UNKNOWN:
01834       throw TypecheckException("Result unknown:\n\n  "
01835                                "Unable to verify TCC:\n\n  "
01836                                +tcc.toString()
01837                                +"\n\nWhich simplified to:\n\n  "
01838                                +simplify(tcc).toString()
01839                                +"\n\nAnd the last formula is unknown "
01840                                "in the current context.");
01841     default:
01842       FatalAssert(false, "Unexpected case");
01843   }
01844   return tccThm;
01845 }
01846 
01847 
01848 void VCL::assertFormula(const Expr& e)
01849 {
01850   // Typecheck the user input
01851   if(!e.getType().isBool()) {
01852     throw TypecheckException("Non-BOOLEAN formula in ASSERT:\n  "
01853            +Expr(ASSERT, e).toString()
01854            +"\nDerived type of the formula:\n  "
01855            +e.getType().toString());
01856   }
01857 
01858   if (getFlags()["pp-batch"].getBool()) {
01859     d_batchedAssertions->push_back(e);
01860   }
01861   else {
01862     // Check if the ofstream is open (as opposed to the command line flag)
01863     if(d_dump) {
01864       Expr e2 = e;
01865       if (getFlags()["preSimplify"].getBool()) {
01866         e2 = simplify(e);
01867       }
01868       if (d_translator->dumpAssertion(e2)) return;
01869     }
01870 
01871     TRACE("vclassertFormula", "VCL::assertFormula(", e, ") {");
01872 
01873     // See if e was already asserted before
01874     if(d_userAssertions->count(e) > 0) {
01875       TRACE_MSG("vclassertFormula", "VCL::assertFormula[repeated assertion] => }");
01876       return;
01877     }
01878     // Check the validity of the TCC
01879     Theorem tccThm;
01880     if(getFlags()["tcc"].getBool()) {
01881       Expr tcc(d_theoryCore->getTCC(e));
01882       tccThm = checkTCC(tcc);
01883     }
01884 
01885     Theorem thm = d_se->newUserAssumption(e);
01886     (*d_userAssertions)[e] = UserAssertion(thm, tccThm, d_nextIdx++);
01887   }
01888   TRACE_MSG("vclassertFormula", "VCL::assertFormula => }");
01889 }
01890 
01891 
01892 void VCL::registerAtom(const Expr& e)
01893 {
01894   //TODO: add to interactive interface
01895   d_se->registerAtom(e);
01896 }
01897 
01898 
01899 Expr VCL::getImpliedLiteral()
01900 {
01901   //TODO: add to interactive interface
01902   Theorem thm = d_se->getImpliedLiteral();
01903   if (thm.isNull()) return Expr();
01904   return thm.getExpr();
01905 }
01906 
01907 
01908 Expr VCL::simplify(const Expr& e) {
01909   //TODO: add to interactive interface
01910   return simplifyThm(e).getRHS();
01911 }
01912 
01913 
01914 Theorem VCL::simplifyThm(const Expr& e)
01915 {
01916   e.getType();
01917   Theorem res = d_theoryCore->getExprTrans()->preprocess(e);
01918   Theorem simpThm =  d_theoryCore->simplify(res.getRHS());
01919   res = d_theoryCore->transitivityRule(res, simpThm);
01920   return res;
01921 }
01922 
01923 
01924 QueryResult VCL::query(const Expr& e)
01925 {
01926   TRACE("query", "VCL::query(", e,") {");
01927   // Typecheck the user input
01928   if(!e.getType().isBool()) {
01929     throw TypecheckException("Non-BOOLEAN formula in QUERY:\n  "
01930            +Expr(QUERY, e).toString()
01931            +"\nDerived type of the formula:\n  "
01932            +e.getType().toString());
01933   }
01934 
01935   Expr qExpr = e;
01936   if (getFlags()["pp-batch"].getBool()) {
01937     // Add batched assertions
01938     vector<Expr> kids;
01939     for (; (*d_batchedAssertionsIdx) < d_batchedAssertions->size();
01940          (*d_batchedAssertionsIdx) = (*d_batchedAssertionsIdx) + 1) {
01941       kids.push_back((*d_batchedAssertions)[(*d_batchedAssertionsIdx)]);
01942     }
01943     if (kids.size() > 0) {
01944       qExpr = kids.size() == 1 ? kids[0] : Expr(AND, kids);
01945       qExpr = qExpr.impExpr(e);
01946     }
01947   }
01948 
01949   if (d_dump && !getFlags()["dump-tcc"].getBool()) {
01950     Expr e2 = qExpr;
01951     if (getFlags()["preSimplify"].getBool()) {
01952       e2 = simplify(qExpr);
01953     }
01954     if (d_translator->dumpQuery(e2)) return UNKNOWN;
01955   }
01956 
01957   // Check the validity of the TCC
01958   Theorem tccThm = d_se->getCommonRules()->trueTheorem();
01959   if(getFlags()["tcc"].getBool()) {
01960     Expr tcc(d_theoryCore->getTCC(qExpr));
01961     if (getFlags()["dump-tcc"].getBool()) {
01962       Expr e2 = tcc;
01963       if (getFlags()["preSimplify"].getBool()) {
01964         e2 = simplify(tcc);
01965       }
01966       if (d_translator->dumpQuery(e2)) return UNKNOWN;
01967     }
01968     // FIXME: we have to guarantee that the TCC of 'tcc' is always valid
01969     tccThm = checkTCC(tcc);
01970   }
01971   Theorem res;
01972   QueryResult qres = d_se->checkValid(qExpr, res);
01973   switch (qres) {
01974     case VALID:
01975       d_lastQuery = d_se->getCommonRules()->queryTCC(res, tccThm);
01976       break;
01977     default:
01978       d_lastQueryTCC = Theorem();
01979       d_lastQuery = Theorem3();
01980       d_lastClosure = Theorem3();
01981   }
01982   TRACE("query", "VCL::query => ",
01983         qres == VALID ? "VALID" :
01984         qres == INVALID ? "INVALID" :
01985         qres == ABORT ? "ABORT" : "UNKNOWN", " }");
01986 
01987   if (d_dump) d_translator->dumpQueryResult(qres);
01988 
01989   return qres;
01990 }
01991 
01992 
01993 QueryResult VCL::checkUnsat(const Expr& e)
01994 {
01995   return query(e.negate());
01996 }
01997 
01998 
01999 QueryResult VCL::checkContinue()
02000 {
02001   if(d_dump) {
02002     d_translator->dump(d_em->newLeafExpr(CONTINUE), true);
02003   }
02004   vector<Expr> assertions;
02005   d_se->getCounterExample(assertions);
02006   Theorem thm;
02007   if (assertions.size() == 0) {
02008     return d_se->restart(falseExpr(), thm);
02009   }
02010   Expr eAnd = assertions.size() == 1 ? assertions[0] : andExpr(assertions);
02011   return d_se->restart(!eAnd, thm);
02012 }
02013 
02014 
02015 QueryResult VCL::restart(const Expr& e)
02016 {
02017   if (d_dump) {
02018     d_translator->dump(Expr(RESTART, e), true);
02019   }
02020   Theorem thm;
02021   return d_se->restart(e, thm);
02022 }
02023 
02024 
02025 void VCL::returnFromCheck()
02026 {
02027   //TODO: add to interactive interface
02028   d_se->returnFromCheck();
02029 }
02030 
02031 
02032 void VCL::getUserAssumptions(vector<Expr>& assumptions)
02033 {
02034   // TODO: add to interactive interface
02035   d_se->getUserAssumptions(assumptions);
02036 }
02037 
02038 
02039 void VCL::getInternalAssumptions(vector<Expr>& assumptions)
02040 {
02041   // TODO: add to interactive interface
02042   d_se->getInternalAssumptions(assumptions);
02043 }
02044 
02045 
02046 void VCL::getAssumptions(vector<Expr>& assumptions)
02047 {
02048   if(d_dump) {
02049     d_translator->dump(d_em->newLeafExpr(ASSUMPTIONS), true);
02050   }
02051   d_se->getAssumptions(assumptions);
02052 }
02053 
02054 
02055 //yeting, for proof translation
02056 Expr VCL::getProofQuery()
02057 {
02058   if (d_lastQuery.isNull()){
02059     throw EvalException
02060       ("Invalid Query,n");
02061   }
02062   return d_lastQuery.getExpr();
02063 
02064   //  Theorem thm = d_se->lastThm();
02065   //  if (thm.isNull()) return;
02066   //  thm.getLeafAssumptions(assumptions);
02067 }
02068 
02069 
02070 void VCL::getAssumptionsUsed(vector<Expr>& assumptions)
02071 {
02072   throw EvalException ("getAssumptionsUsed not currently supported");
02073   if(d_dump) {
02074     d_translator->dump(d_em->newLeafExpr(DUMP_ASSUMPTIONS), true);
02075   }
02076   Theorem thm = d_se->lastThm();
02077   if (thm.isNull()) return;
02078   thm.getLeafAssumptions(assumptions);
02079 }
02080 
02081 
02082 void VCL::getCounterExample(vector<Expr>& assertions, bool inOrder)
02083 {
02084   if(d_dump) {
02085     d_translator->dump(d_em->newLeafExpr(COUNTEREXAMPLE), true);
02086   }
02087   if (!(*d_flags)["translate"].getBool())
02088     d_se->getCounterExample(assertions, inOrder);
02089 }
02090 
02091 
02092 void VCL::getConcreteModel(ExprMap<Expr> & m)
02093 {
02094   if(d_dump) {
02095     d_translator->dump(d_em->newLeafExpr(COUNTERMODEL), true);
02096   }
02097   if (!(*d_flags)["translate"].getBool())
02098     d_se->getConcreteModel(m);
02099 }
02100 
02101 QueryResult VCL::tryModelGeneration() {
02102   if (!d_theoryCore->incomplete()) throw Exception("Model generation should be called only after an UNKNOWN result");
02103   QueryResult qres = UNKNOWN;
02104   int scopeLevel = d_cm->scopeLevel();
02105   try  {
02106           while (qres == UNKNOWN)
02107             {
02108               Theorem thm;
02109               d_se->push();
02110               // Try to generate the model
02111               if (d_se->tryModelGeneration(thm))
02112                 // If success, we are satisfiable
02113                 qres = INVALID;
02114               else
02115                 {
02116                   // Generate the clause to get rid of the faults
02117                   vector<Expr> assumptions;
02118                   thm.getLeafAssumptions(assumptions, true /*negate*/);
02119                   if (!thm.getExpr().isFalse()) assumptions.push_back(thm.getExpr());
02120                   // Pop back to where we were
02121                   while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
02122                   // Restart with the new clause
02123                   qres = restart(orExpr(assumptions));
02124                   // Keep this level
02125                   scopeLevel = d_cm->scopeLevel();
02126                 }
02127             }
02128         } catch (Exception& e) {
02129           // Pop back to where we were
02130           while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
02131         }
02132   return qres;
02133 }
02134 
02135 FormulaValue VCL::value(const Expr& e) {
02136   DebugAssert(!e.isTerm(), "vcl::value: e is not a formula");
02137   return d_se->getValue(e);
02138 }
02139 
02140 bool VCL::inconsistent(vector<Expr>& assumptions)
02141 {
02142   // TODO: add to interactive interface
02143   if (d_theoryCore->inconsistent()) {
02144     // TODO: do we need local getAssumptions?
02145     getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
02146        assumptions);
02147     return true;
02148   }
02149   return false;
02150 }
02151 
02152 bool VCL::inconsistent()
02153 {
02154   return d_theoryCore->inconsistent();
02155 }
02156 
02157 
02158 bool VCL::incomplete() {
02159   // TODO: add to interactive interface
02160   // Return true only after a failed query
02161   return (d_lastQuery.isNull() && d_theoryCore->incomplete());
02162 }
02163 
02164 
02165 bool VCL::incomplete(vector<string>& reasons) {
02166   // TODO: add to interactive interface
02167   // Return true only after a failed query
02168   return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
02169 }
02170 
02171 
02172 Proof VCL::getProof()
02173 {
02174   if(d_dump) {
02175     d_translator->dump(d_em->newLeafExpr(DUMP_PROOF), true);
02176   }
02177 
02178   if(d_lastQuery.isNull())
02179     throw EvalException
02180       ("Method getProof() (or command DUMP_PROOF)\n"
02181        " must be called only after a Valid QUERY");
02182   return d_se->getProof();
02183 }
02184 
02185 
02186 Expr VCL::getTCC(){
02187   static Expr null;
02188   if(d_dump) {
02189     d_translator->dump(d_em->newLeafExpr(DUMP_TCC), true);
02190   }
02191   if(d_lastQueryTCC.isNull()) return null;
02192   else return d_lastQueryTCC.getExpr();
02193 }
02194 
02195 
02196 void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
02197 {
02198   if(d_dump) {
02199     d_translator->dump(d_em->newLeafExpr(DUMP_TCC_ASSUMPTIONS), true);
02200   }
02201   if(d_lastQuery.isNull())
02202     throw EvalException
02203       ("Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
02204        " must be called only after a Valid QUERY");
02205   getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
02206 }
02207 
02208 
02209 Proof VCL::getProofTCC() {
02210   static Proof null;
02211   if(d_dump) {
02212     d_translator->dump(d_em->newLeafExpr(DUMP_TCC_PROOF), true);
02213   }
02214   if(d_lastQueryTCC.isNull()) return null;
02215   else return d_lastQueryTCC.getProof();
02216 }
02217 
02218 
02219 Expr VCL::getClosure() {
02220   static Expr null;
02221   if(d_dump) {
02222     d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE), true);
02223   }
02224   if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
02225     // Construct the proof of closure and cache it in d_lastClosure
02226     d_lastClosure = deriveClosure(d_lastQuery);
02227   }
02228   if(d_lastClosure.isNull()) return null;
02229   else return d_lastClosure.getExpr();
02230 }
02231 
02232 
02233 Proof VCL::getProofClosure() {
02234   static Proof null;
02235   if(d_dump) {
02236     d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE_PROOF), true);
02237   }
02238   if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
02239     // Construct the proof of closure and cache it in d_lastClosure
02240     d_lastClosure = deriveClosure(d_lastQuery);
02241   }
02242   if(d_lastClosure.isNull()) return null;
02243   else return d_lastClosure.getProof();
02244 }
02245 
02246 
02247 int VCL::stackLevel()
02248 {
02249   return d_stackLevel->get();
02250 }
02251 
02252 
02253 void VCL::push()
02254 {
02255   if(d_dump) {
02256     d_translator->dump(d_em->newLeafExpr(PUSH), true);
02257   }
02258   d_se->push();
02259   d_stackLevel->set(stackLevel()+1);
02260 }
02261 
02262 
02263 void VCL::pop()
02264 {
02265   if(d_dump) {
02266     d_translator->dump(d_em->newLeafExpr(POP), true);
02267   }
02268   if (stackLevel() == 0) {
02269     throw EvalException
02270       ("POP called with no previous call to PUSH");
02271   }
02272   int level = stackLevel();
02273   while (level == stackLevel())
02274     d_se->pop();
02275 }
02276 
02277 
02278 void VCL::popto(int toLevel)
02279 {
02280   // Check if the ofstream is open (as opposed to the command line flag)
02281   if(d_dump) {
02282     d_translator->dump(Expr(POPTO, ratExpr(toLevel, 1)), true);
02283   }
02284   if (toLevel < 0) toLevel = 0;
02285   while (stackLevel() > toLevel) {
02286     d_se->pop();
02287   }
02288 }
02289 
02290 
02291 int VCL::scopeLevel()
02292 {
02293   return d_cm->scopeLevel();
02294 }
02295 
02296 
02297 void VCL::pushScope()
02298 {
02299   throw EvalException ("Scope-level push/pop is no longer supported");
02300   d_cm->push();
02301   if(d_dump) {
02302     d_translator->dump(d_em->newLeafExpr(PUSH_SCOPE), true);
02303   }
02304   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02305      dumpTrace(scopeLevel());)
02306 }
02307 
02308 
02309 void VCL::popScope()
02310 {
02311   throw EvalException ("Scope-level push/pop is no longer supported");
02312   if(d_dump) {
02313     d_translator->dump(d_em->newLeafExpr(POP_SCOPE), true);
02314   }
02315   if (scopeLevel() == 1) {
02316     cout << "Cannot POP from scope level 1" << endl;
02317   }
02318   else d_cm->pop();
02319   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02320      dumpTrace(scopeLevel());)
02321 }
02322 
02323 
02324 void VCL::poptoScope(int toLevel)
02325 {
02326   throw EvalException ("Scope-level push/pop is no longer supported");
02327   if(d_dump) {
02328     d_translator->dump(Expr(POPTO_SCOPE, ratExpr(toLevel, 1)), true);
02329   }
02330   if (toLevel < 1) {
02331     d_cm->popto(0);
02332     d_cm->push();
02333   }
02334   else d_cm->popto(toLevel);
02335   IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02336      dumpTrace(scopeLevel());)
02337 }
02338 
02339 
02340 Context* VCL::getCurrentContext()
02341 {
02342   return d_cm->getCurrentContext();
02343 }
02344 
02345 
02346 void VCL::reset()
02347 {
02348   destroy();
02349   init();
02350 }
02351 
02352 void VCL::logAnnotation(const Expr& annot)
02353 {
02354   if (d_dump) {
02355     d_translator->dump(annot);
02356   }
02357 }
02358 
02359 void VCL::loadFile(const string& fileName, InputLanguage lang,
02360        bool interactive, bool calledFromParser) {
02361   // TODO: move these?
02362   Parser parser(this, d_translator, lang, interactive, fileName);
02363   VCCmd cmd(this, &parser, calledFromParser);
02364   cmd.processCommands();
02365 }
02366 
02367 
02368 void VCL::loadFile(istream& is, InputLanguage lang,
02369        bool interactive) {
02370   // TODO: move these?
02371   Parser parser(this, d_translator, lang, is, interactive);
02372   VCCmd cmd(this, &parser);
02373   cmd.processCommands();
02374 }
02375 
02376 
02377 // Verbosity: <= 0 = print nothing, only calculate
02378 //            1 = only print current level
02379 //            n = print n recursive levels
02380 
02381 unsigned long VCL::getMemory(int verbosity)
02382 {
02383   unsigned long memSelf = sizeof(VCL);
02384   unsigned long mem = 0;
02385 
02386   mem += d_cm->getMemory(verbosity - 1);
02387   mem += d_em->getMemory(verbosity - 1);
02388 //   mem += d_tm->getMemory(verbosity - 1);
02389 //   mem += d_se->getMemory(verbosity - 1);
02390 
02391 //   mem += d_theoryCore->getMemory(verbosity - 1);
02392 //   mem += d_theoryUF->getMemory(verbosity - 1);
02393 //   mem += d_theoryArith->getMemory(verbosity - 1);
02394 //   mem += d_theoryArray->getMemory(verbosity - 1);
02395 //   mem += d_theoryQuant->getMemory(verbosity - 1);
02396 //   mem += d_theoryRecords->getMemory(verbosity - 1);
02397 //   mem += d_theorySimulate->getMemory(verbosity - 1);
02398 //   mem += d_theoryBitvector->getMemory(verbosity - 1);
02399 //   mem += d_theoryDatatype->getMemory(verbosity - 1);
02400 //   mem += d_translator->getMemory(verbosity - 1);
02401 
02402 //   mem += getMemoryVec(verbosity, d_theories, false, true);
02403 
02404 //   mem += d_flags->getMemory(verbosity - 1);
02405 //   mem += d_stackLevel->getMemory(verbosity - 1);
02406 //   mem += d_statistics->getMemory(verbosity - 1);
02407 //   mem += d_userAssertions->getMemory(verbosity - 1);
02408 //   mem += d_batchedAssertions->getMemory(verbosity - 1);
02409 //   mem += d_batchedAssertionsIdx->getMemory(verbosity - 1);
02410 
02411   //TODO: how to get memory for Expr and Theorems?
02412 
02413   MemoryTracker::print("VCL", verbosity, memSelf, mem);
02414 
02415   return mem + memSelf;
02416 }
02417 
02418 void VCL::setTimeLimit(unsigned limit) {
02419   d_theoryCore->setTimeLimit(limit);
02420 }