30 #ifndef __CVC4__CVC3_COMPAT_H
31 #define __CVC4__CVC3_COMPAT_H
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_)
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."
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_
57 #include "util/rational.h"
58 #include "util/integer.h"
118 std::vector<std::pair<std::string,bool> >*
sv;
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);
145 CLFlag& operator=(
bool b);
151 CLFlag& operator=(
const std::string& s);
154 CLFlag& operator=(
const char* s);
158 CLFlag& operator=(
const std::pair<std::string,bool>& p);
161 CLFlag& operator=(
const std::vector<std::pair<std::string,bool> >& sv);
168 bool modified()
const;
170 bool display()
const;
177 const bool& getBool()
const;
179 const int& getInt()
const;
181 const std::string& getString()
const;
183 const std::vector<std::pair<std::string,bool> >& getStrVec()
const;
185 const std::string& getHelp()
const;
199 typedef std::map<std::string, CLFlag> FlagMap;
205 void addFlag(
const std::string& name,
const CLFlag& f);
207 size_t countFlags(
const std::string& name)
const;
209 size_t countFlags(
const std::string& name,
210 std::vector<std::string>& names)
const;
213 const CLFlag& getFlag(
const std::string& name)
const;
215 const CLFlag& operator[](
const std::string& name)
const;
219 void setFlag(
const std::string& name,
const CLFlag& f);
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);
242 using namespace CVC4::kind;
284 Expr getExpr()
const;
288 Type operator[](
int i)
const;
292 bool isSubtype()
const;
304 static Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan);
305 Type funType(
const Type& typeRan)
const;
327 Expr eqExpr(
const Expr& right)
const;
328 Expr notExpr()
const;
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;
337 Expr substExpr(
const std::vector<Expr>& oldTerms,
338 const std::vector<Expr>& newTerms)
const;
341 Expr operator!()
const;
342 Expr operator&&(
const Expr& right)
const;
343 Expr operator||(
const Expr& right)
const;
345 static size_t hash(
const Expr& e);
351 bool isFalse()
const;
353 bool isBoolConst()
const;
355 bool isBoundVar()
const;
356 bool isString()
const;
357 bool isSymbol()
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;
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;
379 const std::string& getName()
const;
380 const std::string& getUid()
const;
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;
398 bool isRational()
const;
399 bool isSkolem()
const;
401 const Rational& getRational()
const;
405 Expr getOpExpr()
const;
406 int getOpKind()
const;
407 Expr getExpr()
const;
410 std::vector< std::vector<Expr> > getTriggers()
const;
416 std::vector<Expr> getKids()
const;
429 Expr operator[](
int i)
const;
432 Expr unnegate()
const;
435 bool isInitialized()
const;
438 Type getType()
const;
440 Type lookupType()
const;
445 void pprintnodag()
const;
453 const std::string& getKindName(
int kind);
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
517 std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
518 std::set<ValidityChecker*> d_reverseEmmc;
521 std::vector<Expr> d_exprTypeMapRemove;
522 unsigned d_stackLevel;
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;
529 ConstructorMap d_constructors;
530 SelectorMap d_selectors;
552 virtual CLFlags& getFlags()
const;
554 virtual void reprocessFlags();
585 virtual Type boolType();
587 virtual Type realType();
589 virtual Type intType();
595 virtual Type subrangeType(
const Expr& l,
const Expr& r);
607 virtual Type subtypeType(
const Expr& pred,
const Expr& witness);
611 virtual Type tupleType(
const Type& type0,
const Type& type1);
614 virtual Type tupleType(
const Type& type0,
const Type& type1,
617 virtual Type tupleType(
const std::vector<Type>& types);
621 virtual Type recordType(
const std::string& field,
const Type& type);
625 virtual Type recordType(
const std::string& field0,
const Type& type0,
626 const std::string& field1,
const Type& type1);
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);
634 virtual Type recordType(
const std::vector<std::string>& fields,
635 const std::vector<Type>& types);
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);
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);
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);
668 virtual Type arrayType(
const Type& typeIndex,
const Type& typeData);
671 virtual Type bitvecType(
int n);
674 virtual Type funType(
const Type& typeDom,
const Type& typeRan);
677 virtual Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan);
680 virtual Type createType(
const std::string& typeName);
683 virtual Type createType(
const std::string& typeName,
const Type& def);
686 virtual Type lookupType(
const std::string& typeName);
708 virtual Expr varExpr(
const std::string& name,
const Type& type);
711 virtual Expr varExpr(
const std::string& name,
const Type& type,
722 virtual Expr lookupVar(
const std::string& name,
Type* type);
725 virtual Type getType(
const Expr& e);
728 virtual Type getBaseType(
const Expr& e);
731 virtual Type getBaseType(
const Type& t);
737 virtual Expr stringExpr(
const std::string& str);
740 virtual Expr idExpr(
const std::string& name);
763 virtual Expr listExpr(
const std::vector<Expr>& kids);
766 virtual Expr listExpr(
const Expr& e1);
775 virtual Expr listExpr(
const std::string& op,
776 const std::vector<Expr>& kids);
779 virtual Expr listExpr(
const std::string& op,
const Expr& e1);
782 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
786 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
790 virtual void printExpr(
const Expr& e);
793 virtual void printExpr(
const Expr& e, std::ostream& os);
796 virtual Expr parseExpr(
const Expr& e);
799 virtual Type parseType(
const Expr& e);
809 virtual Expr importExpr(
const Expr& e);
813 virtual Type importType(
const Type& t);
816 virtual void cmdsFromString(
const std::string& s,
823 virtual Expr exprFromString(
const std::string& e,
840 virtual Expr trueExpr();
843 virtual Expr falseExpr();
846 virtual Expr notExpr(
const Expr& child);
849 virtual Expr andExpr(
const Expr& left,
const Expr& right);
852 virtual Expr andExpr(
const std::vector<Expr>& children);
855 virtual Expr orExpr(
const Expr& left,
const Expr& right);
858 virtual Expr orExpr(
const std::vector<Expr>& children);
861 virtual Expr impliesExpr(
const Expr& hyp,
const Expr& conc);
864 virtual Expr iffExpr(
const Expr& left,
const Expr& right);
871 virtual Expr eqExpr(
const Expr& child0,
const Expr& child1);
879 virtual Expr iteExpr(
const Expr& ifpart,
const Expr& thenpart,
880 const Expr& elsepart);
886 virtual Expr distinctExpr(
const std::vector<Expr>& children);
903 virtual Op createOp(
const std::string& name,
const Type& type);
906 virtual Op createOp(
const std::string& name,
const Type& type,
917 virtual Op lookupOp(
const std::string& name,
Type* type);
920 virtual Expr funExpr(
const Op& op,
const Expr& child);
923 virtual Expr funExpr(
const Op& op,
const Expr& left,
const Expr& right);
926 virtual Expr funExpr(
const Op& op,
const Expr& child0,
927 const Expr& child1,
const Expr& child2);
930 virtual Expr funExpr(
const Op& op,
const std::vector<Expr>& children);
951 virtual bool addPairToArithOrder(
const Expr& smaller,
const Expr& bigger);
958 virtual Expr ratExpr(
int n,
int d = 1);
965 virtual Expr ratExpr(
const std::string& n,
const std::string& d,
int base);
973 virtual Expr ratExpr(
const std::string& n,
int base = 10);
976 virtual Expr uminusExpr(
const Expr& child);
979 virtual Expr plusExpr(
const Expr& left,
const Expr& right);
982 virtual Expr plusExpr(
const std::vector<Expr>& children);
985 virtual Expr minusExpr(
const Expr& left,
const Expr& right);
988 virtual Expr multExpr(
const Expr& left,
const Expr& right);
994 virtual Expr divideExpr(
const Expr& numerator,
const Expr& denominator);
997 virtual Expr ltExpr(
const Expr& left,
const Expr& right);
1000 virtual Expr leExpr(
const Expr& left,
const Expr& right);
1003 virtual Expr gtExpr(
const Expr& left,
const Expr& right);
1006 virtual Expr geExpr(
const Expr& left,
const Expr& right);
1020 virtual Expr recordExpr(
const std::string& field,
const Expr& expr);
1024 virtual Expr recordExpr(
const std::string& field0,
const Expr& expr0,
1025 const std::string& field1,
const Expr& expr1);
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);
1040 virtual Expr recordExpr(
const std::vector<std::string>& fields,
1041 const std::vector<Expr>& exprs);
1046 virtual Expr recSelectExpr(
const Expr& record,
const std::string& field);
1053 virtual Expr recUpdateExpr(
const Expr& record,
const std::string& field,
1054 const Expr& newValue);
1068 virtual Expr readExpr(
const Expr& array,
const Expr& index);
1071 virtual Expr writeExpr(
const Expr& array,
const Expr& index,
1072 const Expr& newValue);
1086 virtual Expr newBVConstExpr(
const std::string& s,
int base = 2);
1088 virtual Expr newBVConstExpr(
const std::vector<bool>& bits);
1090 virtual Expr newBVConstExpr(
const Rational& r,
int len = 0);
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);
1098 virtual Expr newBVNegExpr(
const Expr& t1);
1100 virtual Expr newBVAndExpr(
const Expr& t1,
const Expr& t2);
1101 virtual Expr newBVAndExpr(
const std::vector<Expr>& kids);
1103 virtual Expr newBVOrExpr(
const Expr& t1,
const Expr& t2);
1104 virtual Expr newBVOrExpr(
const std::vector<Expr>& kids);
1106 virtual Expr newBVXorExpr(
const Expr& t1,
const Expr& t2);
1107 virtual Expr newBVXorExpr(
const std::vector<Expr>& kids);
1109 virtual Expr newBVXnorExpr(
const Expr& t1,
const Expr& t2);
1110 virtual Expr newBVXnorExpr(
const std::vector<Expr>& kids);
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);
1117 virtual Expr newBVLTExpr(
const Expr& t1,
const Expr& t2);
1118 virtual Expr newBVLEExpr(
const Expr& t1,
const Expr& t2);
1121 virtual Expr newBVSLTExpr(
const Expr& t1,
const Expr& t2);
1122 virtual Expr newBVSLEExpr(
const Expr& t1,
const Expr& t2);
1125 virtual Expr newSXExpr(
const Expr& t1,
int len);
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,
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);
1143 virtual Expr newFixedLeftShiftExpr(
const Expr& t1,
int r);
1145 virtual Expr newFixedConstWidthLeftShiftExpr(
const Expr& t1,
int r);
1147 virtual Expr newFixedRightShiftExpr(
const Expr& t1,
int r);
1151 virtual Expr newBVLSHR(
const Expr& t1,
const Expr& t2);
1153 virtual Expr newBVASHR(
const Expr& t1,
const Expr& t2);
1168 virtual Expr tupleExpr(
const std::vector<Expr>& exprs);
1171 virtual Expr tupleSelectExpr(
const Expr& tuple,
int index);
1174 virtual Expr tupleUpdateExpr(
const Expr& tuple,
int index,
1175 const Expr& newValue);
1178 virtual Expr datatypeConsExpr(
const std::string& constructor,
const std::vector<Expr>& args);
1181 virtual Expr datatypeSelExpr(
const std::string& selector,
const Expr& arg);
1184 virtual Expr datatypeTestExpr(
const std::string& constructor,
const Expr& arg);
1194 virtual Expr boundVarExpr(
const std::string& name,
1195 const std::string& uid,
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);
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);
1228 virtual Expr existsExpr(
const std::vector<Expr>& vars,
const Expr& body);
1231 virtual Op lambdaExpr(
const std::vector<Expr>& vars,
const Expr& body);
1234 virtual Op transClosure(
const Op& op);
1244 virtual Expr simulateExpr(
const Expr& f,
const Expr& s0,
1245 const std::vector<Expr>& inputs,
1264 virtual void setResourceLimit(
unsigned limit);
1271 virtual void setTimeLimit(
unsigned limit);
1276 virtual void assertFormula(
const Expr& e);
1282 virtual void registerAtom(
const Expr& e);
1287 virtual Expr getImpliedLiteral();
1290 virtual Expr simplify(
const Expr& e);
1320 virtual void returnFromCheck();
1328 virtual void getUserAssumptions(std::vector<Expr>& assumptions);
1334 virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
1339 virtual void getAssumptions(std::vector<Expr>& assumptions);
1347 virtual void getAssumptionsUsed(std::vector<Expr>& assumptions);
1349 virtual Expr getProofQuery();
1361 virtual void getCounterExample(std::vector<Expr>& assumptions,
1386 virtual bool inconsistent(std::vector<Expr>& assumptions);
1389 virtual bool inconsistent();
1400 virtual bool incomplete();
1409 virtual bool incomplete(std::vector<std::string>& reasons);
1414 virtual Proof getProof();
1418 virtual Expr getValue(
const Expr& e);
1422 virtual Expr getTCC();
1425 virtual void getAssumptionsTCC(std::vector<Expr>& assumptions);
1429 virtual Proof getProofTCC();
1437 virtual Expr getClosure();
1441 virtual Proof getProofClosure();
1464 virtual int stackLevel();
1467 virtual void push();
1477 virtual void popto(
int stackLevel);
1480 virtual int scopeLevel();
1486 virtual void pushScope();
1492 virtual void popScope();
1501 virtual void poptoScope(
int scopeLevel);
1504 virtual Context* getCurrentContext();
1507 virtual void reset();
1510 virtual void logAnnotation(
const Expr& annot);
1523 virtual void loadFile(
const std::string& fileName,
1526 bool calledFromParser =
false);
1529 virtual void loadFile(std::istream& is,
1547 virtual void printStatistics();
std::vector< std::pair< std::string, bool > > * sv
struct CVC4::options::help__option_t help
Expr class for CVC3 compatibility layer.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
int compare(const Expr &e1, const Expr &e2)
#define PRESENTATION_LANG
SmtEngine: the main public entry point of libcvc4.
A simple representation of a cardinality.
Class encapsulating CVC4 expression types.
[[ Add one-line brief description here ]]
A multi-precision rational constant.
bit-vector unsigned greater than
CLFlagType
Different types of command line flags.
language::input::Language InputLanguage
bit-vector unsigned less than
A collection of state for use by parser implementations.
CVC4's exception base class and some associated utilities.
void insert(Expr a, Expr b)
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
a fixed-width bit-vector constant
Exception thrown in the case of type-checking errors.
std::string QueryResultToString(QueryResult query_result)
struct CVC4::options::interactive__option_t interactive
std::ostream & operator<<(std::ostream &out, CLFlagType clft)
CVC4::TypeCheckingException TypecheckException
real division (user symbol)
std::string int2string(int n)
Macros that should be defined everywhere during the building of the libraries and driver binary...
greater than or equal, x >= y
CVC3 API (compatibility layer for CVC4)
less than or equal, x <= y
bool operator==(const Cardinality &c, CVC3CardinalityKind d)
struct CVC4::options::out__option_t out
bit-vector unsigned less than or equal
CVC4::Statistics Statistics
bool operator!=(const Cardinality &c, CVC3CardinalityKind d)
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.
bit-vector unsigned greater than or equal
Interface for expression types.