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