CVC3
2.4.1
|
Generic API for a validity checker. More...
#include <vc.h>
Public Member Functions | |
ValidityChecker () | |
Constructor. More... | |
virtual | ~ValidityChecker () |
Destructor. More... | |
virtual CLFlags & | getFlags () const =0 |
Return the set of command-line flags. More... | |
virtual void | reprocessFlags ()=0 |
Force reprocessing of all flags. More... | |
Type-related methods | |
Methods for creating and looking up types
| |
virtual Type | boolType ()=0 |
Create type BOOLEAN. More... | |
virtual Type | realType ()=0 |
Create type REAL. More... | |
virtual Type | intType ()=0 |
Create type INT. More... | |
virtual Type | subrangeType (const Expr &l, const Expr &r)=0 |
Create a subrange type [l..r]. More... | |
virtual Type | subtypeType (const Expr &pred, const Expr &witness)=0 |
Creates a subtype defined by the given predicate. More... | |
virtual Type | tupleType (const Type &type0, const Type &type1)=0 |
2-element tuple More... | |
virtual Type | tupleType (const Type &type0, const Type &type1, const Type &type2)=0 |
3-element tuple More... | |
virtual Type | tupleType (const std::vector< Type > &types)=0 |
n-element tuple (from a vector of types) More... | |
virtual Type | recordType (const std::string &field, const Type &type)=0 |
1-element record More... | |
virtual Type | recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0 |
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)=0 |
3-element record More... | |
virtual Type | recordType (const std::vector< std::string > &fields, const std::vector< Type > &types)=0 |
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)=0 |
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)=0 |
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)=0 |
Multiple datatypes. More... | |
virtual Type | arrayType (const Type &typeIndex, const Type &typeData)=0 |
Create an array type (ARRAY typeIndex OF typeData) More... | |
virtual Type | bitvecType (int n)=0 |
Create a bitvector type of length n. More... | |
virtual Type | funType (const Type &typeDom, const Type &typeRan)=0 |
Create a function type typeDom -> typeRan. More... | |
virtual Type | funType (const std::vector< Type > &typeDom, const Type &typeRan)=0 |
Create a function type (t1,t2,...,tn) -> typeRan. More... | |
virtual Type | createType (const std::string &typeName)=0 |
Create named user-defined uninterpreted type. More... | |
virtual Type | createType (const std::string &typeName, const Type &def)=0 |
Create named user-defined interpreted type (type abbreviation) More... | |
virtual Type | lookupType (const std::string &typeName)=0 |
Lookup a user-defined (uninterpreted) type by name. Returns Null if none. More... | |
General Expr methods | |
| |
virtual ExprManager * | getEM ()=0 |
Return the ExprManager. More... | |
virtual Expr | varExpr (const std::string &name, const Type &type)=0 |
Create a variable with a given name and type. More... | |
virtual Expr | varExpr (const std::string &name, const Type &type, const Expr &def)=0 |
Create a variable with a given name, type, and value. More... | |
virtual Expr | lookupVar (const std::string &name, Type *type)=0 |
Get the variable associated with a name, and its type. More... | |
virtual Type | getType (const Expr &e)=0 |
Get the type of the Expr. More... | |
virtual Type | getBaseType (const Expr &e)=0 |
Get the largest supertype of the Expr. More... | |
virtual Type | getBaseType (const Type &t)=0 |
Get the largest supertype of the Type. More... | |
virtual Expr | getTypePred (const Type &t, const Expr &e)=0 |
Get the subtype predicate. More... | |
virtual Expr | stringExpr (const std::string &str)=0 |
Create a string Expr. More... | |
virtual Expr | idExpr (const std::string &name)=0 |
Create an ID Expr. More... | |
virtual Expr | listExpr (const std::vector< Expr > &kids)=0 |
Create a list Expr. More... | |
virtual Expr | listExpr (const Expr &e1)=0 |
Overloaded version of listExpr with one argument. More... | |
virtual Expr | listExpr (const Expr &e1, const Expr &e2)=0 |
Overloaded version of listExpr with two arguments. More... | |
virtual Expr | listExpr (const Expr &e1, const Expr &e2, const Expr &e3)=0 |
Overloaded version of listExpr with three arguments. More... | |
virtual Expr | listExpr (const std::string &op, const std::vector< Expr > &kids)=0 |
Overloaded version of listExpr with string operator and many arguments. More... | |
virtual Expr | listExpr (const std::string &op, const Expr &e1)=0 |
Overloaded version of listExpr with string operator and one argument. More... | |
virtual Expr | listExpr (const std::string &op, const Expr &e1, const Expr &e2)=0 |
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)=0 |
Overloaded version of listExpr with string operator and three arguments. More... | |
virtual void | printExpr (const Expr &e)=0 |
Prints e to the standard output. More... | |
virtual void | printExpr (const Expr &e, std::ostream &os)=0 |
Prints e to the given ostream. More... | |
virtual Expr | parseExpr (const Expr &e)=0 |
Parse an expression using a Theory-specific parser. More... | |
virtual Type | parseType (const Expr &e)=0 |
Parse a type expression using a Theory-specific parser. More... | |
virtual Expr | importExpr (const Expr &e)=0 |
Import the Expr from another instance of ValidityChecker. More... | |
virtual Type | importType (const Type &t)=0 |
Import the Type from another instance of ValidityChecker. More... | |
virtual void | cmdsFromString (const std::string &s, InputLanguage lang=PRESENTATION_LANG)=0 |
Parse a sequence of commands from a presentation language string. More... | |
virtual Expr | exprFromString (const std::string &e)=0 |
Parse an expression from a presentation language string. More... | |
Core expression methods | |
Methods for manipulating core expressions Except for equality and ite, the children provided as arguments must be of type Boolean. | |
virtual Expr | trueExpr ()=0 |
Return TRUE Expr. More... | |
virtual Expr | falseExpr ()=0 |
Return FALSE Expr. More... | |
virtual Expr | notExpr (const Expr &child)=0 |
Create negation. More... | |
virtual Expr | andExpr (const Expr &left, const Expr &right)=0 |
Create 2-element conjunction. More... | |
virtual Expr | andExpr (const std::vector< Expr > &children)=0 |
Create n-element conjunction. More... | |
virtual Expr | orExpr (const Expr &left, const Expr &right)=0 |
Create 2-element disjunction. More... | |
virtual Expr | orExpr (const std::vector< Expr > &children)=0 |
Create n-element disjunction. More... | |
virtual Expr | impliesExpr (const Expr &hyp, const Expr &conc)=0 |
Create Boolean implication. More... | |
virtual Expr | iffExpr (const Expr &left, const Expr &right)=0 |
Create left IFF right (boolean equivalence) More... | |
virtual Expr | eqExpr (const Expr &child0, const Expr &child1)=0 |
Create an equality expression. More... | |
virtual Expr | iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0 |
Create IF ifpart THEN thenpart ELSE elsepart ENDIF. More... | |
virtual Expr | distinctExpr (const std::vector< Expr > &children)=0 |
User-defined (uninterpreted) function methods | |
Methods for manipulating uninterpreted function expressions | |
virtual Op | createOp (const std::string &name, const Type &type)=0 |
Create a named uninterpreted function with a given type. More... | |
virtual Op | createOp (const std::string &name, const Type &type, const Expr &def)=0 |
Create a named user-defined function with a given type. More... | |
virtual Op | lookupOp (const std::string &name, Type *type)=0 |
Get the Op associated with a name, and its type. More... | |
virtual Expr | funExpr (const Op &op, const Expr &child)=0 |
Unary function application (op must be of function type) More... | |
virtual Expr | funExpr (const Op &op, const Expr &left, const Expr &right)=0 |
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)=0 |
Ternary function application (op must be of function type) More... | |
virtual Expr | funExpr (const Op &op, const std::vector< Expr > &children)=0 |
n-ary function application (op must be of function type) More... | |
Arithmetic expression methods | |
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)=0 |
virtual Expr | ratExpr (int n, int d=1)=0 |
Create a rational number with numerator n and denominator d. More... | |
virtual Expr | ratExpr (const std::string &n, const std::string &d, int base)=0 |
Create a rational number with numerator n and denominator d. More... | |
virtual Expr | ratExpr (const std::string &n, int base=10)=0 |
Create a rational from a single string. More... | |
virtual Expr | uminusExpr (const Expr &child)=0 |
Unary minus. More... | |
virtual Expr | plusExpr (const Expr &left, const Expr &right)=0 |
Create 2-element sum (left + right) More... | |
virtual Expr | plusExpr (const std::vector< Expr > &children)=0 |
Create n-element sum. More... | |
virtual Expr | minusExpr (const Expr &left, const Expr &right)=0 |
Make a difference (left - right) More... | |
virtual Expr | multExpr (const Expr &left, const Expr &right)=0 |
Create a product (left * right) More... | |
virtual Expr | powExpr (const Expr &x, const Expr &n)=0 |
Create a power expression (x ^ n); n must be integer. More... | |
virtual Expr | divideExpr (const Expr &numerator, const Expr &denominator)=0 |
Create expression x / y. More... | |
virtual Expr | ltExpr (const Expr &left, const Expr &right)=0 |
Create (left < right) More... | |
virtual Expr | leExpr (const Expr &left, const Expr &right)=0 |
Create (left <= right) More... | |
virtual Expr | gtExpr (const Expr &left, const Expr &right)=0 |
Create (left > right) More... | |
virtual Expr | geExpr (const Expr &left, const Expr &right)=0 |
Create (left >= right) More... | |
Record expression methods | |
Methods for manipulating record expressions | |
virtual Expr | recordExpr (const std::string &field, const Expr &expr)=0 |
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)=0 |
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)=0 |
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)=0 |
Create an n-element record value (# field_i := expr_i #) More... | |
virtual Expr | recSelectExpr (const Expr &record, const std::string &field)=0 |
Create record.field (field selection) More... | |
virtual Expr | recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue)=0 |
Record update; equivalent to "record WITH .field := newValue". More... | |
Array expression methods | |
Methods for manipulating array expressions | |
virtual Expr | readExpr (const Expr &array, const Expr &index)=0 |
Create an expression array[index] (array access) More... | |
virtual Expr | writeExpr (const Expr &array, const Expr &index, const Expr &newValue)=0 |
Array update; equivalent to "array WITH index := newValue". More... | |
Bitvector expression methods | |
Methods for manipulating bitvector expressions | |
virtual Expr | newBVConstExpr (const std::string &s, int base=2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVConstExpr (const std::vector< bool > &bits)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVConstExpr (const Rational &r, int len=0)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newConcatExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newConcatExpr (const std::vector< Expr > &kids)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVExtractExpr (const Expr &e, int hi, int low)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVNegExpr (const Expr &t1)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVAndExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVAndExpr (const std::vector< Expr > &kids)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVOrExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVOrExpr (const std::vector< Expr > &kids)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVXorExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVXorExpr (const std::vector< Expr > &kids)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVXnorExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVXnorExpr (const std::vector< Expr > &kids)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVNandExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVNorExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVCompExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVLTExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVLEExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSLTExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSLEExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newSXExpr (const Expr &t1, int len)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVUminusExpr (const Expr &t1)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSubExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVPlusExpr (int numbits, const std::vector< Expr > &k)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVPlusExpr (int numbits, const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVMultExpr (int numbits, const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVUDivExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVURemExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSDivExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSRemExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSModExpr (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newFixedLeftShiftExpr (const Expr &t1, int r)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newFixedConstWidthLeftShiftExpr (const Expr &t1, int r)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newFixedRightShiftExpr (const Expr &t1, int r)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVSHL (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVLSHR (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Expr | newBVASHR (const Expr &t1, const Expr &t2)=0 |
'numbits' is the number of bits in the result More... | |
virtual Rational | computeBVConst (const Expr &e)=0 |
'numbits' is the number of bits in the result More... | |
Other expression methods | |
Methods for manipulating other kinds of expressions | |
virtual Expr | tupleExpr (const std::vector< Expr > &exprs)=0 |
Tuple expression. More... | |
virtual Expr | tupleSelectExpr (const Expr &tuple, int index)=0 |
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)=0 |
Tuple update; equivalent to "tuple WITH index := newValue". More... | |
virtual Expr | datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args)=0 |
Datatype constructor expression. More... | |
virtual Expr | datatypeSelExpr (const std::string &selector, const Expr &arg)=0 |
Datatype selector expression. More... | |
virtual Expr | datatypeTestExpr (const std::string &constructor, const Expr &arg)=0 |
Datatype tester expression. More... | |
virtual Expr | boundVarExpr (const std::string &name, const std::string &uid, const Type &type)=0 |
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)=0 |
Universal quantifier. More... | |
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)=0 |
Universal quantifier with a trigger. More... | |
virtual Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)=0 |
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)=0 |
Universal quantifier with a set of multi-triggers. More... | |
virtual void | setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers)=0 |
Set triggers for quantifier instantiation. More... | |
virtual void | setTriggers (const Expr &e, const std::vector< Expr > &triggers)=0 |
Set triggers for quantifier instantiation (no multi-triggers) More... | |
virtual void | setTrigger (const Expr &e, const Expr &trigger)=0 |
Set a single trigger for quantifier instantiation. More... | |
virtual void | setMultiTrigger (const Expr &e, const std::vector< Expr > &multiTrigger)=0 |
Set a single multi-trigger for quantifier instantiation. More... | |
virtual Expr | existsExpr (const std::vector< Expr > &vars, const Expr &body)=0 |
Existential quantifier. More... | |
virtual Op | lambdaExpr (const std::vector< Expr > &vars, const Expr &body)=0 |
Lambda-expression. More... | |
virtual Op | transClosure (const Op &op)=0 |
Transitive closure of a binary predicate. More... | |
virtual Expr | simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0 |
Symbolic simulation expression. More... | |
Validity checking methods | |
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)=0 |
Set the resource limit (0==unlimited, 1==exhausted). More... | |
virtual void | setTimeLimit (unsigned limit)=0 |
Set a time limit in tenth of a second,. More... | |
virtual void | assertFormula (const Expr &e)=0 |
Assert a new formula in the current context. More... | |
virtual void | registerAtom (const Expr &e)=0 |
Register an atomic formula of interest. More... | |
virtual Expr | getImpliedLiteral ()=0 |
Return next literal implied by last assertion. Null Expr if none. More... | |
virtual Expr | simplify (const Expr &e)=0 |
Simplify e with respect to the current context. More... | |
virtual QueryResult | query (const Expr &e)=0 |
Check validity of e in the current context. More... | |
virtual QueryResult | checkUnsat (const Expr &e)=0 |
Check satisfiability of the expr in the current context. More... | |
virtual QueryResult | checkContinue ()=0 |
Get the next model. More... | |
virtual QueryResult | restart (const Expr &e)=0 |
Restart the most recent query with e as an additional assertion. More... | |
virtual void | returnFromCheck ()=0 |
Returns to context immediately before last invalid query. More... | |
virtual void | getUserAssumptions (std::vector< Expr > &assumptions)=0 |
Get assumptions made by the user in this and all previous contexts. More... | |
virtual void | getInternalAssumptions (std::vector< Expr > &assumptions)=0 |
Get assumptions made internally in this and all previous contexts. More... | |
virtual void | getAssumptions (std::vector< Expr > &assumptions)=0 |
Get all assumptions made in this and all previous contexts. More... | |
virtual void | getAssumptionsUsed (std::vector< Expr > &assumptions)=0 |
Returns the set of assumptions used in the proof of queried formula. More... | |
virtual Expr | getProofQuery ()=0 |
Set the resource limit (0==unlimited, 1==exhausted). More... | |
virtual void | getCounterExample (std::vector< Expr > &assumptions, bool inOrder=true)=0 |
Return the internal assumptions that make the queried formula false. More... | |
virtual void | getConcreteModel (ExprMap< Expr > &m)=0 |
Will assign concrete values to all user created variables. More... | |
virtual QueryResult | tryModelGeneration ()=0 |
virtual FormulaValue | value (const Expr &e)=0 |
Set the resource limit (0==unlimited, 1==exhausted). More... | |
virtual bool | inconsistent (std::vector< Expr > &assumptions)=0 |
Returns true if the current context is inconsistent. More... | |
virtual bool | inconsistent ()=0 |
Returns true if the current context is inconsistent. More... | |
virtual bool | incomplete ()=0 |
Returns true if the invalid result from last query() is imprecise. More... | |
virtual bool | incomplete (std::vector< std::string > &reasons)=0 |
Returns true if the invalid result from last query() is imprecise. More... | |
virtual Proof | getProof ()=0 |
Returns the proof term for the last proven query. More... | |
virtual Expr | getValue (Expr e)=0 |
Evaluate an expression and return a concrete value in the model. More... | |
virtual Expr | getAssignment ()=0 |
Returns the list of pairs (name value) for each :named attribute. More... | |
virtual Expr | getTCC ()=0 |
Returns the TCC of the last assumption or query. More... | |
virtual void | getAssumptionsTCC (std::vector< Expr > &assumptions)=0 |
Return the set of assumptions used in the proof of the last TCC. More... | |
virtual Proof | getProofTCC ()=0 |
Returns the proof of TCC of the last assumption or query. More... | |
virtual Expr | getClosure ()=0 |
After successful query, return its closure |- Gamma => phi. More... | |
virtual Proof | getProofClosure ()=0 |
Construct a proof of the query closure |- Gamma => phi. More... | |
Context methods | |
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 ()=0 |
Returns the current stack level. Initial level is 0. More... | |
virtual void | push ()=0 |
Checkpoint the current context and increase the scope level. More... | |
virtual void | pop ()=0 |
Restore the current context to its state at the last checkpoint. More... | |
virtual void | popto (int stackLevel)=0 |
Restore the current context to the given stackLevel. More... | |
virtual int | scopeLevel ()=0 |
Returns the current scope level. Initially, the scope level is 1. More... | |
virtual void | pushScope ()=0 |
Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing! More... | |
virtual void | popScope ()=0 |
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)=0 |
Restore the current context to the given scopeLevel. More... | |
virtual Context * | getCurrentContext ()=0 |
Get the current context. More... | |
virtual void | reset ()=0 |
Destroy and recreate validity checker: resets everything except for flags. More... | |
virtual void | logAnnotation (const Expr &annot)=0 |
Add an annotation to the current script - prints annot when translating. More... | |
Reading files | |
Methods for reading external files | |
virtual void | loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)=0 |
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)=0 |
Read and execute the commands from a stream. More... | |
Reporting Statistics | |
Methods for collecting and reporting run-time statistics | |
virtual Statistics & | getStatistics ()=0 |
Get statistics object. More... | |
virtual void | printStatistics ()=0 |
Print collected statistics to stdout. More... | |
Static Public Member Functions | |
static CLFlags | createFlags () |
Create the set of command line flags with default values;. More... | |
static ValidityChecker * | create (const CLFlags &flags) |
Create an instance of ValidityChecker. More... | |
static ValidityChecker * | create () |
Create an instance of ValidityChecker using default flag values. More... | |
Generic API for a validity checker.
Created: Tue Nov 26 18:24:25 2002
All terms and formulas are represented as expressions using the Expr class. The notion of a context is also important. A context is a "background" set of formulas which are assumed to be true or false. Formulas can be added to the context explicitly, using assertFormula, or they may be added as part of processing a query command. At any time, the current set of formulas making up the context can be retrieved using getAssumptions.
|
inlinevirtual |
|
pure virtual |
Return the set of command-line flags.
The flags are returned by reference, and if modified, will have an immediate effect on the subsequent commands. Note that not all flags will have such an effect; some flags are used only at initialization time (like "sat"), and therefore, will not take effect if modified after ValidityChecker is created.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), main(), CVC3::VCCmd::reportResult(), and sighandler().
|
pure virtual |
Force reprocessing of all flags.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
static |
Create the set of command line flags with default values;.
Definition at line 69 of file vcl.cpp.
References CVC3::CLFlags::addFlag(), and IF_DEBUG().
|
static |
Create an instance of ValidityChecker.
flags | is the set of command line flags. |
|
static |
Create an instance of ValidityChecker using default flag values.
|
pure virtual |
Create type BOOLEAN.
Implemented in CVC3::VCL.
|
pure virtual |
Create type REAL.
Implemented in CVC3::VCL.
|
pure virtual |
Create type INT.
Implemented in CVC3::VCL.
Create a subrange type [l..r].
l and r can be Null; l=Null represents minus infinity, r=Null is plus infinity.
Implemented in CVC3::VCL.
|
pure virtual |
Creates a subtype defined by the given predicate.
pred | is a predicate taking one argument of type T and returning Boolean. The resulting type is a subtype of T whose elements x are those satisfying the predicate pred(x). |
witness | is an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove ![]() |
Implemented in CVC3::VCL.
|
pure virtual |
2-element tuple
Implemented in CVC3::VCL.
|
pure virtual |
3-element tuple
Implemented in CVC3::VCL.
n-element tuple (from a vector of types)
Implemented in CVC3::VCL.
|
pure virtual |
1-element record
Implemented in CVC3::VCL.
|
pure virtual |
n-element record (fields and types must be of the same length)
Fields will be sorted automatically
Implemented in CVC3::VCL.
|
pure virtual |
Single datatype, single constructor.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Single datatype, multiple constructors.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.
Implemented in CVC3::VCL.
|
pure virtual |
Multiple datatypes.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.
Implemented in CVC3::VCL.
|
pure virtual |
Create an array type (ARRAY typeIndex OF typeData)
Implemented in CVC3::VCL.
|
pure virtual |
Create a bitvector type of length n.
Implemented in CVC3::VCL.
|
pure virtual |
Create a function type typeDom -> typeRan.
Implemented in CVC3::VCL.
|
pure virtual |
Create a function type (t1,t2,...,tn) -> typeRan.
Implemented in CVC3::VCL.
|
pure virtual |
Create named user-defined uninterpreted type.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Create named user-defined interpreted type (type abbreviation)
Implemented in CVC3::VCL.
|
pure virtual |
Lookup a user-defined (uninterpreted) type by name. Returns Null if none.
Implemented in CVC3::VCL.
|
pure virtual |
Return the ExprManager.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), main(), CVC3::VCCmd::printSymbols(), and CVC3::VCCmd::reportResult().
|
pure virtual |
Create a variable with a given name and type.
name | is the name of the variable |
type | is its type. The type cannot be a function type. |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Create a variable with a given name, type, and value.
Implemented in CVC3::VCL.
Get the subtype predicate.
Implemented in CVC3::VCL.
|
pure virtual |
|
pure virtual |
Create a list Expr.
Intermediate representation for DP-specific expressions. Normally, the first element of the list is a string Expr representing an operator, and the rest of the list are the arguments. For example,
kids.push_back(vc->stringExpr("PLUS")); kids.push_back(x); // x and y are previously created Exprs kids.push_back(y); Expr lst = vc->listExpr(kids);
Or, alternatively (using its overloaded version):
Expr lst = vc->listExpr("PLUS", x, y);
or
vector<Expr> summands; summands.push_back(x); summands.push_back(y); ... Expr lst = vc->listExpr("PLUS", summands);
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
Overloaded version of listExpr with one argument.
Implemented in CVC3::VCL.
Overloaded version of listExpr with two arguments.
Implemented in CVC3::VCL.
|
pure virtual |
Overloaded version of listExpr with three arguments.
Implemented in CVC3::VCL.
|
pure virtual |
Overloaded version of listExpr with string operator and many arguments.
Implemented in CVC3::VCL.
|
pure virtual |
Overloaded version of listExpr with string operator and one argument.
Implemented in CVC3::VCL.
|
pure virtual |
Overloaded version of listExpr with string operator and two arguments.
Implemented in CVC3::VCL.
|
pure virtual |
Overloaded version of listExpr with string operator and three arguments.
Implemented in CVC3::VCL.
|
pure virtual |
Prints e to the standard output.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Prints e to the given ostream.
Implemented in CVC3::VCL.
Parse an expression using a Theory-specific parser.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
Parse a type expression using a Theory-specific parser.
Implemented in CVC3::VCL.
Import the Expr from another instance of ValidityChecker.
When expressions need to be passed among several instances of ValidityChecker, they need to be explicitly imported into the corresponding instance using this method. The return result is an identical expression that belongs to the current instance of ValidityChecker, and can be safely used as part of more complex expressions from the same instance.
Implemented in CVC3::VCL.
Import the Type from another instance of ValidityChecker.
Implemented in CVC3::VCL.
|
pure virtual |
Parse a sequence of commands from a presentation language string.
Implemented in CVC3::VCL.
|
pure virtual |
Parse an expression from a presentation language string.
Implemented in CVC3::VCL.
|
pure virtual |
|
pure virtual |
Create negation.
Implemented in CVC3::VCL.
Create 2-element conjunction.
Implemented in CVC3::VCL.
Create n-element conjunction.
Implemented in CVC3::VCL.
Create 2-element disjunction.
Implemented in CVC3::VCL.
Create n-element disjunction.
Implemented in CVC3::VCL.
|
pure virtual |
Create Boolean implication.
Implemented in CVC3::VCL.
Create left IFF right (boolean equivalence)
Implemented in CVC3::VCL.
|
pure virtual |
Create an equality expression.
The two children must have the same type, and cannot be of type Boolean.
Implemented in CVC3::VCL.
|
pure virtual |
Create IF ifpart THEN thenpart ELSE elsepart ENDIF.
ifpart | must be of type Boolean. |
thenpart | and |
elsepart | must have the same type, which will also be the type of the ite expression. |
Implemented in CVC3::VCL.
|
pure virtual |
Create an expression asserting that all the children are different.
children | the children to be asserted different |
Implemented in CVC3::VCL.
|
pure virtual |
Create a named uninterpreted function with a given type.
name | is the new function's name (as ID Expr) |
type | is a function type ( [range -> domain] ) |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Create a named user-defined function with a given type.
Implemented in CVC3::VCL.
Unary function application (op must be of function type)
Implemented in CVC3::VCL.
|
pure virtual |
Binary function application (op must be of function type)
Implemented in CVC3::VCL.
|
pure virtual |
Ternary function application (op must be of function type)
Implemented in CVC3::VCL.
|
pure virtual |
n-ary function application (op must be of function type)
Implemented in CVC3::VCL.
|
pure virtual |
Add the pair of variables to the variable ordering for aritmetic solving. Terms that are not arithmetic will be ignored.
smaller | the smaller variable |
bigger | the bigger variable |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Create a rational number with numerator n and denominator d.
n | the numerator |
d | the denominator, cannot be 0. |
Implemented in CVC3::VCL.
|
pure virtual |
Create a rational number with numerator n and denominator d.
Here n and d are given as strings. They are converted to arbitrary-precision integers according to the given base.
Implemented in CVC3::VCL.
|
pure virtual |
Create a rational from a single string.
n | can be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format. |
base | is the base in which to interpret the string. |
Implemented in CVC3::VCL.
Unary minus.
Implemented in CVC3::VCL.
Create 2-element sum (left + right)
Implemented in CVC3::VCL.
Create n-element sum.
Implemented in CVC3::VCL.
|
pure virtual |
Make a difference (left - right)
Implemented in CVC3::VCL.
Create a product (left * right)
Implemented in CVC3::VCL.
Create a power expression (x ^ n); n must be integer.
Implemented in CVC3::VCL.
|
pure virtual |
Create expression x / y.
Implemented in CVC3::VCL.
Create (left < right)
Implemented in CVC3::VCL.
Create (left <= right)
Implemented in CVC3::VCL.
Create (left > right)
Implemented in CVC3::VCL.
Create (left >= right)
Implemented in CVC3::VCL.
|
pure virtual |
Create a 1-element record value (# field := expr #)
Fields will be sorted automatically
Implemented in CVC3::VCL.
|
pure virtual |
Create a 2-element record value (# field0 := expr0, field1 := expr1 #)
Fields will be sorted automatically
Implemented in CVC3::VCL.
|
pure virtual |
Create a 3-element record value (# field_i := expr_i #)
Fields will be sorted automatically
Implemented in CVC3::VCL.
|
pure virtual |
Create an n-element record value (# field_i := expr_i #)
fields | |
exprs | must be the same length as fields |
Fields will be sorted automatically
Implemented in CVC3::VCL.
|
pure virtual |
Create record.field (field selection)
Create an expression representing the selection of a field from a record.
Implemented in CVC3::VCL.
|
pure virtual |
Record update; equivalent to "record WITH .field := newValue".
Notice the `.' before field in the presentation language (and the comment above); this is to distinguish it from datatype update.
Implemented in CVC3::VCL.
|
pure virtual |
Create an expression array[index] (array access)
Create an expression for the value of array at the given index
Implemented in CVC3::VCL.
|
pure virtual |
Array update; equivalent to "array WITH index := newValue".
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
|
pure virtual |
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
'numbits' is the number of bits in the result
Implemented in CVC3::VCL.
Tuple expression.
Implemented in CVC3::VCL.
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
Implemented in CVC3::VCL.
|
pure virtual |
Tuple update; equivalent to "tuple WITH index := newValue".
Implemented in CVC3::VCL.
|
pure virtual |
Datatype constructor expression.
Implemented in CVC3::VCL.
|
pure virtual |
Datatype selector expression.
Implemented in CVC3::VCL.
|
pure virtual |
Datatype tester expression.
Implemented in CVC3::VCL.
|
pure virtual |
Create a bound variable with a given name, unique ID (uid) and type.
name | is the name of the variable |
uid | is the unique ID (a string), which must be unique for each variable |
type | is its type. The type cannot be a function type. |
Implemented in CVC3::VCL.
|
pure virtual |
Universal quantifier.
Implemented in CVC3::VCL.
|
pure virtual |
Universal quantifier with a trigger.
Implemented in CVC3::VCL.
|
pure virtual |
Universal quantifier with a set of triggers.
Implemented in CVC3::VCL.
|
pure virtual |
Universal quantifier with a set of multi-triggers.
Implemented in CVC3::VCL.
|
pure virtual |
Set triggers for quantifier instantiation.
e | the expression for which triggers are being set. |
triggers | Each item in triggers is a vector of Expr containing one or more patterns. A pattern is a term or Atomic predicate sub-expression of e. A vector containing more than one pattern is treated as a multi-trigger. Patterns will be matched in the order they occur in the vector. |
Implemented in CVC3::VCL.
|
pure virtual |
Set triggers for quantifier instantiation (no multi-triggers)
Implemented in CVC3::VCL.
|
pure virtual |
Set a single trigger for quantifier instantiation.
Implemented in CVC3::VCL.
|
pure virtual |
Set a single multi-trigger for quantifier instantiation.
Implemented in CVC3::VCL.
|
pure virtual |
Existential quantifier.
Implemented in CVC3::VCL.
|
pure virtual |
Lambda-expression.
Implemented in CVC3::VCL.
Transitive closure of a binary predicate.
Implemented in CVC3::VCL.
|
pure virtual |
Symbolic simulation expression.
f | is the next state function (LAMBDA-expression) |
s0 | is the initial state |
inputs | is the vector of LAMBDA-expressions representing the sequences of inputs to f |
n | is a constant, the number of cycles to run the simulation. |
Implemented in CVC3::VCL.
|
pure virtual |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
Implemented in CVC3::VCL.
|
pure virtual |
Set a time limit in tenth of a second,.
counting the cpu time used by the current process from now on. Currently, when the limit is reached, cvc3 tries to quickly terminate, probably with the status unknown.
Implemented in CVC3::VCL.
|
pure virtual |
Assert a new formula in the current context.
This creates the assumption e |- e. The formula must have Boolean type.
Implemented in CVC3::VCL.
Referenced by SAT::CNF_Manager::cons(), and CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Register an atomic formula of interest.
Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function
Implemented in CVC3::VCL.
|
pure virtual |
Simplify e with respect to the current context.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Check validity of e in the current context.
If it returns VALID, the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible.
e | is the queried formula |
Implemented in CVC3::VCL.
Referenced by SAT::CNF_Manager::cons(), and CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Check satisfiability of the expr in the current context.
Equivalent to query(!e)
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Get the next model.
This method should only be called after a query which returns INVALID. Its return values are as for query().
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Restart the most recent query with e as an additional assertion.
This method should only be called after a query which returns INVALID. Its return values are as for query().
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns to context immediately before last invalid query.
This method should only be called after a query which returns false.
Implemented in CVC3::VCL.
|
pure virtual |
Get assumptions made by the user in this and all previous contexts.
User assumptions are created either by calls to assertFormula or by a call to query. In the latter case, the negated query is added as an assumption.
assumptions | should be empty on entry. |
Implemented in CVC3::VCL.
|
pure virtual |
Get assumptions made internally in this and all previous contexts.
Internal assumptions are literals assumed by the sat solver.
assumptions | should be empty on entry. |
Implemented in CVC3::VCL.
|
pure virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be empty on entry. |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the set of assumptions used in the proof of queried formula.
It returns a subset of getAssumptions(). If the last query was false or there has not yet been a query, it does nothing. NOTE: this functionality is not supported yet
assumptions | should be empty on entry. |
Implemented in CVC3::VCL.
|
pure virtual |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
Implemented in CVC3::VCL.
|
pure virtual |
Return the internal assumptions that make the queried formula false.
This method should only be called after a query which returns false. It will try to return the simplest possible subset of the internal assumptions sufficient to make the queried expression false.
assumptions | should be empty on entry. |
inOrder | if true, returns the assumptions in the order they were made. This is slightly more expensive than inOrder = false. |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::printCounterExample().
Will assign concrete values to all user created variables.
This function should only be called after a query which return false.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), and CVC3::VCCmd::printModel().
|
pure virtual |
If the result of the last query was UNKNOWN try to actually build the model to verify the result.
This function should only be called after a query which return unknown.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
Implemented in CVC3::VCL.
|
pure virtual |
Returns true if the current context is inconsistent.
Also returns a minimal set of assertions used to determine the inconsistency.
assumptions | should be empty on entry. |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns true if the current context is inconsistent.
Implemented in CVC3::VCL.
|
pure virtual |
Returns true if the invalid result from last query() is imprecise.
Some decision procedures in CVC are incomplete (quantifier elimination, non-linear arithmetic, etc.). If any incomplete features were used during the last query(), and the result is "invalid" (query() returns false), then this result is inconclusive. It means that the system gave up the search for contradiction at some point.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), and CVC3::VCCmd::reportResult().
|
pure virtual |
Returns true if the invalid result from last query() is imprecise.
The argument is filled with the reasons for incompleteness (they are intended to be shown to the end user).
Implemented in CVC3::VCL.
|
pure virtual |
Returns the proof term for the last proven query.
If there has not been a successful query, it should return a NULL proof
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
Evaluate an expression and return a concrete value in the model.
If the last query was not invalid, should return NULL expr
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the list of pairs (name value) for each :named attribute.
If the last query was not invalid, should return NULL expr
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the TCC of the last assumption or query.
Returns Null if no assumptions or queries were performed.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Return the set of assumptions used in the proof of the last TCC.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the proof of TCC of the last assumption or query.
Returns Null if no assumptions or queries were performed.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
After successful query, return its closure |- Gamma => phi.
Turn a valid query Gamma |- phi into an implication |- Gamma => phi.
Returns Null if last query was invalid.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Construct a proof of the query closure |- Gamma => phi.
Returns Null if last query was Invalid.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the current stack level. Initial level is 0.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Checkpoint the current context and increase the scope level.
Implemented in CVC3::VCL.
Referenced by SAT::CNF_Manager::cons(), and CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Restore the current context to its state at the last checkpoint.
Implemented in CVC3::VCL.
Referenced by SAT::CNF_Manager::cons(), and CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Restore the current context to the given stackLevel.
stackLevel | should be greater than or equal to 0 and less than or equal to the current scope level. |
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Returns the current scope level. Initially, the scope level is 1.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::printCounterExample(), and CVC3::VCCmd::printModel().
|
pure virtual |
Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing!
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing!
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Restore the current context to the given scopeLevel.
scopeLevel | should be less than or equal to the current scope level. |
If scopeLevel is less than 1, then the current context is reset and the scope level is set to 1.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
|
pure virtual |
Destroy and recreate validity checker: resets everything except for flags.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::processCommands().
|
pure virtual |
Add an annotation to the current script - prints annot when translating.
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand().
|
pure virtual |
Read and execute the commands from a file given by name ("" means stdin)
Implemented in CVC3::VCL.
Referenced by CVC3::VCCmd::evaluateCommand(), and main().
|
pure virtual |
Read and execute the commands from a stream.
Implemented in CVC3::VCL.
|
pure virtual |
|
pure virtual |