22 #ifndef _cvc3__include__vc_h_
23 #define _cvc3__include__vc_h_
107 virtual CLFlags& getFlags()
const = 0;
109 virtual void reprocessFlags() = 0;
140 virtual Type boolType() = 0;
142 virtual Type realType() = 0;
144 virtual Type intType() = 0;
150 virtual Type subrangeType(
const Expr& l,
const Expr& r) = 0;
162 virtual Type subtypeType(
const Expr& pred,
const Expr& witness) = 0;
166 virtual Type tupleType(
const Type& type0,
const Type& type1) = 0;
169 virtual Type tupleType(
const Type& type0,
const Type& type1,
170 const Type& type2) = 0;
172 virtual Type tupleType(
const std::vector<Type>& types) = 0;
176 virtual Type recordType(
const std::string& field,
const Type& type) = 0;
180 virtual Type recordType(
const std::string& field0,
const Type& type0,
181 const std::string& field1,
const Type& type1) = 0;
184 virtual Type recordType(
const std::string& field0,
const Type& type0,
185 const std::string& field1,
const Type& type1,
186 const std::string& field2,
const Type& type2) = 0;
189 virtual Type recordType(
const std::vector<std::string>& fields,
190 const std::vector<Type>& types) = 0;
198 virtual Type dataType(
const std::string& name,
199 const std::string& constructor,
200 const std::vector<std::string>& selectors,
201 const std::vector<Expr>& types) = 0;
207 virtual Type dataType(
const std::string& name,
208 const std::vector<std::string>& constructors,
209 const std::vector<std::vector<std::string> >& selectors,
210 const std::vector<std::vector<Expr> >& types) = 0;
216 virtual void dataType(
const std::vector<std::string>& names,
217 const std::vector<std::vector<std::string> >& constructors,
218 const std::vector<std::vector<std::vector<std::string> > >& selectors,
219 const std::vector<std::vector<std::vector<Expr> > >& types,
220 std::vector<Type>& returnTypes) = 0;
226 virtual Type bitvecType(
int n) = 0;
229 virtual Type funType(
const Type& typeDom,
const Type& typeRan) = 0;
232 virtual Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan) = 0;
235 virtual Type createType(
const std::string& typeName) = 0;
238 virtual Type createType(
const std::string& typeName,
const Type& def) = 0;
241 virtual Type lookupType(
const std::string& typeName) = 0;
263 virtual Expr varExpr(
const std::string& name,
const Type& type) = 0;
266 virtual Expr varExpr(
const std::string& name,
const Type& type,
267 const Expr& def) = 0;
277 virtual Expr lookupVar(
const std::string& name,
Type* type) = 0;
280 virtual Type getType(
const Expr& e) = 0;
283 virtual Type getBaseType(
const Expr& e) = 0;
286 virtual Type getBaseType(
const Type& t) = 0;
289 virtual Expr getTypePred(
const Type&t,
const Expr& e) = 0;
292 virtual Expr stringExpr(
const std::string& str) = 0;
295 virtual Expr idExpr(
const std::string& name) = 0;
318 virtual Expr listExpr(
const std::vector<Expr>& kids) = 0;
321 virtual Expr listExpr(
const Expr& e1) = 0;
324 virtual Expr listExpr(
const Expr& e1,
const Expr& e2) = 0;
330 virtual Expr listExpr(
const std::string& op,
331 const std::vector<Expr>& kids) = 0;
334 virtual Expr listExpr(
const std::string& op,
const Expr& e1) = 0;
337 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
341 virtual Expr listExpr(
const std::string& op,
const Expr& e1,
342 const Expr& e2,
const Expr& e3) = 0;
345 virtual void printExpr(
const Expr& e) = 0;
348 virtual void printExpr(
const Expr& e, std::ostream& os) = 0;
351 virtual Expr parseExpr(
const Expr& e) = 0;
354 virtual Type parseType(
const Expr& e) = 0;
364 virtual Expr importExpr(
const Expr& e) = 0;
368 virtual Type importType(
const Type& t) = 0;
371 virtual void cmdsFromString(
const std::string& s,
375 virtual Expr exprFromString(
const std::string& e) = 0;
391 virtual Expr trueExpr() = 0;
394 virtual Expr falseExpr() = 0;
397 virtual Expr notExpr(
const Expr& child) = 0;
403 virtual Expr andExpr(
const std::vector<Expr>& children) = 0;
409 virtual Expr orExpr(
const std::vector<Expr>& children) = 0;
412 virtual Expr impliesExpr(
const Expr& hyp,
const Expr& conc) = 0;
422 virtual Expr eqExpr(
const Expr& child0,
const Expr& child1) = 0;
430 virtual Expr iteExpr(
const Expr& ifpart,
const Expr& thenpart,
431 const Expr& elsepart) = 0;
437 virtual Expr distinctExpr(
const std::vector<Expr>& children) = 0;
454 virtual Op createOp(
const std::string& name,
const Type& type) = 0;
457 virtual Op createOp(
const std::string& name,
const Type& type,
458 const Expr& def) = 0;
468 virtual Op lookupOp(
const std::string& name,
Type* type) = 0;
471 virtual Expr funExpr(
const Op& op,
const Expr& child) = 0;
477 virtual Expr funExpr(
const Op& op,
const Expr& child0,
478 const Expr& child1,
const Expr& child2) = 0;
481 virtual Expr funExpr(
const Op& op,
const std::vector<Expr>& children) = 0;
502 virtual bool addPairToArithOrder(
const Expr& smaller,
const Expr& bigger) = 0;
509 virtual Expr ratExpr(
int n,
int d = 1) = 0;
516 virtual Expr ratExpr(
const std::string& n,
const std::string& d,
int base) = 0;
524 virtual Expr ratExpr(
const std::string& n,
int base = 10) = 0;
533 virtual Expr plusExpr(
const std::vector<Expr>& children) = 0;
571 virtual Expr recordExpr(
const std::string& field,
const Expr& expr) = 0;
575 virtual Expr recordExpr(
const std::string& field0,
const Expr& expr0,
576 const std::string& field1,
const Expr& expr1) = 0;
580 virtual Expr recordExpr(
const std::string& field0,
const Expr& expr0,
581 const std::string& field1,
const Expr& expr1,
582 const std::string& field2,
const Expr& expr2) = 0;
591 virtual Expr recordExpr(
const std::vector<std::string>& fields,
592 const std::vector<Expr>& exprs) = 0;
597 virtual Expr recSelectExpr(
const Expr& record,
const std::string& field) = 0;
604 virtual Expr recUpdateExpr(
const Expr& record,
const std::string& field,
605 const Expr& newValue) = 0;
619 virtual Expr readExpr(
const Expr& array,
const Expr& index) = 0;
622 virtual Expr writeExpr(
const Expr& array,
const Expr& index,
623 const Expr& newValue) = 0;
637 virtual Expr newBVConstExpr(
const std::string& s,
int base = 2) = 0;
639 virtual Expr newBVConstExpr(
const std::vector<bool>& bits) = 0;
641 virtual Expr newBVConstExpr(
const Rational& r,
int len = 0) = 0;
644 virtual Expr newConcatExpr(
const Expr& t1,
const Expr& t2) = 0;
645 virtual Expr newConcatExpr(
const std::vector<Expr>& kids) = 0;
646 virtual Expr newBVExtractExpr(
const Expr& e,
int hi,
int low) = 0;
649 virtual Expr newBVNegExpr(
const Expr& t1) = 0;
651 virtual Expr newBVAndExpr(
const Expr& t1,
const Expr& t2) = 0;
652 virtual Expr newBVAndExpr(
const std::vector<Expr>& kids) = 0;
654 virtual Expr newBVOrExpr(
const Expr& t1,
const Expr& t2) = 0;
655 virtual Expr newBVOrExpr(
const std::vector<Expr>& kids) = 0;
657 virtual Expr newBVXorExpr(
const Expr& t1,
const Expr& t2) = 0;
658 virtual Expr newBVXorExpr(
const std::vector<Expr>& kids) = 0;
660 virtual Expr newBVXnorExpr(
const Expr& t1,
const Expr& t2) = 0;
661 virtual Expr newBVXnorExpr(
const std::vector<Expr>& kids) = 0;
663 virtual Expr newBVNandExpr(
const Expr& t1,
const Expr& t2) = 0;
664 virtual Expr newBVNorExpr(
const Expr& t1,
const Expr& t2) = 0;
665 virtual Expr newBVCompExpr(
const Expr& t1,
const Expr& t2) = 0;
668 virtual Expr newBVLTExpr(
const Expr& t1,
const Expr& t2) = 0;
669 virtual Expr newBVLEExpr(
const Expr& t1,
const Expr& t2) = 0;
672 virtual Expr newBVSLTExpr(
const Expr& t1,
const Expr& t2) = 0;
673 virtual Expr newBVSLEExpr(
const Expr& t1,
const Expr& t2) = 0;
676 virtual Expr newSXExpr(
const Expr& t1,
int len) = 0;
679 virtual Expr newBVUminusExpr(
const Expr& t1) = 0;
680 virtual Expr newBVSubExpr(
const Expr& t1,
const Expr& t2) = 0;
682 virtual Expr newBVPlusExpr(
int numbits,
const std::vector<Expr>& k) = 0;
683 virtual Expr newBVPlusExpr(
int numbits,
const Expr& t1,
const Expr& t2) = 0;
684 virtual Expr newBVMultExpr(
int numbits,
685 const Expr& t1,
const Expr& t2) = 0;
687 virtual Expr newBVUDivExpr(
const Expr& t1,
const Expr& t2) = 0;
688 virtual Expr newBVURemExpr(
const Expr& t1,
const Expr& t2) = 0;
689 virtual Expr newBVSDivExpr(
const Expr& t1,
const Expr& t2) = 0;
690 virtual Expr newBVSRemExpr(
const Expr& t1,
const Expr& t2) = 0;
691 virtual Expr newBVSModExpr(
const Expr& t1,
const Expr& t2) = 0;
694 virtual Expr newFixedLeftShiftExpr(
const Expr& t1,
int r) = 0;
696 virtual Expr newFixedConstWidthLeftShiftExpr(
const Expr& t1,
int r) = 0;
698 virtual Expr newFixedRightShiftExpr(
const Expr& t1,
int r) = 0;
700 virtual Expr newBVSHL(
const Expr& t1,
const Expr& t2) = 0;
702 virtual Expr newBVLSHR(
const Expr& t1,
const Expr& t2) = 0;
704 virtual Expr newBVASHR(
const Expr& t1,
const Expr& t2) = 0;
719 virtual Expr tupleExpr(
const std::vector<Expr>& exprs) = 0;
722 virtual Expr tupleSelectExpr(
const Expr& tuple,
int index) = 0;
725 virtual Expr tupleUpdateExpr(
const Expr& tuple,
int index,
726 const Expr& newValue) = 0;
729 virtual Expr datatypeConsExpr(
const std::string& constructor,
const std::vector<Expr>& args) = 0;
732 virtual Expr datatypeSelExpr(
const std::string& selector,
const Expr& arg) = 0;
735 virtual Expr datatypeTestExpr(
const std::string& constructor,
const Expr& arg) = 0;
745 virtual Expr boundVarExpr(
const std::string& name,
746 const std::string& uid,
747 const Type& type) = 0;
750 virtual Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body) = 0;
752 virtual Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
753 const Expr& trigger) = 0;
755 virtual Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
756 const std::vector<Expr>& triggers) = 0;
758 virtual Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
759 const std::vector<std::vector<Expr> >& triggers) = 0;
770 virtual void setTriggers(
const Expr& e,
const std::vector<std::vector<Expr> > & triggers) = 0;
772 virtual void setTriggers(
const Expr& e,
const std::vector<Expr>& triggers) = 0;
774 virtual void setTrigger(
const Expr& e,
const Expr& trigger) = 0;
776 virtual void setMultiTrigger(
const Expr& e,
const std::vector<Expr>& multiTrigger) = 0;
779 virtual Expr existsExpr(
const std::vector<Expr>& vars,
const Expr& body) = 0;
782 virtual Op lambdaExpr(
const std::vector<Expr>& vars,
const Expr& body) = 0;
785 virtual Op transClosure(
const Op& op) = 0;
795 virtual Expr simulateExpr(
const Expr& f,
const Expr& s0,
796 const std::vector<Expr>& inputs,
815 virtual void setResourceLimit(
unsigned limit) = 0;
822 virtual void setTimeLimit(
unsigned limit) = 0;
827 virtual void assertFormula(
const Expr& e) = 0;
833 virtual void registerAtom(
const Expr& e) = 0;
838 virtual Expr getImpliedLiteral() = 0;
841 virtual Expr simplify(
const Expr& e) = 0;
871 virtual void returnFromCheck() = 0;
879 virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0;
885 virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0;
890 virtual void getAssumptions(std::vector<Expr>& assumptions) = 0;
898 virtual void getAssumptionsUsed(std::vector<Expr>& assumptions) = 0;
900 virtual Expr getProofQuery() = 0;
912 virtual void getCounterExample(std::vector<Expr>& assumptions,
913 bool inOrder=
true) = 0;
937 virtual bool inconsistent(std::vector<Expr>& assumptions) = 0;
940 virtual bool inconsistent() = 0;
951 virtual bool incomplete() = 0;
960 virtual bool incomplete(std::vector<std::string>& reasons) = 0;
965 virtual Proof getProof() = 0;
973 virtual Expr getAssignment() = 0;
977 virtual Expr getTCC() = 0;
980 virtual void getAssumptionsTCC(std::vector<Expr>& assumptions) = 0;
984 virtual Proof getProofTCC() = 0;
992 virtual Expr getClosure() = 0;
996 virtual Proof getProofClosure() = 0;
1019 virtual int stackLevel() = 0;
1022 virtual void push() = 0;
1025 virtual void pop() = 0;
1032 virtual void popto(
int stackLevel) = 0;
1035 virtual int scopeLevel() = 0;
1041 virtual void pushScope() = 0;
1047 virtual void popScope() = 0;
1056 virtual void poptoScope(
int scopeLevel) = 0;
1059 virtual Context* getCurrentContext() = 0;
1062 virtual void reset() = 0;
1065 virtual void logAnnotation(
const Expr& annot) = 0;
1078 virtual void loadFile(
const std::string& fileName,
1080 bool interactive =
false,
1081 bool calledFromParser =
false) = 0;
1084 virtual void loadFile(std::istream& is,
1086 bool interactive =
false) = 0;
1102 virtual void printStatistics() = 0;