CVC3
|
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 }