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" 90 typedef enum CVC4_PUBLIC {
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);
165 CLFlagType getType()
const;
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);
232 class CVC4_PUBLIC ExprManager;
233 class CVC4_PUBLIC Context;
267 class CVC4_PUBLIC
Expr;
270 class CVC4_PUBLIC
ExprMap :
public std::map<Expr, T> {
274 class CVC4_PUBLIC
ExprHashMap :
public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
284 Expr getExpr()
const;
288 Type operator[](
int i)
const;
292 bool isSubtype()
const;
298 Expr enumerateFinite(Unsigned n)
const;
300 Unsigned sizeFinite()
const;
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;
329 Expr eqExpr(
const Expr& right)
const;
330 Expr notExpr()
const;
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;
339 Expr substExpr(
const std::vector<Expr>& oldTerms,
340 const std::vector<Expr>& newTerms)
const;
343 Expr operator!()
const;
344 Expr operator&&(
const Expr& right)
const;
345 Expr operator||(
const Expr& right)
const;
347 static size_t hash(
const Expr& e);
353 bool isFalse()
const;
355 bool isBoolConst()
const;
357 bool isBoundVar()
const;
358 bool isString()
const;
359 bool isSymbol()
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;
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;
381 std::string getName()
const;
382 std::string getUid()
const;
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;
400 bool isRational()
const;
401 bool isSkolem()
const;
403 const Rational& getRational()
const;
407 Expr getOpExpr()
const;
408 int getOpKind()
const;
409 Expr getExpr()
const;
412 std::vector< std::vector<Expr> > getTriggers()
const;
415 ExprManager* getEM()
const;
418 std::vector<Expr> getKids()
const;
421 ExprIndex getIndex()
const;
431 Expr operator[](
int i)
const;
434 Expr unnegate()
const;
437 bool isInitialized()
const;
440 Type getType()
const;
442 Type lookupType()
const;
447 void pprintnodag()
const;
455 std::string getKindName(
int kind);
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 519 std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
520 std::set<ValidityChecker*> d_reverseEmmc;
523 std::vector<Expr> d_exprTypeMapRemove;
524 unsigned d_stackLevel;
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;
531 ConstructorMap d_constructors;
532 SelectorMap d_selectors;
554 virtual CLFlags& getFlags()
const;
556 virtual void reprocessFlags();
587 virtual Type boolType();
589 virtual Type realType();
591 virtual Type intType();
597 virtual Type subrangeType(
const Expr& l,
const Expr& r);
609 virtual Type subtypeType(
const Expr& pred,
const Expr& witness);
613 virtual Type tupleType(
const Type& type0,
const Type& type1);
616 virtual Type tupleType(
const Type& type0,
const Type& type1,
619 virtual Type tupleType(
const std::vector<Type>& types);
623 virtual Type recordType(
const std::string& field,
const Type& type);
627 virtual Type recordType(
const std::string& field0,
const Type& type0,
628 const std::string& field1,
const Type& type1);
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);
636 virtual Type recordType(
const std::vector<std::string>& fields,
637 const std::vector<Type>& types);
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);
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);
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);
670 virtual Type arrayType(
const Type& typeIndex,
const Type& typeData);
673 virtual Type bitvecType(
int n);
676 virtual Type funType(
const Type& typeDom,
const Type& typeRan);
679 virtual Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan);
682 virtual Type createType(
const std::string& typeName);
685 virtual Type createType(
const std::string& typeName,
const Type& def);
688 virtual Type lookupType(
const std::string& typeName);
702 virtual ExprManager* getEM();
710 virtual Expr varExpr(
const std::string& name,
const Type& type);
713 virtual Expr varExpr(
const std::string& name,
const Type& type,
724 virtual Expr lookupVar(
const std::string& name,
Type* type);
727 virtual Type getType(
const Expr& e);
730 virtual Type getBaseType(
const Expr& e);
733 virtual Type getBaseType(
const Type& t);
739 virtual Expr stringExpr(
const std::string& str);
742 virtual Expr idExpr(
const std::string& name);
765 virtual Expr listExpr(
const std::vector<Expr>& kids);
768 virtual Expr listExpr(
const Expr& e1);
777 virtual Expr listExpr(
const std::string& op,
778 const std::vector<Expr>& kids);
781 virtual Expr listExpr(
const std::string& op,
const Expr& e1);
784 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
788 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
792 virtual void printExpr(
const Expr& e);
795 virtual void printExpr(
const Expr& e, std::ostream& os);
798 virtual Expr parseExpr(
const Expr& e);
801 virtual Type parseType(
const Expr& e);
811 virtual Expr importExpr(
const Expr& e);
815 virtual Type importType(
const Type& t);
818 virtual void cmdsFromString(
const std::string& s,
825 virtual Expr exprFromString(
const std::string& e,
842 virtual Expr trueExpr();
845 virtual Expr falseExpr();
848 virtual Expr notExpr(
const Expr& child);
851 virtual Expr andExpr(
const Expr& left,
const Expr& right);
854 virtual Expr andExpr(
const std::vector<Expr>& children);
857 virtual Expr orExpr(
const Expr& left,
const Expr& right);
860 virtual Expr orExpr(
const std::vector<Expr>& children);
863 virtual Expr impliesExpr(
const Expr& hyp,
const Expr& conc);
866 virtual Expr iffExpr(
const Expr& left,
const Expr& right);
873 virtual Expr eqExpr(
const Expr& child0,
const Expr& child1);
881 virtual Expr iteExpr(
const Expr& ifpart,
const Expr& thenpart,
882 const Expr& elsepart);
888 virtual Expr distinctExpr(
const std::vector<Expr>& children);
905 virtual Op createOp(
const std::string& name,
const Type& type);
908 virtual Op createOp(
const std::string& name,
const Type& type,
919 virtual Op lookupOp(
const std::string& name,
Type* type);
922 virtual Expr funExpr(
const Op& op,
const Expr& child);
925 virtual Expr funExpr(
const Op& op,
const Expr& left,
const Expr& right);
928 virtual Expr funExpr(
const Op& op,
const Expr& child0,
929 const Expr& child1,
const Expr& child2);
932 virtual Expr funExpr(
const Op& op,
const std::vector<Expr>& children);
953 virtual bool addPairToArithOrder(
const Expr& smaller,
const Expr& bigger);
960 virtual Expr ratExpr(
int n,
int d = 1);
967 virtual Expr ratExpr(
const std::string& n,
const std::string& d,
int base);
975 virtual Expr ratExpr(
const std::string& n,
int base = 10);
978 virtual Expr uminusExpr(
const Expr& child);
981 virtual Expr plusExpr(
const Expr& left,
const Expr& right);
984 virtual Expr plusExpr(
const std::vector<Expr>& children);
987 virtual Expr minusExpr(
const Expr& left,
const Expr& right);
990 virtual Expr multExpr(
const Expr& left,
const Expr& right);
996 virtual Expr divideExpr(
const Expr& numerator,
const Expr& denominator);
999 virtual Expr ltExpr(
const Expr& left,
const Expr& right);
1002 virtual Expr leExpr(
const Expr& left,
const Expr& right);
1005 virtual Expr gtExpr(
const Expr& left,
const Expr& right);
1008 virtual Expr geExpr(
const Expr& left,
const Expr& right);
1022 virtual Expr recordExpr(
const std::string& field,
const Expr& expr);
1026 virtual Expr recordExpr(
const std::string& field0,
const Expr& expr0,
1027 const std::string& field1,
const Expr& expr1);
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);
1042 virtual Expr recordExpr(
const std::vector<std::string>& fields,
1043 const std::vector<Expr>& exprs);
1048 virtual Expr recSelectExpr(
const Expr& record,
const std::string& field);
1055 virtual Expr recUpdateExpr(
const Expr& record,
const std::string& field,
1056 const Expr& newValue);
1070 virtual Expr readExpr(
const Expr& array,
const Expr& index);
1073 virtual Expr writeExpr(
const Expr& array,
const Expr& index,
1074 const Expr& newValue);
1088 virtual Expr newBVConstExpr(
const std::string& s,
int base = 2);
1090 virtual Expr newBVConstExpr(
const std::vector<bool>& bits);
1092 virtual Expr newBVConstExpr(
const Rational& r,
int len = 0);
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);
1100 virtual Expr newBVNegExpr(
const Expr& t1);
1102 virtual Expr newBVAndExpr(
const Expr& t1,
const Expr& t2);
1103 virtual Expr newBVAndExpr(
const std::vector<Expr>& kids);
1105 virtual Expr newBVOrExpr(
const Expr& t1,
const Expr& t2);
1106 virtual Expr newBVOrExpr(
const std::vector<Expr>& kids);
1108 virtual Expr newBVXorExpr(
const Expr& t1,
const Expr& t2);
1109 virtual Expr newBVXorExpr(
const std::vector<Expr>& kids);
1111 virtual Expr newBVXnorExpr(
const Expr& t1,
const Expr& t2);
1112 virtual Expr newBVXnorExpr(
const std::vector<Expr>& kids);
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);
1119 virtual Expr newBVLTExpr(
const Expr& t1,
const Expr& t2);
1120 virtual Expr newBVLEExpr(
const Expr& t1,
const Expr& t2);
1123 virtual Expr newBVSLTExpr(
const Expr& t1,
const Expr& t2);
1124 virtual Expr newBVSLEExpr(
const Expr& t1,
const Expr& t2);
1127 virtual Expr newSXExpr(
const Expr& t1,
int len);
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,
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);
1145 virtual Expr newFixedLeftShiftExpr(
const Expr& t1,
int r);
1147 virtual Expr newFixedConstWidthLeftShiftExpr(
const Expr& t1,
int r);
1149 virtual Expr newFixedRightShiftExpr(
const Expr& t1,
int r);
1153 virtual Expr newBVLSHR(
const Expr& t1,
const Expr& t2);
1155 virtual Expr newBVASHR(
const Expr& t1,
const Expr& t2);
1170 virtual Expr tupleExpr(
const std::vector<Expr>& exprs);
1173 virtual Expr tupleSelectExpr(
const Expr& tuple,
int index);
1176 virtual Expr tupleUpdateExpr(
const Expr& tuple,
int index,
1177 const Expr& newValue);
1180 virtual Expr datatypeConsExpr(
const std::string& constructor,
const std::vector<Expr>& args);
1183 virtual Expr datatypeSelExpr(
const std::string& selector,
const Expr& arg);
1186 virtual Expr datatypeTestExpr(
const std::string& constructor,
const Expr& arg);
1196 virtual Expr boundVarExpr(
const std::string& name,
1197 const std::string& uid,
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);
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);
1230 virtual Expr existsExpr(
const std::vector<Expr>& vars,
const Expr& body);
1233 virtual Op lambdaExpr(
const std::vector<Expr>& vars,
const Expr& body);
1236 virtual Op transClosure(
const Op& op);
1246 virtual Expr simulateExpr(
const Expr& f,
const Expr& s0,
1247 const std::vector<Expr>& inputs,
1266 virtual void setResourceLimit(
unsigned limit);
1273 virtual void setTimeLimit(
unsigned limit);
1278 virtual void assertFormula(
const Expr& e);
1284 virtual void registerAtom(
const Expr& e);
1289 virtual Expr getImpliedLiteral();
1292 virtual Expr simplify(
const Expr& e);
1303 virtual QueryResult query(
const Expr& e);
1307 virtual QueryResult checkUnsat(
const Expr& e);
1312 virtual QueryResult checkContinue();
1317 virtual QueryResult restart(
const Expr& e);
1322 virtual void returnFromCheck();
1330 virtual void getUserAssumptions(std::vector<Expr>& assumptions);
1336 virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
1341 virtual void getAssumptions(std::vector<Expr>& assumptions);
1349 virtual void getAssumptionsUsed(std::vector<Expr>& assumptions);
1351 virtual Expr getProofQuery();
1363 virtual void getCounterExample(std::vector<Expr>& assumptions,
1375 virtual QueryResult tryModelGeneration();
1381 virtual FormulaValue value(
const Expr& e);
1388 virtual bool inconsistent(std::vector<Expr>& assumptions);
1391 virtual bool inconsistent();
1402 virtual bool incomplete();
1411 virtual bool incomplete(std::vector<std::string>& reasons);
1416 virtual Proof getProof();
1420 virtual Expr getValue(
const Expr& e);
1424 virtual Expr getTCC();
1427 virtual void getAssumptionsTCC(std::vector<Expr>& assumptions);
1431 virtual Proof getProofTCC();
1439 virtual Expr getClosure();
1443 virtual Proof getProofClosure();
1466 virtual int stackLevel();
1469 virtual void push();
1479 virtual void popto(
int stackLevel);
1482 virtual int scopeLevel();
1488 virtual void pushScope();
1494 virtual void popScope();
1503 virtual void poptoScope(
int scopeLevel);
1506 virtual Context* getCurrentContext();
1509 virtual void reset();
1512 virtual void logAnnotation(
const Expr& annot);
1525 virtual void loadFile(
const std::string& fileName,
1528 bool calledFromParser =
false);
1531 virtual void loadFile(std::istream& is,
1546 virtual Statistics getStatistics();
1549 virtual void printStatistics();
std::vector< std::pair< std::string, bool > > * sv
Iterator type for the children of an Expr.
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 ]]
subtraction of two bit-vectors (68)
A multi-precision rational constant.
bit-vector unsigned greater than (the two bit-vector parameters must have same width) (82) ...
CLFlagType
Different types of command line flags.
language::input::Language InputLanguage
bit-vector unsigned less than (the two bit-vector parameters must have same width) (80) ...
A collection of state for use by parser implementations.
CVC4's exception base class and some associated utilities.
array select; first parameter is an array term, second is the selection index (109) ...
void insert(Expr a, Expr b)
addition of two or more bit-vectors (67)
a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (56) ...
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)
bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (99) ...
CVC4::TypeCheckingException TypecheckException
real division, division by 0 undefined (user symbol) (36)
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 (51)
CVC3 API (compatibility layer for CVC4)
less than or equal, x <= y (49)
bool operator==(const Cardinality &c, CVC3CardinalityKind d)
equality (two parameters only, sorts must match) (8)
struct CVC4::options::out__option_t out
CVC4::Expr::const_iterator iterator
concatenation of two or more bit-vectors (57)
bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (81) ...
CVC4::Statistics Statistics
Vector of pair<string, bool>
array store; first parameter is an array term, second is the store index, third is the term to store ...
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 (the two bit-vector parameters must have same width) (83) ...
Interface for expression types.