CVC3  2.4.1
vcl.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file vcl.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Tue Dec 31 18:27:11 2002
8  *
9  * <hr>
10  * License to use, copy, modify, sell and/or distribute this software
11  * and its documentation for any purpose is hereby granted without
12  * royalty, subject to the terms and conditions defined in the \ref
13  * LICENSE file provided with this distribution.
14  *
15  * <hr>
16  *
17  */
18 /*****************************************************************************/
19 
20 
21 #include <fstream>
22 #include "os.h"
23 #include "vcl.h"
24 #include "parser.h"
25 #include "vc_cmd.h"
26 #include "search_simple.h"
27 #include "search_fast.h"
28 #include "search_sat.h"
29 #include "theory_core.h"
30 #include "theory_uf.h"
31 #include "theory_arith_old.h"
32 #include "theory_arith_new.h"
33 #include "theory_arith3.h"
34 #include "theory_bitvector.h"
35 #include "theory_array.h"
36 #include "theory_quant.h"
37 #include "theory_records.h"
38 #include "theory_simulate.h"
39 #include "theory_datatype.h"
40 #include "theory_datatype_lazy.h"
41 #include "translator.h"
42 #include "typecheck_exception.h"
43 #include "eval_exception.h"
44 #include "expr_transform.h"
45 #include "theorem_manager.h"
46 #include "assumptions.h"
47 #include "parser_exception.h"
48 
49 
50 using namespace std;
51 using namespace CVC3;
52 
53 //namespace CVC3{
54 // VCL* myvcl;
55 //}
56 
57 ///////////////////////////////////////////////////////////////////////////////
58 // Static ValidityChecker methods
59 ///////////////////////////////////////////////////////////////////////////////
60 
61 
62 
63 ValidityChecker* ValidityChecker::create(const CLFlags& flags)
64 {
65  return new VCL(flags);
66 }
67 
68 
69 CLFlags ValidityChecker::createFlags() {
70  CLFlags flags;
71  // We expect the user to type cvc3 -h to get help, which will set
72  // the "help" flag to false; that's why it's initially true.
73 
74  // Overall system control 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)"));
79 
80  // Information printing flags
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."));
92 
93  //Translation related flags
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));
112 
113  // Parser related flags
114  flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax", false));
115 
116  // Pretty-printing related flags
117  flags.addFlag("dagify-exprs",
118  CLFlag(true, "Print expressions with sharing as DAGs"));
119  flags.addFlag("lang", CLFlag("presentation", "Input language "
120  "(presentation, smt, smt2, internal)"));
121  flags.addFlag("output-lang", CLFlag("", "Output language "
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 "));
127 
128  // Search Engine (SAT) related flags
129  flags.addFlag("sat",CLFlag("minisat", "choose a SAT solver to use "
130  "(sat, minisat)"));
131  flags.addFlag("de",CLFlag("dfs", "choose a decision engine to use "
132  "(dfs, sat)"));
133 
134  // Proofs and Assumptions
135  flags.addFlag("proofs", CLFlag(false, "Produce proofs"));
136  flags.addFlag("check-proofs",
137  CLFlag(IF_DEBUG(true ||) false, "Check proofs on-the-fly"));
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"));
141 
142 
143  // Core framework switches
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));
152  flags.addFlag("ite-cond-simp",
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));
164 
165  // Negate the query when translate into tptp
166  flags.addFlag("negate-query", CLFlag(true, "Negate the query when translate into TPTP format"));;
167 
168  // Concrete model generation (counterexamples) flags
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"));
173  // Debugging flags (only for the debug build)
174  // #ifdef _CVC3_DEBUG_MODE
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 \"\")"));
179  // #endif
180  // DP-specific flags
181 
182  // Arithmetic
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));
185  flags.addFlag("var-order",
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)"));
188 
189  flags.addFlag("nonlinear-sign-split", CLFlag(true, "Whether to split on the signs of nontrivial nonlinear terms"));
190 
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)"));
193 
194  // Arrays
195  flags.addFlag("liftReadIte", CLFlag(true, "Lift read of ite"));
196 
197  //for LFSC stuff, disable Tseitin CNF conversion, by Yeting
198  flags.addFlag("cnf-formula", CLFlag(false, "The input must be in CNF. This option automatically enables '-de sat' and disable preprocess"));
199 
200  //for LFSC print out, by Yeting
201  //flags.addFlag("lfsc", CLFlag(false, "the input is already in CNF. This option automatically enables -de sat and disable -preprocess"));
202 
203  // for LFSC print, allows different modes by Liana
204  flags.addFlag("lfsc-mode",
205  CLFlag(0, "lfsc mode 0: off, 1:normal, 2:cvc3-mimic etc."));
206 
207 
208  // Quantifiers
209  flags.addFlag("max-quant-inst", CLFlag(200, "The maximum number of"
210  " naive instantiations"));
211 
212  flags.addFlag("quant-new",
213  CLFlag(true, "If this option is false, only naive instantiation is called"));
214 
215  flags.addFlag("quant-lazy", CLFlag(false, "Instantiate lazily", false));
216 
217  flags.addFlag("quant-sem-match",
218  CLFlag(false, "Attempt to match semantically when instantiating", false));
219 
220 // flags.addFlag("quant-const-match",
221 // CLFlag(true, "When matching semantically, only match with constants", false));
222 
223  flags.addFlag("quant-complete-inst",
224  CLFlag(false, "Try complete instantiation heuristic. +pp-batch will be automatically enabled"));
225 
226  flags.addFlag("quant-max-IL",
227  CLFlag(100, "The maximum Instantiation Level allowed"));
228 
229  flags.addFlag("quant-inst-lcache",
230  CLFlag(true, "Cache instantiations"));
231 
232  flags.addFlag("quant-inst-gcache",
233  CLFlag(false, "Cache instantiations", false));
234 
235  flags.addFlag("quant-inst-tcache",
236  CLFlag(false, "Cache instantiations", false));
237 
238 
239  flags.addFlag("quant-inst-true",
240  CLFlag(true, "Ignore true instantiations"));
241 
242  flags.addFlag("quant-pullvar",
243  CLFlag(false, "Pull out vars", false));
244 
245  flags.addFlag("quant-score",
246  CLFlag(true, "Use instantiation level"));
247 
248  flags.addFlag("quant-polarity",
249  CLFlag(false, "Use polarity ", false));
250 
251  flags.addFlag("quant-eqnew",
252  CLFlag(true, "Use new equality matching"));
253 
254  flags.addFlag("quant-max-score",
255  CLFlag(0, "Maximum initial dynamic score"));
256 
257  flags.addFlag("quant-trans3",
258  CLFlag(true, "Use trans heuristic"));
259 
260  flags.addFlag("quant-trans2",
261  CLFlag(true, "Use trans2 heuristic"));
262 
263  flags.addFlag("quant-naive-num",
264  CLFlag(1000, "Maximum number to call naive instantiation"));
265 
266  flags.addFlag("quant-naive-inst",
267  CLFlag(true, "Use naive instantiation"));
268 
269  flags.addFlag("quant-man-trig",
270  CLFlag(true, "Use manual triggers"));
271 
272  flags.addFlag("quant-gfact",
273  CLFlag(false, "Send facts to core directly", false));
274 
275  flags.addFlag("quant-glimit",
276  CLFlag(1000, "Limit for gfacts", false));
277 
278  flags.addFlag("print-var-type", //by yeting, as requested by Sascha Boehme for proofs
279  CLFlag(false, "Print types for bound variables"));
280 
281  //Bitvectors
282  flags.addFlag("bv32-flag",
283  CLFlag(false, "assume that all bitvectors are 32bits with no overflow", false));
284 
285  // Uninterpreted Functions
286  flags.addFlag("trans-closure",
287  CLFlag(false,"enables transitive closure of binary relations", false));
288 
289  // Datatypes
290  flags.addFlag("dt-smartsplits",
291  CLFlag(true, "enables smart splitting in datatype theory", false));
292  flags.addFlag("dt-lazy",
293  CLFlag(false, "lazy splitting on datatypes", false));
294 
295 
296  return flags;
297 }
298 
299 
300 ValidityChecker* ValidityChecker::create()
301 {
302  return new VCL(createFlags());
303 }
304 
305 
306 ///////////////////////////////////////////////////////////////////////////////
307 // VCL private methods
308 ///////////////////////////////////////////////////////////////////////////////
309 
310 
311 Theorem3 VCL::deriveClosure(const Theorem3& thm) {
312  vector<Expr> assump;
313  set<UserAssertion> assumpSet;
314  // Compute the vector of assumptions for thm, and iteratively move
315  // the assumptions to the RHS until done. Each closure step may
316  // introduce new assumptions from the proofs of TCCs, so those need
317  // to be dealt with in the same way, until no assumptions remain.
318  Theorem3 res = thm;
319  vector<Theorem> tccs;
320  while(true) {
321  {
322  const Assumptions& a(res.getAssumptionsRef());
323  if (a.empty()) break;
324  assump.clear();
325  assumpSet.clear();
326  Assumptions::iterator i=a.begin(), iend=a.end();
327  if(i!=iend) i->clearAllFlags();
328  // Collect the assumptions of 'res' *without* TCCs
329  for(; i!=iend; ++i)
330  getAssumptionsRec(*i, assumpSet, false);
331 
332  // Build the vectors of assumptions and TCCs
333  if(getFlags()["tcc"].getBool()) {
334  tccs.clear();
335  for(set<UserAssertion>::iterator i=assumpSet.begin(),
336  iend=assumpSet.end(); i!=iend; ++i) {
337  assump.push_back(i->thm().getExpr());
338  tccs.push_back(i->tcc());
339  }
340  }
341  }
342  // Derive the closure
343  res = d_se->getCommonRules()->implIntro3(res, assump, tccs);
344  }
345  return res;
346 }
347 
348 
349 //! Recursive assumption graph traversal to find user assumptions
350 /*!
351  * If an assumption has a TCC, traverse the proof of TCC and add its
352  * assumptions to the set recursively.
353  */
354 void VCL::getAssumptionsRec(const Theorem& thm,
355  set<UserAssertion>& assumptions,
356  bool addTCCs) {
357  if(thm.isNull() || thm.isRefl() || thm.isFlagged()) return;
358  thm.setFlag();
359  if(thm.isAssump()) {
360  if(d_userAssertions->count(thm.getExpr())>0) {
361  const UserAssertion& a = (*d_userAssertions)[thm.getExpr()];
362  assumptions.insert(a);
363  if(addTCCs) {
364  DebugAssert(!a.tcc().isNull(), "getAssumptionsRec(a="
365  +a.thm().toString()+", thm = "+thm.toString()+")");
366  getAssumptionsRec(a.tcc(), assumptions, true);
367  }
368  } else { // it's a splitter
369  UserAssertion a(thm, Theorem(), d_nextIdx++);
370  assumptions.insert(a);
371  }
372  }
373  else {
374  const Assumptions& a(thm.getAssumptionsRef());
375  for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
376  getAssumptionsRec(*i, assumptions, addTCCs);
377  }
378 }
379 
380 
381 void VCL::getAssumptions(const Assumptions& a, vector<Expr>& assumptions)
382 {
383  set<UserAssertion> assumpSet;
384  if(a.empty()) return;
385  Assumptions::iterator i=a.begin(), iend=a.end();
386  if(i!=iend) i->clearAllFlags();
387  for(; i!=iend; ++i)
388  getAssumptionsRec(*i, assumpSet, getFlags()["tcc"].getBool());
389  // Order assumptions by their creation time
390  for(set<UserAssertion>::iterator i=assumpSet.begin(), iend=assumpSet.end();
391  i!=iend; ++i)
392  assumptions.push_back(i->thm().getExpr());
393 }
394 
395 
397 void VCL::dumpTrace(int scope) {
398  vector<StrPair> fields;
399  fields.push_back(strPair("scope", int2string(scope)));
400  debugger.dumpTrace("scope", fields);
401 }
402 )
403 
404 
405 ///////////////////////////////////////////////////////////////////////////////
406 // Public VCL methods
407 ///////////////////////////////////////////////////////////////////////////////
408 
409 
410 VCL::VCL(const CLFlags& flags)
411  : d_flags(new CLFlags(flags))
412 {
413  // Set the dependent flags so that they are consistent
414 
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);
419  }
420 
421  if ((*d_flags)["translate"].getBool()) {
422  d_flags->setFlag("printResults", false);
423  }
424 
425  if ((*d_flags)["pp-bryant"].getBool()) {
426  d_flags->setFlag("pp-batch", true);
427  }
428 
429  //added by Yeting
430  if ((*d_flags)["quant-complete-inst"].getBool() && !(*d_flags)["translate"].getBool()) {
431  d_flags->setFlag("pp-batch", true);
432  }
433 
434  //added by Yeting
435  if ((*d_flags)["cnf-formula"].getBool()) {
436  d_flags->setFlag("de", "sat");
437  d_flags->setFlag("preprocess", false);
438  }
439 
440 
441  IF_DEBUG( // Initialize the global debugger
442  CVC3::debugger.init(&((*d_flags)["trace"].getStrVec()),
443  &((*d_flags)["dump-trace"].getString()));
444  )
445  init();
446 }
447 
448 
449 void VCL::init()
450 {
451  d_nextIdx = 0;
452 
453  d_statistics = new Statistics();
454 
455  d_cm = new ContextManager();
456 
457  // Initialize the database of user assertions. It has to be
458  // initialized after d_cm.
459  d_userAssertions = new(true) CDMap<Expr,UserAssertion>(getCurrentContext());
460  d_batchedAssertions = new(true) CDList<Expr>(getCurrentContext());
461  d_batchedAssertionsIdx = new(true) CDO<unsigned>(getCurrentContext(), 0);
462 
463  d_em = new ExprManager(d_cm, *d_flags);
464 
465  d_tm = new TheoremManager(d_cm, d_em, *d_flags);
466  d_em->setTM(d_tm);
467 
468  d_translator = new Translator(d_em,
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());
479 
480  d_dump = d_translator->start((*d_flags)["dump-log"].getString());
481 
482  d_theoryCore = new TheoryCore(d_cm, d_em, d_tm, d_translator, *d_flags, *d_statistics);
483 
484  DebugAssert(d_theories.size() == 0, "Expected empty theories array");
485  d_theories.push_back(d_theoryCore);
486 
487  // Fast rewriting of literals is done by setting their find to true or false.
488  falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr()));
489  trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr()));
490 
491  d_theories.push_back(d_theoryUF = new TheoryUF(d_theoryCore));
492 
493  if ((*d_flags)["arith-new"].getBool()) {
494  d_theories.push_back(d_theoryArith = new TheoryArithNew(d_theoryCore));
495  }
496  else if ((*d_flags)["arith3"].getBool()) {
497  d_theories.push_back(d_theoryArith = new TheoryArith3(d_theoryCore));
498  }
499  else {
500  d_theories.push_back(d_theoryArith = new TheoryArithOld(d_theoryCore));
501  }
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()) {
508  d_theories.push_back(d_theoryDatatype = new TheoryDatatypeLazy(d_theoryCore));
509  }
510  else {
511  d_theories.push_back(d_theoryDatatype = new TheoryDatatype(d_theoryCore));
512  }
513  d_theories.push_back(d_theoryQuant = new TheoryQuant(d_theoryCore));
514 
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);
524 
525  // Must be created after TheoryCore, since it needs it.
526  // When we have more than one search engine, select one to create
527  // based on flags
528  const string& satEngine = (*d_flags)["sat"].getString();
529  if (satEngine == "simple")
530  d_se = new SearchSimple(d_theoryCore);
531  else if (satEngine == "fast")
532  d_se = new SearchEngineFast(d_theoryCore);
533  else if (satEngine == "sat" || satEngine == "minisat")
534  d_se = new SearchSat(d_theoryCore, satEngine);
535  else
536  throw CLException("Unrecognized SAT solver name: "
537  +(*d_flags)["sat"].getString());
538 
539  // Initial scope level should be 1
540  d_cm->push();
541 
542  d_stackLevel = new(true) CDO<int>(d_cm->getCurrentContext(), 0);
543 
544  d_theoryCore->setResourceLimit((unsigned)((*d_flags)["resource"].getInt()));
545  d_theoryCore->setTimeLimit((unsigned)((*d_flags)["stimeout"].getInt()));
546 
547  // myvcl = this;
548 }
549 
550 
551 void VCL::destroy()
552 {
553  popto(0);
554  d_cm->popto(0);
555  delete d_stackLevel;
556  free(d_stackLevel);
557  d_translator->finish();
558  delete d_translator;
559 
560  TRACE_MSG("delete", "Deleting SearchEngine {");
561  delete d_se;
562  TRACE_MSG("delete", "Finished deleting SearchEngine }");
563  // This map contains expressions and theorems; delete it before
564  // d_em, d_tm, and d_cm.
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 }");
573  // and set these to null so their destructors don't blow up
574  d_lastQuery = Theorem3();
575  d_lastQueryTCC = Theorem();
576  d_lastClosure = Theorem3();
577  // Delete ExprManager BEFORE TheoremManager, since Exprs use Theorems
578  TRACE_MSG("delete", "Clearing d_em {");
579  d_em->clear();
580  d_tm->clear();
581  TRACE_MSG("delete", "Finished clearing d_em }");
582 
583  for(size_t i=d_theories.size(); i!= 0; ) {
584  --i;
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, "] }");
589  }
590  d_theories.clear();
591 
592  // TheoremManager does not call ~Theorem() destructors, and only
593  // releases memory. At worst, we'll lose some Assumptions.
594  TRACE_MSG("delete", "Deleting d_tm {");
595  delete d_tm;
596  TRACE_MSG("delete", "Finished deleting d_tm }");
597 
598  TRACE_MSG("delete", "Deleting d_em {");
599  delete d_em;
600  TRACE_MSG("delete", "Finished deleting d_em }");
601 
602  TRACE_MSG("delete", "Deleting d_cm {");
603  delete d_cm;
604  TRACE_MSG("delete", "Finished deleting d_cm }");
605  delete d_statistics;
606  TRACE_MSG("delete", "Finished deleting d_statistics }");
607 }
608 
609 
610 VCL::~VCL()
611 {
612  destroy();
613  TRACE_MSG("delete", "Deleting d_flags [end of ~VCL()]");
614  delete d_flags;
615  // No more TRACE-ing after this point (it needs d_flags)
616  // Finalize the global debugger,
617  // otherwise applications with more than one instance of VCL
618  // may use refer to deallocated flags (e.g. test6 uses 2 VCLs)
619  IF_DEBUG( CVC3::debugger.finalize(); )
620 }
621 
622 
623 void VCL::reprocessFlags() {
624  if (d_se->getName() != (*d_flags)["sat"].getString()) {
625  delete d_se;
626  const string& satEngine = (*d_flags)["sat"].getString();
627  if (satEngine == "simple")
628  d_se = new SearchSimple(d_theoryCore);
629  else if (satEngine == "fast")
630  d_se = new SearchEngineFast(d_theoryCore);
631  else if (satEngine == "sat" || satEngine == "minisat")
632  d_se = new SearchSat(d_theoryCore, satEngine);
633  else
634  throw CLException("Unrecognized SAT solver name: "
635  +(*d_flags)["sat"].getString());
636  }
637 
638  int arithCur;
639  if (d_theoryArith->getName() == "ArithmeticOld") arithCur = 1;
640  else if (d_theoryArith->getName() == "ArithmeticNew") arithCur = 2;
641  else {
642  DebugAssert(d_theoryArith->getName() == "Arithmetic3", "unexpected name");
643  arithCur = 3;
644  }
645 
646  int arithNext;
647  if ((*d_flags)["arith-new"].getBool()) arithNext = 2;
648  else if ((*d_flags)["arith3"].getBool()) arithNext = 3;
649  else arithNext = 1;
650 
651  if (arithCur != arithNext) {
652  delete d_theoryArith;
653  switch (arithNext) {
654  case 1:
655  d_theoryArith = new TheoryArithOld(d_theoryCore);
656  break;
657  case 2:
658  d_theoryArith = new TheoryArithNew(d_theoryCore);
659  break;
660  case 3:
661  d_theoryArith = new TheoryArith3(d_theoryCore);
662  break;
663  }
664  d_theories[2] = d_theoryArith;
665  d_translator->setTheoryArith(d_theoryArith);
666  }
667 
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);
672  }
673 
674  if ((*d_flags)["translate"].getBool()) {
675  d_flags->setFlag("printResults", false);
676  }
677 
678  if ((*d_flags)["pp-bryant"].getBool()) {
679  d_flags->setFlag("pp-batch", true);
680  }
681 
682  //added by Yeting
683  if ((*d_flags)["quant-complete-inst"].getBool() && !(*d_flags)["translate"].getBool()) {
684  d_flags->setFlag("pp-batch", true);
685  }
686 
687  if ((*d_flags)["cnf-formula"].getBool()) {
688  d_flags->setFlag("de", "sat");
689  d_flags->setFlag("preprocess", false);
690  }
691 
692 
693  //TODO: handle more flags
694 }
695 
696 TheoryCore* VCL::core(){
697  return d_theoryCore;
698 }
699 
700 Type VCL::boolType(){
701  return d_theoryCore->boolType();
702 }
703 
704 
705 Type VCL::realType()
706 {
707  return d_theoryArith->realType();
708 }
709 
710 
711 Type VCL::intType() {
712  return d_theoryArith->intType();
713 }
714 
715 
716 Type VCL::subrangeType(const Expr& l, const Expr& r) {
717  return d_theoryArith->subrangeType(l, r);
718 }
719 
720 
721 Type VCL::subtypeType(const Expr& pred, const Expr& witness)
722 {
723  return d_theoryCore->newSubtypeExpr(pred, witness);
724 }
725 
726 
727 Type VCL::tupleType(const Type& type0, const Type& type1)
728 {
729  vector<Type> types;
730  types.push_back(type0);
731  types.push_back(type1);
732  return d_theoryRecords->tupleType(types);
733 }
734 
735 
736 Type VCL::tupleType(const Type& type0, const Type& type1, const Type& type2)
737 {
738  vector<Type> types;
739  types.push_back(type0);
740  types.push_back(type1);
741  types.push_back(type2);
742  return d_theoryRecords->tupleType(types);
743 }
744 
745 
746 Type VCL::tupleType(const vector<Type>& types)
747 {
748  return d_theoryRecords->tupleType(types);
749 }
750 
751 
752 Type VCL::recordType(const string& field, const Type& type)
753 {
754  vector<string> fields;
755  vector<Type> kids;
756  fields.push_back(field);
757  kids.push_back(type);
758  return Type(d_theoryRecords->recordType(fields, kids));
759 }
760 
761 
762 Type VCL::recordType(const string& field0, const Type& type0,
763  const string& field1, const Type& type1) {
764  vector<string> fields;
765  vector<Type> kids;
766  fields.push_back(field0);
767  fields.push_back(field1);
768  kids.push_back(type0);
769  kids.push_back(type1);
770  sort2(fields, kids);
771  return Type(d_theoryRecords->recordType(fields, kids));
772 }
773 
774 
775 Type VCL::recordType(const string& field0, const Type& type0,
776  const string& field1, const Type& type1,
777  const string& field2, const Type& type2)
778 {
779  vector<string> fields;
780  vector<Type> kids;
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);
787  sort2(fields, kids);
788  return Type(d_theoryRecords->recordType(fields, kids));
789 }
790 
791 
792 Type VCL::recordType(const vector<string>& fields,
793  const vector<Type>& types)
794 {
795  DebugAssert(fields.size() == types.size(),
796  "VCL::recordType: number of fields is different \n"
797  "from the number of types");
798  // Create copies of the vectors to sort them
799  vector<string> fs(fields);
800  vector<Type> ts(types);
801  sort2(fs, ts);
802  return Type(d_theoryRecords->recordType(fs, ts));
803 }
804 
805 
806 Type VCL::dataType(const string& name,
807  const string& constructor,
808  const vector<string>& selectors, const vector<Expr>& types)
809 {
810  vector<string> constructors;
811  constructors.push_back(constructor);
812 
813  vector<vector<string> > selectorsVec;
814  selectorsVec.push_back(selectors);
815 
816  vector<vector<Expr> > typesVec;
817  typesVec.push_back(types);
818 
819  return dataType(name, constructors, selectorsVec, typesVec);
820 }
821 
822 
823 Type VCL::dataType(const string& name,
824  const vector<string>& constructors,
825  const vector<vector<string> >& selectors,
826  const vector<vector<Expr> >& types)
827 {
828  Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
829  if(d_dump) {
830  d_translator->dump(res);
831  }
832  return Type(res[0]);
833 }
834 
835 
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)
841 {
842  Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
843  if(d_dump) {
844  d_translator->dump(res);
845  }
846  for (int i = 0; i < res.arity(); ++i) {
847  returnTypes.push_back(Type(res[i]));
848  }
849 }
850 
851 
852 Type VCL::arrayType(const Type& typeIndex, const Type& typeData)
853 {
854  return ::arrayType(typeIndex, typeData);
855 }
856 
857 
858 Type VCL::bitvecType(int n)
859 {
860  return d_theoryBitvector->newBitvectorType(n);
861 }
862 
863 
864 Type VCL::funType(const Type& typeDom, const Type& typeRan)
865 {
866  return typeDom.funType(typeRan);
867 }
868 
869 
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);
873 }
874 
875 
876 Type VCL::createType(const string& typeName)
877 {
878  if(d_dump) {
879  d_translator->dump(Expr(TYPE, listExpr(idExpr(typeName))));
880  }
881  return d_theoryCore->newTypeExpr(typeName);
882 }
883 
884 
885 Type VCL::createType(const string& typeName, const Type& def)
886 {
887  if (d_dump) {
888  d_translator->dump(Expr(TYPE, idExpr(typeName), def.getExpr()), true);
889  }
890  return d_theoryCore->newTypeExpr(typeName, def);
891 }
892 
893 
894 Type VCL::lookupType(const string& typeName)
895 {
896  return d_theoryCore->lookupTypeExpr(typeName);
897 }
898 
899 
900 Expr VCL::varExpr(const string& name, const Type& type)
901 {
902  // Check if the ofstream is open (as opposed to the command line flag)
903  if(d_dump) {
904  d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
905  }
906  return d_theoryCore->newVar(name, type);
907 }
908 
909 
910 Expr VCL::varExpr(const string& name, const Type& type, const Expr& def)
911 {
912  // Check if the ofstream is open (as opposed to the command line flag)
913  if(d_dump) {
914  d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
915  }
916  // Prove the TCCs of the definition
917  if(getFlags()["tcc"].getBool()) {
918  Type tpDef(def.getType()), tpVar(type);
919  // Make sure that def is in the subtype of tpVar; that is, prove
920  // FORALL (x: tpDef): x = def => typePred(tpVar)(x)
921  if(tpDef != tpVar) {
922  // Typecheck the base types
923  if(getBaseType(tpDef) != getBaseType(type)) {
924  throw TypecheckException("Type mismatch in constant definition:\n"
925  "Constant "+name+
926  " is declared with type:\n "
927  +type.toString()
928  +"\nBut the type of definition is\n "
929  +tpDef.toString());
930  }
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));
937  try {
938  checkTCC(quant);
939  } catch(TypecheckException&) {
940  throw TypecheckException
941  ("Type mismatch in constant definition:\n"
942  "Constant "+name+
943  " is declared with type:\n "
944  +type.toString()
945  +"\nBut the type of definition is\n "
946  +def.getType().toString()
947  +"\n\n which is not a subtype of the constant");
948  }
949  }
950  }
951  return d_theoryCore->newVar(name, type, def);
952 }
953 
954 
955 Expr VCL::lookupVar(const string& name, Type* type)
956 {
957  return d_theoryCore->lookupVar(name, type);
958 }
959 
960 
961 Type VCL::getType(const Expr& e)
962 {
963  return e.getType();
964 }
965 
966 
967 Type VCL::getBaseType(const Expr& e)
968 {
969  return d_theoryCore->getBaseType(e);
970 }
971 
972 
973 Type VCL::getBaseType(const Type& t)
974 {
975  return d_theoryCore->getBaseType(t);
976 }
977 
978 
979 Expr VCL::getTypePred(const Type&t, const Expr& e)
980 {
981  return d_theoryCore->getTypePred(t, e);
982 }
983 
984 
985 Expr VCL::stringExpr(const string& str) {
986  return getEM()->newStringExpr(str);
987 }
988 
989 
990 Expr VCL::idExpr(const string& name) {
991  return Expr(ID, stringExpr(name));
992 }
993 
994 
995 Expr VCL::listExpr(const vector<Expr>& kids) {
996  return Expr(RAW_LIST, kids, getEM());
997 }
998 
999 
1000 Expr VCL::listExpr(const Expr& e1) {
1001  return Expr(RAW_LIST, e1);
1002 }
1003 
1004 
1005 Expr VCL::listExpr(const Expr& e1, const Expr& e2) {
1006  return Expr(RAW_LIST, e1, e2);
1007 }
1008 
1009 
1010 Expr VCL::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
1011  return Expr(RAW_LIST, e1, e2, e3);
1012 }
1013 
1014 
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);
1020 }
1021 
1022 
1023 Expr VCL::listExpr(const string& op, const Expr& e1) {
1024  return Expr(RAW_LIST, idExpr(op), e1);
1025 }
1026 
1027 
1028 Expr VCL::listExpr(const string& op, const Expr& e1,
1029  const Expr& e2) {
1030  return Expr(RAW_LIST, idExpr(op), e1, e2);
1031 }
1032 
1033 
1034 Expr VCL::listExpr(const string& op, const Expr& e1,
1035  const Expr& e2, const Expr& e3) {
1036  vector<Expr> kids;
1037  kids.push_back(idExpr(op));
1038  kids.push_back(e1);
1039  kids.push_back(e2);
1040  kids.push_back(e3);
1041  return listExpr(kids);
1042 }
1043 
1044 
1045 void VCL::printExpr(const Expr& e) {
1046  printExpr(e, cout);
1047 }
1048 
1049 
1050 void VCL::printExpr(const Expr& e, ostream& os) {
1051  os << e << endl;
1052 }
1053 
1054 
1055 Expr VCL::parseExpr(const Expr& e) {
1056  return d_theoryCore->parseExprTop(e);
1057 }
1058 
1059 
1060 Type VCL::parseType(const Expr& e) {
1061  return Type(d_theoryCore->parseExpr(e));
1062 }
1063 
1064 
1065 Expr VCL::importExpr(const Expr& e)
1066 {
1067  return d_em->rebuild(e);
1068 }
1069 
1070 
1071 Type VCL::importType(const Type& t)
1072 {
1073  return Type(d_em->rebuild(t.getExpr()));
1074 }
1075 
1076 void VCL::cmdsFromString(const std::string& s, InputLanguage lang=PRESENTATION_LANG)
1077 {
1078  stringstream ss(s,stringstream::in);
1079  return loadFile(ss,lang,false);
1080 }
1081 
1082 Expr VCL::exprFromString(const std::string& s)
1083 {
1084  stringstream ss("PRINT " + s + ";",stringstream::in);
1085  Parser p(this,d_translator,PRESENTATION_LANG,ss);
1086  Expr e = p.next();
1087  if( e.isNull() ) {
1088  throw ParserException("Parser result is null: '" + s + "'");
1089  }
1090  DebugAssert(e.getKind() == RAW_LIST, "Expected list expression");
1091  DebugAssert(e.arity() == 2, "Expected two children");
1092  return parseExpr(e[1]);
1093 }
1094 
1095 Expr VCL::trueExpr()
1096 {
1097  return d_em->trueExpr();
1098 }
1099 
1100 
1101 Expr VCL::falseExpr()
1102 {
1103  return d_em->falseExpr();
1104 }
1105 
1106 
1107 Expr VCL::notExpr(const Expr& child)
1108 {
1109  return !child;
1110 }
1111 
1112 
1114 {
1115  return left && right;
1116 }
1117 
1118 
1119 Expr VCL::andExpr(const vector<Expr>& children)
1120 {
1121  if (children.size() == 0)
1122  throw Exception("andExpr requires at least one child");
1123  return Expr(AND, children);
1124 }
1125 
1126 
1128 {
1129  return left || right;
1130 }
1131 
1132 
1133 Expr VCL::orExpr(const vector<Expr>& children)
1134 {
1135  if (children.size() == 0)
1136  throw Exception("orExpr requires at least one child");
1137  return Expr(OR, children);
1138 }
1139 
1140 
1141 Expr VCL::impliesExpr(const Expr& hyp, const Expr& conc)
1142 {
1143  return hyp.impExpr(conc);
1144 }
1145 
1146 
1147 Expr VCL::iffExpr(const Expr& left, const Expr& right)
1148 {
1149  return left.iffExpr(right);
1150 }
1151 
1152 
1153 Expr VCL::eqExpr(const Expr& child0, const Expr& child1)
1154 {
1155  return child0.eqExpr(child1);
1156 }
1157 
1158 Expr VCL::distinctExpr(const std::vector<Expr>& children)
1159 {
1160  return Expr(DISTINCT, children);
1161 }
1162 
1163 Expr VCL::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart)
1164 {
1165  return ifpart.iteExpr(thenpart, elsepart);
1166 }
1167 
1168 
1169 Op VCL::createOp(const string& name, const Type& type)
1170 {
1171  if (!type.isFunction())
1172  throw Exception("createOp: expected function type");
1173  if(d_dump) {
1174  d_translator->dump(Expr(CONST, idExpr(name), type.getExpr()));
1175  }
1176  return d_theoryCore->newFunction(name, type,
1177  getFlags()["trans-closure"].getBool());
1178 }
1179 
1180 
1181 Op VCL::createOp(const string& name, const Type& type, const Expr& def)
1182 {
1183  if (!type.isFunction())
1184  throw TypecheckException
1185  ("Type error in createOp:\n"
1186  "Constant "+name+
1187  " is declared with type:\n "
1188  +type.toString()
1189  +"\n which is not a function type");
1190  if (getBaseType(type) != getBaseType(def.getType()))
1191  throw TypecheckException
1192  ("Type mismatch in createOp:\n"
1193  "Function "+name+
1194  " is declared with type:\n "
1195  +type.toString()
1196  +"\nBut the type of definition is\n "
1197  +def.getType().toString()
1198  +"\n\n which does not match");
1199  if(d_dump) {
1200  d_translator->dump(Expr(CONST, idExpr(name), type.getExpr(), def), true);
1201  }
1202  // Prove the TCCs of the definition
1203  if(getFlags()["tcc"].getBool()) {
1204  Type tpDef(def.getType());
1205  // Make sure that def is within the subtype; that is, prove
1206  // FORALL (xs: argType): typePred_{return_type}(def(xs))
1207  if(tpDef != type) {
1208  vector<Expr> boundVars;
1209  for (int i = 0; i < type.arity()-1; ++i) {
1210  boundVars.push_back(d_em->newBoundVarExpr(type[i]));
1211  }
1212  Expr app = Expr(def.mkOp(), boundVars);
1213  Expr body(getTypePred(type[type.arity()-1], app));
1214  Expr quant(forallExpr(boundVars, body));
1215  Expr tcc = quant.andExpr(d_theoryCore->getTCC(quant));
1216  // Query the subtyping formula
1217  bool typesMatch = true;
1218  try {
1219  checkTCC(tcc);
1220  } catch (TypecheckException&) {
1221  typesMatch = false;
1222  }
1223  if(!typesMatch) {
1224  throw TypecheckException
1225  ("Type mismatch in createOp:\n"
1226  "Function "+name+
1227  " is declared with type:\n "
1228  +type.toString()
1229  +"\nBut the definition is\n "
1230  +def.toString()
1231  +"\n\nwhose type could not be proved to be a subtype");
1232  }
1233  }
1234  }
1235  return d_theoryCore->newFunction(name, type, def);
1236 }
1237 
1238 
1239 Op VCL::lookupOp(const string& name, Type* type)
1240 {
1241  return d_theoryCore->lookupFunction(name, type);
1242 }
1243 
1244 
1245 Expr VCL::funExpr(const Op& op, const Expr& child)
1246 {
1247  return Expr(op, child);
1248 }
1249 
1250 
1251 Expr VCL::funExpr(const Op& op, const Expr& left, const Expr& right)
1252 {
1253  return Expr(op, left, right);
1254 }
1255 
1256 
1257 Expr VCL::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2)
1258 {
1259  return Expr(op, child0, child1, child2);
1260 }
1261 
1262 
1263 Expr VCL::funExpr(const Op& op, const vector<Expr>& children)
1264 {
1265  return Expr(op, children);
1266 }
1267 
1268 bool VCL::addPairToArithOrder(const Expr& smaller, const Expr& bigger)
1269 {
1270  if (d_dump) {
1271  d_translator->dump(Expr(ARITH_VAR_ORDER, smaller, bigger), true);
1272  }
1273  return d_theoryArith->addPairToArithOrder(smaller, bigger);
1274 }
1275 
1276 Expr VCL::ratExpr(int n, int d)
1277 {
1278  DebugAssert(d != 0,"denominator cannot be 0");
1279  return d_em->newRatExpr(Rational(n,d));
1280 }
1281 
1282 
1283 Expr VCL::ratExpr(const string& n, const string& d, int base)
1284 {
1285  return d_em->newRatExpr(Rational(n.c_str(), d.c_str(), base));
1286 }
1287 
1288 
1289 Expr VCL::ratExpr(const string& n, int base)
1290 {
1291  string::size_type pos = n.rfind(".");
1292  if (pos == string::npos) {
1293  return d_em->newRatExpr(Rational(n.c_str(), base));
1294  }
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);
1299  }
1300  pos = beforedec.rfind(".");
1301  if (pos != string::npos) {
1302  throw Exception("Cannot convert string to rational: "+n);
1303  }
1304  Rational r = Rational(beforedec.c_str(), base);
1305  Rational fracPart = Rational(afterdec.c_str(), base);
1306  if( r < 0 || ((r == 0) && (beforedec.rfind("-") != string::npos)) ) {
1307  r = r - (fracPart / pow(afterdec.size(), (Rational)base));
1308  }
1309  else {
1310  r = r + (fracPart / pow(afterdec.size(), (Rational)base));
1311  }
1312  return d_em->newRatExpr(r);
1313 }
1314 
1315 
1317 {
1318  return -child;
1319 }
1320 
1321 
1323 {
1324  return left + right;
1325 }
1326 
1327 Expr VCL::plusExpr(const std::vector<Expr>& children)
1328 {
1329  return Expr(PLUS, children);
1330 }
1331 
1332 
1334 {
1335  return left - right;
1336 }
1337 
1338 
1340 {
1341  return left * right;
1342 }
1343 
1344 
1345 Expr VCL::powExpr(const Expr& x, const Expr& n)
1346 {
1347  return ::powExpr(n, x);
1348 }
1349 
1350 
1351 Expr VCL::divideExpr(const Expr& num, const Expr& denom)
1352 {
1353  return ::divideExpr(num,denom);
1354 }
1355 
1356 
1358 {
1359  return ::ltExpr(left, right);
1360 }
1361 
1362 
1364 {
1365  return ::leExpr(left, right);
1366 }
1367 
1368 
1370 {
1371  return ::gtExpr(left, right);
1372 }
1373 
1374 
1376 {
1377  return ::geExpr(left, right);
1378 }
1379 
1380 
1381 Expr VCL::recordExpr(const string& field, const Expr& expr)
1382 {
1383  vector<string> fields;
1384  vector<Expr> kids;
1385  kids.push_back(expr);
1386  fields.push_back(field);
1387  return d_theoryRecords->recordExpr(fields, kids);
1388 }
1389 
1390 
1391 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
1392  const string& field1, const Expr& expr1)
1393 {
1394  vector<string> fields;
1395  vector<Expr> kids;
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);
1402 }
1403 
1404 
1405 Expr VCL::recordExpr(const string& field0, const Expr& expr0,
1406  const string& field1, const Expr& expr1,
1407  const string& field2, const Expr& expr2)
1408 {
1409  vector<string> fields;
1410  vector<Expr> kids;
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);
1419 }
1420 
1421 
1422 Expr VCL::recordExpr(const vector<string>& fields,
1423  const vector<Expr>& exprs)
1424 {
1425  DebugAssert(fields.size() > 0, "VCL::recordExpr()");
1426  DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
1427  // Create copies of the vectors to sort them
1428  vector<string> fs(fields);
1429  vector<Expr> es(exprs);
1430  sort2(fs, es);
1431  return d_theoryRecords->recordExpr(fs, es);
1432 }
1433 
1434 
1435 Expr VCL::recSelectExpr(const Expr& record, const string& field)
1436 {
1437  return d_theoryRecords->recordSelect(record, field);
1438 }
1439 
1440 
1441 Expr VCL::recUpdateExpr(const Expr& record, const string& field,
1442  const Expr& newValue)
1443 {
1444  return d_theoryRecords->recordUpdate(record, field, newValue);
1445 }
1446 
1447 
1448 Expr VCL::readExpr(const Expr& array, const Expr& index)
1449 {
1450  return Expr(READ, array, index);
1451 }
1452 
1453 
1454 Expr VCL::writeExpr(const Expr& array, const Expr& index, const Expr& newValue)
1455 {
1456  return Expr(WRITE, array, index, newValue);
1457 }
1458 
1459 
1460 Expr VCL::newBVConstExpr(const std::string& s, int base)
1461 {
1462  return d_theoryBitvector->newBVConstExpr(s, base);
1463 }
1464 
1465 
1466 Expr VCL::newBVConstExpr(const std::vector<bool>& bits)
1467 {
1468  return d_theoryBitvector->newBVConstExpr(bits);
1469 }
1470 
1471 
1472 Expr VCL::newBVConstExpr(const Rational& r, int len)
1473 {
1474  return d_theoryBitvector->newBVConstExpr(r, len);
1475 }
1476 
1477 
1478 Expr VCL::newConcatExpr(const Expr& t1, const Expr& t2)
1479 {
1480  return d_theoryBitvector->newConcatExpr(t1, t2);
1481 }
1482 
1483 
1484 Expr VCL::newConcatExpr(const std::vector<Expr>& kids)
1485 {
1486  return d_theoryBitvector->newConcatExpr(kids);
1487 }
1488 
1489 
1490 Expr VCL::newBVExtractExpr(const Expr& e, int hi, int low)
1491 {
1492  return d_theoryBitvector->newBVExtractExpr(e, hi, low);
1493 }
1494 
1495 
1496 Expr VCL::newBVNegExpr(const Expr& t1)
1497 {
1498  return d_theoryBitvector->newBVNegExpr(t1);
1499 }
1500 
1501 
1502 Expr VCL::newBVAndExpr(const Expr& t1, const Expr& t2)
1503 {
1504  return d_theoryBitvector->newBVAndExpr(t1, t2);
1505 }
1506 
1507 
1508 Expr VCL::newBVAndExpr(const std::vector<Expr>& kids)
1509 {
1510  return d_theoryBitvector->newBVAndExpr(kids);
1511 }
1512 
1513 
1514 Expr VCL::newBVOrExpr(const Expr& t1, const Expr& t2)
1515 {
1516  return d_theoryBitvector->newBVOrExpr(t1, t2);
1517 }
1518 
1519 
1520 Expr VCL::newBVOrExpr(const std::vector<Expr>& kids)
1521 {
1522  return d_theoryBitvector->newBVOrExpr(kids);
1523 }
1524 
1525 
1526 Expr VCL::newBVXorExpr(const Expr& t1, const Expr& t2)
1527 {
1528  return d_theoryBitvector->newBVXorExpr(t1, t2);
1529 }
1530 
1531 
1532 Expr VCL::newBVXorExpr(const std::vector<Expr>& kids)
1533 {
1534  return d_theoryBitvector->newBVXorExpr(kids);
1535 }
1536 
1537 
1538 Expr VCL::newBVXnorExpr(const Expr& t1, const Expr& t2)
1539 {
1540  return d_theoryBitvector->newBVXnorExpr(t1, t2);
1541 }
1542 
1543 
1544 Expr VCL::newBVXnorExpr(const std::vector<Expr>& kids)
1545 {
1546  return d_theoryBitvector->newBVXnorExpr(kids);
1547 }
1548 
1549 
1550 Expr VCL::newBVNandExpr(const Expr& t1, const Expr& t2)
1551 {
1552  return d_theoryBitvector->newBVNandExpr(t1, t2);
1553 }
1554 
1555 
1556 Expr VCL::newBVNorExpr(const Expr& t1, const Expr& t2)
1557 {
1558  return d_theoryBitvector->newBVNorExpr(t1, t2);
1559 }
1560 
1561 
1562 Expr VCL::newBVCompExpr(const Expr& t1, const Expr& t2)
1563 {
1564  return d_theoryBitvector->newBVCompExpr(t1, t2);
1565 }
1566 
1567 
1568 Expr VCL::newBVLTExpr(const Expr& t1, const Expr& t2)
1569 {
1570  return d_theoryBitvector->newBVLTExpr(t1, t2);
1571 }
1572 
1573 
1574 Expr VCL::newBVLEExpr(const Expr& t1, const Expr& t2)
1575 {
1576  return d_theoryBitvector->newBVLEExpr(t1, t2);
1577 }
1578 
1579 
1580 Expr VCL::newBVSLTExpr(const Expr& t1, const Expr& t2)
1581 {
1582  return d_theoryBitvector->newBVSLTExpr(t1, t2);
1583 }
1584 
1585 
1586 Expr VCL::newBVSLEExpr(const Expr& t1, const Expr& t2)
1587 {
1588  return d_theoryBitvector->newBVSLEExpr(t1, t2);
1589 }
1590 
1591 
1592 Expr VCL::newSXExpr(const Expr& t1, int len)
1593 {
1594  return d_theoryBitvector->newSXExpr(t1, len);
1595 }
1596 
1597 
1598 Expr VCL::newBVUminusExpr(const Expr& t1)
1599 {
1600  return d_theoryBitvector->newBVUminusExpr(t1);
1601 }
1602 
1603 
1604 Expr VCL::newBVSubExpr(const Expr& t1, const Expr& t2)
1605 {
1606  return d_theoryBitvector->newBVSubExpr(t1, t2);
1607 }
1608 
1609 
1610 Expr VCL::newBVPlusExpr(int numbits, const std::vector<Expr>& k)
1611 {
1612  return d_theoryBitvector->newBVPlusPadExpr(numbits, k);
1613 }
1614 
1615 Expr VCL::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2)
1616 {
1617  std::vector<Expr> k;
1618  k.push_back(t1);
1619  k.push_back(t2);
1620  return newBVPlusExpr(numbits, k);
1621 }
1622 
1623 
1624 Expr VCL::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2)
1625 {
1626  return d_theoryBitvector->newBVMultPadExpr(numbits, t1, t2);
1627 }
1628 
1629 Expr VCL::newBVUDivExpr(const Expr& t1, const Expr& t2)
1630 {
1631  return d_theoryBitvector->newBVUDivExpr(t1, t2);
1632 }
1633 
1634 Expr VCL::newBVURemExpr(const Expr& t1, const Expr& t2)
1635 {
1636  return d_theoryBitvector->newBVURemExpr(t1, t2);
1637 }
1638 
1639 Expr VCL::newBVSDivExpr(const Expr& t1, const Expr& t2)
1640 {
1641  return d_theoryBitvector->newBVSDivExpr(t1, t2);
1642 }
1643 
1644 Expr VCL::newBVSRemExpr(const Expr& t1, const Expr& t2)
1645 {
1646  return d_theoryBitvector->newBVSRemExpr(t1, t2);
1647 }
1648 
1649 Expr VCL::newBVSModExpr(const Expr& t1, const Expr& t2)
1650 {
1651  return d_theoryBitvector->newBVSModExpr(t1, t2);
1652 }
1653 
1654 
1655 Expr VCL::newFixedLeftShiftExpr(const Expr& t1, int r)
1656 {
1657  return d_theoryBitvector->newFixedLeftShiftExpr(t1, r);
1658 }
1659 
1660 
1661 Expr VCL::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r)
1662 {
1663  return d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t1, r);
1664 }
1665 
1666 
1667 Expr VCL::newFixedRightShiftExpr(const Expr& t1, int r)
1668 {
1669  return d_theoryBitvector->newFixedRightShiftExpr(t1, r);
1670 }
1671 
1672 
1673 Expr VCL::newBVSHL(const Expr& t1, const Expr& t2)
1674 {
1675  return Expr(BVSHL, t1, t2);
1676 }
1677 
1678 
1679 Expr VCL::newBVLSHR(const Expr& t1, const Expr& t2)
1680 {
1681  return Expr(BVLSHR, t1, t2);
1682 }
1683 
1684 
1685 Expr VCL::newBVASHR(const Expr& t1, const Expr& t2)
1686 {
1687  return Expr(BVASHR, t1, t2);
1688 }
1689 
1690 
1691 Rational VCL::computeBVConst(const Expr& e)
1692 {
1693  return d_theoryBitvector->computeBVConst(e);
1694 }
1695 
1696 
1697 Expr VCL::tupleExpr(const vector<Expr>& exprs) {
1698  DebugAssert(exprs.size() > 0, "VCL::tupleExpr()");
1699  return d_theoryRecords->tupleExpr(exprs);
1700 }
1701 
1702 
1703 Expr VCL::tupleSelectExpr(const Expr& tuple, int index)
1704 {
1705  return d_theoryRecords->tupleSelect(tuple, index);
1706 }
1707 
1708 
1709 Expr VCL::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue)
1710 {
1711  return d_theoryRecords->tupleUpdate(tuple, index, newValue);
1712 }
1713 
1714 
1715 Expr VCL::datatypeConsExpr(const string& constructor, const vector<Expr>& args)
1716 {
1717  return d_theoryDatatype->datatypeConsExpr(constructor, args);
1718 }
1719 
1720 
1721 Expr VCL::datatypeSelExpr(const string& selector, const Expr& arg)
1722 {
1723  return d_theoryDatatype->datatypeSelExpr(selector, arg);
1724 }
1725 
1726 
1727 Expr VCL::datatypeTestExpr(const string& constructor, const Expr& arg)
1728 {
1729  return d_theoryDatatype->datatypeTestExpr(constructor, arg);
1730 }
1731 
1732 
1733 Expr VCL::boundVarExpr(const string& name, const string& uid,
1734  const Type& type) {
1735  return d_em->newBoundVarExpr(name, uid, type);
1736 }
1737 
1738 
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);
1742 }
1743 
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);
1748 }
1749 
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);
1754 }
1755 
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);
1760 }
1761 
1762 void VCL::setTriggers(const Expr& e, const vector< vector<Expr> >& triggers) {
1763  e.setTriggers(triggers);
1764 }
1765 
1766 void VCL::setTriggers(const Expr& e, const vector<Expr>& triggers) {
1767  e.setTriggers(triggers);
1768 }
1769 
1770 void VCL::setTrigger(const Expr& e, const Expr& trigger) {
1771  e.setTrigger(trigger);
1772 }
1773 
1774 void VCL::setMultiTrigger(const Expr& e, const vector<Expr>& multiTrigger) {
1775  e.setMultiTrigger(multiTrigger);
1776 }
1777 
1778 Expr VCL::existsExpr(const vector<Expr>& vars, const Expr& body) {
1779  return d_em->newClosureExpr(EXISTS, vars, body);
1780 }
1781 
1782 
1783 Op VCL::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
1784  return d_em->newClosureExpr(LAMBDA, vars, body).mkOp();
1785 }
1786 
1787 Op VCL::transClosure(const Op& op) {
1788  const string& name = op.getExpr().getName();
1789  return d_em->newSymbolExpr(name, TRANS_CLOSURE).mkOp();
1790 }
1791 
1792 
1793 Expr VCL::simulateExpr(const Expr& f, const Expr& s0,
1794  const vector<Expr>& inputs, const Expr& n) {
1795  vector<Expr> kids;
1796  kids.push_back(f);
1797  kids.push_back(s0);
1798  kids.insert(kids.end(), inputs.begin(), inputs.end());
1799  kids.push_back(n);
1800  return Expr(SIMULATE, kids);
1801 }
1802 
1803 
1804 void VCL::setResourceLimit(unsigned limit)
1805 {
1806  d_theoryCore->setResourceLimit(limit);
1807 }
1808 
1809 
1810 Theorem VCL::checkTCC(const Expr& tcc)
1811 {
1812  Theorem tccThm;
1813  d_se->push();
1814  QueryResult res = d_se->checkValid(tcc, tccThm);
1815  switch (res) {
1816  case VALID:
1817  d_lastQueryTCC = tccThm;
1818  d_se->pop();
1819  break;
1820  case INVALID:
1821  throw TypecheckException("Failed TCC:\n\n "
1822  +tcc.toString()
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.");
1827  case ABORT:
1828  throw TypecheckException("Budget exceeded:\n\n "
1829  "Unable to verify TCC:\n\n "
1830  +tcc.toString()
1831  +"\n\nWhich simplified to:\n\n "
1832  +simplify(tcc).toString());
1833  case UNKNOWN:
1834  throw TypecheckException("Result unknown:\n\n "
1835  "Unable to verify TCC:\n\n "
1836  +tcc.toString()
1837  +"\n\nWhich simplified to:\n\n "
1838  +simplify(tcc).toString()
1839  +"\n\nAnd the last formula is unknown "
1840  "in the current context.");
1841  default:
1842  FatalAssert(false, "Unexpected case");
1843  }
1844  return tccThm;
1845 }
1846 
1847 
1848 void VCL::assertFormula(const Expr& e)
1849 {
1850  if (getFlags()["no-save-model"].getBool() && d_modelStackPushed) {
1851  d_modelStackPushed = false;
1852  pop();
1853  }
1854 
1855  // Typecheck the user input
1856  if(!e.getType().isBool()) {
1857  throw TypecheckException("Non-BOOLEAN formula in ASSERT:\n "
1858  +Expr(ASSERT, e).toString()
1859  +"\nDerived type of the formula:\n "
1860  +e.getType().toString());
1861  }
1862 
1863  if (getFlags()["pp-batch"].getBool()) {
1864  d_batchedAssertions->push_back(e);
1865  }
1866  else {
1867  // Check if the ofstream is open (as opposed to the command line flag)
1868  if(d_dump) {
1869  Expr e2 = e;
1870  if (getFlags()["preSimplify"].getBool()) {
1871  e2 = d_theoryCore->getExprTrans()->preprocess(e).getRHS();
1872  }
1873  if (d_translator->dumpAssertion(e2)) return;
1874  }
1875 
1876  TRACE("vclassertFormula", "VCL::assertFormula(", e, ") {");
1877 
1878  // See if e was already asserted before
1879  if(d_userAssertions->count(e) > 0) {
1880  TRACE_MSG("vclassertFormula", "VCL::assertFormula[repeated assertion] => }");
1881  return;
1882  }
1883  // Check the validity of the TCC
1884  Theorem tccThm;
1885  if(getFlags()["tcc"].getBool()) {
1886  Expr tcc(d_theoryCore->getTCC(e));
1887  tccThm = checkTCC(tcc);
1888  }
1889 
1890  Theorem thm = d_se->newUserAssumption(e);
1891  (*d_userAssertions)[e] = UserAssertion(thm, tccThm, d_nextIdx++);
1892  }
1893  TRACE_MSG("vclassertFormula", "VCL::assertFormula => }");
1894 }
1895 
1896 
1897 void VCL::registerAtom(const Expr& e)
1898 {
1899  //TODO: add to interactive interface
1900  d_se->registerAtom(e);
1901 }
1902 
1903 
1904 Expr VCL::getImpliedLiteral()
1905 {
1906  //TODO: add to interactive interface
1907  Theorem thm = d_se->getImpliedLiteral();
1908  if (thm.isNull()) return Expr();
1909  return thm.getExpr();
1910 }
1911 
1912 
1913 Expr VCL::simplify(const Expr& e) {
1914  //TODO: add to interactive interface
1915  return simplifyThm(e).getRHS();
1916 }
1917 
1918 
1919 Theorem VCL::simplifyThm(const Expr& e)
1920 {
1921  e.getType();
1922  Theorem res = d_theoryCore->getExprTrans()->preprocess(e);
1923  Theorem simpThm = d_theoryCore->simplify(res.getRHS());
1924  res = d_theoryCore->transitivityRule(res, simpThm);
1925  return res;
1926 }
1927 
1928 
1929 QueryResult VCL::query(const Expr& e)
1930 {
1931  TRACE("query", "VCL::query(", e,") {");
1932 
1933  if (getFlags()["no-save-model"].getBool()) {
1934  if(d_modelStackPushed) {
1935  d_modelStackPushed = false;
1936  pop();
1937  }
1938  push();
1939  d_modelStackPushed = true;
1940  }
1941 
1942  // Typecheck the user input
1943  if(!e.getType().isBool()) {
1944  throw TypecheckException("Non-BOOLEAN formula in QUERY:\n "
1945  +Expr(QUERY, e).toString()
1946  +"\nDerived type of the formula:\n "
1947  +e.getType().toString());
1948  }
1949 
1950  Expr qExpr = e;
1951  if (getFlags()["pp-batch"].getBool()) {
1952  // Add batched assertions
1953  vector<Expr> kids;
1954  for (; (*d_batchedAssertionsIdx) < d_batchedAssertions->size();
1955  (*d_batchedAssertionsIdx) = (*d_batchedAssertionsIdx) + 1) {
1956  kids.push_back((*d_batchedAssertions)[(*d_batchedAssertionsIdx)]);
1957  }
1958  if (kids.size() > 0) {
1959  qExpr = kids.size() == 1 ? kids[0] : Expr(AND, kids);
1960  qExpr = qExpr.impExpr(e);
1961  }
1962  }
1963 
1964  if (d_dump && !getFlags()["dump-tcc"].getBool()) {
1965  Expr e2 = qExpr;
1966  if (getFlags()["preSimplify"].getBool()) {
1967  e2 = d_theoryCore->getExprTrans()->preprocess(qExpr).getRHS();
1968  }
1969  if (d_translator->dumpQuery(e2)) return UNKNOWN;
1970  }
1971 
1972  // Check the validity of the TCC
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()) {
1977  Expr e2 = tcc;
1978  if (getFlags()["preSimplify"].getBool()) {
1979  e2 = d_theoryCore->getExprTrans()->preprocess(tcc).getRHS();
1980  }
1981  if (d_translator->dumpQuery(e2)) return UNKNOWN;
1982  }
1983  // FIXME: we have to guarantee that the TCC of 'tcc' is always valid
1984  tccThm = checkTCC(tcc);
1985  }
1986  Theorem res;
1987  QueryResult qres = d_se->checkValid(qExpr, res);
1988  switch (qres) {
1989  case VALID:
1990  d_lastQuery = d_se->getCommonRules()->queryTCC(res, tccThm);
1991  break;
1992  default:
1993  d_lastQueryTCC = Theorem();
1994  d_lastQuery = Theorem3();
1995  d_lastClosure = Theorem3();
1996  }
1997  TRACE("query", "VCL::query => ",
1998  qres == VALID ? "VALID" :
1999  qres == INVALID ? "INVALID" :
2000  qres == ABORT ? "ABORT" : "UNKNOWN", " }");
2001 
2002  if (d_dump) d_translator->dumpQueryResult(qres);
2003 
2004  return qres;
2005 }
2006 
2007 
2008 QueryResult VCL::checkUnsat(const Expr& e)
2009 {
2010  return query(e.negate());
2011 }
2012 
2013 
2014 QueryResult VCL::checkContinue()
2015 {
2016  if(d_dump) {
2017  d_translator->dump(d_em->newLeafExpr(CONTINUE), true);
2018  }
2019  vector<Expr> assertions;
2020  d_se->getCounterExample(assertions);
2021  Theorem thm;
2022  if (assertions.size() == 0) {
2023  return d_se->restart(falseExpr(), thm);
2024  }
2025  Expr eAnd = assertions.size() == 1 ? assertions[0] : andExpr(assertions);
2026  return d_se->restart(!eAnd, thm);
2027 }
2028 
2029 
2030 QueryResult VCL::restart(const Expr& e)
2031 {
2032  if (d_dump) {
2033  d_translator->dump(Expr(RESTART, e), true);
2034  }
2035  Theorem thm;
2036  return d_se->restart(e, thm);
2037 }
2038 
2039 
2040 void VCL::returnFromCheck()
2041 {
2042  //TODO: add to interactive interface
2043  d_se->returnFromCheck();
2044 }
2045 
2046 
2047 void VCL::getUserAssumptions(vector<Expr>& assumptions)
2048 {
2049  // TODO: add to interactive interface
2050  d_se->getUserAssumptions(assumptions);
2051 }
2052 
2053 
2054 void VCL::getInternalAssumptions(vector<Expr>& assumptions)
2055 {
2056  // TODO: add to interactive interface
2057  d_se->getInternalAssumptions(assumptions);
2058 }
2059 
2060 
2061 void VCL::getAssumptions(vector<Expr>& assumptions)
2062 {
2063  if(d_dump) {
2064  d_translator->dump(d_em->newLeafExpr(ASSUMPTIONS), true);
2065  }
2066  d_se->getAssumptions(assumptions);
2067 }
2068 
2069 
2070 //yeting, for proof translation
2071 Expr VCL::getProofQuery()
2072 {
2073  if (d_lastQuery.isNull()){
2074  throw EvalException
2075  ("Invalid Query,n");
2076  }
2077  return d_lastQuery.getExpr();
2078 
2079  // Theorem thm = d_se->lastThm();
2080  // if (thm.isNull()) return;
2081  // thm.getLeafAssumptions(assumptions);
2082 }
2083 
2084 
2085 void VCL::getAssumptionsUsed(vector<Expr>& assumptions)
2086 {
2087  throw EvalException ("getAssumptionsUsed not currently supported");
2088  if(d_dump) {
2089  d_translator->dump(d_em->newLeafExpr(DUMP_ASSUMPTIONS), true);
2090  }
2091  Theorem thm = d_se->lastThm();
2092  if (thm.isNull()) return;
2093  thm.getLeafAssumptions(assumptions);
2094 }
2095 
2096 
2097 void VCL::getCounterExample(vector<Expr>& assertions, bool inOrder)
2098 {
2099  if(d_dump) {
2100  d_translator->dump(d_em->newLeafExpr(COUNTEREXAMPLE), true);
2101  }
2102  if (!(*d_flags)["translate"].getBool())
2103  d_se->getCounterExample(assertions, inOrder);
2104 }
2105 
2106 
2107 void VCL::getConcreteModel(ExprMap<Expr> & m)
2108 {
2109  if(d_dump) {
2110  d_translator->dump(d_em->newLeafExpr(COUNTERMODEL), true);
2111  }
2112  if (!(*d_flags)["translate"].getBool())
2113  d_se->getConcreteModel(m);
2114 }
2115 
2116 QueryResult VCL::tryModelGeneration() {
2117  if (!d_theoryCore->incomplete()) throw Exception("Model generation should be called only after an UNKNOWN result");
2118  QueryResult qres = UNKNOWN;
2119  int scopeLevel = d_cm->scopeLevel();
2120  try {
2121  while (qres == UNKNOWN)
2122  {
2123  Theorem thm;
2124  d_se->push();
2125  // Try to generate the model
2126  if (d_se->tryModelGeneration(thm))
2127  // If success, we are satisfiable
2128  qres = INVALID;
2129  else
2130  {
2131  // Generate the clause to get rid of the faults
2132  vector<Expr> assumptions;
2133  thm.getLeafAssumptions(assumptions, true /*negate*/);
2134  if (!thm.getExpr().isFalse()) assumptions.push_back(thm.getExpr());
2135  // Pop back to where we were
2136  while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
2137  // Restart with the new clause
2138  qres = restart(orExpr(assumptions));
2139  // Keep this level
2140  scopeLevel = d_cm->scopeLevel();
2141  }
2142  }
2143  } catch (Exception& e) {
2144  // Pop back to where we were
2145  while (d_cm->scopeLevel() > scopeLevel) d_se->pop();
2146  }
2147  return qres;
2148 }
2149 
2150 FormulaValue VCL::value(const Expr& e) {
2151  DebugAssert(!e.isTerm(), "vcl::value: e is not a formula");
2152  return d_se->getValue(e);
2153 }
2154 
2155 bool VCL::inconsistent(vector<Expr>& assumptions)
2156 {
2157  // TODO: add to interactive interface
2158  if (d_theoryCore->inconsistent()) {
2159  // TODO: do we need local getAssumptions?
2160  getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
2161  assumptions);
2162  return true;
2163  }
2164  return false;
2165 }
2166 
2167 bool VCL::inconsistent()
2168 {
2169  return d_theoryCore->inconsistent();
2170 }
2171 
2172 
2173 bool VCL::incomplete() {
2174  // TODO: add to interactive interface
2175  // Return true only after a failed query
2176  return (d_lastQuery.isNull() && d_theoryCore->incomplete());
2177 }
2178 
2179 
2180 bool VCL::incomplete(vector<string>& reasons) {
2181  // TODO: add to interactive interface
2182  // Return true only after a failed query
2183  return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
2184 }
2185 
2186 
2187 Proof VCL::getProof()
2188 {
2189  if(d_dump) {
2190  d_translator->dump(d_em->newLeafExpr(DUMP_PROOF), true);
2191  }
2192 
2193  if(d_lastQuery.isNull())
2194  throw EvalException
2195  ("Method getProof() (or command DUMP_PROOF)\n"
2196  " must be called only after a Valid QUERY");
2197  return d_se->getProof();
2198 }
2199 
2200 Expr VCL::getAssignment() {
2201  if(d_dump) {
2202  d_translator->dump(d_em->newLeafExpr(GET_ASSIGNMENT), true);
2203  }
2204  return d_theoryCore->getAssignment();
2205 }
2206 
2207 Expr VCL::getValue(Expr e) {
2208  if(d_dump) {
2209  d_translator->dump(Expr(GET_VALUE, e), true);
2210  }
2211  return simplify(e);
2212 }
2213 
2214 Expr VCL::getTCC(){
2215  static Expr null;
2216  if(d_dump) {
2217  d_translator->dump(d_em->newLeafExpr(DUMP_TCC), true);
2218  }
2219  if(d_lastQueryTCC.isNull()) return null;
2220  else return d_lastQueryTCC.getExpr();
2221 }
2222 
2223 
2224 void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
2225 {
2226  if(d_dump) {
2227  d_translator->dump(d_em->newLeafExpr(DUMP_TCC_ASSUMPTIONS), true);
2228  }
2229  if(d_lastQuery.isNull())
2230  throw EvalException
2231  ("Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
2232  " must be called only after a Valid QUERY");
2233  getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
2234 }
2235 
2236 
2237 Proof VCL::getProofTCC() {
2238  static Proof null;
2239  if(d_dump) {
2240  d_translator->dump(d_em->newLeafExpr(DUMP_TCC_PROOF), true);
2241  }
2242  if(d_lastQueryTCC.isNull()) return null;
2243  else return d_lastQueryTCC.getProof();
2244 }
2245 
2246 
2247 Expr VCL::getClosure() {
2248  static Expr null;
2249  if(d_dump) {
2250  d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE), true);
2251  }
2252  if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
2253  // Construct the proof of closure and cache it in d_lastClosure
2254  d_lastClosure = deriveClosure(d_lastQuery);
2255  }
2256  if(d_lastClosure.isNull()) return null;
2257  else return d_lastClosure.getExpr();
2258 }
2259 
2260 
2261 Proof VCL::getProofClosure() {
2262  static Proof null;
2263  if(d_dump) {
2264  d_translator->dump(d_em->newLeafExpr(DUMP_CLOSURE_PROOF), true);
2265  }
2266  if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
2267  // Construct the proof of closure and cache it in d_lastClosure
2268  d_lastClosure = deriveClosure(d_lastQuery);
2269  }
2270  if(d_lastClosure.isNull()) return null;
2271  else return d_lastClosure.getProof();
2272 }
2273 
2274 
2275 int VCL::stackLevel()
2276 {
2277  return d_stackLevel->get();
2278 }
2279 
2280 
2282 {
2283  if (getFlags()["no-save-model"].getBool() && d_modelStackPushed) {
2284  d_modelStackPushed = false;
2285  pop();
2286  } else if (d_dump) {
2287  d_translator->dump(d_em->newLeafExpr(PUSH), true);
2288  }
2289  d_se->push();
2290  d_stackLevel->set(stackLevel()+1);
2291 }
2292 
2293 
2294 void VCL::pop()
2295 {
2296  if (getFlags()["no-save-model"].getBool() && d_modelStackPushed) {
2297  d_modelStackPushed = false;
2298  pop();
2299  } else if (d_dump) {
2300  d_translator->dump(d_em->newLeafExpr(POP), true);
2301  }
2302  if (stackLevel() == 0) {
2303  throw EvalException
2304  ("POP called with no previous call to PUSH");
2305  }
2306  int level = stackLevel();
2307  while (level == stackLevel())
2308  d_se->pop();
2309 }
2310 
2311 
2312 void VCL::popto(int toLevel)
2313 {
2314  // Check if the ofstream is open (as opposed to the command line flag)
2315  if(d_dump) {
2316  d_translator->dump(Expr(POPTO, ratExpr(toLevel, 1)), true);
2317  }
2318  if (toLevel < 0) toLevel = 0;
2319  while (stackLevel() > toLevel) {
2320  d_se->pop();
2321  }
2322 }
2323 
2324 
2325 int VCL::scopeLevel()
2326 {
2327  return d_cm->scopeLevel();
2328 }
2329 
2330 
2331 void VCL::pushScope()
2332 {
2333  throw EvalException ("Scope-level push/pop is no longer supported");
2334  d_cm->push();
2335  if(d_dump) {
2336  d_translator->dump(d_em->newLeafExpr(PUSH_SCOPE), true);
2337  }
2338  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
2339  dumpTrace(scopeLevel());)
2340 }
2341 
2342 
2343 void VCL::popScope()
2344 {
2345  throw EvalException ("Scope-level push/pop is no longer supported");
2346  if(d_dump) {
2347  d_translator->dump(d_em->newLeafExpr(POP_SCOPE), true);
2348  }
2349  if (scopeLevel() == 1) {
2350  cout << "Cannot POP from scope level 1" << endl;
2351  }
2352  else d_cm->pop();
2353  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
2354  dumpTrace(scopeLevel());)
2355 }
2356 
2357 
2358 void VCL::poptoScope(int toLevel)
2359 {
2360  throw EvalException ("Scope-level push/pop is no longer supported");
2361  if(d_dump) {
2362  d_translator->dump(Expr(POPTO_SCOPE, ratExpr(toLevel, 1)), true);
2363  }
2364  if (toLevel < 1) {
2365  d_cm->popto(0);
2366  d_cm->push();
2367  }
2368  else d_cm->popto(toLevel);
2369  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
2370  dumpTrace(scopeLevel());)
2371 }
2372 
2373 
2374 Context* VCL::getCurrentContext()
2375 {
2376  return d_cm->getCurrentContext();
2377 }
2378 
2379 
2381 {
2382  destroy();
2383  init();
2384 }
2385 
2386 void VCL::logAnnotation(const Expr& annot)
2387 {
2388  if (d_dump) {
2389  d_translator->dump(annot);
2390  }
2391 }
2392 
2393 void VCL::loadFile(const string& fileName, InputLanguage lang,
2394  bool interactive, bool calledFromParser) {
2395  // TODO: move these?
2396  Parser parser(this, d_translator, lang, interactive, fileName);
2397  VCCmd cmd(this, &parser, calledFromParser);
2398  cmd.processCommands();
2399 }
2400 
2401 
2402 void VCL::loadFile(istream& is, InputLanguage lang,
2403  bool interactive) {
2404  // TODO: move these?
2405  Parser parser(this, d_translator, lang, is, interactive);
2406  VCCmd cmd(this, &parser);
2407  cmd.processCommands();
2408 }
2409 
2410 
2411 // Verbosity: <= 0 = print nothing, only calculate
2412 // 1 = only print current level
2413 // n = print n recursive levels
2414 
2415 unsigned long VCL::getMemory(int verbosity)
2416 {
2417  unsigned long memSelf = sizeof(VCL);
2418  unsigned long mem = 0;
2419 
2420  mem += d_cm->getMemory(verbosity - 1);
2421  mem += d_em->getMemory(verbosity - 1);
2422 // mem += d_tm->getMemory(verbosity - 1);
2423 // mem += d_se->getMemory(verbosity - 1);
2424 
2425 // mem += d_theoryCore->getMemory(verbosity - 1);
2426 // mem += d_theoryUF->getMemory(verbosity - 1);
2427 // mem += d_theoryArith->getMemory(verbosity - 1);
2428 // mem += d_theoryArray->getMemory(verbosity - 1);
2429 // mem += d_theoryQuant->getMemory(verbosity - 1);
2430 // mem += d_theoryRecords->getMemory(verbosity - 1);
2431 // mem += d_theorySimulate->getMemory(verbosity - 1);
2432 // mem += d_theoryBitvector->getMemory(verbosity - 1);
2433 // mem += d_theoryDatatype->getMemory(verbosity - 1);
2434 // mem += d_translator->getMemory(verbosity - 1);
2435 
2436 // mem += getMemoryVec(verbosity, d_theories, false, true);
2437 
2438 // mem += d_flags->getMemory(verbosity - 1);
2439 // mem += d_stackLevel->getMemory(verbosity - 1);
2440 // mem += d_statistics->getMemory(verbosity - 1);
2441 // mem += d_userAssertions->getMemory(verbosity - 1);
2442 // mem += d_batchedAssertions->getMemory(verbosity - 1);
2443 // mem += d_batchedAssertionsIdx->getMemory(verbosity - 1);
2444 
2445  //TODO: how to get memory for Expr and Theorems?
2446 
2447  MemoryTracker::print("VCL", verbosity, memSelf, mem);
2448 
2449  return mem + memSelf;
2450 }
2451 
2452 void VCL::setTimeLimit(unsigned limit) {
2453  d_theoryCore->setTimeLimit(limit);
2454 }
Expr minusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:205
int arity() const
Definition: expr.h:1201
ExprStream & pop(ExprStream &os)
Restore the indentation.
bool isNull() const
Definition: expr.h:1223
const Expr & getExpr() const
Definition: expr_op.h:84
Implementation of the simple search engine.
Definition: search_simple.h:41
Expr ltExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:221
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
An exception thrown by the parser.
Definition: vcl.h:48
static Type funType(const std::vector< Type > &typeDom, const Type &typeRan)
Definition: expr.cpp:641
QueryResult
Definition: queryresult.h:32
void clearAllFlags() const
Clear the flag attribute in all the theorems.
Definition: theorem.cpp:422
virtual const Expr & getExpr() const
TheoremValue * thm() const
Definition: theorem.h:133
An exception to be thrown at typecheck error.
Definition: kinds.h:84
void setTriggers(const std::vector< std::vector< Expr > > &triggers) const
Set the triggers for a closure Expr.
Definition: expr.h:1076
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
Definition: theorem.cpp:274
Type arrayType(const Type &type1, const Type &type2)
Definition: theory_array.h:116
bool isFalse() const
Definition: expr.h:355
InputLanguage
Different input languages.
Definition: lang.h:30
IF_DEBUG(void VCL::dumpTrace(int scope){vector< StrPair > fields;fields.push_back(strPair("scope", int2string(scope)));debugger.dumpTrace("scope", fields);}) VCL
Definition: vcl.cpp:396
MS C++ specific settings.
Definition: type.h:42
"Theory" of symbolic simulation.
This theory handles uninterpreted functions.
Definition: theory_uf.h:48
Definition: kinds.h:85
Generally Useful Expression Transformations.
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
Definition: kinds.h:123
FormulaValue
Definition: formula_value.h:31
Definition: kinds.h:240
Expr gtExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:225
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
Search engine that connects to a generic SAT reasoning module.
Definition: search_sat.h:40
Definition: kinds.h:96
iterator end() const
Definition: assumptions.h:152
Expr andExpr(const Expr &right) const
Definition: expr.h:941
Definition: kinds.h:97
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
const Theorem & thm() const
Fetching a Theorem.
Definition: vcl.h:99
void addFlag(const std::string &name, const CLFlag &f)
friend ExprStream & pop(ExprStream &os)
Restore the indentation to the previous position.
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Expr impExpr(const Expr &right) const
Definition: expr.h:969
void setTrigger(const Expr &trigger) const
Definition: expr.h:1096
Theorem3.
Definition: theorem.h:308
This theory handles datatypes.
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
const Expr & getExpr() const
Definition: type.h:52
Implementation of a symbolic simulator.
iterator begin() const
Definition: assumptions.h:151
Search engine that uses an external SAT engine.
void sort2(std::vector< std::string > &keys, std::vector< T > &vals)
Sort two vectors based on the first vector.
Definition: cvc_util.h:82
Definition: kinds.h:44
int arity() const
Definition: type.h:55
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
std::string toString() const
Definition: theorem.h:404
const Theorem & tcc() const
Fetching a TCC.
Definition: vcl.h:101
This theory handles datatypes.
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Expr rebuild(ExprManager *em) const
Create a Boolean variable out of the expression.
Definition: expr.h:981
Main implementation of ValidityChecker for CVC3.
static int left(int i)
Definition: minisat_heap.h:53
bool isFlagged() const
Check if the flag attribute is set.
Definition: theorem.cpp:416
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
Abstraction over different operating systems.
Expr negate() const
Definition: expr.h:937
Implementation of a faster search engine, using newer techniques.
Definition: search_fast.h:86
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
std::string int2string(int n)
Definition: cvc_util.h:46
void processCommands()
Definition: vc_cmd.cpp:944
const Expr & getRHS() const
Definition: theorem.cpp:246
std::string toString() const
Definition: type.h:80
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
Definition: theory_arith.h:216
Generic API for a validity checker.
Definition: vc.h:92
size_t size_type
Definition: hash_table.h:75
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expression Manager.
Definition: expr_manager.h:58
This theory handles records.
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
const std::string & getName() const
Definition: expr.h:1050
Definition: kinds.h:94
This theory handles arrays.
Definition: theory_array.h:50
static int right(int i)
Definition: minisat_heap.h:54
An exception to be thrown by the smtlib translator.
Expr plusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:199
Definition: kinds.h:125
bool isRefl() const
Definition: theorem.h:171
Op mkOp() const
Make the expr into an operator.
Definition: expr.h:1178
bool empty() const
Definition: assumptions.h:95
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
void setMultiTrigger(const std::vector< Expr > &multiTrigger) const
Definition: expr.h:1107
Expr geExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:227
Definition: kinds.h:93
Definition: kinds.h:53
Definition: kinds.h:63
Definition: kinds.h:124
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
Expr uminusExpr(const Expr &child)
Definition: theory_arith.h:197
Definition: kinds.h:99
std::pair< std::string, T > strPair(const std::string &f, const T &t)
Definition: cvc_util.h:74
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
Expr leExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:223
bool isFunction() const
Definition: type.h:62
bool isAssump() const
Definition: theorem.cpp:395
Structure to hold user assertions indexed by declaration order.
Definition: vcl.h:88
Definition: kinds.h:229
Expr divideExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:219
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
Definition: kinds.h:67
This theory handles quantifiers.
Definition: theory_quant.h:186
Expr multExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:207
Nice SAL-like language for manually written specs.
Definition: lang.h:32
void setFlag() const
Set the flag attribute.
Definition: theorem.cpp:429
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
const Assumptions & getAssumptionsRef() const
Definition: theorem.h:365