|
| ValidityChecker () |
| Constructor. More...
|
|
virtual | ~ValidityChecker () |
| Destructor. More...
|
|
virtual CLFlags & | getFlags () const |
| Return the set of command-line flags. More...
|
|
virtual void | reprocessFlags () |
| Force reprocessing of all flags. More...
|
|
|
Methods for creating and looking up types
- See Also
- class Type
|
virtual Type | boolType () |
| Create type BOOLEAN. More...
|
|
virtual Type | realType () |
| Create type REAL. More...
|
|
virtual Type | intType () |
| Create type INT. More...
|
|
virtual Type | subrangeType (const Expr &l, const Expr &r) |
| Create a subrange type [l..r]. More...
|
|
virtual Type | subtypeType (const Expr &pred, const Expr &witness) |
| Creates a subtype defined by the given predicate. More...
|
|
virtual Type | tupleType (const Type &type0, const Type &type1) |
| 2-element tuple More...
|
|
virtual Type | tupleType (const Type &type0, const Type &type1, const Type &type2) |
| 3-element tuple More...
|
|
virtual Type | tupleType (const std::vector< Type > &types) |
| n-element tuple (from a vector of types) More...
|
|
virtual Type | recordType (const std::string &field, const Type &type) |
| 1-element record More...
|
|
virtual Type | recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1) |
| 2-element record More...
|
|
virtual Type | recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2) |
| 3-element record More...
|
|
virtual Type | recordType (const std::vector< std::string > &fields, const std::vector< Type > &types) |
| n-element record (fields and types must be of the same length) More...
|
|
virtual Type | dataType (const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types) |
| Single datatype, single constructor. More...
|
|
virtual Type | dataType (const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types) |
| Single datatype, multiple constructors. More...
|
|
virtual void | dataType (const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes) |
| Multiple datatypes. More...
|
|
virtual Type | arrayType (const Type &typeIndex, const Type &typeData) |
| Create an array type (ARRAY typeIndex OF typeData) More...
|
|
virtual Type | bitvecType (int n) |
| Create a bitvector type of length n. More...
|
|
virtual Type | funType (const Type &typeDom, const Type &typeRan) |
| Create a function type typeDom -> typeRan. More...
|
|
virtual Type | funType (const std::vector< Type > &typeDom, const Type &typeRan) |
| Create a function type (t1,t2,...,tn) -> typeRan. More...
|
|
virtual Type | createType (const std::string &typeName) |
| Create named user-defined uninterpreted type. More...
|
|
virtual Type | createType (const std::string &typeName, const Type &def) |
| Create named user-defined interpreted type (type abbreviation) More...
|
|
virtual Type | lookupType (const std::string &typeName) |
| Lookup a user-defined (uninterpreted) type by name. Returns Null if none. More...
|
|
|
- See Also
- class Expr
-
class ExprManager
|
virtual ExprManager * | getEM () |
| Return the ExprManager. More...
|
|
virtual Expr | varExpr (const std::string &name, const Type &type) |
| Create a variable with a given name and type. More...
|
|
virtual Expr | varExpr (const std::string &name, const Type &type, const Expr &def) |
| Create a variable with a given name, type, and value. More...
|
|
virtual Expr | lookupVar (const std::string &name, Type *type) |
| Get the variable associated with a name, and its type. More...
|
|
virtual Type | getType (const Expr &e) |
| Get the type of the Expr. More...
|
|
virtual Type | getBaseType (const Expr &e) |
| Get the largest supertype of the Expr. More...
|
|
virtual Type | getBaseType (const Type &t) |
| Get the largest supertype of the Type. More...
|
|
virtual Expr | getTypePred (const Type &t, const Expr &e) |
| Get the subtype predicate. More...
|
|
virtual Expr | stringExpr (const std::string &str) |
| Create a string Expr. More...
|
|
virtual Expr | idExpr (const std::string &name) |
| Create an ID Expr. More...
|
|
virtual Expr | listExpr (const std::vector< Expr > &kids) |
| Create a list Expr. More...
|
|
virtual Expr | listExpr (const Expr &e1) |
| Overloaded version of listExpr with one argument. More...
|
|
virtual Expr | listExpr (const Expr &e1, const Expr &e2) |
| Overloaded version of listExpr with two arguments. More...
|
|
virtual Expr | listExpr (const Expr &e1, const Expr &e2, const Expr &e3) |
| Overloaded version of listExpr with three arguments. More...
|
|
virtual Expr | listExpr (const std::string &op, const std::vector< Expr > &kids) |
| Overloaded version of listExpr with string operator and many arguments. More...
|
|
virtual Expr | listExpr (const std::string &op, const Expr &e1) |
| Overloaded version of listExpr with string operator and one argument. More...
|
|
virtual Expr | listExpr (const std::string &op, const Expr &e1, const Expr &e2) |
| Overloaded version of listExpr with string operator and two arguments. More...
|
|
virtual Expr | listExpr (const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3) |
| Overloaded version of listExpr with string operator and three arguments. More...
|
|
virtual void | printExpr (const Expr &e) |
| Prints e to the standard output. More...
|
|
virtual void | printExpr (const Expr &e, std::ostream &os) |
| Prints e to the given ostream. More...
|
|
virtual Expr | parseExpr (const Expr &e) |
| Parse an expression using a Theory-specific parser. More...
|
|
virtual Type | parseType (const Expr &e) |
| Parse a type expression using a Theory-specific parser. More...
|
|
virtual Expr | importExpr (const Expr &e) |
| Import the Expr from another instance of ValidityChecker. More...
|
|
virtual Type | importType (const Type &t) |
| Import the Type from another instance of ValidityChecker. More...
|
|
virtual void | cmdsFromString (const std::string &s, InputLanguage lang=PRESENTATION_LANG) |
| Parse a sequence of commands from a presentation language string. More...
|
|
virtual Expr | exprFromString (const std::string &e, InputLanguage lang=PRESENTATION_LANG) |
| Parse an expression from a presentation language string. More...
|
|
|
Methods for manipulating core expressions
Except for equality and ite, the children provided as arguments must be of type Boolean.
|
virtual Expr | trueExpr () |
| Return TRUE Expr. More...
|
|
virtual Expr | falseExpr () |
| Return FALSE Expr. More...
|
|
virtual Expr | notExpr (const Expr &child) |
| Create negation. More...
|
|
virtual Expr | andExpr (const Expr &left, const Expr &right) |
| Create 2-element conjunction. More...
|
|
virtual Expr | andExpr (const std::vector< Expr > &children) |
| Create n-element conjunction. More...
|
|
virtual Expr | orExpr (const Expr &left, const Expr &right) |
| Create 2-element disjunction. More...
|
|
virtual Expr | orExpr (const std::vector< Expr > &children) |
| Create n-element disjunction. More...
|
|
virtual Expr | impliesExpr (const Expr &hyp, const Expr &conc) |
| Create Boolean implication. More...
|
|
virtual Expr | iffExpr (const Expr &left, const Expr &right) |
| Create left IFF right (boolean equivalence) More...
|
|
virtual Expr | eqExpr (const Expr &child0, const Expr &child1) |
| Create an equality expression. More...
|
|
virtual Expr | iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart) |
| Create IF ifpart THEN thenpart ELSE elsepart ENDIF. More...
|
|
virtual Expr | distinctExpr (const std::vector< Expr > &children) |
| Create an expression asserting that all the children are different. More...
|
|
|
Methods for manipulating uninterpreted function expressions
|
virtual Op | createOp (const std::string &name, const Type &type) |
| Create a named uninterpreted function with a given type. More...
|
|
virtual Op | createOp (const std::string &name, const Type &type, const Expr &def) |
| Create a named user-defined function with a given type. More...
|
|
virtual Op | lookupOp (const std::string &name, Type *type) |
| Get the Op associated with a name, and its type. More...
|
|
virtual Expr | funExpr (const Op &op, const Expr &child) |
| Unary function application (op must be of function type) More...
|
|
virtual Expr | funExpr (const Op &op, const Expr &left, const Expr &right) |
| Binary function application (op must be of function type) More...
|
|
virtual Expr | funExpr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) |
| Ternary function application (op must be of function type) More...
|
|
virtual Expr | funExpr (const Op &op, const std::vector< Expr > &children) |
| n-ary function application (op must be of function type) More...
|
|
|
Methods for manipulating arithmetic expressions
These functions create arithmetic expressions. The children provided as arguments must be of type Real.
|
virtual bool | addPairToArithOrder (const Expr &smaller, const Expr &bigger) |
|
virtual Expr | ratExpr (int n, int d=1) |
| Create a rational number with numerator n and denominator d. More...
|
|
virtual Expr | ratExpr (const std::string &n, const std::string &d, int base) |
| Create a rational number with numerator n and denominator d. More...
|
|
virtual Expr | ratExpr (const std::string &n, int base=10) |
| Create a rational from a single string. More...
|
|
virtual Expr | uminusExpr (const Expr &child) |
| Unary minus. More...
|
|
virtual Expr | plusExpr (const Expr &left, const Expr &right) |
| Create 2-element sum (left + right) More...
|
|
virtual Expr | plusExpr (const std::vector< Expr > &children) |
| Create n-element sum. More...
|
|
virtual Expr | minusExpr (const Expr &left, const Expr &right) |
| Make a difference (left - right) More...
|
|
virtual Expr | multExpr (const Expr &left, const Expr &right) |
| Create a product (left * right) More...
|
|
virtual Expr | powExpr (const Expr &x, const Expr &n) |
| Create a power expression (x ^ n); n must be integer. More...
|
|
virtual Expr | divideExpr (const Expr &numerator, const Expr &denominator) |
| Create expression x / y. More...
|
|
virtual Expr | ltExpr (const Expr &left, const Expr &right) |
| Create (left < right) More...
|
|
virtual Expr | leExpr (const Expr &left, const Expr &right) |
| Create (left <= right) More...
|
|
virtual Expr | gtExpr (const Expr &left, const Expr &right) |
| Create (left > right) More...
|
|
virtual Expr | geExpr (const Expr &left, const Expr &right) |
| Create (left >= right) More...
|
|
|
Methods for manipulating record expressions
|
virtual Expr | recordExpr (const std::string &field, const Expr &expr) |
| Create a 1-element record value (# field := expr #) More...
|
|
virtual Expr | recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1) |
| Create a 2-element record value (# field0 := expr0, field1 := expr1 #) More...
|
|
virtual Expr | recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2) |
| Create a 3-element record value (# field_i := expr_i #) More...
|
|
virtual Expr | recordExpr (const std::vector< std::string > &fields, const std::vector< Expr > &exprs) |
| Create an n-element record value (# field_i := expr_i #) More...
|
|
virtual Expr | recSelectExpr (const Expr &record, const std::string &field) |
| Create record.field (field selection) More...
|
|
virtual Expr | recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue) |
| Record update; equivalent to "record WITH .field := newValue". More...
|
|
|
Methods for manipulating array expressions
|
virtual Expr | readExpr (const Expr &array, const Expr &index) |
| Create an expression array[index] (array access) More...
|
|
virtual Expr | writeExpr (const Expr &array, const Expr &index, const Expr &newValue) |
| Array update; equivalent to "array WITH index := newValue". More...
|
|
|
Methods for manipulating bitvector expressions
|
virtual Expr | newBVConstExpr (const std::string &s, int base=2) |
|
virtual Expr | newBVConstExpr (const std::vector< bool > &bits) |
|
virtual Expr | newBVConstExpr (const Rational &r, int len=0) |
|
virtual Expr | newConcatExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newConcatExpr (const std::vector< Expr > &kids) |
|
virtual Expr | newBVExtractExpr (const Expr &e, int hi, int low) |
|
virtual Expr | newBVNegExpr (const Expr &t1) |
|
virtual Expr | newBVAndExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVAndExpr (const std::vector< Expr > &kids) |
|
virtual Expr | newBVOrExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVOrExpr (const std::vector< Expr > &kids) |
|
virtual Expr | newBVXorExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVXorExpr (const std::vector< Expr > &kids) |
|
virtual Expr | newBVXnorExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVXnorExpr (const std::vector< Expr > &kids) |
|
virtual Expr | newBVNandExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVNorExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVCompExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVLTExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVLEExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVSLTExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVSLEExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newSXExpr (const Expr &t1, int len) |
|
virtual Expr | newBVUminusExpr (const Expr &t1) |
|
virtual Expr | newBVSubExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVPlusExpr (int numbits, const std::vector< Expr > &k) |
| 'numbits' is the number of bits in the result More...
|
|
virtual Expr | newBVPlusExpr (int numbits, const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVMultExpr (int numbits, const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVUDivExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVURemExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVSDivExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVSRemExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVSModExpr (const Expr &t1, const Expr &t2) |
|
virtual Expr | newFixedLeftShiftExpr (const Expr &t1, int r) |
|
virtual Expr | newFixedConstWidthLeftShiftExpr (const Expr &t1, int r) |
|
virtual Expr | newFixedRightShiftExpr (const Expr &t1, int r) |
|
virtual Expr | newBVSHL (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVLSHR (const Expr &t1, const Expr &t2) |
|
virtual Expr | newBVASHR (const Expr &t1, const Expr &t2) |
|
virtual Rational | computeBVConst (const Expr &e) |
|
|
Methods for manipulating other kinds of expressions
|
virtual Expr | tupleExpr (const std::vector< Expr > &exprs) |
| Tuple expression. More...
|
|
virtual Expr | tupleSelectExpr (const Expr &tuple, int index) |
| Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) More...
|
|
virtual Expr | tupleUpdateExpr (const Expr &tuple, int index, const Expr &newValue) |
| Tuple update; equivalent to "tuple WITH index := newValue". More...
|
|
virtual Expr | datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args) |
| Datatype constructor expression. More...
|
|
virtual Expr | datatypeSelExpr (const std::string &selector, const Expr &arg) |
| Datatype selector expression. More...
|
|
virtual Expr | datatypeTestExpr (const std::string &constructor, const Expr &arg) |
| Datatype tester expression. More...
|
|
virtual Expr | boundVarExpr (const std::string &name, const std::string &uid, const Type &type) |
| Create a bound variable with a given name, unique ID (uid) and type. More...
|
|
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body) |
| Universal quantifier. More...
|
|
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const Expr &trigger) |
| Universal quantifier with a trigger. More...
|
|
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) |
| Universal quantifier with a set of triggers. More...
|
|
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) |
| Universal quantifier with a set of multi-triggers. More...
|
|
virtual void | setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers) |
| Set triggers for quantifier instantiation. More...
|
|
virtual void | setTriggers (const Expr &e, const std::vector< Expr > &triggers) |
| Set triggers for quantifier instantiation (no multi-triggers) More...
|
|
virtual void | setTrigger (const Expr &e, const Expr &trigger) |
| Set a single trigger for quantifier instantiation. More...
|
|
virtual void | setMultiTrigger (const Expr &e, const std::vector< Expr > &multiTrigger) |
| Set a single multi-trigger for quantifier instantiation. More...
|
|
virtual Expr | existsExpr (const std::vector< Expr > &vars, const Expr &body) |
| Existential quantifier. More...
|
|
virtual Op | lambdaExpr (const std::vector< Expr > &vars, const Expr &body) |
| Lambda-expression. More...
|
|
virtual Op | transClosure (const Op &op) |
| Transitive closure of a binary predicate. More...
|
|
virtual Expr | simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n) |
| Symbolic simulation expression. More...
|
|
|
Methods related to validity checking
This group includes methods for asserting formulas, checking validity in the given logical context, manipulating the scope level of the context, etc.
|
virtual void | setResourceLimit (unsigned limit) |
| Set the resource limit (0==unlimited, 1==exhausted). More...
|
|
virtual void | setTimeLimit (unsigned limit) |
| Set a time limit in tenth of a second,. More...
|
|
virtual void | assertFormula (const Expr &e) |
| Assert a new formula in the current context. More...
|
|
virtual void | registerAtom (const Expr &e) |
| Register an atomic formula of interest. More...
|
|
virtual Expr | getImpliedLiteral () |
| Return next literal implied by last assertion. Null Expr if none. More...
|
|
virtual Expr | simplify (const Expr &e) |
| Simplify e with respect to the current context. More...
|
|
virtual QueryResult | query (const Expr &e) |
| Check validity of e in the current context. More...
|
|
virtual QueryResult | checkUnsat (const Expr &e) |
| Check satisfiability of the expr in the current context. More...
|
|
virtual QueryResult | checkContinue () |
| Get the next model. More...
|
|
virtual QueryResult | restart (const Expr &e) |
| Restart the most recent query with e as an additional assertion. More...
|
|
virtual void | returnFromCheck () |
| Returns to context immediately before last invalid query. More...
|
|
virtual void | getUserAssumptions (std::vector< Expr > &assumptions) |
| Get assumptions made by the user in this and all previous contexts. More...
|
|
virtual void | getInternalAssumptions (std::vector< Expr > &assumptions) |
| Get assumptions made internally in this and all previous contexts. More...
|
|
virtual void | getAssumptions (std::vector< Expr > &assumptions) |
| Get all assumptions made in this and all previous contexts. More...
|
|
virtual void | getAssumptionsUsed (std::vector< Expr > &assumptions) |
| Returns the set of assumptions used in the proof of queried formula. More...
|
|
virtual Expr | getProofQuery () |
|
virtual void | getCounterExample (std::vector< Expr > &assumptions, bool inOrder=true) |
| Return the internal assumptions that make the queried formula false. More...
|
|
virtual void | getConcreteModel (ExprMap< Expr > &m) |
| Will assign concrete values to all user created variables. More...
|
|
virtual QueryResult | tryModelGeneration () |
| If the result of the last query was UNKNOWN try to actually build the model to verify the result. More...
|
|
virtual FormulaValue | value (const Expr &e) |
|
virtual bool | inconsistent (std::vector< Expr > &assumptions) |
| Returns true if the current context is inconsistent. More...
|
|
virtual bool | inconsistent () |
| Returns true if the current context is inconsistent. More...
|
|
virtual bool | incomplete () |
| Returns true if the invalid result from last query() is imprecise. More...
|
|
virtual bool | incomplete (std::vector< std::string > &reasons) |
| Returns true if the invalid result from last query() is imprecise. More...
|
|
virtual Proof | getProof () |
| Returns the proof term for the last proven query. More...
|
|
virtual Expr | getValue (const Expr &e) |
| Evaluate an expression and return a concrete value in the model. More...
|
|
virtual Expr | getTCC () |
| Returns the TCC of the last assumption or query. More...
|
|
virtual void | getAssumptionsTCC (std::vector< Expr > &assumptions) |
| Return the set of assumptions used in the proof of the last TCC. More...
|
|
virtual Proof | getProofTCC () |
| Returns the proof of TCC of the last assumption or query. More...
|
|
virtual Expr | getClosure () |
| After successful query, return its closure |- Gamma => phi. More...
|
|
virtual Proof | getProofClosure () |
| Construct a proof of the query closure |- Gamma => phi. More...
|
|
|
Methods for manipulating contexts
Contexts support stack-based push and pop. There are two separate notions of the current context stack. stackLevel(), push(), pop(), and popto() work with the user-level notion of the stack.
scopeLevel(), pushScope(), popScope(), and poptoScope() work with the internal stack which is more fine-grained than the user stack.
Do not use the scope methods unless you know what you are doing.
|
virtual int | stackLevel () |
| Returns the current stack level. Initial level is 0. More...
|
|
virtual void | push () |
| Checkpoint the current context and increase the scope level. More...
|
|
virtual void | pop () |
| Restore the current context to its state at the last checkpoint. More...
|
|
virtual void | popto (int stackLevel) |
| Restore the current context to the given stackLevel. More...
|
|
virtual int | scopeLevel () |
| Returns the current scope level. Initially, the scope level is 1. More...
|
|
virtual void | pushScope () |
| Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing! More...
|
|
virtual void | popScope () |
| Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing! More...
|
|
virtual void | poptoScope (int scopeLevel) |
| Restore the current context to the given scopeLevel. More...
|
|
virtual Context * | getCurrentContext () |
| Get the current context. More...
|
|
virtual void | reset () |
| Destroy and recreate validity checker: resets everything except for flags. More...
|
|
virtual void | logAnnotation (const Expr &annot) |
| Add an annotation to the current script - prints annot when translating. More...
|
|
|
Methods for reading external files
|
virtual void | loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false) |
| Read and execute the commands from a file given by name ("" means stdin) More...
|
|
virtual void | loadFile (std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) |
| Read and execute the commands from a stream. More...
|
|
|
Methods for collecting and reporting run-time statistics
|
virtual Statistics | getStatistics () |
| Get statistics object. More...
|
|
virtual void | printStatistics () |
| Print collected statistics to stdout. More...
|
|