CVC3  2.4.1
vc.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file vc.h
4  * \brief Generic API for a validity checker
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Tue Nov 26 17:45:10 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__vc_h_
23 #define _cvc3__include__vc_h_
24 
25 #include "os.h"
26 #include "queryresult.h"
27 #include "expr.h"
28 #include "formula_value.h"
29 
30 /*****************************************************************************/
31 /*! Note that this list of modules is very incomplete
32  */
33 /*****************************************************************************/
34 
35 /*****************************************************************************/
36 /*!
37  *\defgroup CVC3 CVC3
38  *\brief The top level group which includes all of CVC3 documentation.
39  *@{
40  */
41 /*****************************************************************************/
42 
43 /*****************************************************************************/
44 /*!
45  *\defgroup BuildingBlocks Building Blocks
46  *\brief Code providing basic infrastructure
47  */
48 /*****************************************************************************/
49 
50 /*****************************************************************************/
51 /*!
52  *\defgroup VC Validity Checker
53  *\brief The modules that make up the validity checker
54  */
55 /*****************************************************************************/
56 
57 /*@}*/ // end of group CVC3
58 
59 /*****************************************************************************/
60 /*!
61  *\defgroup VC_API Validity Checker API
62  * \ingroup VC
63  *\brief The library interface of the validity checker (class ValidityChecker)
64  */
65 /*****************************************************************************/
66 
67 namespace CVC3 {
68 
69 class Context;
70 class CLFlags;
71 class Statistics;
72 
73 /*****************************************************************************/
74 /*!
75  *\class ValidityChecker
76  *\brief Generic API for a validity checker
77  *\ingroup VC_API
78  *\anchor vc
79  *
80  * Author: Clark Barrett
81  *
82  * Created: Tue Nov 26 18:24:25 2002
83  *
84  * All terms and formulas are represented as expressions using the Expr class.
85  * The notion of a context is also important. A context is a "background" set
86  * of formulas which are assumed to be true or false. Formulas can be added to
87  * the context explicitly, using assertFormula, or they may be added as part of
88  * processing a query command. At any time, the current set of formulas making
89  * up the context can be retrieved using getAssumptions.
90  */
91 /*****************************************************************************/
93 
94 public:
95  //! Constructor
97  //! Destructor
98  virtual ~ValidityChecker() {}
99 
100  //! Return the set of command-line flags
101  /*! The flags are returned by reference, and if modified, will have an
102  immediate effect on the subsequent commands. Note that not all flags will
103  have such an effect; some flags are used only at initialization time (like
104  "sat"), and therefore, will not take effect if modified after
105  ValidityChecker is created.
106  */
107  virtual CLFlags& getFlags() const = 0;
108  //! Force reprocessing of all flags
109  virtual void reprocessFlags() = 0;
110 
111  /***************************************************************************/
112  /*
113  * Static methods
114  */
115  /***************************************************************************/
116 
117  //! Create the set of command line flags with default values;
118  /*!
119  \return the set of flags by value
120  */
121  static CLFlags createFlags();
122  //! Create an instance of ValidityChecker
123  /*!
124  \param flags is the set of command line flags.
125  */
126  static ValidityChecker* create(const CLFlags& flags);
127  //! Create an instance of ValidityChecker using default flag values.
128  static ValidityChecker* create();
129 
130  /***************************************************************************/
131  /*!
132  *\name Type-related methods
133  * Methods for creating and looking up types
134  *\sa class Type
135  *@{
136  */
137  /***************************************************************************/
138 
139  // Basic types
140  virtual Type boolType() = 0; //!< Create type BOOLEAN
141 
142  virtual Type realType() = 0; //!< Create type REAL
143 
144  virtual Type intType() = 0; //!< Create type INT
145 
146  //! Create a subrange type [l..r]
147  /*! l and r can be Null; l=Null represents minus infinity, r=Null is
148  * plus infinity.
149  */
150  virtual Type subrangeType(const Expr& l, const Expr& r) = 0;
151 
152  //! Creates a subtype defined by the given predicate
153  /*!
154  * \param pred is a predicate taking one argument of type T and returning
155  * Boolean. The resulting type is a subtype of T whose elements x are those
156  * satisfying the predicate pred(x).
157  *
158  * \param witness is an expression of type T for which pred holds (if a Null
159  * expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$.
160  * if the witness check fails, a TypecheckException is thrown.
161  */
162  virtual Type subtypeType(const Expr& pred, const Expr& witness) = 0;
163 
164  // Tuple types
165  //! 2-element tuple
166  virtual Type tupleType(const Type& type0, const Type& type1) = 0;
167 
168  //! 3-element tuple
169  virtual Type tupleType(const Type& type0, const Type& type1,
170  const Type& type2) = 0;
171  //! n-element tuple (from a vector of types)
172  virtual Type tupleType(const std::vector<Type>& types) = 0;
173 
174  // Record types
175  //! 1-element record
176  virtual Type recordType(const std::string& field, const Type& type) = 0;
177 
178  //! 2-element record
179  /*! Fields will be sorted automatically */
180  virtual Type recordType(const std::string& field0, const Type& type0,
181  const std::string& field1, const Type& type1) = 0;
182  //! 3-element record
183  /*! Fields will be sorted automatically */
184  virtual Type recordType(const std::string& field0, const Type& type0,
185  const std::string& field1, const Type& type1,
186  const std::string& field2, const Type& type2) = 0;
187  //! n-element record (fields and types must be of the same length)
188  /*! Fields will be sorted automatically */
189  virtual Type recordType(const std::vector<std::string>& fields,
190  const std::vector<Type>& types) = 0;
191 
192  // Datatypes
193 
194  //! Single datatype, single constructor
195  /*! The types are either type exressions (obtained from a type with
196  * getExpr()) or string expressions containing the name of (one of) the
197  * dataType(s) being defined. */
198  virtual Type dataType(const std::string& name,
199  const std::string& constructor,
200  const std::vector<std::string>& selectors,
201  const std::vector<Expr>& types) = 0;
202 
203  //! Single datatype, multiple constructors
204  /*! The types are either type exressions (obtained from a type with
205  * getExpr()) or string expressions containing the name of (one of) the
206  * dataType(s) being defined. */
207  virtual Type dataType(const std::string& name,
208  const std::vector<std::string>& constructors,
209  const std::vector<std::vector<std::string> >& selectors,
210  const std::vector<std::vector<Expr> >& types) = 0;
211 
212  //! Multiple datatypes
213  /*! The types are either type exressions (obtained from a type with
214  * getExpr()) or string expressions containing the name of (one of) the
215  * dataType(s) being defined. */
216  virtual void dataType(const std::vector<std::string>& names,
217  const std::vector<std::vector<std::string> >& constructors,
218  const std::vector<std::vector<std::vector<std::string> > >& selectors,
219  const std::vector<std::vector<std::vector<Expr> > >& types,
220  std::vector<Type>& returnTypes) = 0;
221 
222  //! Create an array type (ARRAY typeIndex OF typeData)
223  virtual Type arrayType(const Type& typeIndex, const Type& typeData) = 0;
224 
225  //! Create a bitvector type of length n
226  virtual Type bitvecType(int n) = 0;
227 
228  //! Create a function type typeDom -> typeRan
229  virtual Type funType(const Type& typeDom, const Type& typeRan) = 0;
230 
231  //! Create a function type (t1,t2,...,tn) -> typeRan
232  virtual Type funType(const std::vector<Type>& typeDom, const Type& typeRan) = 0;
233 
234  //! Create named user-defined uninterpreted type
235  virtual Type createType(const std::string& typeName) = 0;
236 
237  //! Create named user-defined interpreted type (type abbreviation)
238  virtual Type createType(const std::string& typeName, const Type& def) = 0;
239 
240  //! Lookup a user-defined (uninterpreted) type by name. Returns Null if none.
241  virtual Type lookupType(const std::string& typeName) = 0;
242 
243  /*@}*/ // End of Type-related methods
244 
245  /***************************************************************************/
246  /*!
247  *\name General Expr methods
248  *\sa class Expr
249  *\sa class ExprManager
250  *@{
251  */
252  /***************************************************************************/
253 
254  //! Return the ExprManager
255  virtual ExprManager* getEM() = 0;
256 
257  //! Create a variable with a given name and type
258  /*!
259  \param name is the name of the variable
260  \param type is its type. The type cannot be a function type.
261  \return an Expr representation of a new variable
262  */
263  virtual Expr varExpr(const std::string& name, const Type& type) = 0;
264 
265  //! Create a variable with a given name, type, and value
266  virtual Expr varExpr(const std::string& name, const Type& type,
267  const Expr& def) = 0;
268 
269  //! Get the variable associated with a name, and its type
270  /*!
271  \param name is the variable name
272  \param type is where the type value is returned
273 
274  \return a variable by the name. If there is no such Expr, a NULL \
275  Expr is returned.
276  */
277  virtual Expr lookupVar(const std::string& name, Type* type) = 0;
278 
279  //! Get the type of the Expr.
280  virtual Type getType(const Expr& e) = 0;
281 
282  //! Get the largest supertype of the Expr.
283  virtual Type getBaseType(const Expr& e) = 0;
284 
285  //! Get the largest supertype of the Type.
286  virtual Type getBaseType(const Type& t) = 0;
287 
288  //! Get the subtype predicate
289  virtual Expr getTypePred(const Type&t, const Expr& e) = 0;
290 
291  //! Create a string Expr
292  virtual Expr stringExpr(const std::string& str) = 0;
293 
294  //! Create an ID Expr
295  virtual Expr idExpr(const std::string& name) = 0;
296 
297  //! Create a list Expr
298  /*! Intermediate representation for DP-specific expressions.
299  * Normally, the first element of the list is a string Expr
300  * representing an operator, and the rest of the list are the
301  * arguments. For example,
302  *
303  * kids.push_back(vc->stringExpr("PLUS"));
304  * kids.push_back(x); // x and y are previously created Exprs
305  * kids.push_back(y);
306  * Expr lst = vc->listExpr(kids);
307  *
308  * Or, alternatively (using its overloaded version):
309  *
310  * Expr lst = vc->listExpr("PLUS", x, y);
311  *
312  * or
313  *
314  * vector<Expr> summands;
315  * summands.push_back(x); summands.push_back(y); ...
316  * Expr lst = vc->listExpr("PLUS", summands);
317  */
318  virtual Expr listExpr(const std::vector<Expr>& kids) = 0;
319 
320  //! Overloaded version of listExpr with one argument
321  virtual Expr listExpr(const Expr& e1) = 0;
322 
323  //! Overloaded version of listExpr with two arguments
324  virtual Expr listExpr(const Expr& e1, const Expr& e2) = 0;
325 
326  //! Overloaded version of listExpr with three arguments
327  virtual Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3) = 0;
328 
329  //! Overloaded version of listExpr with string operator and many arguments
330  virtual Expr listExpr(const std::string& op,
331  const std::vector<Expr>& kids) = 0;
332 
333  //! Overloaded version of listExpr with string operator and one argument
334  virtual Expr listExpr(const std::string& op, const Expr& e1) = 0;
335 
336  //! Overloaded version of listExpr with string operator and two arguments
337  virtual Expr listExpr(const std::string& op, const Expr& e1,
338  const Expr& e2) = 0;
339 
340  //! Overloaded version of listExpr with string operator and three arguments
341  virtual Expr listExpr(const std::string& op, const Expr& e1,
342  const Expr& e2, const Expr& e3) = 0;
343 
344  //! Prints e to the standard output
345  virtual void printExpr(const Expr& e) = 0;
346 
347  //! Prints e to the given ostream
348  virtual void printExpr(const Expr& e, std::ostream& os) = 0;
349 
350  //! Parse an expression using a Theory-specific parser
351  virtual Expr parseExpr(const Expr& e) = 0;
352 
353  //! Parse a type expression using a Theory-specific parser
354  virtual Type parseType(const Expr& e) = 0;
355 
356  //! Import the Expr from another instance of ValidityChecker
357  /*! When expressions need to be passed among several instances of
358  * ValidityChecker, they need to be explicitly imported into the
359  * corresponding instance using this method. The return result is
360  * an identical expression that belongs to the current instance of
361  * ValidityChecker, and can be safely used as part of more complex
362  * expressions from the same instance.
363  */
364  virtual Expr importExpr(const Expr& e) = 0;
365 
366  //! Import the Type from another instance of ValidityChecker
367  /*! \sa getType() */
368  virtual Type importType(const Type& t) = 0;
369 
370  //! Parse a sequence of commands from a presentation language string
371  virtual void cmdsFromString(const std::string& s,
373 
374  //! Parse an expression from a presentation language string
375  virtual Expr exprFromString(const std::string& e) = 0;
376 
377  /*@}*/ // End of General Expr Methods
378 
379  /***************************************************************************/
380  /*!
381  *\name Core expression methods
382  * Methods for manipulating core expressions
383  *
384  * Except for equality and ite, the children provided as arguments must be of
385  * type Boolean.
386  *@{
387  */
388  /***************************************************************************/
389 
390  //! Return TRUE Expr
391  virtual Expr trueExpr() = 0;
392 
393  //! Return FALSE Expr
394  virtual Expr falseExpr() = 0;
395 
396  //! Create negation
397  virtual Expr notExpr(const Expr& child) = 0;
398 
399  //! Create 2-element conjunction
400  virtual Expr andExpr(const Expr& left, const Expr& right) = 0;
401 
402  //! Create n-element conjunction
403  virtual Expr andExpr(const std::vector<Expr>& children) = 0;
404 
405  //! Create 2-element disjunction
406  virtual Expr orExpr(const Expr& left, const Expr& right) = 0;
407 
408  //! Create n-element disjunction
409  virtual Expr orExpr(const std::vector<Expr>& children) = 0;
410 
411  //! Create Boolean implication
412  virtual Expr impliesExpr(const Expr& hyp, const Expr& conc) = 0;
413 
414  //! Create left IFF right (boolean equivalence)
415  virtual Expr iffExpr(const Expr& left, const Expr& right) = 0;
416 
417  //! Create an equality expression.
418  /*!
419  The two children must have the same type, and cannot be of type
420  Boolean.
421  */
422  virtual Expr eqExpr(const Expr& child0, const Expr& child1) = 0;
423 
424  //! Create IF ifpart THEN thenpart ELSE elsepart ENDIF
425  /*!
426  \param ifpart must be of type Boolean.
427  \param thenpart and \param elsepart must have the same type, which will
428  also be the type of the ite expression.
429  */
430  virtual Expr iteExpr(const Expr& ifpart, const Expr& thenpart,
431  const Expr& elsepart) = 0;
432 
433  /**
434  * Create an expression asserting that all the children are different.
435  * @param children the children to be asserted different
436  */
437  virtual Expr distinctExpr(const std::vector<Expr>& children) = 0;
438 
439  /*@}*/ // End of Core expression methods
440 
441  /***************************************************************************/
442  /*!
443  *\name User-defined (uninterpreted) function methods
444  * Methods for manipulating uninterpreted function expressions
445  *@{
446  */
447  /***************************************************************************/
448 
449  //! Create a named uninterpreted function with a given type
450  /*!
451  \param name is the new function's name (as ID Expr)
452  \param type is a function type ( [range -> domain] )
453  */
454  virtual Op createOp(const std::string& name, const Type& type) = 0;
455 
456  //! Create a named user-defined function with a given type
457  virtual Op createOp(const std::string& name, const Type& type,
458  const Expr& def) = 0;
459 
460  //! Get the Op associated with a name, and its type
461  /*!
462  \param name is the operator name
463  \param type is where the type value is returned
464 
465  \return an Op by the name. If there is no such Op, a NULL \
466  Op is returned.
467  */
468  virtual Op lookupOp(const std::string& name, Type* type) = 0;
469 
470  //! Unary function application (op must be of function type)
471  virtual Expr funExpr(const Op& op, const Expr& child) = 0;
472 
473  //! Binary function application (op must be of function type)
474  virtual Expr funExpr(const Op& op, const Expr& left, const Expr& right) = 0;
475 
476  //! Ternary function application (op must be of function type)
477  virtual Expr funExpr(const Op& op, const Expr& child0,
478  const Expr& child1, const Expr& child2) = 0;
479 
480  //! n-ary function application (op must be of function type)
481  virtual Expr funExpr(const Op& op, const std::vector<Expr>& children) = 0;
482 
483  /*@}*/ // End of User-defined (uninterpreted) function methods
484 
485  /***************************************************************************/
486  /*!
487  *\name Arithmetic expression methods
488  * Methods for manipulating arithmetic expressions
489  *
490  * These functions create arithmetic expressions. The children provided
491  * as arguments must be of type Real.
492  *@{
493  */
494  /***************************************************************************/
495 
496  /*!
497  * Add the pair of variables to the variable ordering for aritmetic solving.
498  * Terms that are not arithmetic will be ignored.
499  * \param smaller the smaller variable
500  * \param bigger the bigger variable
501  */
502  virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger) = 0;
503 
504  //! Create a rational number with numerator n and denominator d.
505  /*!
506  \param n the numerator
507  \param d the denominator, cannot be 0.
508  */
509  virtual Expr ratExpr(int n, int d = 1) = 0;
510 
511  //! Create a rational number with numerator n and denominator d.
512  /*!
513  Here n and d are given as strings. They are converted to
514  arbitrary-precision integers according to the given base.
515  */
516  virtual Expr ratExpr(const std::string& n, const std::string& d, int base) = 0;
517 
518  //! Create a rational from a single string.
519  /*!
520  \param n can be a string containing an integer, a pair of integers
521  "nnn/ddd", or a number in the fixed or floating point format.
522  \param base is the base in which to interpret the string.
523  */
524  virtual Expr ratExpr(const std::string& n, int base = 10) = 0;
525 
526  //! Unary minus.
527  virtual Expr uminusExpr(const Expr& child) = 0;
528 
529  //! Create 2-element sum (left + right)
530  virtual Expr plusExpr(const Expr& left, const Expr& right) = 0;
531 
532  //! Create n-element sum
533  virtual Expr plusExpr(const std::vector<Expr>& children) = 0;
534 
535  //! Make a difference (left - right)
536  virtual Expr minusExpr(const Expr& left, const Expr& right) = 0;
537 
538  //! Create a product (left * right)
539  virtual Expr multExpr(const Expr& left, const Expr& right) = 0;
540 
541  //! Create a power expression (x ^ n); n must be integer
542  virtual Expr powExpr(const Expr& x, const Expr& n) = 0;
543 
544  //! Create expression x / y
545  virtual Expr divideExpr(const Expr& numerator, const Expr& denominator) = 0;
546 
547  //! Create (left < right)
548  virtual Expr ltExpr(const Expr& left, const Expr& right) = 0;
549 
550  //! Create (left <= right)
551  virtual Expr leExpr(const Expr& left, const Expr& right) = 0;
552 
553  //! Create (left > right)
554  virtual Expr gtExpr(const Expr& left, const Expr& right) = 0;
555 
556  //! Create (left >= right)
557  virtual Expr geExpr(const Expr& left, const Expr& right) = 0;
558 
559  /*@}*/ // End of Arithmetic expression methods
560 
561  /***************************************************************************/
562  /*!
563  *\name Record expression methods
564  * Methods for manipulating record expressions
565  *@{
566  */
567  /***************************************************************************/
568 
569  //! Create a 1-element record value (# field := expr #)
570  /*! Fields will be sorted automatically */
571  virtual Expr recordExpr(const std::string& field, const Expr& expr) = 0;
572 
573  //! Create a 2-element record value (# field0 := expr0, field1 := expr1 #)
574  /*! Fields will be sorted automatically */
575  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
576  const std::string& field1, const Expr& expr1) = 0;
577 
578  //! Create a 3-element record value (# field_i := expr_i #)
579  /*! Fields will be sorted automatically */
580  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
581  const std::string& field1, const Expr& expr1,
582  const std::string& field2, const Expr& expr2) = 0;
583 
584  //! Create an n-element record value (# field_i := expr_i #)
585  /*!
586  * \param fields
587  * \param exprs must be the same length as fields
588  *
589  * Fields will be sorted automatically
590  */
591  virtual Expr recordExpr(const std::vector<std::string>& fields,
592  const std::vector<Expr>& exprs) = 0;
593 
594  //! Create record.field (field selection)
595  /*! Create an expression representing the selection of a field from
596  a record. */
597  virtual Expr recSelectExpr(const Expr& record, const std::string& field) = 0;
598 
599  //! Record update; equivalent to "record WITH .field := newValue"
600  /*! Notice the `.' before field in the presentation language (and
601  the comment above); this is to distinguish it from datatype
602  update.
603  */
604  virtual Expr recUpdateExpr(const Expr& record, const std::string& field,
605  const Expr& newValue) = 0;
606 
607  /*@}*/ // End of Record expression methods
608 
609  /***************************************************************************/
610  /*!
611  *\name Array expression methods
612  * Methods for manipulating array expressions
613  *@{
614  */
615  /***************************************************************************/
616 
617  //! Create an expression array[index] (array access)
618  /*! Create an expression for the value of array at the given index */
619  virtual Expr readExpr(const Expr& array, const Expr& index) = 0;
620 
621  //! Array update; equivalent to "array WITH index := newValue"
622  virtual Expr writeExpr(const Expr& array, const Expr& index,
623  const Expr& newValue) = 0;
624 
625  /*@}*/ // End of Array expression methods
626 
627  /***************************************************************************/
628  /*!
629  *\name Bitvector expression methods
630  * Methods for manipulating bitvector expressions
631  *@{
632  */
633  /***************************************************************************/
634 
635  // Bitvector constants
636  // From a string of digits in a given base
637  virtual Expr newBVConstExpr(const std::string& s, int base = 2) = 0;
638  // From a vector of bools
639  virtual Expr newBVConstExpr(const std::vector<bool>& bits) = 0;
640  // From a rational: bitvector is of length 'len', or the min. needed length when len=0.
641  virtual Expr newBVConstExpr(const Rational& r, int len = 0) = 0;
642 
643  // Concat and extract
644  virtual Expr newConcatExpr(const Expr& t1, const Expr& t2) = 0;
645  virtual Expr newConcatExpr(const std::vector<Expr>& kids) = 0;
646  virtual Expr newBVExtractExpr(const Expr& e, int hi, int low) = 0;
647 
648  // Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor
649  virtual Expr newBVNegExpr(const Expr& t1) = 0;
650 
651  virtual Expr newBVAndExpr(const Expr& t1, const Expr& t2) = 0;
652  virtual Expr newBVAndExpr(const std::vector<Expr>& kids) = 0;
653 
654  virtual Expr newBVOrExpr(const Expr& t1, const Expr& t2) = 0;
655  virtual Expr newBVOrExpr(const std::vector<Expr>& kids) = 0;
656 
657  virtual Expr newBVXorExpr(const Expr& t1, const Expr& t2) = 0;
658  virtual Expr newBVXorExpr(const std::vector<Expr>& kids) = 0;
659 
660  virtual Expr newBVXnorExpr(const Expr& t1, const Expr& t2) = 0;
661  virtual Expr newBVXnorExpr(const std::vector<Expr>& kids) = 0;
662 
663  virtual Expr newBVNandExpr(const Expr& t1, const Expr& t2) = 0;
664  virtual Expr newBVNorExpr(const Expr& t1, const Expr& t2) = 0;
665  virtual Expr newBVCompExpr(const Expr& t1, const Expr& t2) = 0;
666 
667  // Unsigned bitvector inequalities
668  virtual Expr newBVLTExpr(const Expr& t1, const Expr& t2) = 0;
669  virtual Expr newBVLEExpr(const Expr& t1, const Expr& t2) = 0;
670 
671  // Signed bitvector inequalities
672  virtual Expr newBVSLTExpr(const Expr& t1, const Expr& t2) = 0;
673  virtual Expr newBVSLEExpr(const Expr& t1, const Expr& t2) = 0;
674 
675  // Sign-extend t1 to a total of len bits
676  virtual Expr newSXExpr(const Expr& t1, int len) = 0;
677 
678  // Bitvector arithmetic: unary minus, plus, subtract, multiply
679  virtual Expr newBVUminusExpr(const Expr& t1) = 0;
680  virtual Expr newBVSubExpr(const Expr& t1, const Expr& t2) = 0;
681  //! 'numbits' is the number of bits in the result
682  virtual Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k) = 0;
683  virtual Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) = 0;
684  virtual Expr newBVMultExpr(int numbits,
685  const Expr& t1, const Expr& t2) = 0;
686 
687  virtual Expr newBVUDivExpr(const Expr& t1, const Expr& t2) = 0;
688  virtual Expr newBVURemExpr(const Expr& t1, const Expr& t2) = 0;
689  virtual Expr newBVSDivExpr(const Expr& t1, const Expr& t2) = 0;
690  virtual Expr newBVSRemExpr(const Expr& t1, const Expr& t2) = 0;
691  virtual Expr newBVSModExpr(const Expr& t1, const Expr& t2) = 0;
692 
693  // Left shift by r bits: result is old size + r bits
694  virtual Expr newFixedLeftShiftExpr(const Expr& t1, int r) = 0;
695  // Left shift by r bits: result is same size as t1
696  virtual Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) = 0;
697  // Logical right shift by r bits: result is same size as t1
698  virtual Expr newFixedRightShiftExpr(const Expr& t1, int r) = 0;
699  // Left shift with shift parameter an arbitrary bit-vector expr
700  virtual Expr newBVSHL(const Expr& t1, const Expr& t2) = 0;
701  // Logical right shift with shift parameter an arbitrary bit-vector expr
702  virtual Expr newBVLSHR(const Expr& t1, const Expr& t2) = 0;
703  // Arithmetic right shift with shift parameter an arbitrary bit-vector expr
704  virtual Expr newBVASHR(const Expr& t1, const Expr& t2) = 0;
705  // Get value of BV Constant
706  virtual Rational computeBVConst(const Expr& e) = 0;
707 
708  /*@}*/ // End of Bitvector expression methods
709 
710  /***************************************************************************/
711  /*!
712  *\name Other expression methods
713  * Methods for manipulating other kinds of expressions
714  *@{
715  */
716  /***************************************************************************/
717 
718  //! Tuple expression
719  virtual Expr tupleExpr(const std::vector<Expr>& exprs) = 0;
720 
721  //! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
722  virtual Expr tupleSelectExpr(const Expr& tuple, int index) = 0;
723 
724  //! Tuple update; equivalent to "tuple WITH index := newValue"
725  virtual Expr tupleUpdateExpr(const Expr& tuple, int index,
726  const Expr& newValue) = 0;
727 
728  //! Datatype constructor expression
729  virtual Expr datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) = 0;
730 
731  //! Datatype selector expression
732  virtual Expr datatypeSelExpr(const std::string& selector, const Expr& arg) = 0;
733 
734  //! Datatype tester expression
735  virtual Expr datatypeTestExpr(const std::string& constructor, const Expr& arg) = 0;
736 
737  //! Create a bound variable with a given name, unique ID (uid) and type
738  /*!
739  \param name is the name of the variable
740  \param uid is the unique ID (a string), which must be unique for
741  each variable
742  \param type is its type. The type cannot be a function type.
743  \return an Expr representation of a new variable
744  */
745  virtual Expr boundVarExpr(const std::string& name,
746  const std::string& uid,
747  const Type& type) = 0;
748 
749  //! Universal quantifier
750  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body) = 0;
751  //! Universal quantifier with a trigger
752  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
753  const Expr& trigger) = 0;
754  //! Universal quantifier with a set of triggers.
755  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
756  const std::vector<Expr>& triggers) = 0;
757  //! Universal quantifier with a set of multi-triggers.
758  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
759  const std::vector<std::vector<Expr> >& triggers) = 0;
760 
761  //! Set triggers for quantifier instantiation
762  /*!
763  * \param e the expression for which triggers are being set.
764  * \param triggers Each item in triggers is a vector of Expr containing one
765  * or more patterns. A pattern is a term or Atomic predicate sub-expression
766  * of e. A vector containing more than one pattern is treated as a
767  * multi-trigger. Patterns will be matched in the order they occur in
768  * the vector.
769  */
770  virtual void setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers) = 0;
771  //! Set triggers for quantifier instantiation (no multi-triggers)
772  virtual void setTriggers(const Expr& e, const std::vector<Expr>& triggers) = 0;
773  //! Set a single trigger for quantifier instantiation
774  virtual void setTrigger(const Expr& e, const Expr& trigger) = 0;
775  //! Set a single multi-trigger for quantifier instantiation
776  virtual void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger) = 0;
777 
778  //! Existential quantifier
779  virtual Expr existsExpr(const std::vector<Expr>& vars, const Expr& body) = 0;
780 
781  //! Lambda-expression
782  virtual Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body) = 0;
783 
784  //! Transitive closure of a binary predicate
785  virtual Op transClosure(const Op& op) = 0;
786 
787  //! Symbolic simulation expression
788  /*!
789  * \param f is the next state function (LAMBDA-expression)
790  * \param s0 is the initial state
791  * \param inputs is the vector of LAMBDA-expressions representing
792  * the sequences of inputs to f
793  * \param n is a constant, the number of cycles to run the simulation.
794  */
795  virtual Expr simulateExpr(const Expr& f, const Expr& s0,
796  const std::vector<Expr>& inputs,
797  const Expr& n) = 0;
798 
799  /*@}*/ // End of Other expression methods
800 
801  /***************************************************************************/
802  /*!
803  *\name Validity checking methods
804  * Methods related to validity checking
805  *
806  * This group includes methods for asserting formulas, checking
807  * validity in the given logical context, manipulating the scope
808  * level of the context, etc.
809  *@{
810  */
811  /***************************************************************************/
812 
813  //! Set the resource limit (0==unlimited, 1==exhausted).
814  /*! Currently, the limit is the total number of processed facts. */
815  virtual void setResourceLimit(unsigned limit) = 0;
816 
817  //! Set a time limit in tenth of a second,
818  /*! counting the cpu time used by the current process from now on.
819  * Currently, when the limit is reached, cvc3 tries to quickly
820  * terminate, probably with the status unknown.
821  */
822  virtual void setTimeLimit(unsigned limit) = 0;
823 
824  //! Assert a new formula in the current context.
825  /*! This creates the assumption e |- e. The formula must have Boolean type.
826  */
827  virtual void assertFormula(const Expr& e) = 0;
828 
829  //! Register an atomic formula of interest.
830  /*! Registered atoms are tracked by the decision procedures. If one of them
831  is deduced to be true or false, it is added to a list of implied literals.
832  Implied literals can be retrieved with the getImpliedLiteral function */
833  virtual void registerAtom(const Expr& e) = 0;
834 
835  //! Return next literal implied by last assertion. Null Expr if none.
836  /*! Returned literals are either registered atomic formulas or their negation
837  */
838  virtual Expr getImpliedLiteral() = 0;
839 
840  //! Simplify e with respect to the current context
841  virtual Expr simplify(const Expr& e) = 0;
842 
843  //! Check validity of e in the current context.
844  /*! If it returns VALID, the scope and context are the same
845  * as when called. If it returns INVALID, the context will be one which
846  * falsifies the query. If it returns UNKNOWN, the context will falsify the
847  * query, but the context may be inconsistent. Finally, if it returns
848  * ABORT, the context will be one which satisfies as much as possible.
849  *
850  * \param e is the queried formula
851  */
852  virtual QueryResult query(const Expr& e) = 0;
853 
854  //! Check satisfiability of the expr in the current context.
855  /*! Equivalent to query(!e) */
856  virtual QueryResult checkUnsat(const Expr& e) = 0;
857 
858  //! Get the next model
859  /*! This method should only be called after a query which returns
860  INVALID. Its return values are as for query(). */
861  virtual QueryResult checkContinue() = 0;
862 
863  //! Restart the most recent query with e as an additional assertion.
864  /*! This method should only be called after a query which returns
865  INVALID. Its return values are as for query(). */
866  virtual QueryResult restart(const Expr& e) = 0;
867 
868  //! Returns to context immediately before last invalid query.
869  /*! This method should only be called after a query which returns false.
870  */
871  virtual void returnFromCheck() = 0;
872 
873  //! Get assumptions made by the user in this and all previous contexts.
874  /*! User assumptions are created either by calls to assertFormula or by a
875  * call to query. In the latter case, the negated query is added as an
876  * assumption.
877  * \param assumptions should be empty on entry.
878  */
879  virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0;
880 
881  //! Get assumptions made internally in this and all previous contexts.
882  /*! Internal assumptions are literals assumed by the sat solver.
883  * \param assumptions should be empty on entry.
884  */
885  virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0;
886 
887  //! Get all assumptions made in this and all previous contexts.
888  /*! \param assumptions should be empty on entry.
889  */
890  virtual void getAssumptions(std::vector<Expr>& assumptions) = 0;
891 
892  //! Returns the set of assumptions used in the proof of queried formula.
893  /*! It returns a subset of getAssumptions(). If the last query was false
894  * or there has not yet been a query, it does nothing.
895  * NOTE: this functionality is not supported yet
896  * \param assumptions should be empty on entry.
897  */
898  virtual void getAssumptionsUsed(std::vector<Expr>& assumptions) = 0;
899 
900  virtual Expr getProofQuery() = 0;
901 
902 
903  //! Return the internal assumptions that make the queried formula false.
904  /*! This method should only be called after a query which returns
905  false. It will try to return the simplest possible subset of
906  the internal assumptions sufficient to make the queried expression
907  false.
908  \param assumptions should be empty on entry.
909  \param inOrder if true, returns the assumptions in the order they
910  were made. This is slightly more expensive than inOrder = false.
911  */
912  virtual void getCounterExample(std::vector<Expr>& assumptions,
913  bool inOrder=true) = 0;
914 
915  //! Will assign concrete values to all user created variables
916  /*! This function should only be called after a query which return false.
917  */
918  virtual void getConcreteModel(ExprMap<Expr> & m) = 0;
919 
920  //! If the result of the last query was UNKNOWN try to actually build the model
921  //! to verify the result.
922  /*! This function should only be called after a query which return unknown.
923  */
924  virtual QueryResult tryModelGeneration() = 0;
925 
926  //:ALEX: returns the current truth value of a formula
927  // returns UNKNOWN_VAL if e is not associated
928  // with a boolean variable in the SAT module,
929  // i.e. if its value can not determined without search.
930  virtual FormulaValue value(const Expr& e) = 0;
931 
932  //! Returns true if the current context is inconsistent.
933  /*! Also returns a minimal set of assertions used to determine the
934  inconsistency.
935  \param assumptions should be empty on entry.
936  */
937  virtual bool inconsistent(std::vector<Expr>& assumptions) = 0;
938 
939  //! Returns true if the current context is inconsistent.
940  virtual bool inconsistent() = 0;
941 
942  //! Returns true if the invalid result from last query() is imprecise
943  /*!
944  * Some decision procedures in CVC are incomplete (quantifier
945  * elimination, non-linear arithmetic, etc.). If any incomplete
946  * features were used during the last query(), and the result is
947  * "invalid" (query() returns false), then this result is
948  * inconclusive. It means that the system gave up the search for
949  * contradiction at some point.
950  */
951  virtual bool incomplete() = 0;
952 
953  //! Returns true if the invalid result from last query() is imprecise
954  /*!
955  * \sa incomplete()
956  *
957  * The argument is filled with the reasons for incompleteness (they
958  * are intended to be shown to the end user).
959  */
960  virtual bool incomplete(std::vector<std::string>& reasons) = 0;
961 
962  //! Returns the proof term for the last proven query
963  /*! If there has not been a successful query, it should return a NULL proof
964  */
965  virtual Proof getProof() = 0;
966 
967  //! Evaluate an expression and return a concrete value in the model
968  /*! If the last query was not invalid, should return NULL expr */
969  virtual Expr getValue(Expr e) = 0;
970 
971  //! Returns the list of pairs (name value) for each :named attribute.
972  /*! If the last query was not invalid, should return NULL expr */
973  virtual Expr getAssignment() = 0;
974 
975  //! Returns the TCC of the last assumption or query
976  /*! Returns Null if no assumptions or queries were performed. */
977  virtual Expr getTCC() = 0;
978 
979  //! Return the set of assumptions used in the proof of the last TCC
980  virtual void getAssumptionsTCC(std::vector<Expr>& assumptions) = 0;
981 
982  //! Returns the proof of TCC of the last assumption or query
983  /*! Returns Null if no assumptions or queries were performed. */
984  virtual Proof getProofTCC() = 0;
985 
986  //! After successful query, return its closure |- Gamma => phi
987  /*! Turn a valid query Gamma |- phi into an implication
988  * |- Gamma => phi.
989  *
990  * Returns Null if last query was invalid.
991  */
992  virtual Expr getClosure() = 0;
993 
994  //! Construct a proof of the query closure |- Gamma => phi
995  /*! Returns Null if last query was Invalid. */
996  virtual Proof getProofClosure() = 0;
997 
998  /*@}*/ // End of Validity checking methods
999 
1000  /***************************************************************************/
1001  /*!
1002  *\name Context methods
1003  * Methods for manipulating contexts
1004  *
1005  * Contexts support stack-based push and pop. There are two
1006  * separate notions of the current context stack. stackLevel(), push(),
1007  * pop(), and popto() work with the user-level notion of the stack.
1008  *
1009  * scopeLevel(), pushScope(), popScope(), and poptoScope() work with
1010  * the internal stack which is more fine-grained than the user
1011  * stack.
1012  *
1013  * Do not use the scope methods unless you know what you are doing.
1014  * *@{
1015  */
1016  /***************************************************************************/
1017 
1018  //! Returns the current stack level. Initial level is 0.
1019  virtual int stackLevel() = 0;
1020 
1021  //! Checkpoint the current context and increase the scope level
1022  virtual void push() = 0;
1023 
1024  //! Restore the current context to its state at the last checkpoint
1025  virtual void pop() = 0;
1026 
1027  //! Restore the current context to the given stackLevel.
1028  /*!
1029  \param stackLevel should be greater than or equal to 0 and less
1030  than or equal to the current scope level.
1031  */
1032  virtual void popto(int stackLevel) = 0;
1033 
1034  //! Returns the current scope level. Initially, the scope level is 1.
1035  virtual int scopeLevel() = 0;
1036 
1037  /*! @brief Checkpoint the current context and increase the
1038  * <strong>internal</strong> scope level. Do not use unless you
1039  * know what you're doing!
1040  */
1041  virtual void pushScope() = 0;
1042 
1043  /*! @brief Restore the current context to its state at the last
1044  * <strong>internal</strong> checkpoint. Do not use unless you know
1045  * what you're doing!
1046  */
1047  virtual void popScope() = 0;
1048 
1049  //! Restore the current context to the given scopeLevel.
1050  /*!
1051  \param scopeLevel should be less than or equal to the current scope level.
1052 
1053  If scopeLevel is less than 1, then the current context is reset
1054  and the scope level is set to 1.
1055  */
1056  virtual void poptoScope(int scopeLevel) = 0;
1057 
1058  //! Get the current context
1059  virtual Context* getCurrentContext() = 0;
1060 
1061  //! Destroy and recreate validity checker: resets everything except for flags
1062  virtual void reset() = 0;
1063 
1064  //! Add an annotation to the current script - prints annot when translating
1065  virtual void logAnnotation(const Expr& annot) = 0;
1066 
1067  /*@}*/ // End of Context methods
1068 
1069  /***************************************************************************/
1070  /*!
1071  *\name Reading files
1072  * Methods for reading external files
1073  *@{
1074  */
1075  /***************************************************************************/
1076 
1077  //! Read and execute the commands from a file given by name ("" means stdin)
1078  virtual void loadFile(const std::string& fileName,
1080  bool interactive = false,
1081  bool calledFromParser = false) = 0;
1082 
1083  //! Read and execute the commands from a stream
1084  virtual void loadFile(std::istream& is,
1086  bool interactive = false) = 0;
1087 
1088  /*@}*/ // End of methods for reading files
1089 
1090  /***************************************************************************/
1091  /*!
1092  *\name Reporting Statistics
1093  * Methods for collecting and reporting run-time statistics
1094  *@{
1095  */
1096  /***************************************************************************/
1097 
1098  //! Get statistics object
1099  virtual Statistics& getStatistics() = 0;
1100 
1101  //! Print collected statistics to stdout
1102  virtual void printStatistics() = 0;
1103 
1104  /*@}*/ // End of Statistics Methods
1105 
1106 
1107 }; // End of class ValidityChecker
1108 
1109 } // End of namespace CVC3
1110 
1111 #endif