CVC3
vcl.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file vcl.h
4  * \brief Main implementation of ValidityChecker for CVC3.
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Wed Dec 11 14:40:39 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__include__vcl_h_
23 #define _cvc3__include__vcl_h_
24 
25 #include <queue>
26 
27 #include "vc.h"
28 #include "command_line_flags.h"
29 #include "statistics.h"
30 #include "cdmap.h"
31 #include "cdlist.h"
32 
33 namespace CVC3 {
34 
35  class SearchEngine;
36  class Theory;
37  class TheoryCore;
38  class TheoryUF;
39  class TheoryArith;
40  class TheoryArray;
41  class TheoryQuant;
42  class TheoryRecords;
43  class TheorySimulate;
44  class TheoryBitvector;
45  class TheoryDatatype;
46  class Translator;
47 
48 class CVC_DLL VCL : public ValidityChecker {
49 
50  //! Pointers to main system components
55 
56  //! Pointers to theories
67 
68  //! All theories are stored in this common vector
69  /*! This includes TheoryCore and TheoryArith. */
70  std::vector<Theory*> d_theories;
71 
72  //! Command line flags
74 
75  //! User-level view of the scope stack
77 
78  //! True iff we've pushed the stack artificially to avoid polluting context
80 
81  //! Run-time statistics
83 
84  //! Next index for user assertion
85  size_t d_nextIdx;
86 
87  //! Structure to hold user assertions indexed by declaration order
88  class UserAssertion {
89  size_t d_idx;
90  Theorem d_thm; //! The theorem of the assertion (a |- a)
91  Theorem d_tcc; //! The proof of its TCC
92  public:
93  //! Default constructor
95  //! Constructor
96  UserAssertion(const Theorem& thm, const Theorem& tcc, size_t idx)
97  : d_idx(idx), d_thm(thm), d_tcc(tcc) { }
98  //! Fetching a Theorem
99  const Theorem& thm() const { return d_thm; }
100  //! Fetching a TCC
101  const Theorem& tcc() const { return d_tcc; }
102  //! Auto-conversion to Theorem
103  operator Theorem() { return d_thm; }
104  //! Comparison for use in std::map, to sort in declaration order
105  friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) {
106  return (a1.d_idx < a2.d_idx);
107  }
108  };
109 
110  //! Backtracking map of user assertions
112 
113  //! Backtracking map of assertions when assertion batching is on
115 
116  //! Index into batched Assertions
118 
119  //! Result of the last query()
120  /*! Saved for printing assumptions and proofs. Normally it is
121  * Theorem3, but query() on a TCC returns a 2-valued Theorem. */
123 
124  //! Result of the last query(e, true) (for a TCC).
126 
127  //! Closure of the last query(e): |- Gamma => e
129 
130  //! Whether to dump a trace (or a translated version)
131  bool d_dump;
132 
133  // Private methods
134 
135  //! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi"
136  Theorem3 deriveClosure(const Theorem3& thm);
137 
138  //! Recursive assumption graph traversal to find user assumptions
139  /*!
140  * If an assumption has a TCC, traverse the proof of TCC and add its
141  * assumptions to the set recursively.
142  */
143  void getAssumptionsRec(const Theorem& thm,
144  std::set<UserAssertion>& assumptions,
145  bool addTCCs);
146 
147  //! Get set of user assertions from the set of assumptions
148  void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions);
149 
150  //! Check the tcc
151  Theorem checkTCC(const Expr& tcc);
152 
153 #ifdef _CVC3_DEBUG_MODE
154  //! Print an entry to the dump file: change of scope
155  void dumpTrace(int scope);
156 #endif
157 
158  //! Initialize everything except flags
159  void init(void);
160  //! Destroy everything except flags
161  void destroy(void);
162 
163 public:
164  // Takes the vector of command line flags.
165  VCL(const CLFlags& flags);
166  ~VCL();
167 
168  // Implementation of vc.h virtual functions
169 
170  CLFlags& getFlags() const { return *d_flags; }
171  void reprocessFlags();
172 
173  TheoryCore* core();
174 
175  Type boolType();
176  Type realType();
177  Type intType();
178  Type subrangeType(const Expr& l, const Expr& r);
179  Type subtypeType(const Expr& pred, const Expr& witness);
180  Type tupleType(const Type& type0, const Type& type1);
181  Type tupleType(const Type& type0, const Type& type1, const Type& type2);
182  Type tupleType(const std::vector<Type>& types);
183  Type recordType(const std::string& field, const Type& type);
184  Type recordType(const std::string& field0, const Type& type0,
185  const std::string& field1, const Type& type1);
186  Type recordType(const std::string& field0, const Type& type0,
187  const std::string& field1, const Type& type1,
188  const std::string& field2, const Type& type2);
189  Type recordType(const std::vector<std::string>& fields,
190  const std::vector<Type>& types);
191  Type dataType(const std::string& name,
192  const std::string& constructor,
193  const std::vector<std::string>& selectors,
194  const std::vector<Expr>& types);
195  Type dataType(const std::string& name,
196  const std::vector<std::string>& constructors,
197  const std::vector<std::vector<std::string> >& selectors,
198  const std::vector<std::vector<Expr> >& types);
199  void dataType(const std::vector<std::string>& names,
200  const std::vector<std::vector<std::string> >& constructors,
201  const std::vector<std::vector<std::vector<std::string> > >& selectors,
202  const std::vector<std::vector<std::vector<Expr> > >& types,
203  std::vector<Type>& returnTypes);
204  Type arrayType(const Type& typeIndex, const Type& typeData);
205  Type bitvecType(int n);
206  Type funType(const Type& typeDom, const Type& typeRan);
207  Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
208  Type createType(const std::string& typeName);
209  Type createType(const std::string& typeName, const Type& def);
210  Type lookupType(const std::string& typeName);
211 
212  ExprManager* getEM() { return d_em; }
213  Expr varExpr(const std::string& name, const Type& type);
214  Expr varExpr(const std::string& name, const Type& type, const Expr& def);
215  Expr lookupVar(const std::string& name, Type* type);
216  Type getType(const Expr& e);
217  Type getBaseType(const Expr& e);
218  Type getBaseType(const Type& e);
219  Expr getTypePred(const Type&t, const Expr& e);
220  Expr stringExpr(const std::string& str);
221  Expr idExpr(const std::string& name);
222  Expr listExpr(const std::vector<Expr>& kids);
223  Expr listExpr(const Expr& e1);
224  Expr listExpr(const Expr& e1, const Expr& e2);
225  Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
226  Expr listExpr(const std::string& op, const std::vector<Expr>& kids);
227  Expr listExpr(const std::string& op, const Expr& e1);
228  Expr listExpr(const std::string& op, const Expr& e1,
229  const Expr& e2);
230  Expr listExpr(const std::string& op, const Expr& e1,
231  const Expr& e2, const Expr& e3);
232  void printExpr(const Expr& e);
233  void printExpr(const Expr& e, std::ostream& os);
234  Expr parseExpr(const Expr& e);
235  Type parseType(const Expr& e);
236  Expr importExpr(const Expr& e);
237  Type importType(const Type& t);
238  void cmdsFromString(const std::string& s, InputLanguage lang);
239  Expr exprFromString(const std::string& s);
240 
241  Expr trueExpr();
242  Expr falseExpr();
243  Expr notExpr(const Expr& child);
244  Expr andExpr(const Expr& left, const Expr& right);
245  Expr andExpr(const std::vector<Expr>& children);
246  Expr orExpr(const Expr& left, const Expr& right);
247  Expr orExpr(const std::vector<Expr>& children);
248  Expr impliesExpr(const Expr& hyp, const Expr& conc);
249  Expr iffExpr(const Expr& left, const Expr& right);
250  Expr eqExpr(const Expr& child0, const Expr& child1);
251  Expr distinctExpr(const std::vector<Expr>& children);
252  Expr iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart);
253 
254  Op createOp(const std::string& name, const Type& type);
255  Op createOp(const std::string& name, const Type& type, const Expr& def);
256  Op lookupOp(const std::string& name, Type* type);
257  Expr funExpr(const Op& op, const Expr& child);
258  Expr funExpr(const Op& op, const Expr& left, const Expr& right);
259  Expr funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2);
260  Expr funExpr(const Op& op, const std::vector<Expr>& children);
261 
262  bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
263  Expr ratExpr(int n, int d);
264  Expr ratExpr(const std::string& n, const std::string& d, int base);
265  Expr ratExpr(const std::string& n, int base);
266  Expr uminusExpr(const Expr& child);
267  Expr plusExpr(const Expr& left, const Expr& right);
268  Expr plusExpr(const std::vector<Expr>& children);
269  Expr minusExpr(const Expr& left, const Expr& right);
270  Expr multExpr(const Expr& left, const Expr& right);
271  Expr powExpr(const Expr& x, const Expr& n);
272  Expr divideExpr(const Expr& left, const Expr& right);
273  Expr ltExpr(const Expr& left, const Expr& right);
274  Expr leExpr(const Expr& left, const Expr& right);
275  Expr gtExpr(const Expr& left, const Expr& right);
276  Expr geExpr(const Expr& left, const Expr& right);
277 
278  Expr recordExpr(const std::string& field, const Expr& expr);
279  Expr recordExpr(const std::string& field0, const Expr& expr0,
280  const std::string& field1, const Expr& expr1);
281  Expr recordExpr(const std::string& field0, const Expr& expr0,
282  const std::string& field1, const Expr& expr1,
283  const std::string& field2, const Expr& expr2);
284  Expr recordExpr(const std::vector<std::string>& fields,
285  const std::vector<Expr>& exprs);
286  Expr recSelectExpr(const Expr& record, const std::string& field);
287  Expr recUpdateExpr(const Expr& record, const std::string& field,
288  const Expr& newValue);
289 
290  Expr readExpr(const Expr& array, const Expr& index);
291  Expr writeExpr(const Expr& array, const Expr& index, const Expr& newValue);
292 
293  Expr newBVConstExpr(const std::string& s, int base);
294  Expr newBVConstExpr(const std::vector<bool>& bits);
295  Expr newBVConstExpr(const Rational& r, int len);
296  Expr newConcatExpr(const Expr& t1, const Expr& t2);
297  Expr newConcatExpr(const std::vector<Expr>& kids);
298  Expr newBVExtractExpr(const Expr& e, int hi, int low);
299  Expr newBVNegExpr(const Expr& t1);
300  Expr newBVAndExpr(const Expr& t1, const Expr& t2);
301  Expr newBVAndExpr(const std::vector<Expr>& kids);
302  Expr newBVOrExpr(const Expr& t1, const Expr& t2);
303  Expr newBVOrExpr(const std::vector<Expr>& kids);
304  Expr newBVXorExpr(const Expr& t1, const Expr& t2);
305  Expr newBVXorExpr(const std::vector<Expr>& kids);
306  Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
307  Expr newBVXnorExpr(const std::vector<Expr>& kids);
308  Expr newBVNandExpr(const Expr& t1, const Expr& t2);
309  Expr newBVNorExpr(const Expr& t1, const Expr& t2);
310  Expr newBVCompExpr(const Expr& t1, const Expr& t2);
311  Expr newBVLTExpr(const Expr& t1, const Expr& t2);
312  Expr newBVLEExpr(const Expr& t1, const Expr& t2);
313  Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
314  Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
315  Expr newSXExpr(const Expr& t1, int len);
316  Expr newBVUminusExpr(const Expr& t1);
317  Expr newBVSubExpr(const Expr& t1, const Expr& t2);
318  Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
319  Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2);
320  Expr newBVMultExpr(int numbits, const Expr& t1, const Expr& t2);
321  Expr newBVUDivExpr(const Expr& t1, const Expr& t2);
322  Expr newBVURemExpr(const Expr& t1, const Expr& t2);
323  Expr newBVSDivExpr(const Expr& t1, const Expr& t2);
324  Expr newBVSRemExpr(const Expr& t1, const Expr& t2);
325  Expr newBVSModExpr(const Expr& t1, const Expr& t2);
326  Expr newFixedLeftShiftExpr(const Expr& t1, int r);
327  Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
328  Expr newFixedRightShiftExpr(const Expr& t1, int r);
329  Expr newBVSHL(const Expr& t1, const Expr& t2);
330  Expr newBVLSHR(const Expr& t1, const Expr& t2);
331  Expr newBVASHR(const Expr& t1, const Expr& t2);
332  Rational computeBVConst(const Expr& e);
333 
334  Expr tupleExpr(const std::vector<Expr>& exprs);
335  Expr tupleSelectExpr(const Expr& tuple, int index);
336  Expr tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue);
337  Expr datatypeConsExpr(const std::string& constructor,
338  const std::vector<Expr>& args);
339  Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
340  Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
341  Expr boundVarExpr(const std::string& name, const std::string& uid,
342  const Type& type);
343  Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
344  Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, const Expr& trigger);
345  Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
346  const std::vector<Expr>& triggers);
347  Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
348  const std::vector<std::vector<Expr> >& triggers);
349 
350  void setTriggers(const Expr& e, const std::vector<std::vector<Expr> >& triggers);
351  void setTriggers(const Expr& e, const std::vector<Expr>& triggers);
352  void setTrigger(const Expr& e, const Expr& trigger);
353  void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger);
354 
355  Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
356  Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
357  Op transClosure(const Op& op);
358  Expr simulateExpr(const Expr& f, const Expr& s0,
359  const std::vector<Expr>& inputs, const Expr& n);
360 
361  void setResourceLimit(unsigned limit);
362  void setTimeLimit(unsigned limit);
363  void assertFormula(const Expr& e);
364  void registerAtom(const Expr& e);
365  Expr getImpliedLiteral();
366  Expr simplify(const Expr& e);
367  Theorem simplifyThm(const Expr& e);
368  QueryResult query(const Expr& e);
369  QueryResult checkUnsat(const Expr& e);
370  QueryResult checkContinue();
371  QueryResult restart(const Expr& e);
372  void returnFromCheck();
373  void getUserAssumptions(std::vector<Expr>& assumptions);
374  void getInternalAssumptions(std::vector<Expr>& assumptions);
375  void getAssumptions(std::vector<Expr>& assumptions);
376  void getAssumptionsUsed(std::vector<Expr>& assumptions);
377  Expr getProofQuery();
378  void getCounterExample(std::vector<Expr>& assumptions, bool inOrder);
379  void getConcreteModel(ExprMap<Expr> & m);
380  QueryResult tryModelGeneration();
381  FormulaValue value(const Expr& e);
382  bool inconsistent(std::vector<Expr>& assumptions);
383  bool inconsistent();
384  bool incomplete();
385  bool incomplete(std::vector<std::string>& reasons);
386  Proof getProof();
387  Expr getAssignment();
388  Expr getValue(Expr e);
389  Expr getTCC();
390  void getAssumptionsTCC(std::vector<Expr>& assumptions);
391  Proof getProofTCC();
392  Expr getClosure();
393  Proof getProofClosure();
394 
395  int stackLevel();
396  void push();
397  void pop();
398  void popto(int stackLevel);
399  int scopeLevel();
400  void pushScope();
401  void popScope();
402  void poptoScope(int scopeLevel);
403  Context* getCurrentContext();
404  void reset();
405  void logAnnotation(const Expr& annot);
406 
407  void loadFile(const std::string& fileName,
409  bool interactive = false,
410  bool calledFromParser = false);
411  void loadFile(std::istream& is,
413  bool interactive = false);
414 
415  Statistics& getStatistics() { return *d_statistics; }
416  void printStatistics() { std::cout << *d_statistics << std::endl; }
417  unsigned long getMemory(int verbosity = 0);
418 
419 };
420 
421 }
422 
423 #endif