65 return new VCL(flags);
75 flags.
addFlag(
"timeout",
CLFlag(0,
"Kill cvc3 process after given number of seconds (0==no limit)"));
76 flags.
addFlag(
"stimeout",
CLFlag(0,
"Set time resource limit in tenths of seconds for a query(0==no limit)"));
77 flags.
addFlag(
"resource",
CLFlag(0,
"Set finite resource limit (0==no limit)"));
78 flags.
addFlag(
"mm",
CLFlag(
"chunks",
"Memory manager (chunks, malloc)"));
81 flags.
addFlag(
"help",
CLFlag(
true,
"print usage information and exit"));
82 flags.
addFlag(
"unsupported",
CLFlag(
true,
"print usage for old/unsupported/experimental options"));
83 flags.
addFlag(
"version",
CLFlag(
true,
"print version information and exit"));
84 flags.
addFlag(
"interactive",
CLFlag(
false,
"Interactive mode"));
85 flags.
addFlag(
"stats",
CLFlag(
false,
"Print run-time statistics"));
86 flags.
addFlag(
"seed",
CLFlag(1,
"Set the seed for random sequence"));
87 flags.
addFlag(
"printResults",
CLFlag(
true,
"Print results of interactive commands."));
88 flags.
addFlag(
"dump-log",
CLFlag(
"",
"Dump API call log in CVC3 input "
89 "format to given file "
90 "(off when file name is \"\")"));
91 flags.
addFlag(
"parse-only",
CLFlag(
false,
"Parse the input, then exit."));
94 flags.
addFlag(
"expResult",
CLFlag(
"",
"For smtlib translation. Give the expected result",
false));
95 flags.
addFlag(
"category",
CLFlag(
"unknown",
"For smtlib translation. Give the category",
false));
96 flags.
addFlag(
"translate",
CLFlag(
false,
"Produce a complete translation from "
97 "the input language to output language. "));
98 flags.
addFlag(
"real2int",
CLFlag(
false,
"When translating, convert reals to integers.",
false));
99 flags.
addFlag(
"convertArith",
CLFlag(
false,
"When translating, try to rewrite arith terms into smt-lib subset",
false));
100 flags.
addFlag(
"convert2diff",
CLFlag(
"",
"When translating, try to force into difference logic. Legal values are int and real.",
false));
101 flags.
addFlag(
"iteLiftArith",
CLFlag(
false,
"For translation. If true, ite's are lifted out of arith exprs.",
false));
102 flags.
addFlag(
"convertArray",
CLFlag(
false,
"For translation. If true, arrays are converted to uninterpreted functions if possible.",
false));
103 flags.
addFlag(
"combineAssump",
CLFlag(
false,
"For translation. If true, assumptions are combined into the query.",
false));
104 flags.
addFlag(
"convert2array",
CLFlag(
false,
"For translation. If true, try to convert to array-only theory",
false));
105 flags.
addFlag(
"convertToBV",
CLFlag(0,
"For translation. Set to nonzero to convert ints to bv's of that length",
false));
106 flags.
addFlag(
"convert-eq-iff",
CLFlag(
false,
"Convert equality on Boolean expressions to iff.",
false));
107 flags.
addFlag(
"preSimplify",
CLFlag(
false,
"Simplify each assertion or query before translating it",
false));
108 flags.
addFlag(
"dump-tcc",
CLFlag(
false,
"Compute and dump TCC only"));
109 flags.
addFlag(
"trans-skip-pp",
CLFlag(
false,
"Skip preprocess step in translation module",
false));
110 flags.
addFlag(
"trans-skip-difficulty",
CLFlag(
false,
"Leave out difficulty attribute during translation to SMT v2.0",
false));
111 flags.
addFlag(
"promote",
CLFlag(
true,
"Promote undefined logic combinations to defined logic combinations during translation to SMT",
false));
114 flags.
addFlag(
"old-func-syntax",
CLFlag(
false,
"Enable parsing of old-style function syntax",
false));
118 CLFlag(
true,
"Print expressions with sharing as DAGs"));
119 flags.
addFlag(
"lang",
CLFlag(
"presentation",
"Input language "
120 "(presentation, smt, smt2, internal)"));
122 "(presentation, smtlib, simplify, internal, lisp, tptp, spass)"));
123 flags.
addFlag(
"indent",
CLFlag(
false,
"Print expressions with indentation"));
124 flags.
addFlag(
"width",
CLFlag(80,
"Suggested line width for printing"));
125 flags.
addFlag(
"print-depth",
CLFlag(-1,
"Max. depth to print expressions "));
126 flags.
addFlag(
"print-assump",
CLFlag(
false,
"Print assumptions in Theorems "));
129 flags.
addFlag(
"sat",
CLFlag(
"minisat",
"choose a SAT solver to use "
131 flags.
addFlag(
"de",
CLFlag(
"dfs",
"choose a decision engine to use "
138 flags.
addFlag(
"minimizeClauses",
CLFlag(
false,
"Use brute-force minimization of clauses",
false));
139 flags.
addFlag(
"dynack",
CLFlag(
false,
"Use dynamic Ackermannization",
false));
140 flags.
addFlag(
"smart-clauses",
CLFlag(
true,
"Learn multiple clauses per conflict"));
144 flags.
addFlag(
"tcc",
CLFlag(
false,
"Check TCCs for each ASSERT and QUERY"));
145 flags.
addFlag(
"cnf",
CLFlag(
true,
"Convert top-level Boolean formulas to CNF",
false));
146 flags.
addFlag(
"ignore-cnf-vars",
CLFlag(
false,
"Do not split on aux. CNF vars (with +cnf)",
false));
147 flags.
addFlag(
"orig-formula",
CLFlag(
false,
"Preserve the original formula with +cnf (for splitter heuristics)",
false));
148 flags.
addFlag(
"liftITE",
CLFlag(
false,
"Eagerly lift all ITE exprs"));
149 flags.
addFlag(
"iflift",
CLFlag(
false,
"Translate if-then-else terms to CNF (with +cnf)",
false));
150 flags.
addFlag(
"circuit",
CLFlag(
false,
"With +cnf, use circuit propagation",
false));
151 flags.
addFlag(
"un-ite-ify",
CLFlag(
false,
"Unconvert ITE expressions",
false));
153 CLFlag(
false,
"Replace ITE condition by TRUE/FALSE in subexprs",
false));
154 flags.
addFlag(
"preprocess",
CLFlag(
true,
"Preprocess queries"));
155 flags.
addFlag(
"pp-pushneg",
CLFlag(
false,
"Push negation in preprocessor"));
156 flags.
addFlag(
"pp-bryant",
CLFlag(
false,
"Enable Bryant algorithm for UF",
false));
157 flags.
addFlag(
"pp-budget",
CLFlag(0,
"Budget for new preprocessing step",
false));
158 flags.
addFlag(
"pp-care",
CLFlag(
true,
"Enable care-set preprocessing step",
false));
159 flags.
addFlag(
"simp-and",
CLFlag(
false,
"Rewrite x&y to x&y[x/true]",
false));
160 flags.
addFlag(
"simp-or",
CLFlag(
false,
"Rewrite x|y to x|y[x/false]",
false));
161 flags.
addFlag(
"pp-batch",
CLFlag(
false,
"Ignore assumptions until query, then process all at once"));
162 flags.
addFlag(
"no-save-model",
CLFlag(
false,
"Do NOT save model assumptions in context after invalid / sat query"));
163 flags.
addFlag(
"internal::userSetNoSaveModel",
CLFlag(
false,
"set if user gave +no-save-model or -no-save-model explicitly",
false));
166 flags.
addFlag(
"negate-query",
CLFlag(
true,
"Negate the query when translate into TPTP format"));;
169 flags.
addFlag(
"counterexample",
CLFlag(
false,
"Dump counterexample if formula is invalid or satisfiable"));
170 flags.
addFlag(
"model",
CLFlag(
false,
"Dump model if formula is invalid or satisfiable"));
171 flags.
addFlag(
"unknown-check-model",
CLFlag(
false,
"Try to generate model if formula is unknown"));
172 flags.
addFlag(
"applications",
CLFlag(
true,
"Add relevant function applications and array accesses to the concrete countermodel"));
175 vector<pair<string,bool> > sv;
176 flags.
addFlag(
"trace",
CLFlag(sv,
"Tracing. Multiple flags add up."));
177 flags.
addFlag(
"dump-trace",
CLFlag(
"",
"Dump debugging trace to "
178 "given file (off when file name is \"\")"));
183 flags.
addFlag(
"arith-new",
CLFlag(
false,
"Use new arithmetic dp",
false));
184 flags.
addFlag(
"arith3",
CLFlag(
false,
"Use old arithmetic dp that works well with combined theories",
false));
186 CLFlag(
false,
"Use simple variable order in arith",
false));
187 flags.
addFlag(
"ineq-delay",
CLFlag(0,
"Accumulate this many inequalities before processing (-1 for don't process until necessary)"));
189 flags.
addFlag(
"nonlinear-sign-split",
CLFlag(
true,
"Whether to split on the signs of nontrivial nonlinear terms"));
191 flags.
addFlag(
"grayshadow-threshold",
CLFlag(-1,
"Ignore gray shadows bigger than this (makes solver incomplete)"));
192 flags.
addFlag(
"pathlength-threshold",
CLFlag(-1,
"Ignore gray shadows bigger than this (makes solver incomplete)"));
195 flags.
addFlag(
"liftReadIte",
CLFlag(
true,
"Lift read of ite"));
198 flags.
addFlag(
"cnf-formula",
CLFlag(
false,
"The input must be in CNF. This option automatically enables '-de sat' and disable preprocess"));
205 CLFlag(0,
"lfsc mode 0: off, 1:normal, 2:cvc3-mimic etc."));
209 flags.
addFlag(
"max-quant-inst",
CLFlag(200,
"The maximum number of"
210 " naive instantiations"));
213 CLFlag(
true,
"If this option is false, only naive instantiation is called"));
215 flags.
addFlag(
"quant-lazy",
CLFlag(
false,
"Instantiate lazily",
false));
217 flags.
addFlag(
"quant-sem-match",
218 CLFlag(
false,
"Attempt to match semantically when instantiating",
false));
223 flags.
addFlag(
"quant-complete-inst",
224 CLFlag(
false,
"Try complete instantiation heuristic. +pp-batch will be automatically enabled"));
227 CLFlag(100,
"The maximum Instantiation Level allowed"));
229 flags.
addFlag(
"quant-inst-lcache",
230 CLFlag(
true,
"Cache instantiations"));
232 flags.
addFlag(
"quant-inst-gcache",
233 CLFlag(
false,
"Cache instantiations",
false));
235 flags.
addFlag(
"quant-inst-tcache",
236 CLFlag(
false,
"Cache instantiations",
false));
239 flags.
addFlag(
"quant-inst-true",
240 CLFlag(
true,
"Ignore true instantiations"));
243 CLFlag(
false,
"Pull out vars",
false));
246 CLFlag(
true,
"Use instantiation level"));
248 flags.
addFlag(
"quant-polarity",
249 CLFlag(
false,
"Use polarity ",
false));
252 CLFlag(
true,
"Use new equality matching"));
254 flags.
addFlag(
"quant-max-score",
255 CLFlag(0,
"Maximum initial dynamic score"));
258 CLFlag(
true,
"Use trans heuristic"));
261 CLFlag(
true,
"Use trans2 heuristic"));
263 flags.
addFlag(
"quant-naive-num",
264 CLFlag(1000,
"Maximum number to call naive instantiation"));
266 flags.
addFlag(
"quant-naive-inst",
267 CLFlag(
true,
"Use naive instantiation"));
269 flags.
addFlag(
"quant-man-trig",
270 CLFlag(
true,
"Use manual triggers"));
273 CLFlag(
false,
"Send facts to core directly",
false));
276 CLFlag(1000,
"Limit for gfacts",
false));
278 flags.
addFlag(
"print-var-type",
279 CLFlag(
false,
"Print types for bound variables"));
283 CLFlag(
false,
"assume that all bitvectors are 32bits with no overflow",
false));
287 CLFlag(
false,
"enables transitive closure of binary relations",
false));
290 flags.
addFlag(
"dt-smartsplits",
291 CLFlag(
true,
"enables smart splitting in datatype theory",
false));
293 CLFlag(
false,
"lazy splitting on datatypes",
false));
302 return new VCL(createFlags());
313 set<UserAssertion> assumpSet;
319 vector<Theorem> tccs;
323 if (a.empty())
break;
330 getAssumptionsRec(*i, assumpSet,
false);
333 if(getFlags()[
"tcc"].getBool()) {
335 for(set<UserAssertion>::iterator i=assumpSet.begin(),
336 iend=assumpSet.end(); i!=iend; ++i) {
338 tccs.push_back(i->tcc());
343 res = d_se->getCommonRules()->implIntro3(res, assump, tccs);
354 void VCL::getAssumptionsRec(
const Theorem& thm,
355 set<UserAssertion>& assumptions,
360 if(d_userAssertions->count(thm.
getExpr())>0) {
362 assumptions.insert(a);
366 getAssumptionsRec(a.
tcc(), assumptions,
true);
370 assumptions.insert(a);
376 getAssumptionsRec(*i, assumptions, addTCCs);
381 void VCL::getAssumptions(
const Assumptions& a, vector<Expr>& assumptions)
383 set<UserAssertion> assumpSet;
384 if(a.
empty())
return;
388 getAssumptionsRec(*i, assumpSet, getFlags()[
"tcc"].getBool());
390 for(set<UserAssertion>::iterator i=assumpSet.begin(), iend=assumpSet.end();
397 void VCL::dumpTrace(
int scope) {
398 vector<StrPair> fields;
400 debugger.dumpTrace(
"scope", fields);
415 if ((*d_flags)[
"dump-tcc"].getBool()) {
416 d_flags->setFlag(
"translate",
true);
417 d_flags->setFlag(
"pp-batch",
true);
418 d_flags->setFlag(
"tcc",
true);
421 if ((*d_flags)[
"translate"].getBool()) {
422 d_flags->setFlag(
"printResults",
false);
425 if ((*d_flags)[
"pp-bryant"].getBool()) {
426 d_flags->setFlag(
"pp-batch",
true);
430 if ((*d_flags)[
"quant-complete-inst"].getBool() && !(*d_flags)[
"translate"].getBool()) {
431 d_flags->setFlag(
"pp-batch",
true);
435 if ((*d_flags)[
"cnf-formula"].getBool()) {
436 d_flags->setFlag(
"de",
"sat");
437 d_flags->setFlag(
"preprocess",
false);
442 CVC3::debugger.init(&((*d_flags)[
"trace"].getStrVec()),
443 &((*d_flags)[
"dump-trace"].getString()));
460 d_batchedAssertions =
new(
true)
CDList<Expr>(getCurrentContext());
461 d_batchedAssertionsIdx =
new(
true)
CDO<unsigned>(getCurrentContext(), 0);
469 (*d_flags)[
"translate"].getBool(),
470 (*d_flags)[
"real2int"].getBool(),
471 (*d_flags)[
"convertArith"].getBool(),
472 (*d_flags)[
"convert2diff"].getString(),
473 (*d_flags)[
"iteLiftArith"].getBool(),
474 (*d_flags)[
"expResult"].getString(),
475 (*d_flags)[
"category"].getString(),
476 (*d_flags)[
"convertArray"].getBool(),
477 (*d_flags)[
"combineAssump"].getBool(),
478 (*d_flags)[
"convertToBV"].getInt());
480 d_dump = d_translator->start((*d_flags)[
"dump-log"].getString());
482 d_theoryCore =
new TheoryCore(d_cm, d_em, d_tm, d_translator, *d_flags, *d_statistics);
484 DebugAssert(d_theories.size() == 0,
"Expected empty theories array");
485 d_theories.push_back(d_theoryCore);
488 falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr()));
489 trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr()));
491 d_theories.push_back(d_theoryUF =
new TheoryUF(d_theoryCore));
493 if ((*d_flags)[
"arith-new"].getBool()) {
494 d_theories.push_back(d_theoryArith =
new TheoryArithNew(d_theoryCore));
496 else if ((*d_flags)[
"arith3"].getBool()) {
497 d_theories.push_back(d_theoryArith =
new TheoryArith3(d_theoryCore));
500 d_theories.push_back(d_theoryArith =
new TheoryArithOld(d_theoryCore));
502 d_theoryCore->getExprTrans()->setTheoryArith(d_theoryArith);
503 d_theories.push_back(d_theoryArray =
new TheoryArray(d_theoryCore));
504 d_theories.push_back(d_theoryRecords =
new TheoryRecords(d_theoryCore));
505 d_theories.push_back(d_theorySimulate =
new TheorySimulate(d_theoryCore));
506 d_theories.push_back(d_theoryBitvector =
new TheoryBitvector(d_theoryCore));
507 if ((*d_flags)[
"dt-lazy"].getBool()) {
511 d_theories.push_back(d_theoryDatatype =
new TheoryDatatype(d_theoryCore));
513 d_theories.push_back(d_theoryQuant =
new TheoryQuant(d_theoryCore));
515 d_translator->setTheoryCore(d_theoryCore);
516 d_translator->setTheoryUF(d_theoryUF);
517 d_translator->setTheoryArith(d_theoryArith);
518 d_translator->setTheoryArray(d_theoryArray);
519 d_translator->setTheoryQuant(d_theoryQuant);
520 d_translator->setTheoryRecords(d_theoryRecords);
521 d_translator->setTheorySimulate(d_theorySimulate);
522 d_translator->setTheoryBitvector(d_theoryBitvector);
523 d_translator->setTheoryDatatype(d_theoryDatatype);
528 const string& satEngine = (*d_flags)[
"sat"].getString();
529 if (satEngine ==
"simple")
531 else if (satEngine ==
"fast")
533 else if (satEngine ==
"sat" || satEngine ==
"minisat")
534 d_se =
new SearchSat(d_theoryCore, satEngine);
537 +(*d_flags)[
"sat"].getString());
542 d_stackLevel =
new(
true)
CDO<int>(d_cm->getCurrentContext(), 0);
544 d_theoryCore->setResourceLimit((
unsigned)((*d_flags)[
"resource"].getInt()));
545 d_theoryCore->setTimeLimit((
unsigned)((*d_flags)[
"stimeout"].getInt()));
557 d_translator->finish();
560 TRACE_MSG(
"delete",
"Deleting SearchEngine {");
562 TRACE_MSG(
"delete",
"Finished deleting SearchEngine }");
565 TRACE_MSG(
"delete",
"Deleting d_userAssertions {");
566 delete d_batchedAssertionsIdx;
567 free(d_batchedAssertionsIdx);
568 delete d_batchedAssertions;
569 free(d_batchedAssertions);
570 delete d_userAssertions;
571 free(d_userAssertions);
572 TRACE_MSG(
"delete",
"Finished deleting d_userAssertions }");
581 TRACE_MSG(
"delete",
"Finished clearing d_em }");
583 for(
size_t i=d_theories.size(); i!= 0; ) {
585 string name(d_theories[i]->getName());
586 TRACE(
"delete",
"Deleting Theory[", name,
"] {");
587 delete d_theories[i];
588 TRACE(
"delete",
"Finished deleting Theory[", name,
"] }");
596 TRACE_MSG(
"delete",
"Finished deleting d_tm }");
600 TRACE_MSG(
"delete",
"Finished deleting d_em }");
604 TRACE_MSG(
"delete",
"Finished deleting d_cm }");
606 TRACE_MSG(
"delete",
"Finished deleting d_statistics }");
613 TRACE_MSG(
"delete",
"Deleting d_flags [end of ~VCL()]");
619 IF_DEBUG( CVC3::debugger.finalize(); )
623 void VCL::reprocessFlags() {
624 if (d_se->getName() != (*d_flags)[
"sat"].getString()) {
626 const string& satEngine = (*d_flags)[
"sat"].getString();
627 if (satEngine ==
"simple")
629 else if (satEngine ==
"fast")
631 else if (satEngine ==
"sat" || satEngine ==
"minisat")
632 d_se =
new SearchSat(d_theoryCore, satEngine);
635 +(*d_flags)[
"sat"].getString());
639 if (d_theoryArith->getName() ==
"ArithmeticOld") arithCur = 1;
640 else if (d_theoryArith->getName() ==
"ArithmeticNew") arithCur = 2;
642 DebugAssert(d_theoryArith->getName() ==
"Arithmetic3",
"unexpected name");
647 if ((*d_flags)[
"arith-new"].getBool()) arithNext = 2;
648 else if ((*d_flags)[
"arith3"].getBool()) arithNext = 3;
651 if (arithCur != arithNext) {
652 delete d_theoryArith;
664 d_theories[2] = d_theoryArith;
665 d_translator->setTheoryArith(d_theoryArith);
668 if ((*d_flags)[
"dump-tcc"].getBool()) {
669 d_flags->setFlag(
"translate",
true);
670 d_flags->setFlag(
"pp-batch",
true);
671 d_flags->setFlag(
"tcc",
true);
674 if ((*d_flags)[
"translate"].getBool()) {
675 d_flags->setFlag(
"printResults",
false);
678 if ((*d_flags)[
"pp-bryant"].getBool()) {
679 d_flags->setFlag(
"pp-batch",
true);
683 if ((*d_flags)[
"quant-complete-inst"].getBool() && !(*d_flags)[
"translate"].getBool()) {
684 d_flags->setFlag(
"pp-batch",
true);
687 if ((*d_flags)[
"cnf-formula"].getBool()) {
688 d_flags->setFlag(
"de",
"sat");
689 d_flags->setFlag(
"preprocess",
false);
701 return d_theoryCore->boolType();
707 return d_theoryArith->realType();
712 return d_theoryArith->intType();
717 return d_theoryArith->subrangeType(l, r);
723 return d_theoryCore->newSubtypeExpr(pred, witness);
730 types.push_back(type0);
731 types.push_back(type1);
732 return d_theoryRecords->tupleType(types);
739 types.push_back(type0);
740 types.push_back(type1);
741 types.push_back(type2);
742 return d_theoryRecords->tupleType(types);
746 Type VCL::tupleType(
const vector<Type>& types)
748 return d_theoryRecords->tupleType(types);
752 Type VCL::recordType(
const string& field,
const Type& type)
754 vector<string> fields;
756 fields.push_back(field);
757 kids.push_back(type);
758 return Type(d_theoryRecords->recordType(fields, kids));
762 Type VCL::recordType(
const string& field0,
const Type& type0,
763 const string& field1,
const Type& type1) {
764 vector<string> fields;
766 fields.push_back(field0);
767 fields.push_back(field1);
768 kids.push_back(type0);
769 kids.push_back(type1);
771 return Type(d_theoryRecords->recordType(fields, kids));
775 Type VCL::recordType(
const string& field0,
const Type& type0,
776 const string& field1,
const Type& type1,
777 const string& field2,
const Type& type2)
779 vector<string> fields;
781 fields.push_back(field0);
782 fields.push_back(field1);
783 fields.push_back(field2);
784 kids.push_back(type0);
785 kids.push_back(type1);
786 kids.push_back(type2);
788 return Type(d_theoryRecords->recordType(fields, kids));
792 Type VCL::recordType(
const vector<string>& fields,
793 const vector<Type>& types)
796 "VCL::recordType: number of fields is different \n"
797 "from the number of types");
799 vector<string> fs(fields);
800 vector<Type> ts(types);
802 return Type(d_theoryRecords->recordType(fs, ts));
806 Type VCL::dataType(
const string& name,
807 const string& constructor,
808 const vector<string>& selectors,
const vector<Expr>& types)
810 vector<string> constructors;
811 constructors.push_back(constructor);
813 vector<vector<string> > selectorsVec;
814 selectorsVec.push_back(selectors);
816 vector<vector<Expr> > typesVec;
817 typesVec.push_back(types);
819 return dataType(name, constructors, selectorsVec, typesVec);
823 Type VCL::dataType(
const string& name,
824 const vector<string>& constructors,
825 const vector<vector<string> >& selectors,
826 const vector<vector<Expr> >& types)
828 Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
830 d_translator->dump(res);
836 void VCL::dataType(
const vector<string>& names,
837 const vector<vector<string> >& constructors,
838 const vector<vector<vector<string> > >& selectors,
839 const vector<vector<vector<Expr> > >& types,
840 vector<Type>& returnTypes)
842 Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
844 d_translator->dump(res);
846 for (
int i = 0; i < res.
arity(); ++i) {
847 returnTypes.push_back(
Type(res[i]));
860 return d_theoryBitvector->newBitvectorType(n);
866 return typeDom.
funType(typeRan);
870 Type VCL::funType(
const vector<Type>& typeDom,
const Type& typeRan) {
871 DebugAssert(typeDom.size() >= 1,
"VCL::funType: missing domain types");
872 return Type::funType(typeDom, typeRan);
876 Type VCL::createType(
const string& typeName)
879 d_translator->dump(
Expr(
TYPE, listExpr(idExpr(typeName))));
881 return d_theoryCore->newTypeExpr(typeName);
885 Type VCL::createType(
const string& typeName,
const Type& def)
890 return d_theoryCore->newTypeExpr(typeName, def);
894 Type VCL::lookupType(
const string& typeName)
896 return d_theoryCore->lookupTypeExpr(typeName);
900 Expr VCL::varExpr(
const string& name,
const Type& type)
906 return d_theoryCore->newVar(name, type);
910 Expr VCL::varExpr(
const string& name,
const Type& type,
const Expr& def)
917 if(getFlags()[
"tcc"].getBool()) {
923 if(getBaseType(tpDef) != getBaseType(type)) {
926 " is declared with type:\n "
928 +
"\nBut the type of definition is\n "
931 TRACE(
"tccs",
"CONST def: "+name+
" : "+tpVar.toString()
932 +
" := <value> : ", tpDef,
";");
933 vector<Expr> boundVars;
934 boundVars.push_back(boundVarExpr(name,
"tcc", tpDef));
935 Expr body(boundVars[0].eqExpr(def).impExpr(getTypePred(tpVar, boundVars[0])));
936 Expr quant(forallExpr(boundVars, body));
941 (
"Type mismatch in constant definition:\n"
943 " is declared with type:\n "
945 +
"\nBut the type of definition is\n "
947 +
"\n\n which is not a subtype of the constant");
951 return d_theoryCore->newVar(name, type, def);
955 Expr VCL::lookupVar(
const string& name,
Type* type)
957 return d_theoryCore->lookupVar(name, type);
969 return d_theoryCore->getBaseType(e);
975 return d_theoryCore->getBaseType(t);
981 return d_theoryCore->getTypePred(t, e);
985 Expr VCL::stringExpr(
const string& str) {
986 return getEM()->newStringExpr(str);
990 Expr VCL::idExpr(
const string& name) {
991 return Expr(
ID, stringExpr(name));
995 Expr VCL::listExpr(
const vector<Expr>& kids) {
1015 Expr VCL::listExpr(
const string& op,
const vector<Expr>& kids) {
1016 vector<Expr> newKids;
1017 newKids.push_back(idExpr(op));
1018 newKids.insert(newKids.end(), kids.begin(), kids.end());
1019 return listExpr(newKids);
1037 kids.push_back(idExpr(op));
1041 return listExpr(kids);
1045 void VCL::printExpr(
const Expr& e) {
1050 void VCL::printExpr(
const Expr& e, ostream& os) {
1056 return d_theoryCore->parseExprTop(e);
1061 return Type(d_theoryCore->parseExpr(e));
1078 stringstream ss(s,stringstream::in);
1079 return loadFile(ss,lang,
false);
1082 Expr VCL::exprFromString(
const std::string& s)
1084 stringstream ss(
"PRINT " + s +
";",stringstream::in);
1092 return parseExpr(e[1]);
1097 return d_em->trueExpr();
1103 return d_em->falseExpr();
1115 return left &&
right;
1121 if (children.size() == 0)
1122 throw Exception(
"andExpr requires at least one child");
1129 return left ||
right;
1135 if (children.size() == 0)
1136 throw Exception(
"orExpr requires at least one child");
1137 return Expr(
OR, children);
1155 return child0.
eqExpr(child1);
1158 Expr VCL::distinctExpr(
const std::vector<Expr>& children)
1165 return ifpart.
iteExpr(thenpart, elsepart);
1169 Op VCL::createOp(
const string& name,
const Type& type)
1172 throw Exception(
"createOp: expected function type");
1176 return d_theoryCore->newFunction(name, type,
1177 getFlags()[
"trans-closure"].getBool());
1181 Op VCL::createOp(
const string& name,
const Type& type,
const Expr& def)
1185 (
"Type error in createOp:\n"
1187 " is declared with type:\n "
1189 +
"\n which is not a function type");
1190 if (getBaseType(type) != getBaseType(def.
getType()))
1192 (
"Type mismatch in createOp:\n"
1194 " is declared with type:\n "
1196 +
"\nBut the type of definition is\n "
1198 +
"\n\n which does not match");
1203 if(getFlags()[
"tcc"].getBool()) {
1208 vector<Expr> boundVars;
1209 for (
int i = 0; i < type.
arity()-1; ++i) {
1210 boundVars.push_back(d_em->newBoundVarExpr(type[i]));
1213 Expr body(getTypePred(type[type.
arity()-1], app));
1214 Expr quant(forallExpr(boundVars, body));
1215 Expr tcc = quant.
andExpr(d_theoryCore->getTCC(quant));
1217 bool typesMatch =
true;
1225 (
"Type mismatch in createOp:\n"
1227 " is declared with type:\n "
1229 +
"\nBut the definition is\n "
1231 +
"\n\nwhose type could not be proved to be a subtype");
1235 return d_theoryCore->newFunction(name, type, def);
1239 Op VCL::lookupOp(
const string& name,
Type* type)
1241 return d_theoryCore->lookupFunction(name, type);
1247 return Expr(op, child);
1253 return Expr(op, left, right);
1259 return Expr(op, child0, child1, child2);
1263 Expr VCL::funExpr(
const Op& op,
const vector<Expr>& children)
1265 return Expr(op, children);
1268 bool VCL::addPairToArithOrder(
const Expr& smaller,
const Expr& bigger)
1273 return d_theoryArith->addPairToArithOrder(smaller, bigger);
1279 return d_em->newRatExpr(
Rational(n,d));
1283 Expr VCL::ratExpr(
const string& n,
const string& d,
int base)
1285 return d_em->newRatExpr(
Rational(n.c_str(), d.c_str(), base));
1289 Expr VCL::ratExpr(
const string& n,
int base)
1292 if (pos == string::npos) {
1293 return d_em->newRatExpr(
Rational(n.c_str(), base));
1295 string afterdec = n.substr(pos+1);
1296 string beforedec = n.substr(0, pos);
1297 if (afterdec.size() == 0 || beforedec.size() == 0) {
1298 throw Exception(
"Cannot convert string to rational: "+n);
1300 pos = beforedec.rfind(
".");
1301 if (pos != string::npos) {
1302 throw Exception(
"Cannot convert string to rational: "+n);
1306 if( r < 0 || ((r == 0) && (beforedec.rfind(
"-") != string::npos)) ) {
1307 r = r - (fracPart /
pow(afterdec.size(), (
Rational)base));
1310 r = r + (fracPart /
pow(afterdec.size(), (
Rational)base));
1312 return d_em->newRatExpr(r);
1324 return left +
right;
1335 return left -
right;
1341 return left *
right;
1381 Expr VCL::recordExpr(
const string& field,
const Expr& expr)
1383 vector<string> fields;
1385 kids.push_back(expr);
1386 fields.push_back(field);
1387 return d_theoryRecords->recordExpr(fields, kids);
1391 Expr VCL::recordExpr(
const string& field0,
const Expr& expr0,
1392 const string& field1,
const Expr& expr1)
1394 vector<string> fields;
1396 fields.push_back(field0);
1397 fields.push_back(field1);
1398 kids.push_back(expr0);
1399 kids.push_back(expr1);
1400 sort2(fields, kids);
1401 return d_theoryRecords->recordExpr(fields, kids);
1405 Expr VCL::recordExpr(
const string& field0,
const Expr& expr0,
1406 const string& field1,
const Expr& expr1,
1407 const string& field2,
const Expr& expr2)
1409 vector<string> fields;
1411 fields.push_back(field0);
1412 fields.push_back(field1);
1413 fields.push_back(field2);
1414 kids.push_back(expr0);
1415 kids.push_back(expr1);
1416 kids.push_back(expr2);
1417 sort2(fields, kids);
1418 return d_theoryRecords->recordExpr(fields, kids);
1422 Expr VCL::recordExpr(
const vector<string>& fields,
1423 const vector<Expr>& exprs)
1425 DebugAssert(fields.size() > 0,
"VCL::recordExpr()");
1426 DebugAssert(fields.size() == exprs.size(),
"VCL::recordExpr()");
1428 vector<string> fs(fields);
1429 vector<Expr> es(exprs);
1431 return d_theoryRecords->recordExpr(fs, es);
1435 Expr VCL::recSelectExpr(
const Expr& record,
const string& field)
1437 return d_theoryRecords->recordSelect(record, field);
1441 Expr VCL::recUpdateExpr(
const Expr& record,
const string& field,
1442 const Expr& newValue)
1444 return d_theoryRecords->recordUpdate(record, field, newValue);
1456 return Expr(
WRITE, array, index, newValue);
1460 Expr VCL::newBVConstExpr(
const std::string& s,
int base)
1462 return d_theoryBitvector->newBVConstExpr(s, base);
1466 Expr VCL::newBVConstExpr(
const std::vector<bool>& bits)
1468 return d_theoryBitvector->newBVConstExpr(bits);
1474 return d_theoryBitvector->newBVConstExpr(r, len);
1480 return d_theoryBitvector->newConcatExpr(t1, t2);
1484 Expr VCL::newConcatExpr(
const std::vector<Expr>& kids)
1486 return d_theoryBitvector->newConcatExpr(kids);
1490 Expr VCL::newBVExtractExpr(
const Expr& e,
int hi,
int low)
1492 return d_theoryBitvector->newBVExtractExpr(e, hi, low);
1498 return d_theoryBitvector->newBVNegExpr(t1);
1504 return d_theoryBitvector->newBVAndExpr(t1, t2);
1508 Expr VCL::newBVAndExpr(
const std::vector<Expr>& kids)
1510 return d_theoryBitvector->newBVAndExpr(kids);
1516 return d_theoryBitvector->newBVOrExpr(t1, t2);
1520 Expr VCL::newBVOrExpr(
const std::vector<Expr>& kids)
1522 return d_theoryBitvector->newBVOrExpr(kids);
1528 return d_theoryBitvector->newBVXorExpr(t1, t2);
1532 Expr VCL::newBVXorExpr(
const std::vector<Expr>& kids)
1534 return d_theoryBitvector->newBVXorExpr(kids);
1540 return d_theoryBitvector->newBVXnorExpr(t1, t2);
1544 Expr VCL::newBVXnorExpr(
const std::vector<Expr>& kids)
1546 return d_theoryBitvector->newBVXnorExpr(kids);
1552 return d_theoryBitvector->newBVNandExpr(t1, t2);
1558 return d_theoryBitvector->newBVNorExpr(t1, t2);
1564 return d_theoryBitvector->newBVCompExpr(t1, t2);
1570 return d_theoryBitvector->newBVLTExpr(t1, t2);
1576 return d_theoryBitvector->newBVLEExpr(t1, t2);
1582 return d_theoryBitvector->newBVSLTExpr(t1, t2);
1588 return d_theoryBitvector->newBVSLEExpr(t1, t2);
1594 return d_theoryBitvector->newSXExpr(t1, len);
1600 return d_theoryBitvector->newBVUminusExpr(t1);
1606 return d_theoryBitvector->newBVSubExpr(t1, t2);
1610 Expr VCL::newBVPlusExpr(
int numbits,
const std::vector<Expr>& k)
1612 return d_theoryBitvector->newBVPlusPadExpr(numbits, k);
1617 std::vector<Expr> k;
1620 return newBVPlusExpr(numbits, k);
1626 return d_theoryBitvector->newBVMultPadExpr(numbits, t1, t2);
1631 return d_theoryBitvector->newBVUDivExpr(t1, t2);
1636 return d_theoryBitvector->newBVURemExpr(t1, t2);
1641 return d_theoryBitvector->newBVSDivExpr(t1, t2);
1646 return d_theoryBitvector->newBVSRemExpr(t1, t2);
1651 return d_theoryBitvector->newBVSModExpr(t1, t2);
1657 return d_theoryBitvector->newFixedLeftShiftExpr(t1, r);
1661 Expr VCL::newFixedConstWidthLeftShiftExpr(
const Expr& t1,
int r)
1663 return d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t1, r);
1667 Expr VCL::newFixedRightShiftExpr(
const Expr& t1,
int r)
1669 return d_theoryBitvector->newFixedRightShiftExpr(t1, r);
1693 return d_theoryBitvector->computeBVConst(e);
1697 Expr VCL::tupleExpr(
const vector<Expr>& exprs) {
1698 DebugAssert(exprs.size() > 0,
"VCL::tupleExpr()");
1699 return d_theoryRecords->tupleExpr(exprs);
1703 Expr VCL::tupleSelectExpr(
const Expr& tuple,
int index)
1705 return d_theoryRecords->tupleSelect(tuple, index);
1709 Expr VCL::tupleUpdateExpr(
const Expr& tuple,
int index,
const Expr& newValue)
1711 return d_theoryRecords->tupleUpdate(tuple, index, newValue);
1715 Expr VCL::datatypeConsExpr(
const string& constructor,
const vector<Expr>& args)
1717 return d_theoryDatatype->datatypeConsExpr(constructor, args);
1721 Expr VCL::datatypeSelExpr(
const string& selector,
const Expr& arg)
1723 return d_theoryDatatype->datatypeSelExpr(selector, arg);
1727 Expr VCL::datatypeTestExpr(
const string& constructor,
const Expr& arg)
1729 return d_theoryDatatype->datatypeTestExpr(constructor, arg);
1733 Expr VCL::boundVarExpr(
const string& name,
const string& uid,
1735 return d_em->newBoundVarExpr(name, uid, type);
1739 Expr VCL::forallExpr(
const vector<Expr>& vars,
const Expr& body) {
1740 DebugAssert(vars.size() > 0,
"VCL::foralLExpr()");
1741 return d_em->newClosureExpr(
FORALL, vars, body);
1744 Expr VCL::forallExpr(
const vector<Expr>& vars,
const Expr& body,
1745 const Expr& trigger) {
1746 DebugAssert(vars.size() > 0,
"VCL::foralLExpr()");
1747 return d_em->newClosureExpr(
FORALL, vars, body, trigger);
1750 Expr VCL::forallExpr(
const vector<Expr>& vars,
const Expr& body,
1751 const vector<Expr>& triggers) {
1752 DebugAssert(vars.size() > 0,
"VCL::foralLExpr()");
1753 return d_em->newClosureExpr(
FORALL, vars, body, triggers);
1756 Expr VCL::forallExpr(
const vector<Expr>& vars,
const Expr& body,
1757 const vector<vector<Expr> >& triggers) {
1758 DebugAssert(vars.size() > 0,
"VCL::foralLExpr()");
1759 return d_em->newClosureExpr(
FORALL, vars, body, triggers);
1762 void VCL::setTriggers(
const Expr& e,
const vector< vector<Expr> >& triggers) {
1766 void VCL::setTriggers(
const Expr& e,
const vector<Expr>& triggers) {
1770 void VCL::setTrigger(
const Expr& e,
const Expr& trigger) {
1774 void VCL::setMultiTrigger(
const Expr& e,
const vector<Expr>& multiTrigger) {
1778 Expr VCL::existsExpr(
const vector<Expr>& vars,
const Expr& body) {
1779 return d_em->newClosureExpr(
EXISTS, vars, body);
1783 Op VCL::lambdaExpr(
const vector<Expr>& vars,
const Expr& body) {
1784 return d_em->newClosureExpr(
LAMBDA, vars, body).mkOp();
1787 Op VCL::transClosure(
const Op& op) {
1794 const vector<Expr>& inputs,
const Expr& n) {
1798 kids.insert(kids.end(), inputs.begin(), inputs.end());
1804 void VCL::setResourceLimit(
unsigned limit)
1806 d_theoryCore->setResourceLimit(limit);
1817 d_lastQueryTCC = tccThm;
1823 +
"\n\nWhich simplified to:\n\n "
1824 +simplify(tcc).toString()
1825 +
"\n\nAnd the last formula is not valid "
1826 "in the current context.");
1829 "Unable to verify TCC:\n\n "
1831 +
"\n\nWhich simplified to:\n\n "
1832 +simplify(tcc).toString());
1835 "Unable to verify TCC:\n\n "
1837 +
"\n\nWhich simplified to:\n\n "
1838 +simplify(tcc).toString()
1839 +
"\n\nAnd the last formula is unknown "
1840 "in the current context.");
1848 void VCL::assertFormula(
const Expr& e)
1850 if (getFlags()[
"no-save-model"].getBool() && d_modelStackPushed) {
1851 d_modelStackPushed =
false;
1859 +
"\nDerived type of the formula:\n "
1863 if (getFlags()[
"pp-batch"].getBool()) {
1864 d_batchedAssertions->push_back(e);
1870 if (getFlags()[
"preSimplify"].getBool()) {
1871 e2 = d_theoryCore->getExprTrans()->preprocess(e).getRHS();
1873 if (d_translator->dumpAssertion(e2))
return;
1876 TRACE(
"vclassertFormula",
"VCL::assertFormula(", e,
") {");
1879 if(d_userAssertions->count(e) > 0) {
1880 TRACE_MSG(
"vclassertFormula",
"VCL::assertFormula[repeated assertion] => }");
1885 if(getFlags()[
"tcc"].getBool()) {
1886 Expr tcc(d_theoryCore->getTCC(e));
1887 tccThm = checkTCC(tcc);
1890 Theorem thm = d_se->newUserAssumption(e);
1891 (*d_userAssertions)[e] =
UserAssertion(thm, tccThm, d_nextIdx++);
1893 TRACE_MSG(
"vclassertFormula",
"VCL::assertFormula => }");
1897 void VCL::registerAtom(
const Expr& e)
1900 d_se->registerAtom(e);
1907 Theorem thm = d_se->getImpliedLiteral();
1915 return simplifyThm(e).getRHS();
1922 Theorem res = d_theoryCore->getExprTrans()->preprocess(e);
1924 res = d_theoryCore->transitivityRule(res, simpThm);
1931 TRACE(
"query",
"VCL::query(", e,
") {");
1933 if (getFlags()[
"no-save-model"].getBool()) {
1934 if(d_modelStackPushed) {
1935 d_modelStackPushed =
false;
1939 d_modelStackPushed =
true;
1946 +
"\nDerived type of the formula:\n "
1951 if (getFlags()[
"pp-batch"].getBool()) {
1954 for (; (*d_batchedAssertionsIdx) < d_batchedAssertions->size();
1955 (*d_batchedAssertionsIdx) = (*d_batchedAssertionsIdx) + 1) {
1956 kids.push_back((*d_batchedAssertions)[(*d_batchedAssertionsIdx)]);
1958 if (kids.size() > 0) {
1959 qExpr = kids.size() == 1 ? kids[0] :
Expr(
AND, kids);
1964 if (d_dump && !getFlags()[
"dump-tcc"].getBool()) {
1966 if (getFlags()[
"preSimplify"].getBool()) {
1967 e2 = d_theoryCore->getExprTrans()->preprocess(qExpr).getRHS();
1969 if (d_translator->dumpQuery(e2))
return UNKNOWN;
1973 Theorem tccThm = d_se->getCommonRules()->trueTheorem();
1974 if(getFlags()[
"tcc"].getBool()) {
1975 Expr tcc(d_theoryCore->getTCC(qExpr));
1976 if (getFlags()[
"dump-tcc"].getBool()) {
1978 if (getFlags()[
"preSimplify"].getBool()) {
1979 e2 = d_theoryCore->getExprTrans()->preprocess(tcc).getRHS();
1981 if (d_translator->dumpQuery(e2))
return UNKNOWN;
1984 tccThm = checkTCC(tcc);
1990 d_lastQuery = d_se->getCommonRules()->queryTCC(res, tccThm);
1997 TRACE(
"query",
"VCL::query => ",
1998 qres ==
VALID ?
"VALID" :
2000 qres ==
ABORT ?
"ABORT" :
"UNKNOWN",
" }");
2002 if (d_dump) d_translator->dumpQueryResult(qres);
2010 return query(e.
negate());
2017 d_translator->dump(d_em->newLeafExpr(
CONTINUE),
true);
2019 vector<Expr> assertions;
2020 d_se->getCounterExample(assertions);
2022 if (assertions.size() == 0) {
2023 return d_se->restart(falseExpr(), thm);
2025 Expr eAnd = assertions.size() == 1 ? assertions[0] :
andExpr(assertions);
2026 return d_se->restart(!eAnd, thm);
2036 return d_se->restart(e, thm);
2040 void VCL::returnFromCheck()
2043 d_se->returnFromCheck();
2047 void VCL::getUserAssumptions(vector<Expr>& assumptions)
2050 d_se->getUserAssumptions(assumptions);
2054 void VCL::getInternalAssumptions(vector<Expr>& assumptions)
2057 d_se->getInternalAssumptions(assumptions);
2061 void VCL::getAssumptions(vector<Expr>& assumptions)
2064 d_translator->dump(d_em->newLeafExpr(
ASSUMPTIONS),
true);
2066 d_se->getAssumptions(assumptions);
2073 if (d_lastQuery.isNull()){
2075 (
"Invalid Query,n");
2077 return d_lastQuery.getExpr();
2085 void VCL::getAssumptionsUsed(vector<Expr>& assumptions)
2087 throw EvalException (
"getAssumptionsUsed not currently supported");
2091 Theorem thm = d_se->lastThm();
2092 if (thm.
isNull())
return;
2097 void VCL::getCounterExample(vector<Expr>& assertions,
bool inOrder)
2102 if (!(*d_flags)[
"translate"].getBool())
2103 d_se->getCounterExample(assertions, inOrder);
2110 d_translator->dump(d_em->newLeafExpr(
COUNTERMODEL),
true);
2112 if (!(*d_flags)[
"translate"].getBool())
2113 d_se->getConcreteModel(m);
2117 if (!d_theoryCore->incomplete())
throw Exception(
"Model generation should be called only after an UNKNOWN result");
2119 int scopeLevel = d_cm->scopeLevel();
2126 if (d_se->tryModelGeneration(thm))
2132 vector<Expr> assumptions;
2136 while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
2138 qres = restart(
orExpr(assumptions));
2140 scopeLevel = d_cm->scopeLevel();
2145 while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
2152 return d_se->getValue(e);
2155 bool VCL::inconsistent(vector<Expr>& assumptions)
2158 if (d_theoryCore->inconsistent()) {
2160 getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
2167 bool VCL::inconsistent()
2169 return d_theoryCore->inconsistent();
2173 bool VCL::incomplete() {
2176 return (d_lastQuery.isNull() && d_theoryCore->incomplete());
2180 bool VCL::incomplete(vector<string>& reasons) {
2183 return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
2190 d_translator->dump(d_em->newLeafExpr(
DUMP_PROOF),
true);
2193 if(d_lastQuery.isNull())
2195 (
"Method getProof() (or command DUMP_PROOF)\n"
2196 " must be called only after a Valid QUERY");
2197 return d_se->getProof();
2204 return d_theoryCore->getAssignment();
2217 d_translator->dump(d_em->newLeafExpr(
DUMP_TCC),
true);
2219 if(d_lastQueryTCC.isNull())
return null;
2220 else return d_lastQueryTCC.getExpr();
2224 void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
2229 if(d_lastQuery.isNull())
2231 (
"Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
2232 " must be called only after a Valid QUERY");
2233 getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
2242 if(d_lastQueryTCC.isNull())
return null;
2243 else return d_lastQueryTCC.getProof();
2250 d_translator->dump(d_em->newLeafExpr(
DUMP_CLOSURE),
true);
2252 if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
2254 d_lastClosure = deriveClosure(d_lastQuery);
2256 if(d_lastClosure.isNull())
return null;
2257 else return d_lastClosure.getExpr();
2266 if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
2268 d_lastClosure = deriveClosure(d_lastQuery);
2270 if(d_lastClosure.isNull())
return null;
2271 else return d_lastClosure.getProof();
2275 int VCL::stackLevel()
2277 return d_stackLevel->get();
2283 if (getFlags()[
"no-save-model"].getBool() && d_modelStackPushed) {
2284 d_modelStackPushed =
false;
2286 }
else if (d_dump) {
2287 d_translator->dump(d_em->newLeafExpr(
PUSH),
true);
2290 d_stackLevel->set(stackLevel()+1);
2296 if (getFlags()[
"no-save-model"].getBool() && d_modelStackPushed) {
2297 d_modelStackPushed =
false;
2299 }
else if (d_dump) {
2300 d_translator->dump(d_em->newLeafExpr(
POP),
true);
2302 if (stackLevel() == 0) {
2304 (
"POP called with no previous call to PUSH");
2306 int level = stackLevel();
2307 while (level == stackLevel())
2312 void VCL::popto(
int toLevel)
2316 d_translator->dump(
Expr(
POPTO, ratExpr(toLevel, 1)),
true);
2318 if (toLevel < 0) toLevel = 0;
2319 while (stackLevel() > toLevel) {
2325 int VCL::scopeLevel()
2327 return d_cm->scopeLevel();
2331 void VCL::pushScope()
2333 throw EvalException (
"Scope-level push/pop is no longer supported");
2336 d_translator->dump(d_em->newLeafExpr(
PUSH_SCOPE),
true);
2338 IF_DEBUG(
if((*d_flags)[
"dump-trace"].getString() !=
"")
2339 dumpTrace(scopeLevel());)
2343 void VCL::popScope()
2345 throw EvalException (
"Scope-level push/pop is no longer supported");
2347 d_translator->dump(d_em->newLeafExpr(
POP_SCOPE),
true);
2349 if (scopeLevel() == 1) {
2350 cout <<
"Cannot POP from scope level 1" <<
endl;
2353 IF_DEBUG(
if((*d_flags)[
"dump-trace"].getString() !=
"")
2354 dumpTrace(scopeLevel());)
2358 void VCL::poptoScope(
int toLevel)
2360 throw EvalException (
"Scope-level push/pop is no longer supported");
2368 else d_cm->popto(toLevel);
2369 IF_DEBUG(
if((*d_flags)[
"dump-trace"].getString() !=
"")
2370 dumpTrace(scopeLevel());)
2376 return d_cm->getCurrentContext();
2386 void VCL::logAnnotation(
const Expr& annot)
2389 d_translator->dump(annot);
2394 bool interactive,
bool calledFromParser) {
2396 Parser parser(
this, d_translator, lang, interactive, fileName);
2397 VCCmd cmd(
this, &parser, calledFromParser);
2405 Parser parser(
this, d_translator, lang, is, interactive);
2406 VCCmd cmd(
this, &parser);
2415 unsigned long VCL::getMemory(
int verbosity)
2417 unsigned long memSelf =
sizeof(
VCL);
2418 unsigned long mem = 0;
2420 mem += d_cm->getMemory(verbosity - 1);
2421 mem += d_em->getMemory(verbosity - 1);
2447 MemoryTracker::print(
"VCL", verbosity, memSelf, mem);
2449 return mem + memSelf;
2452 void VCL::setTimeLimit(
unsigned limit) {
2453 d_theoryCore->setTimeLimit(limit);