cvc4-1.4
cvc3_compat.h
Go to the documentation of this file.
1 /********************* */
28 #include "cvc4_public.h"
29 
30 #ifndef __CVC4__CVC3_COMPAT_H
31 #define __CVC4__CVC3_COMPAT_H
32 
33 // keep the CVC3 include guard also
34 #if defined(_cvc3__include__vc_h_) || \
35  defined(_cvc3__expr_h_) || \
36  defined(_cvc3__command_line_flags_h_) || \
37  defined(_cvc3__include__queryresult_h_) || \
38  defined(_cvc3__include__formula_value_h_)
39 
40 #error "A CVC3 header file was included before CVC4's cvc3_compat.h header. Please include cvc3_compat.h rather than any CVC3 headers."
41 
42 #else
43 
44 // define these so the files are skipped if the user #includes them too
45 #define _cvc3__expr_h_
46 #define _cvc3__include__vc_h_
47 #define _cvc3__command_line_flags_h_
48 #define _cvc3__include__queryresult_h_
49 #define _cvc3__include__formula_value_h_
50 
51 #include "expr/expr_manager.h"
52 #include "expr/expr.h"
53 #include "expr/type.h"
54 
55 #include "smt/smt_engine.h"
56 
57 #include "util/rational.h"
58 #include "util/integer.h"
59 
60 #include "util/exception.h"
61 #include "util/hash.h"
62 
63 #include "parser/parser.h"
64 
65 #include <stdlib.h>
66 #include <map>
67 #include <utility>
68 
69 //class CInterface;
70 
71 namespace CVC3 {
72 
86 
87 std::string int2string(int n) CVC4_PUBLIC;
88 
90 typedef enum CVC4_PUBLIC {
96 } CLFlagType;
97 
98 std::ostream& operator<<(std::ostream& out, CLFlagType clft) CVC4_PUBLIC;
99 
110 class CVC4_PUBLIC CLFlag {
112  CLFlagType d_tp;
114  union {
115  bool b;
116  int i;
117  std::string* s;
118  std::vector<std::pair<std::string,bool> >* sv;
119  } d_data;
120 
121 public:
122 
124  CLFlag(bool b, const std::string& help, bool display = true);
126  CLFlag(int i, const std::string& help, bool display = true);
128  CLFlag(const std::string& s, const std::string& help, bool display = true);
130  CLFlag(const char* s, const std::string& help, bool display = true);
132  CLFlag(const std::vector<std::pair<std::string,bool> >& sv,
133  const std::string& help, bool display = true);
135  CLFlag();
137  CLFlag(const CLFlag& f);
139  ~CLFlag();
140 
142  CLFlag& operator=(const CLFlag& f);
144 
145  CLFlag& operator=(bool b);
147 
148  CLFlag& operator=(int i);
150 
151  CLFlag& operator=(const std::string& s);
153 
154  CLFlag& operator=(const char* s);
156 
158  CLFlag& operator=(const std::pair<std::string,bool>& p);
160 
161  CLFlag& operator=(const std::vector<std::pair<std::string,bool> >& sv);
162 
163  // Accessor methods
165  CLFlagType getType() const;
168  bool modified() const;
170  bool display() const;
171 
172  // The value accessors return a reference. For the system-wide
173  // flags, this reference will remain valid throughout the run of the
174  // program, even if the flag's value changes. So, the reference can
175  // be cached, and the value can be checked directly (which is more
176  // efficient).
177  const bool& getBool() const;
178 
179  const int& getInt() const;
180 
181  const std::string& getString() const;
182 
183  const std::vector<std::pair<std::string,bool> >& getStrVec() const;
184 
185  const std::string& getHelp() const;
186 
187 };/* class CLFlag */
188 
190 // Class CLFlag (for Command Line Flag)
191 //
192 // Author: Sergey Berezin
193 // Date: Fri May 30 14:10:48 2003
194 //
195 // Database of command line flags.
197 
198 class CVC4_PUBLIC CLFlags {
199  typedef std::map<std::string, CLFlag> FlagMap;
200  FlagMap d_map;
201 
202 public:
203  // Public methods
204  // Add a new flag. The name must be a complete flag name.
205  void addFlag(const std::string& name, const CLFlag& f);
206  // Count how many flags match the name prefix
207  size_t countFlags(const std::string& name) const;
208  // Match the name prefix and add all the matching names to the vector
209  size_t countFlags(const std::string& name,
210  std::vector<std::string>& names) const;
211  // Retrieve an existing flag. The 'name' must be a full name of an
212  // existing flag.
213  const CLFlag& getFlag(const std::string& name) const;
214 
215  const CLFlag& operator[](const std::string& name) const;
216 
217  // Setting the flag to a new value, but preserving the help string.
218  // The 'name' prefix must uniquely resolve to an existing flag.
219  void setFlag(const std::string& name, const CLFlag& f);
220 
221  // Variants of setFlag for all the types
222  void setFlag(const std::string& name, bool b);
223  void setFlag(const std::string& name, int i);
224  void setFlag(const std::string& name, const std::string& s);
225  void setFlag(const std::string& name, const char* s);
226  void setFlag(const std::string& name, const std::pair<std::string, bool>& p);
227  void setFlag(const std::string& name,
228  const std::vector<std::pair<std::string, bool> >& sv);
229 
230 };/* class CLFlags */
231 
232 class CVC4_PUBLIC ExprManager;
233 class CVC4_PUBLIC Context;
234 class CVC4_PUBLIC Proof {};
235 class CVC4_PUBLIC Theorem {};
236 
237 using CVC4::InputLanguage;
238 using CVC4::Integer;
239 using CVC4::Rational;
240 using CVC4::Exception;
241 using CVC4::Cardinality;
242 using namespace CVC4::kind;
243 
244 typedef size_t ExprIndex;
246 typedef size_t Unsigned;
247 
248 static const int READ = ::CVC4::kind::SELECT;
249 static const int WRITE = ::CVC4::kind::STORE;
250 
251 // CVC4 has a more sophisticated Cardinality type;
252 // but we can support comparison against CVC3's more
253 // coarse-grained Cardinality.
254 enum CVC4_PUBLIC CVC3CardinalityKind {
258 };/* enum CVC3CardinalityKind */
259 
260 std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c) CVC4_PUBLIC;
261 
266 
267 class CVC4_PUBLIC Expr;
268 
269 template <class T>
270 class CVC4_PUBLIC ExprMap : public std::map<Expr, T> {
271 };/* class ExprMap<T> */
272 
273 template <class T>
274 class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
275 public:
276  void insert(Expr a, Expr b);
277 };/* class ExprHashMap<T> */
278 
279 class CVC4_PUBLIC Type : public CVC4::Type {
280 public:
281  Type();
282  Type(const CVC4::Type& type);
283  Type(const Type& type);
284  Expr getExpr() const;
285 
286  // Reasoning about children
287  int arity() const;
288  Type operator[](int i) const;
289 
290  // Core testers
291  bool isBool() const;
292  bool isSubtype() const;
294  Cardinality card() const;
296 
298  Expr enumerateFinite(Unsigned n) const;
300  Unsigned sizeFinite() const;
301 
302  // Core constructors
303  static Type typeBool(ExprManager* em);
304  static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
305  Type funType(const Type& typeRan) const;
306 
307 };/* class CVC3::Type */
308 
309 class CVC4_PUBLIC Expr;
310 typedef Expr Op;
311 
319 class CVC4_PUBLIC Expr : public CVC4::Expr {
320 public:
322 
323  Expr();
324  Expr(const Expr& e);
325  Expr(const CVC4::Expr& e);
326  Expr(CVC4::Kind k);
327 
328  // Compound expression constructors
329  Expr eqExpr(const Expr& right) const;
330  Expr notExpr() const;
331  Expr negate() const; // avoid double-negatives
332  Expr andExpr(const Expr& right) const;
333  Expr orExpr(const Expr& right) const;
334  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
335  Expr iffExpr(const Expr& right) const;
336  Expr impExpr(const Expr& right) const;
337  Expr xorExpr(const Expr& right) const;
338 
339  Expr substExpr(const std::vector<Expr>& oldTerms,
340  const std::vector<Expr>& newTerms) const;
341  Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
342 
343  Expr operator!() const;
344  Expr operator&&(const Expr& right) const;
345  Expr operator||(const Expr& right) const;
346 
347  static size_t hash(const Expr& e);
348 
349  size_t hash() const;
350 
351  // Core expression testers
352 
353  bool isFalse() const;
354  bool isTrue() const;
355  bool isBoolConst() const;
356  bool isVar() const;
357  bool isBoundVar() const;
358  bool isString() const;
359  bool isSymbol() const;
360  bool isTerm() const;
361  bool isType() const;
362  bool isClosure() const;
363  bool isQuantifier() const;
364  bool isForall() const;
365  bool isExists() const;
366  bool isLambda() const;
367  bool isApply() const;
368  bool isTheorem() const;
369  bool isConstant() const;
370  bool isRawList() const;
371 
372  bool isAtomic() const;
373  bool isAtomicFormula() const;
374  bool isAbsAtomicFormula() const;
375  bool isLiteral() const;
376  bool isAbsLiteral() const;
377  bool isBoolConnective() const;
378  bool isPropLiteral() const;
379  bool isPropAtom() const;
380 
381  std::string getName() const;
382  std::string getUid() const;
383 
384  std::string getString() const;
385  std::vector<Expr> getVars() const;
386  Expr getExistential() const;
387  int getBoundIndex() const;
388  Expr getBody() const;
389  Theorem getTheorem() const;
390 
391  bool isEq() const;
392  bool isNot() const;
393  bool isAnd() const;
394  bool isOr() const;
395  bool isITE() const;
396  bool isIff() const;
397  bool isImpl() const;
398  bool isXor() const;
399 
400  bool isRational() const;
401  bool isSkolem() const;
402 
403  const Rational& getRational() const;
404 
405  Op mkOp() const;
406  Op getOp() const;
407  Expr getOpExpr() const;
408  int getOpKind() const;
409  Expr getExpr() const;// since people are used to doing getOp().getExpr() in CVC3
410 
412  std::vector< std::vector<Expr> > getTriggers() const;
413 
414  // Get the expression manager. The expression must be non-null.
415  ExprManager* getEM() const;
416 
417  // Return a ref to the vector of children.
418  std::vector<Expr> getKids() const;
419 
420  // Get the index field
421  ExprIndex getIndex() const;
422 
423  // Return the number of children. Note, that an application of a
424  // user-defined function has the arity of that function (the number
425  // of arguments), and the function name itself is part of the
426  // operator.
427  int arity() const;
428 
429  // Return the ith child. As with arity, it's also the ith argument
430  // in function application.
431  Expr operator[](int i) const;
432 
434  Expr unnegate() const;
435 
436  // Check if Expr is not Null
437  bool isInitialized() const;
438 
440  Type getType() const;
442  Type lookupType() const;
443 
445  void pprint() const;
447  void pprintnodag() const;
448 
449 };/* class CVC3::Expr */
450 
451 bool isArrayLiteral(const Expr&) CVC4_PUBLIC;
452 
453 class CVC4_PUBLIC ExprManager : public CVC4::ExprManager {
454 public:
455  std::string getKindName(int kind);
457  InputLanguage getInputLang() const;
459  InputLanguage getOutputLang() const;
460 };/* class CVC3::ExprManager */
461 
463 
464 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
465 #define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB_V1
466 #define SMTLIB_V2_LANG ::CVC4::language::input::LANG_SMTLIB_V2
467 #define TPTP_LANG ::CVC4::language::input::LANG_TPTP
468 #define AST_LANG ::CVC4::language::input::LANG_AST
469 
470 /*****************************************************************************/
471 /*
472  * Type for result of queries. VALID and UNSATISFIABLE are treated as
473  * equivalent, as are SATISFIABLE and INVALID.
474  */
475 /*****************************************************************************/
476 typedef enum CVC4_PUBLIC QueryResult {
478  INVALID = 0,
479  VALID = 1,
483 } QueryResult;
484 
485 std::ostream& operator<<(std::ostream& out, QueryResult qr);
486 std::string QueryResultToString(QueryResult query_result);
487 
488 /*****************************************************************************/
489 /*
490  * Type for truth value of formulas.
491  */
492 /*****************************************************************************/
493 typedef enum CVC4_PUBLIC FormulaValue {
497 } FormulaValue;
498 
499 std::ostream& operator<<(std::ostream& out, FormulaValue fv) CVC4_PUBLIC;
500 
501 /*****************************************************************************/
513 /*****************************************************************************/
514 class CVC4_PUBLIC ValidityChecker {
515 
516  CLFlags* d_clflags;
517  CVC4::Options d_options;
518  CVC3::ExprManager* d_em;
519  std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
520  std::set<ValidityChecker*> d_reverseEmmc;
521  CVC4::SmtEngine* d_smt;
522  CVC4::parser::Parser* d_parserContext;
523  std::vector<Expr> d_exprTypeMapRemove;
524  unsigned d_stackLevel;
525 
526  friend class Type; // to reach in to d_exprTypeMapRemove
527 
528  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
529  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
530 
531  ConstructorMap d_constructors;
532  SelectorMap d_selectors;
533 
534  ValidityChecker(const CLFlags& clflags);
535 
536  void setUpOptions(CVC4::Options& options, const CLFlags& clflags);
537 
538  // helper function for bitvectors
539  Expr bvpad(int len, const Expr& e);
540 
541 public:
543  ValidityChecker();
545  virtual ~ValidityChecker();
546 
548 
554  virtual CLFlags& getFlags() const;
556  virtual void reprocessFlags();
557 
558  /***************************************************************************/
559  /*
560  * Static methods
561  */
562  /***************************************************************************/
563 
565 
568  static CLFlags createFlags();
570 
573  static ValidityChecker* create(const CLFlags& flags);
575  static ValidityChecker* create();
576 
577  /***************************************************************************/
584  /***************************************************************************/
585 
586  // Basic types
587  virtual Type boolType();
588 
589  virtual Type realType();
590 
591  virtual Type intType();
592 
594 
597  virtual Type subrangeType(const Expr& l, const Expr& r);
598 
600 
609  virtual Type subtypeType(const Expr& pred, const Expr& witness);
610 
611  // Tuple types
613  virtual Type tupleType(const Type& type0, const Type& type1);
614 
616  virtual Type tupleType(const Type& type0, const Type& type1,
617  const Type& type2);
619  virtual Type tupleType(const std::vector<Type>& types);
620 
621  // Record types
623  virtual Type recordType(const std::string& field, const Type& type);
624 
626 
627  virtual Type recordType(const std::string& field0, const Type& type0,
628  const std::string& field1, const Type& type1);
630 
631  virtual Type recordType(const std::string& field0, const Type& type0,
632  const std::string& field1, const Type& type1,
633  const std::string& field2, const Type& type2);
635 
636  virtual Type recordType(const std::vector<std::string>& fields,
637  const std::vector<Type>& types);
638 
639  // Datatypes
640 
642 
645  virtual Type dataType(const std::string& name,
646  const std::string& constructor,
647  const std::vector<std::string>& selectors,
648  const std::vector<Expr>& types);
649 
651 
654  virtual Type dataType(const std::string& name,
655  const std::vector<std::string>& constructors,
656  const std::vector<std::vector<std::string> >& selectors,
657  const std::vector<std::vector<Expr> >& types);
658 
660 
663  virtual void dataType(const std::vector<std::string>& names,
664  const std::vector<std::vector<std::string> >& constructors,
665  const std::vector<std::vector<std::vector<std::string> > >& selectors,
666  const std::vector<std::vector<std::vector<Expr> > >& types,
667  std::vector<Type>& returnTypes);
668 
670  virtual Type arrayType(const Type& typeIndex, const Type& typeData);
671 
673  virtual Type bitvecType(int n);
674 
676  virtual Type funType(const Type& typeDom, const Type& typeRan);
677 
679  virtual Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
680 
682  virtual Type createType(const std::string& typeName);
683 
685  virtual Type createType(const std::string& typeName, const Type& def);
686 
688  virtual Type lookupType(const std::string& typeName);
689  // End of Type-related methods
691 
692  /***************************************************************************/
699  /***************************************************************************/
700 
702  virtual ExprManager* getEM();
703 
705 
710  virtual Expr varExpr(const std::string& name, const Type& type);
711 
713  virtual Expr varExpr(const std::string& name, const Type& type,
714  const Expr& def);
715 
717 
724  virtual Expr lookupVar(const std::string& name, Type* type);
725 
727  virtual Type getType(const Expr& e);
728 
730  virtual Type getBaseType(const Expr& e);
731 
733  virtual Type getBaseType(const Type& t);
734 
736  virtual Expr getTypePred(const Type&t, const Expr& e);
737 
739  virtual Expr stringExpr(const std::string& str);
740 
742  virtual Expr idExpr(const std::string& name);
743 
745 
765  virtual Expr listExpr(const std::vector<Expr>& kids);
766 
768  virtual Expr listExpr(const Expr& e1);
769 
771  virtual Expr listExpr(const Expr& e1, const Expr& e2);
772 
774  virtual Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
775 
777  virtual Expr listExpr(const std::string& op,
778  const std::vector<Expr>& kids);
779 
781  virtual Expr listExpr(const std::string& op, const Expr& e1);
782 
784  virtual Expr listExpr(const std::string& op, const Expr& e1,
785  const Expr& e2);
786 
788  virtual Expr listExpr(const std::string& op, const Expr& e1,
789  const Expr& e2, const Expr& e3);
790 
792  virtual void printExpr(const Expr& e);
793 
795  virtual void printExpr(const Expr& e, std::ostream& os);
796 
798  virtual Expr parseExpr(const Expr& e);
799 
801  virtual Type parseType(const Expr& e);
802 
804 
811  virtual Expr importExpr(const Expr& e);
812 
814 
815  virtual Type importType(const Type& t);
816 
818  virtual void cmdsFromString(const std::string& s,
820 
822 
825  virtual Expr exprFromString(const std::string& e,
827  // End of General Expr Methods
829 
830  /***************************************************************************/
839  /***************************************************************************/
840 
842  virtual Expr trueExpr();
843 
845  virtual Expr falseExpr();
846 
848  virtual Expr notExpr(const Expr& child);
849 
851  virtual Expr andExpr(const Expr& left, const Expr& right);
852 
854  virtual Expr andExpr(const std::vector<Expr>& children);
855 
857  virtual Expr orExpr(const Expr& left, const Expr& right);
858 
860  virtual Expr orExpr(const std::vector<Expr>& children);
861 
863  virtual Expr impliesExpr(const Expr& hyp, const Expr& conc);
864 
866  virtual Expr iffExpr(const Expr& left, const Expr& right);
867 
869 
873  virtual Expr eqExpr(const Expr& child0, const Expr& child1);
874 
876 
881  virtual Expr iteExpr(const Expr& ifpart, const Expr& thenpart,
882  const Expr& elsepart);
883 
888  virtual Expr distinctExpr(const std::vector<Expr>& children);
889  // End of Core expression methods
891 
892  /***************************************************************************/
898  /***************************************************************************/
899 
901 
905  virtual Op createOp(const std::string& name, const Type& type);
906 
908  virtual Op createOp(const std::string& name, const Type& type,
909  const Expr& def);
910 
912 
919  virtual Op lookupOp(const std::string& name, Type* type);
920 
922  virtual Expr funExpr(const Op& op, const Expr& child);
923 
925  virtual Expr funExpr(const Op& op, const Expr& left, const Expr& right);
926 
928  virtual Expr funExpr(const Op& op, const Expr& child0,
929  const Expr& child1, const Expr& child2);
930 
932  virtual Expr funExpr(const Op& op, const std::vector<Expr>& children);
933  // End of User-defined (uninterpreted) function methods
935 
936  /***************************************************************************/
945  /***************************************************************************/
946 
953  virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
954 
956 
960  virtual Expr ratExpr(int n, int d = 1);
961 
963 
967  virtual Expr ratExpr(const std::string& n, const std::string& d, int base);
968 
970 
975  virtual Expr ratExpr(const std::string& n, int base = 10);
976 
978  virtual Expr uminusExpr(const Expr& child);
979 
981  virtual Expr plusExpr(const Expr& left, const Expr& right);
982 
984  virtual Expr plusExpr(const std::vector<Expr>& children);
985 
987  virtual Expr minusExpr(const Expr& left, const Expr& right);
988 
990  virtual Expr multExpr(const Expr& left, const Expr& right);
991 
993  virtual Expr powExpr(const Expr& x, const Expr& n);
994 
996  virtual Expr divideExpr(const Expr& numerator, const Expr& denominator);
997 
999  virtual Expr ltExpr(const Expr& left, const Expr& right);
1000 
1002  virtual Expr leExpr(const Expr& left, const Expr& right);
1003 
1005  virtual Expr gtExpr(const Expr& left, const Expr& right);
1006 
1008  virtual Expr geExpr(const Expr& left, const Expr& right);
1009  // End of Arithmetic expression methods
1011 
1012  /***************************************************************************/
1018  /***************************************************************************/
1019 
1021 
1022  virtual Expr recordExpr(const std::string& field, const Expr& expr);
1023 
1025 
1026  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
1027  const std::string& field1, const Expr& expr1);
1028 
1030 
1031  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
1032  const std::string& field1, const Expr& expr1,
1033  const std::string& field2, const Expr& expr2);
1034 
1036 
1042  virtual Expr recordExpr(const std::vector<std::string>& fields,
1043  const std::vector<Expr>& exprs);
1044 
1046 
1048  virtual Expr recSelectExpr(const Expr& record, const std::string& field);
1049 
1051 
1055  virtual Expr recUpdateExpr(const Expr& record, const std::string& field,
1056  const Expr& newValue);
1057  // End of Record expression methods
1059 
1060  /***************************************************************************/
1066  /***************************************************************************/
1067 
1069 
1070  virtual Expr readExpr(const Expr& array, const Expr& index);
1071 
1073  virtual Expr writeExpr(const Expr& array, const Expr& index,
1074  const Expr& newValue);
1075  // End of Array expression methods
1077 
1078  /***************************************************************************/
1084  /***************************************************************************/
1085 
1086  // Bitvector constants
1087  // From a string of digits in a given base
1088  virtual Expr newBVConstExpr(const std::string& s, int base = 2);
1089  // From a vector of bools
1090  virtual Expr newBVConstExpr(const std::vector<bool>& bits);
1091  // From a rational: bitvector is of length 'len', or the min. needed length when len=0.
1092  virtual Expr newBVConstExpr(const Rational& r, int len = 0);
1093 
1094  // Concat and extract
1095  virtual Expr newConcatExpr(const Expr& t1, const Expr& t2);
1096  virtual Expr newConcatExpr(const std::vector<Expr>& kids);
1097  virtual Expr newBVExtractExpr(const Expr& e, int hi, int low);
1098 
1099  // Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor
1100  virtual Expr newBVNegExpr(const Expr& t1);
1101 
1102  virtual Expr newBVAndExpr(const Expr& t1, const Expr& t2);
1103  virtual Expr newBVAndExpr(const std::vector<Expr>& kids);
1104 
1105  virtual Expr newBVOrExpr(const Expr& t1, const Expr& t2);
1106  virtual Expr newBVOrExpr(const std::vector<Expr>& kids);
1107 
1108  virtual Expr newBVXorExpr(const Expr& t1, const Expr& t2);
1109  virtual Expr newBVXorExpr(const std::vector<Expr>& kids);
1110 
1111  virtual Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
1112  virtual Expr newBVXnorExpr(const std::vector<Expr>& kids);
1113 
1114  virtual Expr newBVNandExpr(const Expr& t1, const Expr& t2);
1115  virtual Expr newBVNorExpr(const Expr& t1, const Expr& t2);
1116  virtual Expr newBVCompExpr(const Expr& t1, const Expr& t2);
1117 
1118  // Unsigned bitvector inequalities
1119  virtual Expr newBVLTExpr(const Expr& t1, const Expr& t2);
1120  virtual Expr newBVLEExpr(const Expr& t1, const Expr& t2);
1121 
1122  // Signed bitvector inequalities
1123  virtual Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
1124  virtual Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
1125 
1126  // Sign-extend t1 to a total of len bits
1127  virtual Expr newSXExpr(const Expr& t1, int len);
1128 
1129  // Bitvector arithmetic: unary minus, plus, subtract, multiply
1130  virtual Expr newBVUminusExpr(const Expr& t1);
1131  virtual Expr newBVSubExpr(const Expr& t1, const Expr& t2);
1133  virtual Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
1134  virtual Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2);
1135  virtual Expr newBVMultExpr(int numbits,
1136  const Expr& t1, const Expr& t2);
1137 
1138  virtual Expr newBVUDivExpr(const Expr& t1, const Expr& t2);
1139  virtual Expr newBVURemExpr(const Expr& t1, const Expr& t2);
1140  virtual Expr newBVSDivExpr(const Expr& t1, const Expr& t2);
1141  virtual Expr newBVSRemExpr(const Expr& t1, const Expr& t2);
1142  virtual Expr newBVSModExpr(const Expr& t1, const Expr& t2);
1143 
1144  // Left shift by r bits: result is old size + r bits
1145  virtual Expr newFixedLeftShiftExpr(const Expr& t1, int r);
1146  // Left shift by r bits: result is same size as t1
1147  virtual Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
1148  // Logical right shift by r bits: result is same size as t1
1149  virtual Expr newFixedRightShiftExpr(const Expr& t1, int r);
1150  // Left shift with shift parameter an arbitrary bit-vector expr
1151  virtual Expr newBVSHL(const Expr& t1, const Expr& t2);
1152  // Logical right shift with shift parameter an arbitrary bit-vector expr
1153  virtual Expr newBVLSHR(const Expr& t1, const Expr& t2);
1154  // Arithmetic right shift with shift parameter an arbitrary bit-vector expr
1155  virtual Expr newBVASHR(const Expr& t1, const Expr& t2);
1156  // Get value of BV Constant
1157  virtual Rational computeBVConst(const Expr& e);
1158  // End of Bitvector expression methods
1160 
1161  /***************************************************************************/
1167  /***************************************************************************/
1168 
1170  virtual Expr tupleExpr(const std::vector<Expr>& exprs);
1171 
1173  virtual Expr tupleSelectExpr(const Expr& tuple, int index);
1174 
1176  virtual Expr tupleUpdateExpr(const Expr& tuple, int index,
1177  const Expr& newValue);
1178 
1180  virtual Expr datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args);
1181 
1183  virtual Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
1184 
1186  virtual Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
1187 
1189 
1196  virtual Expr boundVarExpr(const std::string& name,
1197  const std::string& uid,
1198  const Type& type);
1199 
1201  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
1203  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1204  const Expr& trigger);
1206  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1207  const std::vector<Expr>& triggers);
1209  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1210  const std::vector<std::vector<Expr> >& triggers);
1211 
1213 
1221  virtual void setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers);
1223  virtual void setTriggers(const Expr& e, const std::vector<Expr>& triggers);
1225  virtual void setTrigger(const Expr& e, const Expr& trigger);
1227  virtual void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger);
1228 
1230  virtual Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
1231 
1233  virtual Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
1234 
1236  virtual Op transClosure(const Op& op);
1237 
1239 
1246  virtual Expr simulateExpr(const Expr& f, const Expr& s0,
1247  const std::vector<Expr>& inputs,
1248  const Expr& n);
1249  // End of Other expression methods
1251 
1252  /***************************************************************************/
1262  /***************************************************************************/
1263 
1265 
1266  virtual void setResourceLimit(unsigned limit);
1267 
1269 
1273  virtual void setTimeLimit(unsigned limit);
1274 
1276 
1278  virtual void assertFormula(const Expr& e);
1279 
1281 
1284  virtual void registerAtom(const Expr& e);
1285 
1287 
1289  virtual Expr getImpliedLiteral();
1290 
1292  virtual Expr simplify(const Expr& e);
1293 
1295 
1303  virtual QueryResult query(const Expr& e);
1304 
1306 
1307  virtual QueryResult checkUnsat(const Expr& e);
1308 
1310 
1312  virtual QueryResult checkContinue();
1313 
1315 
1317  virtual QueryResult restart(const Expr& e);
1318 
1320 
1322  virtual void returnFromCheck();
1323 
1325 
1330  virtual void getUserAssumptions(std::vector<Expr>& assumptions);
1331 
1333 
1336  virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
1337 
1339 
1341  virtual void getAssumptions(std::vector<Expr>& assumptions);
1342 
1344 
1349  virtual void getAssumptionsUsed(std::vector<Expr>& assumptions);
1350 
1351  virtual Expr getProofQuery();
1352 
1353 
1355 
1363  virtual void getCounterExample(std::vector<Expr>& assumptions,
1364  bool inOrder=true);
1365 
1367 
1369  virtual void getConcreteModel(ExprMap<Expr> & m);
1370 
1373 
1375  virtual QueryResult tryModelGeneration();
1376 
1377  //:ALEX: returns the current truth value of a formula
1378  // returns UNKNOWN_VAL if e is not associated
1379  // with a boolean variable in the SAT module,
1380  // i.e. if its value can not determined without search.
1381  virtual FormulaValue value(const Expr& e);
1382 
1384 
1388  virtual bool inconsistent(std::vector<Expr>& assumptions);
1389 
1391  virtual bool inconsistent();
1392 
1394 
1402  virtual bool incomplete();
1403 
1405 
1411  virtual bool incomplete(std::vector<std::string>& reasons);
1412 
1414 
1416  virtual Proof getProof();
1417 
1419 
1420  virtual Expr getValue(const Expr& e);
1421 
1423 
1424  virtual Expr getTCC();
1425 
1427  virtual void getAssumptionsTCC(std::vector<Expr>& assumptions);
1428 
1430 
1431  virtual Proof getProofTCC();
1432 
1434 
1439  virtual Expr getClosure();
1440 
1442 
1443  virtual Proof getProofClosure();
1444  // End of Validity checking methods
1446 
1447  /***************************************************************************/
1463  /***************************************************************************/
1464 
1466  virtual int stackLevel();
1467 
1469  virtual void push();
1470 
1472  virtual void pop();
1473 
1475 
1479  virtual void popto(int stackLevel);
1480 
1482  virtual int scopeLevel();
1483 
1488  virtual void pushScope();
1489 
1494  virtual void popScope();
1495 
1497 
1503  virtual void poptoScope(int scopeLevel);
1504 
1506  virtual Context* getCurrentContext();
1507 
1509  virtual void reset();
1510 
1512  virtual void logAnnotation(const Expr& annot);
1513  // End of Context methods
1515 
1516  /***************************************************************************/
1522  /***************************************************************************/
1523 
1525  virtual void loadFile(const std::string& fileName,
1527  bool interactive = false,
1528  bool calledFromParser = false);
1529 
1531  virtual void loadFile(std::istream& is,
1533  bool interactive = false);
1534  // End of methods for reading files
1536 
1537  /***************************************************************************/
1543  /***************************************************************************/
1544 
1546  virtual Statistics getStatistics();
1547 
1549  virtual void printStatistics();
1550  // End of Statistics Methods
1552 
1553 };/* class ValidityChecker */
1554 
1555 template <class T>
1557  (*this)[a] = b;
1558 }
1559 
1560 // Comparison (the way that CVC3 does it)
1561 int compare(const Expr& e1, const Expr& e2);
1562 
1563 }/* CVC3 namespace */
1564 
1565 #endif /* _cvc3__include__vc_h_ */
1566 #endif /* __CVC4__CVC3_COMPAT_H */
std::vector< std::pair< std::string, bool > > * sv
Definition: cvc3_compat.h:118
Iterator type for the children of an Expr.
Definition: expr.h:415
void * Expr
const CVC4::Kind BVGE
Definition: cvc3_compat.h:80
struct CVC4::options::help__option_t help
Expr class for CVC3 compatibility layer.
Definition: cvc3_compat.h:319
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
const CVC4::Kind BVLE
Definition: cvc3_compat.h:78
Definition: kind.h:57
const CVC4::Kind DIVIDE
Definition: cvc3_compat.h:76
QueryResult
Definition: cvc3_compat.h:476
const CVC4::Kind BVCONST
Definition: cvc3_compat.h:83
int compare(const Expr &e1, const Expr &e2)
const CVC4::Kind CONCAT
Definition: cvc3_compat.h:85
#define PRESENTATION_LANG
Definition: cvc3_compat.h:464
SmtEngine: the main public entry point of libcvc4.
A simple representation of a cardinality.
Definition: cardinality.h:65
Class encapsulating CVC4 expression types.
Definition: type.h:89
[[ Add one-line brief description here ]]
const CVC4::Kind GE
Definition: cvc3_compat.h:75
subtraction of two bit-vectors (68)
Definition: kind.h:140
A multi-precision rational constant.
bit-vector unsigned greater than (the two bit-vector parameters must have same width) (82) ...
Definition: kind.h:154
FormulaValue
Definition: cvc3_compat.h:493
CLFlagType
Different types of command line flags.
Definition: cvc3_compat.h:90
language::input::Language InputLanguage
Definition: language.h:165
bit-vector unsigned less than (the two bit-vector parameters must have same width) (80) ...
Definition: kind.h:152
A collection of state for use by parser implementations.
CVC4&#39;s exception base class and some associated utilities.
array select; first parameter is an array term, second is the selection index (109) ...
Definition: kind.h:183
void insert(Expr a, Expr b)
Definition: cvc3_compat.h:1556
addition of two or more bit-vectors (67)
Definition: kind.h:139
a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (56) ...
Definition: kind.h:128
const CVC4::Kind BVLT
Definition: cvc3_compat.h:77
Exception thrown in the case of type-checking errors.
Definition: expr.h:151
std::string QueryResultToString(QueryResult query_result)
struct CVC4::options::interactive__option_t interactive
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Expr Op
Definition: cvc3_compat.h:309
const CVC4::Kind LE
Definition: cvc3_compat.h:74
std::ostream & operator<<(std::ostream &out, CLFlagType clft)
bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (99) ...
Definition: kind.h:171
CVC4::TypeCheckingException TypecheckException
Definition: cvc3_compat.h:245
real division, division by 0 undefined (user symbol) (36)
Definition: kind.h:106
std::string int2string(int n)
Macros that should be defined everywhere during the building of the libraries and driver binary...
expr_manager.h
greater than or equal, x >= y (51)
Definition: kind.h:121
CVC3 API (compatibility layer for CVC4)
Definition: cvc3_compat.h:514
less than or equal, x <= y (49)
Definition: kind.h:119
size_t ExprIndex
Definition: cvc3_compat.h:244
bool operator==(const Cardinality &c, CVC3CardinalityKind d)
const CVC4::Kind EQ
Definition: cvc3_compat.h:73
const CVC4::Kind BVPLUS
Definition: cvc3_compat.h:81
equality (two parameters only, sorts must match) (8)
Definition: kind.h:72
CVC3CardinalityKind
Definition: cvc3_compat.h:254
const CVC4::Kind BVGT
Definition: cvc3_compat.h:79
struct CVC4::options::out__option_t out
const CVC4::Kind EXTRACT
Definition: cvc3_compat.h:84
size_t Unsigned
Definition: cvc3_compat.h:246
expr.h
CVC4::Expr::const_iterator iterator
Definition: cvc3_compat.h:321
void * Type
concatenation of two or more bit-vectors (57)
Definition: kind.h:129
bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (81) ...
Definition: kind.h:153
CVC4::Statistics Statistics
Definition: cvc3_compat.h:462
Vector of pair<string, bool>
Definition: cvc3_compat.h:95
array store; first parameter is an array term, second is the store index, third is the term to store ...
Definition: kind.h:184
bool operator!=(const Cardinality &c, CVC3CardinalityKind d)
std::string * s
Definition: cvc3_compat.h:117
bool isArrayLiteral(const Expr &)
This class encapsulates all of the state of a parser, including the name of the file, line number and column information, and in-scope declarations.
Definition: parser.h:106
const CVC4::Kind BVSUB
Definition: cvc3_compat.h:82
Kind_t
Definition: kind.h:60
bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (83) ...
Definition: kind.h:155
Interface for expression types.