00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
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
00054
00055
00056
00057
00058
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
00072
00073
00074
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
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
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
00110 flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax", false));
00111
00112
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
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
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
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
00159 flags.addFlag("negate-query", CLFlag(true, "Negate the query when translate into TPTP format"));;
00160
00161
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
00167
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
00173
00174
00175
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
00188 flags.addFlag("liftReadIte", CLFlag(true, "Lift read of ite"));
00189
00190
00191 flags.addFlag("cnf-formula", CLFlag(false, "the input is already in CNF. This option automatically enables -de sat and disable -preprocess"));
00192
00193
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
00206
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",
00264 CLFlag(false, "Print types for bound variables"));
00265
00266
00267 flags.addFlag("bv32-flag",
00268 CLFlag(false, "assume that all bitvectors are 32bits with no overflow", false));
00269
00270
00271 flags.addFlag("trans-closure",
00272 CLFlag(false,"enables transitive closure of binary relations", false));
00273
00274
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
00292
00293
00294
00295 Theorem3 VCL::deriveClosure(const Theorem3& thm) {
00296 vector<Expr> assump;
00297 set<UserAssertion> assumpSet;
00298
00299
00300
00301
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
00313 for(; i!=iend; ++i)
00314 getAssumptionsRec(*i, assumpSet, false);
00315
00316
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
00327 res = d_se->getCommonRules()->implIntro3(res, assump, tccs);
00328 }
00329 return res;
00330 }
00331
00332
00333
00334
00335
00336
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 {
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
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
00391
00392
00393
00394 VCL::VCL(const CLFlags& flags)
00395 : d_flags(new CLFlags(flags))
00396 {
00397
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
00414 if ((*d_flags)["quant-complete-inst"].getBool()) {
00415 d_flags->setFlag("pp-batch", true);
00416 }
00417
00418
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(
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
00442
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
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
00510
00511
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
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
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
00548
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
00558 d_lastQuery = Theorem3();
00559 d_lastQueryTCC = Theorem();
00560 d_lastClosure = Theorem3();
00561
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
00577
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
00600
00601
00602
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
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
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 std::vector<std::string>& fields,
00779 const std::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
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 std::string& name,
00793 const std::string& constructor,
00794 const std::vector<std::string>& selectors,
00795 const std::vector<Expr>& types)
00796 {
00797 vector<string> constructors;
00798 constructors.push_back(constructor);
00799
00800 vector<vector<string> > selectorsVec;
00801 selectorsVec.push_back(selectors);
00802
00803 vector<vector<Expr> > typesVec;
00804 typesVec.push_back(types);
00805
00806 return dataType(name, constructors, selectorsVec, typesVec);
00807 }
00808
00809
00810 Type VCL::dataType(const std::string& name,
00811 const std::vector<std::string>& constructors,
00812 const std::vector<std::vector<std::string> >& selectors,
00813 const std::vector<std::vector<Expr> >& types)
00814 {
00815 Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
00816 if(d_dump) {
00817 d_translator->dump(res);
00818 }
00819 return Type(res[0]);
00820 }
00821
00822
00823 void VCL::dataType(const std::vector<std::string>& names,
00824 const std::vector<std::vector<std::string> >& constructors,
00825 const std::vector<std::vector<std::vector<std::string> > >& selectors,
00826 const std::vector<std::vector<std::vector<Expr> > >& types,
00827 std::vector<Type>& returnTypes)
00828 {
00829 Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
00830 if(d_dump) {
00831 d_translator->dump(res);
00832 }
00833 for (int i = 0; i < res.arity(); ++i) {
00834 returnTypes.push_back(Type(res[i]));
00835 }
00836 }
00837
00838
00839 Type VCL::arrayType(const Type& typeIndex, const Type& typeData)
00840 {
00841 return ::arrayType(typeIndex, typeData);
00842 }
00843
00844
00845 Type VCL::bitvecType(int n)
00846 {
00847 return d_theoryBitvector->newBitvectorType(n);
00848 }
00849
00850
00851 Type VCL::funType(const Type& typeDom, const Type& typeRan)
00852 {
00853 return typeDom.funType(typeRan);
00854 }
00855
00856
00857 Type VCL::funType(const vector<Type>& typeDom, const Type& typeRan) {
00858 DebugAssert(typeDom.size() >= 1, "VCL::funType: missing domain types");
00859 return Type::funType(typeDom, typeRan);
00860 }
00861
00862
00863 Type VCL::createType(const string& typeName)
00864 {
00865 if(d_dump) {
00866 d_translator->dump(Expr(TYPE, listExpr(idExpr(typeName))));
00867 }
00868 return d_theoryCore->newTypeExpr(typeName);
00869 }
00870
00871
00872 Type VCL::createType(const string& typeName, const Type& def)
00873 {
00874 if (d_dump) {
00875 d_translator->dump(Expr(TYPE, idExpr(typeName), def.getExpr()), true);
00876 }
00877 return d_theoryCore->newTypeExpr(typeName, def);
00878 }
00879
00880
00881 Type VCL::lookupType(const string& typeName)
00882 {
00883 return d_theoryCore->lookupTypeExpr(typeName);
00884 }
00885
00886
00887 Expr VCL::varExpr(const string& name, const Type& type)
00888 {
00889
00890 if(d_dump) {
00891 d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
00892 }
00893 return d_theoryCore->newVar(name, type);
00894 }
00895
00896
00897 Expr VCL::varExpr(const string& name, const Type& type, const Expr& def)
00898 {
00899
00900 if(d_dump) {
00901 d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
00902 }
00903
00904 if(getFlags()["tcc"].getBool()) {
00905 Type tpDef(def.getType()), tpVar(type);
00906
00907
00908 if(tpDef != tpVar) {
00909
00910 if(getBaseType(tpDef) != getBaseType(type)) {
00911 throw TypecheckException("Type mismatch in constant definition:\n"
00912 "Constant "+name+
00913 " is declared with type:\n "
00914 +type.toString()
00915 +"\nBut the type of definition is\n "
00916 +tpDef.toString());
00917 }
00918 TRACE("tccs", "CONST def: "+name+" : "+tpVar.toString()
00919 +" := <value> : ", tpDef, ";");
00920 vector<Expr> boundVars;
00921 boundVars.push_back(boundVarExpr(name, "tcc", tpDef));
00922 Expr body(boundVars[0].eqExpr(def).impExpr(getTypePred(tpVar, boundVars[0])));
00923 Expr quant(forallExpr(boundVars, body));
00924 try {
00925 checkTCC(quant);
00926 } catch(TypecheckException&) {
00927 throw TypecheckException
00928 ("Type mismatch in constant definition:\n"
00929 "Constant "+name+
00930 " is declared with type:\n "
00931 +type.toString()
00932 +"\nBut the type of definition is\n "
00933 +def.getType().toString()
00934 +"\n\n which is not a subtype of the constant");
00935 }
00936 }
00937 }
00938 return d_theoryCore->newVar(name, type, def);
00939 }
00940
00941
00942 Expr VCL::lookupVar(const string& name, Type* type)
00943 {
00944 return d_theoryCore->lookupVar(name, type);
00945 }
00946
00947
00948 Type VCL::getType(const Expr& e)
00949 {
00950 return e.getType();
00951 }
00952
00953
00954 Type VCL::getBaseType(const Expr& e)
00955 {
00956 return d_theoryCore->getBaseType(e);
00957 }
00958
00959
00960 Type VCL::getBaseType(const Type& t)
00961 {
00962 return d_theoryCore->getBaseType(t);
00963 }
00964
00965
00966 Expr VCL::getTypePred(const Type&t, const Expr& e)
00967 {
00968 return d_theoryCore->getTypePred(t, e);
00969 }
00970
00971
00972 Expr VCL::stringExpr(const string& str) {
00973 return getEM()->newStringExpr(str);
00974 }
00975
00976
00977 Expr VCL::idExpr(const string& name) {
00978 return Expr(ID, stringExpr(name));
00979 }
00980
00981
00982 Expr VCL::listExpr(const vector<Expr>& kids) {
00983 return Expr(RAW_LIST, kids, getEM());
00984 }
00985
00986
00987 Expr VCL::listExpr(const Expr& e1) {
00988 return Expr(RAW_LIST, e1);
00989 }
00990
00991
00992 Expr VCL::listExpr(const Expr& e1, const Expr& e2) {
00993 return Expr(RAW_LIST, e1, e2);
00994 }
00995
00996
00997 Expr VCL::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
00998 return Expr(RAW_LIST, e1, e2, e3);
00999 }
01000
01001
01002 Expr VCL::listExpr(const string& op, const vector<Expr>& kids) {
01003 vector<Expr> newKids;
01004 newKids.push_back(idExpr(op));
01005 newKids.insert(newKids.end(), kids.begin(), kids.end());
01006 return listExpr(newKids);
01007 }
01008
01009
01010 Expr VCL::listExpr(const string& op, const Expr& e1) {
01011 return Expr(RAW_LIST, idExpr(op), e1);
01012 }
01013
01014
01015 Expr VCL::listExpr(const string& op, const Expr& e1,
01016 const Expr& e2) {
01017 return Expr(RAW_LIST, idExpr(op), e1, e2);
01018 }
01019
01020
01021 Expr VCL::listExpr(const string& op, const Expr& e1,
01022 const Expr& e2, const Expr& e3) {
01023 vector<Expr> kids;
01024 kids.push_back(idExpr(op));
01025 kids.push_back(e1);
01026 kids.push_back(e2);
01027 kids.push_back(e3);
01028 return listExpr(kids);
01029 }
01030
01031
01032 void VCL::printExpr(const Expr& e) {
01033 printExpr(e, cout);
01034 }
01035
01036
01037 void VCL::printExpr(const Expr& e, ostream& os) {
01038 os << e << endl;
01039 }
01040
01041
01042 Expr VCL::parseExpr(const Expr& e) {
01043 return d_theoryCore->parseExprTop(e);
01044 }
01045
01046
01047 Type VCL::parseType(const Expr& e) {
01048 return Type(d_theoryCore->parseExpr(e));
01049 }
01050
01051
01052 Expr VCL::importExpr(const Expr& e)
01053 {
01054 return d_em->rebuild(e);
01055 }
01056
01057
01058 Type VCL::importType(const Type& t)
01059 {
01060 return Type(d_em->rebuild(t.getExpr()));
01061 }
01062
01063 void VCL::cmdsFromString(const std::string& s, InputLanguage lang=PRESENTATION_LANG)
01064 {
01065 stringstream ss(s,stringstream::in);
01066 return loadFile(ss,lang,false);
01067 }
01068
01069 Expr VCL::exprFromString(const std::string& s)
01070 {
01071 stringstream ss("PRINT " + s + ";",stringstream::in);
01072 Parser p(this,PRESENTATION_LANG,ss);
01073 Expr e = p.next();
01074 if( e.isNull() ) {
01075 throw ParserException("Parser result is null: '" + s + "'");
01076 }
01077 DebugAssert(e.getKind() == RAW_LIST, "Expected list expression");
01078 DebugAssert(e.arity() == 2, "Expected two children");
01079 return parseExpr(e[1]);
01080 }
01081
01082 Expr VCL::trueExpr()
01083 {
01084 return d_em->trueExpr();
01085 }
01086
01087
01088 Expr VCL::falseExpr()
01089 {
01090 return d_em->falseExpr();
01091 }
01092
01093
01094 Expr VCL::notExpr(const Expr& child)
01095 {
01096 return !child;
01097 }
01098
01099
01100 Expr VCL::andExpr(const Expr& left, const Expr& right)
01101 {
01102 return left && right;
01103 }
01104
01105
01106 Expr VCL::andExpr(const vector<Expr>& children)
01107 {
01108 if (children.size() == 0)
01109 throw Exception("andExpr requires at least one child");
01110 return Expr(AND, children);
01111 }
01112
01113
01114 Expr VCL::orExpr(const Expr& left, const Expr& right)
01115 {
01116 return left || right;
01117 }
01118
01119
01120 Expr VCL::orExpr(const vector<Expr>& children)
01121 {
01122 if (children.size() == 0)
01123 throw Exception("orExpr requires at least one child");
01124 return Expr(OR, children);
01125 }
01126
01127
01128 Expr VCL::impliesExpr(const Expr& hyp, const Expr& conc)
01129 {
01130 return hyp.impExpr(conc);
01131 }
01132
01133
01134 Expr VCL::iffExpr(const Expr& left, const Expr& right)
01135 {
01136 return left.iffExpr(right);
01137 }
01138
01139
01140 Expr VCL::eqExpr(const Expr& child0, const Expr& child1)
01141 {
01142 return child0.eqExpr(child1);
01143 }
01144
01145 Expr VCL::distinctExpr(const std::vector<Expr>& children)
01146 {
01147 return Expr(DISTINCT, children);
01148 }
01149
01150 Expr VCL::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart)
01151 {
01152 return ifpart.iteExpr(thenpart, elsepart);
01153 }
01154
01155
01156 Op VCL::createOp(const string& name, const Type& type)
01157 {
01158 if (!type.isFunction())
01159 throw Exception("createOp: expected function type");
01160 if(d_dump) {
01161 d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
01162 }
01163 return d_theoryCore->newFunction(name, type,
01164 getFlags()["trans-closure"].getBool());
01165 }
01166
01167
01168 Op VCL::createOp(const string& name, const Type& type, const Expr& def)
01169 {
01170 if (!type.isFunction())
01171 throw TypecheckException
01172 ("Type error in createOp:\n"
01173 "Constant "+name+
01174 " is declared with type:\n "
01175 +type.toString()
01176 +"\n which is not a function type");
01177 if (getBaseType(type) != getBaseType(def.getType()))
01178 throw TypecheckException
01179 ("Type mismatch in createOp:\n"
01180 "Function "+name+
01181 " is declared with type:\n "
01182 +type.toString()
01183 +"\nBut the type of definition is\n "
01184 +def.getType().toString()
01185 +"\n\n which does not match");
01186 if(d_dump) {
01187 d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
01188 }
01189
01190 if(getFlags()["tcc"].getBool()) {
01191 Type tpDef(def.getType());
01192
01193
01194 if(tpDef != type) {
01195 vector<Expr> boundVars;
01196 for (int i = 0; i < type.arity()-1; ++i) {
01197 boundVars.push_back(d_em->newBoundVarExpr(type[i]));
01198 }
01199 Expr app = Expr(def.mkOp(), boundVars);
01200 Expr body(getTypePred(type[type.arity()-1], app));
01201 Expr quant(forallExpr(boundVars, body));
01202 Expr tcc = quant.andExpr(d_theoryCore->getTCC(quant));
01203
01204 bool typesMatch = true;
01205 try {
01206 checkTCC(tcc);
01207 } catch (TypecheckException&) {
01208 typesMatch = false;
01209 }
01210 if(!typesMatch) {
01211 throw TypecheckException
01212 ("Type mismatch in createOp:\n"
01213 "Function "+name+
01214 " is declared with type:\n "
01215 +type.toString()
01216 +"\nBut the definition is\n "
01217 +def.toString()
01218 +"\n\nwhose type could not be proved to be a subtype");
01219 }
01220 }
01221 }
01222 return d_theoryCore->newFunction(name, type, def);
01223 }
01224
01225
01226 Op VCL::lookupOp(const string& name, Type* type)
01227 {
01228 return d_theoryCore->lookupFunction(name, type);
01229 }
01230
01231
01232 Expr VCL::funExpr(const Op& op, const Expr& child)
01233 {
01234 return Expr(op, child);
01235 }
01236
01237
01238 Expr VCL::funExpr(const Op& op, const Expr& left, const Expr& right)
01239 {
01240 return Expr(op, left, right);
01241 }
01242
01243
01244 Expr VCL::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2)
01245 {
01246 return Expr(op, child0, child1, child2);
01247 }
01248
01249
01250 Expr VCL::funExpr(const Op& op, const vector<Expr>& children)
01251 {
01252 return Expr(op, children);
01253 }
01254
01255 bool VCL::addPairToArithOrder(const Expr& smaller, const Expr& bigger)
01256 {
01257 if (d_dump) {
01258 d_translator->dump(Expr(ARITH_VAR_ORDER, smaller, bigger), true);
01259 }
01260 return d_theoryArith->addPairToArithOrder(smaller, bigger);
01261 }
01262
01263 Expr VCL::ratExpr(int n, int d)
01264 {
01265 DebugAssert(d != 0,"denominator cannot be 0");
01266 return d_em->newRatExpr(Rational(n,d));
01267 }
01268
01269
01270 Expr VCL::ratExpr(const string& n, const string& d, int base)
01271 {
01272 return d_em->newRatExpr(Rational(n.c_str(), d.c_str(), base));
01273 }
01274
01275
01276 Expr VCL::ratExpr(const string& n, int base)
01277 {
01278 string::size_type pos = n.rfind(".");
01279 if (pos == string::npos) {
01280 return d_em->newRatExpr(Rational(n.c_str(), base));
01281 }
01282 string afterdec = n.substr(pos+1);
01283 string beforedec = n.substr(0, pos);
01284 if (afterdec.size() == 0 || beforedec.size() == 0) {
01285 throw Exception("Cannot convert string to rational: "+n);
01286 }
01287 pos = beforedec.rfind(".");
01288 if (pos != string::npos) {
01289 throw Exception("Cannot convert string to rational: "+n);
01290 }
01291 Rational r = Rational(beforedec.c_str(), base);
01292 Rational fracPart = Rational(afterdec.c_str(), base);
01293 if( r < 0 ) {
01294 r = r - (fracPart / pow(afterdec.size(), base));
01295 }
01296 else {
01297 r = r + (fracPart / pow(afterdec.size(), base));
01298 }
01299 return d_em->newRatExpr(r);
01300 }
01301
01302
01303 Expr VCL::uminusExpr(const Expr& child)
01304 {
01305 return -child;
01306 }
01307
01308
01309 Expr VCL::plusExpr(const Expr& left, const Expr& right)
01310 {
01311 return left + right;
01312 }
01313
01314 Expr VCL::plusExpr(const std::vector<Expr>& children)
01315 {
01316 return Expr(PLUS, children);
01317 }
01318
01319
01320 Expr VCL::minusExpr(const Expr& left, const Expr& right)
01321 {
01322 return left - right;
01323 }
01324
01325
01326 Expr VCL::multExpr(const Expr& left, const Expr& right)
01327 {
01328 return left * right;
01329 }
01330
01331
01332 Expr VCL::powExpr(const Expr& x, const Expr& n)
01333 {
01334 return ::powExpr(n, x);
01335 }
01336
01337
01338 Expr VCL::divideExpr(const Expr& num, const Expr& denom)
01339 {
01340 return ::divideExpr(num,denom);
01341 }
01342
01343
01344 Expr VCL::ltExpr(const Expr& left, const Expr& right)
01345 {
01346 return ::ltExpr(left, right);
01347 }
01348
01349
01350 Expr VCL::leExpr(const Expr& left, const Expr& right)
01351 {
01352 return ::leExpr(left, right);
01353 }
01354
01355
01356 Expr VCL::gtExpr(const Expr& left, const Expr& right)
01357 {
01358 return ::gtExpr(left, right);
01359 }
01360
01361
01362 Expr VCL::geExpr(const Expr& left, const Expr& right)
01363 {
01364 return ::geExpr(left, right);
01365 }
01366
01367
01368 Expr VCL::recordExpr(const string& field, const Expr& expr)
01369 {
01370 vector<string> fields;
01371 vector<Expr> kids;
01372 kids.push_back(expr);
01373 fields.push_back(field);
01374 return d_theoryRecords->recordExpr(fields, kids);
01375 }
01376
01377
01378 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01379 const string& field1, const Expr& expr1)
01380 {
01381 vector<string> fields;
01382 vector<Expr> kids;
01383 fields.push_back(field0);
01384 fields.push_back(field1);
01385 kids.push_back(expr0);
01386 kids.push_back(expr1);
01387 sort2(fields, kids);
01388 return d_theoryRecords->recordExpr(fields, kids);
01389 }
01390
01391
01392 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
01393 const string& field1, const Expr& expr1,
01394 const string& field2, const Expr& expr2)
01395 {
01396 vector<string> fields;
01397 vector<Expr> kids;
01398 fields.push_back(field0);
01399 fields.push_back(field1);
01400 fields.push_back(field2);
01401 kids.push_back(expr0);
01402 kids.push_back(expr1);
01403 kids.push_back(expr2);
01404 sort2(fields, kids);
01405 return d_theoryRecords->recordExpr(fields, kids);
01406 }
01407
01408
01409 Expr VCL::recordExpr(const std::vector<std::string>& fields,
01410 const std::vector<Expr>& exprs)
01411 {
01412 DebugAssert(fields.size() > 0, "VCL::recordExpr()");
01413 DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
01414
01415 vector<string> fs(fields);
01416 vector<Expr> es(exprs);
01417 sort2(fs, es);
01418 return d_theoryRecords->recordExpr(fs, es);
01419 }
01420
01421
01422 Expr VCL::recSelectExpr(const Expr& record, const string& field)
01423 {
01424 return d_theoryRecords->recordSelect(record, field);
01425 }
01426
01427
01428 Expr VCL::recUpdateExpr(const Expr& record, const string& field,
01429 const Expr& newValue)
01430 {
01431 return d_theoryRecords->recordUpdate(record, field, newValue);
01432 }
01433
01434
01435 Expr VCL::readExpr(const Expr& array, const Expr& index)
01436 {
01437 return Expr(READ, array, index);
01438 }
01439
01440
01441 Expr VCL::writeExpr(const Expr& array, const Expr& index, const Expr& newValue)
01442 {
01443 return Expr(WRITE, array, index, newValue);
01444 }
01445
01446
01447 Expr VCL::newBVConstExpr(const std::string& s, int base)
01448 {
01449 return d_theoryBitvector->newBVConstExpr(s, base);
01450 }
01451
01452
01453 Expr VCL::newBVConstExpr(const std::vector<bool>& bits)
01454 {
01455 return d_theoryBitvector->newBVConstExpr(bits);
01456 }
01457
01458
01459 Expr VCL::newBVConstExpr(const Rational& r, int len)
01460 {
01461 return d_theoryBitvector->newBVConstExpr(r, len);
01462 }
01463
01464
01465 Expr VCL::newConcatExpr(const Expr& t1, const Expr& t2)
01466 {
01467 return d_theoryBitvector->newConcatExpr(t1, t2);
01468 }
01469
01470
01471 Expr VCL::newConcatExpr(const std::vector<Expr>& kids)
01472 {
01473 return d_theoryBitvector->newConcatExpr(kids);
01474 }
01475
01476
01477 Expr VCL::newBVExtractExpr(const Expr& e, int hi, int low)
01478 {
01479 return d_theoryBitvector->newBVExtractExpr(e, hi, low);
01480 }
01481
01482
01483 Expr VCL::newBVNegExpr(const Expr& t1)
01484 {
01485 return d_theoryBitvector->newBVNegExpr(t1);
01486 }
01487
01488
01489 Expr VCL::newBVAndExpr(const Expr& t1, const Expr& t2)
01490 {
01491 return d_theoryBitvector->newBVAndExpr(t1, t2);
01492 }
01493
01494
01495 Expr VCL::newBVAndExpr(const std::vector<Expr>& kids)
01496 {
01497 return d_theoryBitvector->newBVAndExpr(kids);
01498 }
01499
01500
01501 Expr VCL::newBVOrExpr(const Expr& t1, const Expr& t2)
01502 {
01503 return d_theoryBitvector->newBVOrExpr(t1, t2);
01504 }
01505
01506
01507 Expr VCL::newBVOrExpr(const std::vector<Expr>& kids)
01508 {
01509 return d_theoryBitvector->newBVOrExpr(kids);
01510 }
01511
01512
01513 Expr VCL::newBVXorExpr(const Expr& t1, const Expr& t2)
01514 {
01515 return d_theoryBitvector->newBVXorExpr(t1, t2);
01516 }
01517
01518
01519 Expr VCL::newBVXorExpr(const std::vector<Expr>& kids)
01520 {
01521 return d_theoryBitvector->newBVXorExpr(kids);
01522 }
01523
01524
01525 Expr VCL::newBVXnorExpr(const Expr& t1, const Expr& t2)
01526 {
01527 return d_theoryBitvector->newBVXnorExpr(t1, t2);
01528 }
01529
01530
01531 Expr VCL::newBVXnorExpr(const std::vector<Expr>& kids)
01532 {
01533 return d_theoryBitvector->newBVXnorExpr(kids);
01534 }
01535
01536
01537 Expr VCL::newBVNandExpr(const Expr& t1, const Expr& t2)
01538 {
01539 return d_theoryBitvector->newBVNandExpr(t1, t2);
01540 }
01541
01542
01543 Expr VCL::newBVNorExpr(const Expr& t1, const Expr& t2)
01544 {
01545 return d_theoryBitvector->newBVNorExpr(t1, t2);
01546 }
01547
01548
01549 Expr VCL::newBVCompExpr(const Expr& t1, const Expr& t2)
01550 {
01551 return d_theoryBitvector->newBVCompExpr(t1, t2);
01552 }
01553
01554
01555 Expr VCL::newBVLTExpr(const Expr& t1, const Expr& t2)
01556 {
01557 return d_theoryBitvector->newBVLTExpr(t1, t2);
01558 }
01559
01560
01561 Expr VCL::newBVLEExpr(const Expr& t1, const Expr& t2)
01562 {
01563 return d_theoryBitvector->newBVLEExpr(t1, t2);
01564 }
01565
01566
01567 Expr VCL::newBVSLTExpr(const Expr& t1, const Expr& t2)
01568 {
01569 return d_theoryBitvector->newBVSLTExpr(t1, t2);
01570 }
01571
01572
01573 Expr VCL::newBVSLEExpr(const Expr& t1, const Expr& t2)
01574 {
01575 return d_theoryBitvector->newBVSLEExpr(t1, t2);
01576 }
01577
01578
01579 Expr VCL::newSXExpr(const Expr& t1, int len)
01580 {
01581 return d_theoryBitvector->newSXExpr(t1, len);
01582 }
01583
01584
01585 Expr VCL::newBVUminusExpr(const Expr& t1)
01586 {
01587 return d_theoryBitvector->newBVUminusExpr(t1);
01588 }
01589
01590
01591 Expr VCL::newBVSubExpr(const Expr& t1, const Expr& t2)
01592 {
01593 return d_theoryBitvector->newBVSubExpr(t1, t2);
01594 }
01595
01596
01597 Expr VCL::newBVPlusExpr(int numbits, const std::vector<Expr>& k)
01598 {
01599 return d_theoryBitvector->newBVPlusPadExpr(numbits, k);
01600 }
01601
01602 Expr VCL::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2)
01603 {
01604 std::vector<Expr> k;
01605 k.push_back(t1);
01606 k.push_back(t2);
01607 return newBVPlusExpr(numbits, k);
01608 }
01609
01610
01611 Expr VCL::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2)
01612 {
01613 return d_theoryBitvector->newBVMultPadExpr(numbits, t1, t2);
01614 }
01615
01616 Expr VCL::newBVUDivExpr(const Expr& t1, const Expr& t2)
01617 {
01618 return d_theoryBitvector->newBVUDivExpr(t1, t2);
01619 }
01620
01621 Expr VCL::newBVURemExpr(const Expr& t1, const Expr& t2)
01622 {
01623 return d_theoryBitvector->newBVURemExpr(t1, t2);
01624 }
01625
01626 Expr VCL::newBVSDivExpr(const Expr& t1, const Expr& t2)
01627 {
01628 return d_theoryBitvector->newBVSDivExpr(t1, t2);
01629 }
01630
01631 Expr VCL::newBVSRemExpr(const Expr& t1, const Expr& t2)
01632 {
01633 return d_theoryBitvector->newBVSRemExpr(t1, t2);
01634 }
01635
01636 Expr VCL::newBVSModExpr(const Expr& t1, const Expr& t2)
01637 {
01638 return d_theoryBitvector->newBVSModExpr(t1, t2);
01639 }
01640
01641
01642 Expr VCL::newFixedLeftShiftExpr(const Expr& t1, int r)
01643 {
01644 return d_theoryBitvector->newFixedLeftShiftExpr(t1, r);
01645 }
01646
01647
01648 Expr VCL::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r)
01649 {
01650 return d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t1, r);
01651 }
01652
01653
01654 Expr VCL::newFixedRightShiftExpr(const Expr& t1, int r)
01655 {
01656 return d_theoryBitvector->newFixedRightShiftExpr(t1, r);
01657 }
01658
01659
01660 Rational VCL::computeBVConst(const Expr& e)
01661 {
01662 return d_theoryBitvector->computeBVConst(e);
01663 }
01664
01665
01666 Expr VCL::tupleExpr(const vector<Expr>& exprs) {
01667 DebugAssert(exprs.size() > 0, "VCL::tupleExpr()");
01668 return d_theoryRecords->tupleExpr(exprs);
01669 }
01670
01671
01672 Expr VCL::tupleSelectExpr(const Expr& tuple, int index)
01673 {
01674 return d_theoryRecords->tupleSelect(tuple, index);
01675 }
01676
01677
01678 Expr VCL::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue)
01679 {
01680 return d_theoryRecords->tupleUpdate(tuple, index, newValue);
01681 }
01682
01683
01684 Expr VCL::datatypeConsExpr(const string& constructor, const vector<Expr>& args)
01685 {
01686 return d_theoryDatatype->datatypeConsExpr(constructor, args);
01687 }
01688
01689
01690 Expr VCL::datatypeSelExpr(const string& selector, const Expr& arg)
01691 {
01692 return d_theoryDatatype->datatypeSelExpr(selector, arg);
01693 }
01694
01695
01696 Expr VCL::datatypeTestExpr(const string& constructor, const Expr& arg)
01697 {
01698 return d_theoryDatatype->datatypeTestExpr(constructor, arg);
01699 }
01700
01701
01702 Expr VCL::boundVarExpr(const string& name, const string& uid,
01703 const Type& type) {
01704 return d_em->newBoundVarExpr(name, uid, type);
01705 }
01706
01707
01708 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body) {
01709 DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01710 return d_em->newClosureExpr(FORALL, vars, body);
01711 }
01712
01713 Expr VCL::forallExpr(const vector<Expr>& vars, const Expr& body,
01714 const vector<vector<Expr> >& triggers) {
01715 DebugAssert(vars.size() > 0, "VCL::foralLExpr()");
01716 return d_em->newClosureExpr(FORALL, vars, body, triggers);
01717 }
01718
01719 void VCL::setTriggers(const Expr& e, const std::vector< std::vector<Expr> >& triggers) {
01720 e.setTriggers(triggers);
01721 }
01722
01723
01724 Expr VCL::existsExpr(const vector<Expr>& vars, const Expr& body) {
01725 return d_em->newClosureExpr(EXISTS, vars, body);
01726 }
01727
01728
01729 Op VCL::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
01730 return d_em->newClosureExpr(LAMBDA, vars, body).mkOp();
01731 }
01732
01733 Op VCL::transClosure(const Op& op) {
01734 const string& name = op.getExpr().getName();
01735 return d_em->newSymbolExpr(name, TRANS_CLOSURE).mkOp();
01736 }
01737
01738
01739 Expr VCL::simulateExpr(const Expr& f, const Expr& s0,
01740 const vector<Expr>& inputs, const Expr& n) {
01741 vector<Expr> kids;
01742 kids.push_back(f);
01743 kids.push_back(s0);
01744 kids.insert(kids.end(), inputs.begin(), inputs.end());
01745 kids.push_back(n);
01746 return Expr(SIMULATE, kids);
01747 }
01748
01749
01750 void VCL::setResourceLimit(unsigned limit)
01751 {
01752 d_theoryCore->setResourceLimit(limit);
01753 }
01754
01755
01756 Theorem VCL::checkTCC(const Expr& tcc)
01757 {
01758 Theorem tccThm;
01759 d_se->push();
01760 QueryResult res = d_se->checkValid(tcc, tccThm);
01761 switch (res) {
01762 case VALID:
01763 d_lastQueryTCC = tccThm;
01764 d_se->pop();
01765 break;
01766 case INVALID:
01767 throw TypecheckException("Failed TCC:\n\n "
01768 +tcc.toString()
01769 +"\n\nWhich simplified to:\n\n "
01770 +simplify(tcc).toString()
01771 +"\n\nAnd the last formula is not valid "
01772 "in the current context.");
01773 case ABORT:
01774 throw TypecheckException("Budget exceeded:\n\n "
01775 "Unable to verify TCC:\n\n "
01776 +tcc.toString()
01777 +"\n\nWhich simplified to:\n\n "
01778 +simplify(tcc).toString());
01779 case UNKNOWN:
01780 throw TypecheckException("Result unknown:\n\n "
01781 "Unable to verify TCC:\n\n "
01782 +tcc.toString()
01783 +"\n\nWhich simplified to:\n\n "
01784 +simplify(tcc).toString()
01785 +"\n\nAnd the last formula is unknown "
01786 "in the current context.");
01787 default:
01788 FatalAssert(false, "Unexpected case");
01789 }
01790 return tccThm;
01791 }
01792
01793
01794 void VCL::assertFormula(const Expr& e)
01795 {
01796
01797 if(!e.getType().isBool()) {
01798 throw TypecheckException("Non-BOOLEAN formula in ASSERT:\n "
01799 +Expr(ASSERT, e).toString()
01800 +"\nDerived type of the formula:\n "
01801 +e.getType().toString());
01802 }
01803
01804 if (getFlags()["pp-batch"].getBool()) {
01805 d_batchedAssertions->push_back(e);
01806 }
01807 else {
01808
01809 if(d_dump) {
01810 Expr e2 = e;
01811 if (getFlags()["preSimplify"].getBool()) {
01812 e2 = simplify(e);
01813 }
01814 if (d_translator->dumpAssertion(e2)) return;
01815 }
01816
01817 TRACE("vclassertFormula", "VCL::assertFormula(", e, ") {");
01818
01819
01820 if(d_userAssertions->count(e) > 0) {
01821 TRACE_MSG("vclassertFormula", "VCL::assertFormula[repeated assertion] => }");
01822 return;
01823 }
01824
01825 Theorem tccThm;
01826 if(getFlags()["tcc"].getBool()) {
01827 Expr tcc(d_theoryCore->getTCC(e));
01828 tccThm = checkTCC(tcc);
01829 }
01830
01831 Theorem thm = d_se->newUserAssumption(e);
01832 (*d_userAssertions)[e] = UserAssertion(thm, tccThm, d_nextIdx++);
01833 }
01834 TRACE_MSG("vclassertFormula", "VCL::assertFormula => }");
01835 }
01836
01837
01838 void VCL::registerAtom(const Expr& e)
01839 {
01840
01841 d_se->registerAtom(e);
01842 }
01843
01844
01845 Expr VCL::getImpliedLiteral()
01846 {
01847
01848 Theorem thm = d_se->getImpliedLiteral();
01849 if (thm.isNull()) return Expr();
01850 return thm.getExpr();
01851 }
01852
01853
01854 Expr VCL::simplify(const Expr& e) {
01855
01856 return simplifyThm(e).getRHS();
01857 }
01858
01859
01860 Theorem VCL::simplifyThm(const Expr& e)
01861 {
01862 e.getType();
01863 Theorem res = d_theoryCore->getExprTrans()->preprocess(e);
01864 Theorem simpThm = d_theoryCore->simplify(res.getRHS());
01865 res = d_theoryCore->transitivityRule(res, simpThm);
01866 return res;
01867 }
01868
01869
01870 QueryResult VCL::query(const Expr& e)
01871 {
01872 TRACE("query", "VCL::query(", e,") {");
01873
01874 if(!e.getType().isBool()) {
01875 throw TypecheckException("Non-BOOLEAN formula in QUERY:\n "
01876 +Expr(QUERY, e).toString()
01877 +"\nDerived type of the formula:\n "
01878 +e.getType().toString());
01879 }
01880
01881 Expr qExpr = e;
01882 if (getFlags()["pp-batch"].getBool()) {
01883
01884 vector<Expr> kids;
01885 for (; (*d_batchedAssertionsIdx) < d_batchedAssertions->size();
01886 (*d_batchedAssertionsIdx) = (*d_batchedAssertionsIdx) + 1) {
01887 kids.push_back((*d_batchedAssertions)[(*d_batchedAssertionsIdx)]);
01888 }
01889 if (kids.size() > 0) {
01890 qExpr = kids.size() == 1 ? kids[0] : Expr(AND, kids);
01891 qExpr = qExpr.impExpr(e);
01892 }
01893 }
01894
01895 if (d_dump && !getFlags()["dump-tcc"].getBool()) {
01896 Expr e2 = qExpr;
01897 if (getFlags()["preSimplify"].getBool()) {
01898 e2 = simplify(qExpr);
01899 }
01900 if (d_translator->dumpQuery(e2)) return UNKNOWN;
01901 }
01902
01903
01904 Theorem tccThm = d_se->getCommonRules()->trueTheorem();
01905 if(getFlags()["tcc"].getBool()) {
01906 Expr tcc(d_theoryCore->getTCC(qExpr));
01907 if (getFlags()["dump-tcc"].getBool()) {
01908 Expr e2 = tcc;
01909 if (getFlags()["preSimplify"].getBool()) {
01910 e2 = simplify(tcc);
01911 }
01912 if (d_translator->dumpQuery(e2)) return UNKNOWN;
01913 }
01914
01915 tccThm = checkTCC(tcc);
01916 }
01917 Theorem res;
01918 QueryResult qres = d_se->checkValid(qExpr, res);
01919 switch (qres) {
01920 case VALID:
01921 d_lastQuery = d_se->getCommonRules()->queryTCC(res, tccThm);
01922 break;
01923 default:
01924 d_lastQueryTCC = Theorem();
01925 d_lastQuery = Theorem3();
01926 d_lastClosure = Theorem3();
01927 }
01928 TRACE("query", "VCL::query => ",
01929 qres == VALID ? "VALID" :
01930 qres == INVALID ? "INVALID" :
01931 qres == ABORT ? "ABORT" : "UNKNOWN", " }");
01932
01933 if (d_dump) d_translator->dumpQueryResult(qres);
01934
01935 return qres;
01936 }
01937
01938
01939 QueryResult VCL::checkUnsat(const Expr& e)
01940 {
01941 return query(e.negate());
01942 }
01943
01944
01945 QueryResult VCL::checkContinue()
01946 {
01947 if(d_dump) {
01948 d_translator->dump(d_em->newLeafExpr(CONTINUE), true);
01949 }
01950 vector<Expr> assertions;
01951 d_se->getCounterExample(assertions);
01952 Theorem thm;
01953 if (assertions.size() == 0) {
01954 return d_se->restart(falseExpr(), thm);
01955 }
01956 Expr eAnd = assertions.size() == 1 ? assertions[0] : andExpr(assertions);
01957 return d_se->restart(!eAnd, thm);
01958 }
01959
01960
01961 QueryResult VCL::restart(const Expr& e)
01962 {
01963 if (d_dump) {
01964 d_translator->dump(Expr(RESTART, e), true);
01965 }
01966 Theorem thm;
01967 return d_se->restart(e, thm);
01968 }
01969
01970
01971 void VCL::returnFromCheck()
01972 {
01973
01974 d_se->returnFromCheck();
01975 }
01976
01977
01978 void VCL::getUserAssumptions(vector<Expr>& assumptions)
01979 {
01980
01981 d_se->getUserAssumptions(assumptions);
01982 }
01983
01984
01985 void VCL::getInternalAssumptions(vector<Expr>& assumptions)
01986 {
01987
01988 d_se->getInternalAssumptions(assumptions);
01989 }
01990
01991
01992 void VCL::getAssumptions(vector<Expr>& assumptions)
01993 {
01994 if(d_dump) {
01995 d_translator->dump(d_em->newLeafExpr(ASSUMPTIONS), true);
01996 }
01997 d_se->getAssumptions(assumptions);
01998 }
01999
02000
02001
02002 Expr VCL::getProofQuery()
02003 {
02004 if (d_lastQuery.isNull()){
02005 throw EvalException
02006 ("Invalid Query,n");
02007 }
02008 return d_lastQuery.getExpr();
02009
02010
02011
02012
02013 }
02014
02015
02016 void VCL::getAssumptionsUsed(vector<Expr>& assumptions)
02017 {
02018 throw EvalException ("getAssumptionsUsed not currently supported");
02019 if(d_dump) {
02020 d_translator->dump(d_em->newLeafExpr(DUMP_ASSUMPTIONS), true);
02021 }
02022 Theorem thm = d_se->lastThm();
02023 if (thm.isNull()) return;
02024 thm.getLeafAssumptions(assumptions);
02025 }
02026
02027
02028 void VCL::getCounterExample(vector<Expr>& assertions, bool inOrder)
02029 {
02030 if(d_dump) {
02031 d_translator->dump(d_em->newLeafExpr(COUNTEREXAMPLE), true);
02032 }
02033 if (!(*d_flags)["translate"].getBool())
02034 d_se->getCounterExample(assertions, inOrder);
02035 }
02036
02037
02038 void VCL::getConcreteModel(ExprMap<Expr> & m)
02039 {
02040 if(d_dump) {
02041 d_translator->dump(d_em->newLeafExpr(COUNTERMODEL), true);
02042 }
02043 if (!(*d_flags)["translate"].getBool())
02044 d_se->getConcreteModel(m);
02045 }
02046
02047 QueryResult VCL::tryModelGeneration() {
02048 if (!d_theoryCore->incomplete()) throw Exception("Model generation should be called only after an UNKNOWN result");
02049 QueryResult qres = UNKNOWN;
02050 int scopeLevel = d_cm->scopeLevel();
02051 try {
02052 while (qres == UNKNOWN)
02053 {
02054 Theorem thm;
02055 d_se->push();
02056
02057 if (d_se->tryModelGeneration(thm))
02058
02059 qres = INVALID;
02060 else
02061 {
02062
02063 vector<Expr> assumptions;
02064 thm.getLeafAssumptions(assumptions, true );
02065 if (!thm.getExpr().isFalse()) assumptions.push_back(thm.getExpr());
02066
02067 while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
02068
02069 qres = restart(orExpr(assumptions));
02070
02071 scopeLevel = d_cm->scopeLevel();
02072 }
02073 }
02074 } catch (Exception& e) {
02075
02076 while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
02077 }
02078 return qres;
02079 }
02080
02081 FormulaValue VCL::value(const Expr& e) {
02082 DebugAssert(!e.isTerm(), "vcl::value: e is not a formula");
02083 return d_se->getValue(e);
02084 }
02085
02086 bool VCL::inconsistent(vector<Expr>& assumptions)
02087 {
02088
02089 if (d_theoryCore->inconsistent()) {
02090
02091 getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
02092 assumptions);
02093 return true;
02094 }
02095 return false;
02096 }
02097
02098 bool VCL::inconsistent()
02099 {
02100 return d_theoryCore->inconsistent();
02101 }
02102
02103
02104 bool VCL::incomplete() {
02105
02106
02107 return (d_lastQuery.isNull() && d_theoryCore->incomplete());
02108 }
02109
02110
02111 bool VCL::incomplete(std::vector<std::string>& reasons) {
02112
02113
02114 return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
02115 }
02116
02117
02118 Proof VCL::getProof()
02119 {
02120 if(d_dump) {
02121 d_translator->dump(d_em->newLeafExpr(DUMP_PROOF), true);
02122 }
02123
02124 if(d_lastQuery.isNull())
02125 throw EvalException
02126 ("Method getProof() (or command DUMP_PROOF)\n"
02127 " must be called only after a Valid QUERY");
02128 return d_se->getProof();
02129 }
02130
02131
02132 Expr VCL::getTCC(){
02133 static Expr null;
02134 if(d_dump) {
02135 d_translator->dump(d_em->newLeafExpr(DUMP_TCC), true);
02136 }
02137 if(d_lastQueryTCC.isNull()) return null;
02138 else return d_lastQueryTCC.getExpr();
02139 }
02140
02141
02142 void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
02143 {
02144 if(d_dump) {
02145 d_translator->dump(d_em->newLeafExpr(DUMP_TCC_ASSUMPTIONS), true);
02146 }
02147 if(d_lastQuery.isNull())
02148 throw EvalException
02149 ("Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
02150 " must be called only after a Valid QUERY");
02151 getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
02152 }
02153
02154
02155 Proof VCL::getProofTCC() {
02156 static Proof null;
02157 if(d_dump) {
02158 d_translator->dump(d_em->newLeafExpr(DUMP_TCC_PROOF), true);
02159 }
02160 if(d_lastQueryTCC.isNull()) return null;
02161 else return d_lastQueryTCC.getProof();
02162 }
02163
02164
02165 Expr VCL::getClosure() {
02166 static Expr null;
02167 if(d_dump) {
02168 d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE), true);
02169 }
02170 if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
02171
02172 d_lastClosure = deriveClosure(d_lastQuery);
02173 }
02174 if(d_lastClosure.isNull()) return null;
02175 else return d_lastClosure.getExpr();
02176 }
02177
02178
02179 Proof VCL::getProofClosure() {
02180 static Proof null;
02181 if(d_dump) {
02182 d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE_PROOF), true);
02183 }
02184 if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
02185
02186 d_lastClosure = deriveClosure(d_lastQuery);
02187 }
02188 if(d_lastClosure.isNull()) return null;
02189 else return d_lastClosure.getProof();
02190 }
02191
02192
02193 int VCL::stackLevel()
02194 {
02195 return d_stackLevel->get();
02196 }
02197
02198
02199 void VCL::push()
02200 {
02201 if(d_dump) {
02202 d_translator->dump(d_em->newLeafExpr(PUSH), true);
02203 }
02204 d_se->push();
02205 d_stackLevel->set(stackLevel()+1);
02206 }
02207
02208
02209 void VCL::pop()
02210 {
02211 if(d_dump) {
02212 d_translator->dump(d_em->newLeafExpr(POP), true);
02213 }
02214 if (stackLevel() == 0) {
02215 throw EvalException
02216 ("POP called with no previous call to PUSH");
02217 }
02218 int level = stackLevel();
02219 while (level == stackLevel())
02220 d_se->pop();
02221 }
02222
02223
02224 void VCL::popto(int toLevel)
02225 {
02226
02227 if(d_dump) {
02228 d_translator->dump(Expr(POPTO, ratExpr(toLevel, 1)), true);
02229 }
02230 if (toLevel < 0) toLevel = 0;
02231 while (stackLevel() > toLevel) {
02232 d_se->pop();
02233 }
02234 }
02235
02236
02237 int VCL::scopeLevel()
02238 {
02239 return d_cm->scopeLevel();
02240 }
02241
02242
02243 void VCL::pushScope()
02244 {
02245 throw EvalException ("Scope-level push/pop is no longer supported");
02246 d_cm->push();
02247 if(d_dump) {
02248 d_translator->dump(d_em->newLeafExpr(PUSH_SCOPE), true);
02249 }
02250 IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02251 dumpTrace(scopeLevel());)
02252 }
02253
02254
02255 void VCL::popScope()
02256 {
02257 throw EvalException ("Scope-level push/pop is no longer supported");
02258 if(d_dump) {
02259 d_translator->dump(d_em->newLeafExpr(POP_SCOPE), true);
02260 }
02261 if (scopeLevel() == 1) {
02262 cout << "Cannot POP from scope level 1" << endl;
02263 }
02264 else d_cm->pop();
02265 IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02266 dumpTrace(scopeLevel());)
02267 }
02268
02269
02270 void VCL::poptoScope(int toLevel)
02271 {
02272 throw EvalException ("Scope-level push/pop is no longer supported");
02273 if(d_dump) {
02274 d_translator->dump(Expr(POPTO_SCOPE, ratExpr(toLevel, 1)), true);
02275 }
02276 if (toLevel < 1) {
02277 d_cm->popto(0);
02278 d_cm->push();
02279 }
02280 else d_cm->popto(toLevel);
02281 IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
02282 dumpTrace(scopeLevel());)
02283 }
02284
02285
02286 Context* VCL::getCurrentContext()
02287 {
02288 return d_cm->getCurrentContext();
02289 }
02290
02291
02292 void VCL::reset()
02293 {
02294 destroy();
02295 init();
02296 }
02297
02298 void VCL::loadFile(const string& fileName, InputLanguage lang,
02299 bool interactive, bool calledFromParser) {
02300
02301 Parser parser(this, lang, interactive, fileName);
02302 VCCmd cmd(this, &parser, calledFromParser);
02303 cmd.processCommands();
02304 }
02305
02306
02307 void VCL::loadFile(istream& is, InputLanguage lang,
02308 bool interactive) {
02309
02310 Parser parser(this, lang, is, interactive);
02311 VCCmd cmd(this, &parser);
02312 cmd.processCommands();
02313 }
02314
02315
02316
02317
02318
02319
02320 unsigned long VCL::getMemory(int verbosity)
02321 {
02322 unsigned long memSelf = sizeof(VCL);
02323 unsigned long mem = 0;
02324
02325 mem += d_cm->getMemory(verbosity - 1);
02326 mem += d_em->getMemory(verbosity - 1);
02327
02328
02329
02330
02331
02332
02333
02334
02335
02336
02337
02338
02339
02340
02341
02342
02343
02344
02345
02346
02347
02348
02349
02350
02351
02352 MemoryTracker::print("VCL", verbosity, memSelf, mem);
02353
02354 return mem + memSelf;
02355 }
02356
02357 void VCL::setTimeLimit(unsigned limit) {
02358 d_theoryCore->setTimeLimit(limit);
02359 }