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