cvc4-1.3
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 
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 
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 
233 class CVC4_PUBLIC Context;
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.
258 };/* enum CVC3CardinalityKind */
259 
260 std::ostream& operator<<(std::ostream& out, CVC3CardinalityKind c) CVC4_PUBLIC;
261 
262 bool operator==(const Cardinality& c, CVC3CardinalityKind d) CVC4_PUBLIC;
263 bool operator==(CVC3CardinalityKind d, const Cardinality& c) CVC4_PUBLIC;
264 bool operator!=(const Cardinality& c, CVC3CardinalityKind d) CVC4_PUBLIC;
265 bool operator!=(CVC3CardinalityKind d, const Cardinality& c) CVC4_PUBLIC;
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 
310 typedef Expr Op;
311 
319 class CVC4_PUBLIC Expr : public CVC4::Expr {
320 public:
321  Expr();
322  Expr(const Expr& e);
323  Expr(const CVC4::Expr& e);
324  Expr(CVC4::Kind k);
325 
326  // Compound expression constructors
327  Expr eqExpr(const Expr& right) const;
328  Expr notExpr() const;
329  Expr negate() const; // avoid double-negatives
330  Expr andExpr(const Expr& right) const;
331  Expr orExpr(const Expr& right) const;
332  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
333  Expr iffExpr(const Expr& right) const;
334  Expr impExpr(const Expr& right) const;
335  Expr xorExpr(const Expr& right) const;
336 
337  Expr substExpr(const std::vector<Expr>& oldTerms,
338  const std::vector<Expr>& newTerms) const;
339  Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
340 
341  Expr operator!() const;
342  Expr operator&&(const Expr& right) const;
343  Expr operator||(const Expr& right) const;
344 
345  static size_t hash(const Expr& e);
346 
347  size_t hash() const;
348 
349  // Core expression testers
350 
351  bool isFalse() const;
352  bool isTrue() const;
353  bool isBoolConst() const;
354  bool isVar() const;
355  bool isBoundVar() const;
356  bool isString() const;
357  bool isSymbol() const;
358  bool isTerm() const;
359  bool isType() const;
360  bool isClosure() const;
361  bool isQuantifier() const;
362  bool isForall() const;
363  bool isExists() const;
364  bool isLambda() const;
365  bool isApply() const;
366  bool isTheorem() const;
367  bool isConstant() const;
368  bool isRawList() const;
369 
370  bool isAtomic() const;
371  bool isAtomicFormula() const;
372  bool isAbsAtomicFormula() const;
373  bool isLiteral() const;
374  bool isAbsLiteral() const;
375  bool isBoolConnective() const;
376  bool isPropLiteral() const;
377  bool isPropAtom() const;
378 
379  const std::string& getName() const;
380  const std::string& getUid() const;
381 
382  const std::string& getString() const;
383  const std::vector<Expr>& getVars() const;
384  const Expr& getExistential() const;
385  int getBoundIndex() const;
386  const Expr& getBody() const;
387  const Theorem& getTheorem() const;
388 
389  bool isEq() const;
390  bool isNot() const;
391  bool isAnd() const;
392  bool isOr() const;
393  bool isITE() const;
394  bool isIff() const;
395  bool isImpl() const;
396  bool isXor() const;
397 
398  bool isRational() const;
399  bool isSkolem() const;
400 
401  const Rational& getRational() const;
402 
403  Op mkOp() const;
404  Op getOp() const;
405  Expr getOpExpr() const;
406  int getOpKind() const;
407  Expr getExpr() const;// since people are used to doing getOp().getExpr() in CVC3
408 
410  std::vector< std::vector<Expr> > getTriggers() const;
411 
412  // Get the expression manager. The expression must be non-null.
413  ExprManager* getEM() const;
414 
415  // Return a ref to the vector of children.
416  std::vector<Expr> getKids() const;
417 
418  // Get the index field
419  ExprIndex getIndex() const;
420 
421  // Return the number of children. Note, that an application of a
422  // user-defined function has the arity of that function (the number
423  // of arguments), and the function name itself is part of the
424  // operator.
425  int arity() const;
426 
427  // Return the ith child. As with arity, it's also the ith argument
428  // in function application.
429  Expr operator[](int i) const;
430 
432  Expr unnegate() const;
433 
434  // Check if Expr is not Null
435  bool isInitialized() const;
436 
438  Type getType() const;
440  Type lookupType() const;
441 
443  void pprint() const;
445  void pprintnodag() const;
446 
447 };/* class CVC3::Expr */
448 
449 bool isArrayLiteral(const Expr&) CVC4_PUBLIC;
450 
451 class CVC4_PUBLIC ExprManager : public CVC4::ExprManager {
452 public:
453  const std::string& getKindName(int kind);
455  InputLanguage getInputLang() const;
457  InputLanguage getOutputLang() const;
458 };/* class CVC3::ExprManager */
459 
461 
462 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
463 #define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB_V1
464 #define SMTLIB_V2_LANG ::CVC4::language::input::LANG_SMTLIB_V2
465 #define TPTP_LANG ::CVC4::language::input::LANG_TPTP
466 #define AST_LANG ::CVC4::language::input::LANG_AST
467 
468 /*****************************************************************************/
469 /*
470  * Type for result of queries. VALID and UNSATISFIABLE are treated as
471  * equivalent, as are SATISFIABLE and INVALID.
472  */
473 /*****************************************************************************/
474 typedef enum CVC4_PUBLIC QueryResult {
476  INVALID = 0,
477  VALID = 1,
481 } QueryResult;
482 
483 std::ostream& operator<<(std::ostream& out, QueryResult qr);
484 std::string QueryResultToString(QueryResult query_result);
485 
486 /*****************************************************************************/
487 /*
488  * Type for truth value of formulas.
489  */
490 /*****************************************************************************/
491 typedef enum CVC4_PUBLIC FormulaValue {
495 } FormulaValue;
496 
497 std::ostream& operator<<(std::ostream& out, FormulaValue fv) CVC4_PUBLIC;
498 
499 /*****************************************************************************/
511 /*****************************************************************************/
513 
514  CLFlags* d_clflags;
515  CVC4::Options d_options;
516  CVC3::ExprManager* d_em;
517  std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
518  std::set<ValidityChecker*> d_reverseEmmc;
519  CVC4::SmtEngine* d_smt;
520  CVC4::parser::Parser* d_parserContext;
521  std::vector<Expr> d_exprTypeMapRemove;
522  unsigned d_stackLevel;
523 
524  friend class Type; // to reach in to d_exprTypeMapRemove
525 
526  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
527  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
528 
529  ConstructorMap d_constructors;
530  SelectorMap d_selectors;
531 
532  ValidityChecker(const CLFlags& clflags);
533 
534  void setUpOptions(CVC4::Options& options, const CLFlags& clflags);
535 
536  // helper function for bitvectors
537  Expr bvpad(int len, const Expr& e);
538 
539 public:
541  ValidityChecker();
543  virtual ~ValidityChecker();
544 
546 
552  virtual CLFlags& getFlags() const;
554  virtual void reprocessFlags();
555 
556  /***************************************************************************/
557  /*
558  * Static methods
559  */
560  /***************************************************************************/
561 
563 
566  static CLFlags createFlags();
568 
571  static ValidityChecker* create(const CLFlags& flags);
573  static ValidityChecker* create();
574 
575  /***************************************************************************/
582  /***************************************************************************/
583 
584  // Basic types
585  virtual Type boolType();
586 
587  virtual Type realType();
588 
589  virtual Type intType();
590 
592 
595  virtual Type subrangeType(const Expr& l, const Expr& r);
596 
598 
607  virtual Type subtypeType(const Expr& pred, const Expr& witness);
608 
609  // Tuple types
611  virtual Type tupleType(const Type& type0, const Type& type1);
612 
614  virtual Type tupleType(const Type& type0, const Type& type1,
615  const Type& type2);
617  virtual Type tupleType(const std::vector<Type>& types);
618 
619  // Record types
621  virtual Type recordType(const std::string& field, const Type& type);
622 
624 
625  virtual Type recordType(const std::string& field0, const Type& type0,
626  const std::string& field1, const Type& type1);
628 
629  virtual Type recordType(const std::string& field0, const Type& type0,
630  const std::string& field1, const Type& type1,
631  const std::string& field2, const Type& type2);
633 
634  virtual Type recordType(const std::vector<std::string>& fields,
635  const std::vector<Type>& types);
636 
637  // Datatypes
638 
640 
643  virtual Type dataType(const std::string& name,
644  const std::string& constructor,
645  const std::vector<std::string>& selectors,
646  const std::vector<Expr>& types);
647 
649 
652  virtual Type dataType(const std::string& name,
653  const std::vector<std::string>& constructors,
654  const std::vector<std::vector<std::string> >& selectors,
655  const std::vector<std::vector<Expr> >& types);
656 
658 
661  virtual void dataType(const std::vector<std::string>& names,
662  const std::vector<std::vector<std::string> >& constructors,
663  const std::vector<std::vector<std::vector<std::string> > >& selectors,
664  const std::vector<std::vector<std::vector<Expr> > >& types,
665  std::vector<Type>& returnTypes);
666 
668  virtual Type arrayType(const Type& typeIndex, const Type& typeData);
669 
671  virtual Type bitvecType(int n);
672 
674  virtual Type funType(const Type& typeDom, const Type& typeRan);
675 
677  virtual Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
678 
680  virtual Type createType(const std::string& typeName);
681 
683  virtual Type createType(const std::string& typeName, const Type& def);
684 
686  virtual Type lookupType(const std::string& typeName);
687  // End of Type-related methods
689 
690  /***************************************************************************/
697  /***************************************************************************/
698 
700  virtual ExprManager* getEM();
701 
703 
708  virtual Expr varExpr(const std::string& name, const Type& type);
709 
711  virtual Expr varExpr(const std::string& name, const Type& type,
712  const Expr& def);
713 
715 
722  virtual Expr lookupVar(const std::string& name, Type* type);
723 
725  virtual Type getType(const Expr& e);
726 
728  virtual Type getBaseType(const Expr& e);
729 
731  virtual Type getBaseType(const Type& t);
732 
734  virtual Expr getTypePred(const Type&t, const Expr& e);
735 
737  virtual Expr stringExpr(const std::string& str);
738 
740  virtual Expr idExpr(const std::string& name);
741 
743 
763  virtual Expr listExpr(const std::vector<Expr>& kids);
764 
766  virtual Expr listExpr(const Expr& e1);
767 
769  virtual Expr listExpr(const Expr& e1, const Expr& e2);
770 
772  virtual Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
773 
775  virtual Expr listExpr(const std::string& op,
776  const std::vector<Expr>& kids);
777 
779  virtual Expr listExpr(const std::string& op, const Expr& e1);
780 
782  virtual Expr listExpr(const std::string& op, const Expr& e1,
783  const Expr& e2);
784 
786  virtual Expr listExpr(const std::string& op, const Expr& e1,
787  const Expr& e2, const Expr& e3);
788 
790  virtual void printExpr(const Expr& e);
791 
793  virtual void printExpr(const Expr& e, std::ostream& os);
794 
796  virtual Expr parseExpr(const Expr& e);
797 
799  virtual Type parseType(const Expr& e);
800 
802 
809  virtual Expr importExpr(const Expr& e);
810 
812 
813  virtual Type importType(const Type& t);
814 
816  virtual void cmdsFromString(const std::string& s,
818 
820 
823  virtual Expr exprFromString(const std::string& e,
825  // End of General Expr Methods
827 
828  /***************************************************************************/
837  /***************************************************************************/
838 
840  virtual Expr trueExpr();
841 
843  virtual Expr falseExpr();
844 
846  virtual Expr notExpr(const Expr& child);
847 
849  virtual Expr andExpr(const Expr& left, const Expr& right);
850 
852  virtual Expr andExpr(const std::vector<Expr>& children);
853 
855  virtual Expr orExpr(const Expr& left, const Expr& right);
856 
858  virtual Expr orExpr(const std::vector<Expr>& children);
859 
861  virtual Expr impliesExpr(const Expr& hyp, const Expr& conc);
862 
864  virtual Expr iffExpr(const Expr& left, const Expr& right);
865 
867 
871  virtual Expr eqExpr(const Expr& child0, const Expr& child1);
872 
874 
879  virtual Expr iteExpr(const Expr& ifpart, const Expr& thenpart,
880  const Expr& elsepart);
881 
886  virtual Expr distinctExpr(const std::vector<Expr>& children);
887  // End of Core expression methods
889 
890  /***************************************************************************/
896  /***************************************************************************/
897 
899 
903  virtual Op createOp(const std::string& name, const Type& type);
904 
906  virtual Op createOp(const std::string& name, const Type& type,
907  const Expr& def);
908 
910 
917  virtual Op lookupOp(const std::string& name, Type* type);
918 
920  virtual Expr funExpr(const Op& op, const Expr& child);
921 
923  virtual Expr funExpr(const Op& op, const Expr& left, const Expr& right);
924 
926  virtual Expr funExpr(const Op& op, const Expr& child0,
927  const Expr& child1, const Expr& child2);
928 
930  virtual Expr funExpr(const Op& op, const std::vector<Expr>& children);
931  // End of User-defined (uninterpreted) function methods
933 
934  /***************************************************************************/
943  /***************************************************************************/
944 
951  virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
952 
954 
958  virtual Expr ratExpr(int n, int d = 1);
959 
961 
965  virtual Expr ratExpr(const std::string& n, const std::string& d, int base);
966 
968 
973  virtual Expr ratExpr(const std::string& n, int base = 10);
974 
976  virtual Expr uminusExpr(const Expr& child);
977 
979  virtual Expr plusExpr(const Expr& left, const Expr& right);
980 
982  virtual Expr plusExpr(const std::vector<Expr>& children);
983 
985  virtual Expr minusExpr(const Expr& left, const Expr& right);
986 
988  virtual Expr multExpr(const Expr& left, const Expr& right);
989 
991  virtual Expr powExpr(const Expr& x, const Expr& n);
992 
994  virtual Expr divideExpr(const Expr& numerator, const Expr& denominator);
995 
997  virtual Expr ltExpr(const Expr& left, const Expr& right);
998 
1000  virtual Expr leExpr(const Expr& left, const Expr& right);
1001 
1003  virtual Expr gtExpr(const Expr& left, const Expr& right);
1004 
1006  virtual Expr geExpr(const Expr& left, const Expr& right);
1007  // End of Arithmetic expression methods
1009 
1010  /***************************************************************************/
1016  /***************************************************************************/
1017 
1019 
1020  virtual Expr recordExpr(const std::string& field, const Expr& expr);
1021 
1023 
1024  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
1025  const std::string& field1, const Expr& expr1);
1026 
1028 
1029  virtual Expr recordExpr(const std::string& field0, const Expr& expr0,
1030  const std::string& field1, const Expr& expr1,
1031  const std::string& field2, const Expr& expr2);
1032 
1034 
1040  virtual Expr recordExpr(const std::vector<std::string>& fields,
1041  const std::vector<Expr>& exprs);
1042 
1044 
1046  virtual Expr recSelectExpr(const Expr& record, const std::string& field);
1047 
1049 
1053  virtual Expr recUpdateExpr(const Expr& record, const std::string& field,
1054  const Expr& newValue);
1055  // End of Record expression methods
1057 
1058  /***************************************************************************/
1064  /***************************************************************************/
1065 
1067 
1068  virtual Expr readExpr(const Expr& array, const Expr& index);
1069 
1071  virtual Expr writeExpr(const Expr& array, const Expr& index,
1072  const Expr& newValue);
1073  // End of Array expression methods
1075 
1076  /***************************************************************************/
1082  /***************************************************************************/
1083 
1084  // Bitvector constants
1085  // From a string of digits in a given base
1086  virtual Expr newBVConstExpr(const std::string& s, int base = 2);
1087  // From a vector of bools
1088  virtual Expr newBVConstExpr(const std::vector<bool>& bits);
1089  // From a rational: bitvector is of length 'len', or the min. needed length when len=0.
1090  virtual Expr newBVConstExpr(const Rational& r, int len = 0);
1091 
1092  // Concat and extract
1093  virtual Expr newConcatExpr(const Expr& t1, const Expr& t2);
1094  virtual Expr newConcatExpr(const std::vector<Expr>& kids);
1095  virtual Expr newBVExtractExpr(const Expr& e, int hi, int low);
1096 
1097  // Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor
1098  virtual Expr newBVNegExpr(const Expr& t1);
1099 
1100  virtual Expr newBVAndExpr(const Expr& t1, const Expr& t2);
1101  virtual Expr newBVAndExpr(const std::vector<Expr>& kids);
1102 
1103  virtual Expr newBVOrExpr(const Expr& t1, const Expr& t2);
1104  virtual Expr newBVOrExpr(const std::vector<Expr>& kids);
1105 
1106  virtual Expr newBVXorExpr(const Expr& t1, const Expr& t2);
1107  virtual Expr newBVXorExpr(const std::vector<Expr>& kids);
1108 
1109  virtual Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
1110  virtual Expr newBVXnorExpr(const std::vector<Expr>& kids);
1111 
1112  virtual Expr newBVNandExpr(const Expr& t1, const Expr& t2);
1113  virtual Expr newBVNorExpr(const Expr& t1, const Expr& t2);
1114  virtual Expr newBVCompExpr(const Expr& t1, const Expr& t2);
1115 
1116  // Unsigned bitvector inequalities
1117  virtual Expr newBVLTExpr(const Expr& t1, const Expr& t2);
1118  virtual Expr newBVLEExpr(const Expr& t1, const Expr& t2);
1119 
1120  // Signed bitvector inequalities
1121  virtual Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
1122  virtual Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
1123 
1124  // Sign-extend t1 to a total of len bits
1125  virtual Expr newSXExpr(const Expr& t1, int len);
1126 
1127  // Bitvector arithmetic: unary minus, plus, subtract, multiply
1128  virtual Expr newBVUminusExpr(const Expr& t1);
1129  virtual Expr newBVSubExpr(const Expr& t1, const Expr& t2);
1131  virtual Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
1132  virtual Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2);
1133  virtual Expr newBVMultExpr(int numbits,
1134  const Expr& t1, const Expr& t2);
1135 
1136  virtual Expr newBVUDivExpr(const Expr& t1, const Expr& t2);
1137  virtual Expr newBVURemExpr(const Expr& t1, const Expr& t2);
1138  virtual Expr newBVSDivExpr(const Expr& t1, const Expr& t2);
1139  virtual Expr newBVSRemExpr(const Expr& t1, const Expr& t2);
1140  virtual Expr newBVSModExpr(const Expr& t1, const Expr& t2);
1141 
1142  // Left shift by r bits: result is old size + r bits
1143  virtual Expr newFixedLeftShiftExpr(const Expr& t1, int r);
1144  // Left shift by r bits: result is same size as t1
1145  virtual Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
1146  // Logical right shift by r bits: result is same size as t1
1147  virtual Expr newFixedRightShiftExpr(const Expr& t1, int r);
1148  // Left shift with shift parameter an arbitrary bit-vector expr
1149  virtual Expr newBVSHL(const Expr& t1, const Expr& t2);
1150  // Logical right shift with shift parameter an arbitrary bit-vector expr
1151  virtual Expr newBVLSHR(const Expr& t1, const Expr& t2);
1152  // Arithmetic right shift with shift parameter an arbitrary bit-vector expr
1153  virtual Expr newBVASHR(const Expr& t1, const Expr& t2);
1154  // Get value of BV Constant
1155  virtual Rational computeBVConst(const Expr& e);
1156  // End of Bitvector expression methods
1158 
1159  /***************************************************************************/
1165  /***************************************************************************/
1166 
1168  virtual Expr tupleExpr(const std::vector<Expr>& exprs);
1169 
1171  virtual Expr tupleSelectExpr(const Expr& tuple, int index);
1172 
1174  virtual Expr tupleUpdateExpr(const Expr& tuple, int index,
1175  const Expr& newValue);
1176 
1178  virtual Expr datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args);
1179 
1181  virtual Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
1182 
1184  virtual Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
1185 
1187 
1194  virtual Expr boundVarExpr(const std::string& name,
1195  const std::string& uid,
1196  const Type& type);
1197 
1199  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
1201  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1202  const Expr& trigger);
1204  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1205  const std::vector<Expr>& triggers);
1207  virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
1208  const std::vector<std::vector<Expr> >& triggers);
1209 
1211 
1219  virtual void setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers);
1221  virtual void setTriggers(const Expr& e, const std::vector<Expr>& triggers);
1223  virtual void setTrigger(const Expr& e, const Expr& trigger);
1225  virtual void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger);
1226 
1228  virtual Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
1229 
1231  virtual Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
1232 
1234  virtual Op transClosure(const Op& op);
1235 
1237 
1244  virtual Expr simulateExpr(const Expr& f, const Expr& s0,
1245  const std::vector<Expr>& inputs,
1246  const Expr& n);
1247  // End of Other expression methods
1249 
1250  /***************************************************************************/
1260  /***************************************************************************/
1261 
1263 
1264  virtual void setResourceLimit(unsigned limit);
1265 
1267 
1271  virtual void setTimeLimit(unsigned limit);
1272 
1274 
1276  virtual void assertFormula(const Expr& e);
1277 
1279 
1282  virtual void registerAtom(const Expr& e);
1283 
1285 
1287  virtual Expr getImpliedLiteral();
1288 
1290  virtual Expr simplify(const Expr& e);
1291 
1293 
1301  virtual QueryResult query(const Expr& e);
1302 
1304 
1305  virtual QueryResult checkUnsat(const Expr& e);
1306 
1308 
1310  virtual QueryResult checkContinue();
1311 
1313 
1315  virtual QueryResult restart(const Expr& e);
1316 
1318 
1320  virtual void returnFromCheck();
1321 
1323 
1328  virtual void getUserAssumptions(std::vector<Expr>& assumptions);
1329 
1331 
1334  virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
1335 
1337 
1339  virtual void getAssumptions(std::vector<Expr>& assumptions);
1340 
1342 
1347  virtual void getAssumptionsUsed(std::vector<Expr>& assumptions);
1348 
1349  virtual Expr getProofQuery();
1350 
1351 
1353 
1361  virtual void getCounterExample(std::vector<Expr>& assumptions,
1362  bool inOrder=true);
1363 
1365 
1367  virtual void getConcreteModel(ExprMap<Expr> & m);
1368 
1371 
1373  virtual QueryResult tryModelGeneration();
1374 
1375  //:ALEX: returns the current truth value of a formula
1376  // returns UNKNOWN_VAL if e is not associated
1377  // with a boolean variable in the SAT module,
1378  // i.e. if its value can not determined without search.
1379  virtual FormulaValue value(const Expr& e);
1380 
1382 
1386  virtual bool inconsistent(std::vector<Expr>& assumptions);
1387 
1389  virtual bool inconsistent();
1390 
1392 
1400  virtual bool incomplete();
1401 
1403 
1409  virtual bool incomplete(std::vector<std::string>& reasons);
1410 
1412 
1414  virtual Proof getProof();
1415 
1417 
1418  virtual Expr getValue(const Expr& e);
1419 
1421 
1422  virtual Expr getTCC();
1423 
1425  virtual void getAssumptionsTCC(std::vector<Expr>& assumptions);
1426 
1428 
1429  virtual Proof getProofTCC();
1430 
1432 
1437  virtual Expr getClosure();
1438 
1440 
1441  virtual Proof getProofClosure();
1442  // End of Validity checking methods
1444 
1445  /***************************************************************************/
1461  /***************************************************************************/
1462 
1464  virtual int stackLevel();
1465 
1467  virtual void push();
1468 
1470  virtual void pop();
1471 
1473 
1477  virtual void popto(int stackLevel);
1478 
1480  virtual int scopeLevel();
1481 
1486  virtual void pushScope();
1487 
1492  virtual void popScope();
1493 
1495 
1501  virtual void poptoScope(int scopeLevel);
1502 
1504  virtual Context* getCurrentContext();
1505 
1507  virtual void reset();
1508 
1510  virtual void logAnnotation(const Expr& annot);
1511  // End of Context methods
1513 
1514  /***************************************************************************/
1520  /***************************************************************************/
1521 
1523  virtual void loadFile(const std::string& fileName,
1525  bool interactive = false,
1526  bool calledFromParser = false);
1527 
1529  virtual void loadFile(std::istream& is,
1531  bool interactive = false);
1532  // End of methods for reading files
1534 
1535  /***************************************************************************/
1541  /***************************************************************************/
1542 
1544  virtual Statistics getStatistics();
1545 
1547  virtual void printStatistics();
1548  // End of Statistics Methods
1550 
1551 };/* class ValidityChecker */
1552 
1553 template <class T>
1555  (*this)[a] = b;
1556 }
1557 
1558 // Comparison (the way that CVC3 does it)
1559 int compare(const Expr& e1, const Expr& e2);
1560 
1561 }/* CVC3 namespace */
1562 
1563 #endif /* _cvc3__include__vc_h_ */
1564 #endif /* __CVC4__CVC3_COMPAT_H */
std::vector< std::pair< std::string, bool > > * sv
Definition: cvc3_compat.h:118
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:226
const CVC4::Kind BVLE
Definition: cvc3_compat.h:78
const CVC4::Kind DIVIDE
Definition: cvc3_compat.h:76
QueryResult
Definition: cvc3_compat.h:474
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:462
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:88
[[ Add one-line brief description here ]]
const CVC4::Kind GE
Definition: cvc3_compat.h:75
bit-vector subtraction
Definition: kind.h:140
A multi-precision rational constant.
bit-vector unsigned greater than
Definition: kind.h:154
FormulaValue
Definition: cvc3_compat.h:491
CLFlagType
Different types of command line flags.
Definition: cvc3_compat.h:90
language::input::Language InputLanguage
Definition: language.h:149
bit-vector unsigned less than
Definition: kind.h:152
A collection of state for use by parser implementations.
CVC4's exception base class and some associated utilities.
array select
Definition: kind.h:180
void insert(Expr a, Expr b)
Definition: cvc3_compat.h:1554
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
bit-vector addition
Definition: kind.h:139
a fixed-width bit-vector constant
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:150
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
Definition: kind.h:168
CVC4::TypeCheckingException TypecheckException
Definition: cvc3_compat.h:245
real division (user symbol)
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
Definition: kind.h:121
CVC3 API (compatibility layer for CVC4)
Definition: cvc3_compat.h:512
less than or equal, x <= y
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
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
void * Context
size_t Unsigned
Definition: cvc3_compat.h:246
expr.h
void * Type
bit-vector concatenation
Definition: kind.h:129
bit-vector unsigned less than or equal
Definition: kind.h:153
CVC4::Statistics Statistics
Definition: cvc3_compat.h:460
Vector of pair
Definition: cvc3_compat.h:95
array store
Definition: kind.h:181
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
Definition: kind.h:155
Interface for expression types.