CVC3
Public Member Functions | Static Public Member Functions | List of all members
CVC3::ValidityChecker Class Referenceabstract

Generic API for a validity checker. More...

#include <vc.h>

Inherited by CVC3::VCL.

Collaboration diagram for CVC3::ValidityChecker:
Collaboration graph

Public Member Functions

 ValidityChecker ()
 Constructor.
 
virtual ~ValidityChecker ()
 Destructor.
 
virtual CLFlagsgetFlags () const =0
 Return the set of command-line flags.
 
virtual void reprocessFlags ()=0
 Force reprocessing of all flags.
 
Type-related methods

Methods for creating and looking up types

See Also
class Type
virtual Type boolType ()=0
 Create type BOOLEAN.
 
virtual Type realType ()=0
 Create type REAL.
 
virtual Type intType ()=0
 Create type INT.
 
virtual Type subrangeType (const Expr &l, const Expr &r)=0
 Create a subrange type [l..r].
 
virtual Type subtypeType (const Expr &pred, const Expr &witness)=0
 Creates a subtype defined by the given predicate.
 
virtual Type tupleType (const Type &type0, const Type &type1)=0
 2-element tuple
 
virtual Type tupleType (const Type &type0, const Type &type1, const Type &type2)=0
 3-element tuple
 
virtual Type tupleType (const std::vector< Type > &types)=0
 n-element tuple (from a vector of types)
 
virtual Type recordType (const std::string &field, const Type &type)=0
 1-element record
 
virtual Type recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0
 2-element record
 
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
 
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)
 
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.
 
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.
 
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.
 
virtual Type arrayType (const Type &typeIndex, const Type &typeData)=0
 Create an array type (ARRAY typeIndex OF typeData)
 
virtual Type bitvecType (int n)=0
 Create a bitvector type of length n.
 
virtual Type funType (const Type &typeDom, const Type &typeRan)=0
 Create a function type typeDom -> typeRan.
 
virtual Type funType (const std::vector< Type > &typeDom, const Type &typeRan)=0
 Create a function type (t1,t2,...,tn) -> typeRan.
 
virtual Type createType (const std::string &typeName)=0
 Create named user-defined uninterpreted type.
 
virtual Type createType (const std::string &typeName, const Type &def)=0
 Create named user-defined interpreted type (type abbreviation)
 
virtual Type lookupType (const std::string &typeName)=0
 Lookup a user-defined (uninterpreted) type by name. Returns Null if none.
 
General Expr methods
See Also
class Expr
class ExprManager
virtual ExprManagergetEM ()=0
 Return the ExprManager.
 
virtual Expr varExpr (const std::string &name, const Type &type)=0
 Create a variable with a given name and type.
 
virtual Expr varExpr (const std::string &name, const Type &type, const Expr &def)=0
 Create a variable with a given name, type, and value.
 
virtual Expr lookupVar (const std::string &name, Type *type)=0
 Get the variable associated with a name, and its type.
 
virtual Type getType (const Expr &e)=0
 Get the type of the Expr.
 
virtual Type getBaseType (const Expr &e)=0
 Get the largest supertype of the Expr.
 
virtual Type getBaseType (const Type &t)=0
 Get the largest supertype of the Type.
 
virtual Expr getTypePred (const Type &t, const Expr &e)=0
 Get the subtype predicate.
 
virtual Expr stringExpr (const std::string &str)=0
 Create a string Expr.
 
virtual Expr idExpr (const std::string &name)=0
 Create an ID Expr.
 
virtual Expr listExpr (const std::vector< Expr > &kids)=0
 Create a list Expr.
 
virtual Expr listExpr (const Expr &e1)=0
 Overloaded version of listExpr with one argument.
 
virtual Expr listExpr (const Expr &e1, const Expr &e2)=0
 Overloaded version of listExpr with two arguments.
 
virtual Expr listExpr (const Expr &e1, const Expr &e2, const Expr &e3)=0
 Overloaded version of listExpr with three arguments.
 
virtual Expr listExpr (const std::string &op, const std::vector< Expr > &kids)=0
 Overloaded version of listExpr with string operator and many arguments.
 
virtual Expr listExpr (const std::string &op, const Expr &e1)=0
 Overloaded version of listExpr with string operator and one argument.
 
virtual Expr listExpr (const std::string &op, const Expr &e1, const Expr &e2)=0
 Overloaded version of listExpr with string operator and two arguments.
 
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.
 
virtual void printExpr (const Expr &e)=0
 Prints e to the standard output.
 
virtual void printExpr (const Expr &e, std::ostream &os)=0
 Prints e to the given ostream.
 
virtual Expr parseExpr (const Expr &e)=0
 Parse an expression using a Theory-specific parser.
 
virtual Type parseType (const Expr &e)=0
 Parse a type expression using a Theory-specific parser.
 
virtual Expr importExpr (const Expr &e)=0
 Import the Expr from another instance of ValidityChecker.
 
virtual Type importType (const Type &t)=0
 Import the Type from another instance of ValidityChecker.
 
virtual void cmdsFromString (const std::string &s, InputLanguage lang=PRESENTATION_LANG)=0
 Parse a sequence of commands from a presentation language string.
 
virtual Expr exprFromString (const std::string &e)=0
 Parse an expression from a presentation language string.
 
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.
 
virtual Expr falseExpr ()=0
 Return FALSE Expr.
 
virtual Expr notExpr (const Expr &child)=0
 Create negation.
 
virtual Expr andExpr (const Expr &left, const Expr &right)=0
 Create 2-element conjunction.
 
virtual Expr andExpr (const std::vector< Expr > &children)=0
 Create n-element conjunction.
 
virtual Expr orExpr (const Expr &left, const Expr &right)=0
 Create 2-element disjunction.
 
virtual Expr orExpr (const std::vector< Expr > &children)=0
 Create n-element disjunction.
 
virtual Expr impliesExpr (const Expr &hyp, const Expr &conc)=0
 Create Boolean implication.
 
virtual Expr iffExpr (const Expr &left, const Expr &right)=0
 Create left IFF right (boolean equivalence)
 
virtual Expr eqExpr (const Expr &child0, const Expr &child1)=0
 Create an equality expression.
 
virtual Expr iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0
 Create IF ifpart THEN thenpart ELSE elsepart ENDIF.
 
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.
 
virtual Op createOp (const std::string &name, const Type &type, const Expr &def)=0
 Create a named user-defined function with a given type.
 
virtual Op lookupOp (const std::string &name, Type *type)=0
 Get the Op associated with a name, and its type.
 
virtual Expr funExpr (const Op &op, const Expr &child)=0
 Unary function application (op must be of function type)
 
virtual Expr funExpr (const Op &op, const Expr &left, const Expr &right)=0
 Binary function application (op must be of function type)
 
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)
 
virtual Expr funExpr (const Op &op, const std::vector< Expr > &children)=0
 n-ary function application (op must be of function type)
 
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.
 
virtual Expr ratExpr (const std::string &n, const std::string &d, int base)=0
 Create a rational number with numerator n and denominator d.
 
virtual Expr ratExpr (const std::string &n, int base=10)=0
 Create a rational from a single string.
 
virtual Expr uminusExpr (const Expr &child)=0
 Unary minus.
 
virtual Expr plusExpr (const Expr &left, const Expr &right)=0
 Create 2-element sum (left + right)
 
virtual Expr plusExpr (const std::vector< Expr > &children)=0
 Create n-element sum.
 
virtual Expr minusExpr (const Expr &left, const Expr &right)=0
 Make a difference (left - right)
 
virtual Expr multExpr (const Expr &left, const Expr &right)=0
 Create a product (left * right)
 
virtual Expr powExpr (const Expr &x, const Expr &n)=0
 Create a power expression (x ^ n); n must be integer.
 
virtual Expr divideExpr (const Expr &numerator, const Expr &denominator)=0
 Create expression x / y.
 
virtual Expr ltExpr (const Expr &left, const Expr &right)=0
 Create (left < right)
 
virtual Expr leExpr (const Expr &left, const Expr &right)=0
 Create (left <= right)
 
virtual Expr gtExpr (const Expr &left, const Expr &right)=0
 Create (left > right)
 
virtual Expr geExpr (const Expr &left, const Expr &right)=0
 Create (left >= right)
 
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 #)
 
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 #)
 
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 #)
 
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 #)
 
virtual Expr recSelectExpr (const Expr &record, const std::string &field)=0
 Create record.field (field selection)
 
virtual Expr recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue)=0
 Record update; equivalent to "record WITH .field := newValue".
 
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)
 
virtual Expr writeExpr (const Expr &array, const Expr &index, const Expr &newValue)=0
 Array update; equivalent to "array WITH index := newValue".
 
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
 
virtual Expr newBVConstExpr (const std::vector< bool > &bits)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVConstExpr (const Rational &r, int len=0)=0
 'numbits' is the number of bits in the result
 
virtual Expr newConcatExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newConcatExpr (const std::vector< Expr > &kids)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVExtractExpr (const Expr &e, int hi, int low)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVNegExpr (const Expr &t1)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVAndExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVAndExpr (const std::vector< Expr > &kids)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVOrExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVOrExpr (const std::vector< Expr > &kids)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVXorExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVXorExpr (const std::vector< Expr > &kids)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVXnorExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVXnorExpr (const std::vector< Expr > &kids)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVNandExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVNorExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVCompExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVLTExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVLEExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSLTExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSLEExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newSXExpr (const Expr &t1, int len)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVUminusExpr (const Expr &t1)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSubExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVPlusExpr (int numbits, const std::vector< Expr > &k)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVPlusExpr (int numbits, const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVMultExpr (int numbits, const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVUDivExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVURemExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSDivExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSRemExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSModExpr (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newFixedLeftShiftExpr (const Expr &t1, int r)=0
 'numbits' is the number of bits in the result
 
virtual Expr newFixedConstWidthLeftShiftExpr (const Expr &t1, int r)=0
 'numbits' is the number of bits in the result
 
virtual Expr newFixedRightShiftExpr (const Expr &t1, int r)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVSHL (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVLSHR (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Expr newBVASHR (const Expr &t1, const Expr &t2)=0
 'numbits' is the number of bits in the result
 
virtual Rational computeBVConst (const Expr &e)=0
 'numbits' is the number of bits in the result
 
Other expression methods

Methods for manipulating other kinds of expressions

virtual Expr tupleExpr (const std::vector< Expr > &exprs)=0
 Tuple expression.
 
virtual Expr tupleSelectExpr (const Expr &tuple, int index)=0
 Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
 
virtual Expr tupleUpdateExpr (const Expr &tuple, int index, const Expr &newValue)=0
 Tuple update; equivalent to "tuple WITH index := newValue".
 
virtual Expr datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args)=0
 Datatype constructor expression.
 
virtual Expr datatypeSelExpr (const std::string &selector, const Expr &arg)=0
 Datatype selector expression.
 
virtual Expr datatypeTestExpr (const std::string &constructor, const Expr &arg)=0
 Datatype tester expression.
 
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.
 
virtual Expr forallExpr (const std::vector< Expr > &vars, const Expr &body)=0
 Universal quantifier.
 
virtual Expr forallExpr (const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)=0
 Universal quantifier with a trigger.
 
virtual Expr forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)=0
 Universal quantifier with a set of triggers.
 
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.
 
virtual void setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers)=0
 Set triggers for quantifier instantiation.
 
virtual void setTriggers (const Expr &e, const std::vector< Expr > &triggers)=0
 Set triggers for quantifier instantiation (no multi-triggers)
 
virtual void setTrigger (const Expr &e, const Expr &trigger)=0
 Set a single trigger for quantifier instantiation.
 
virtual void setMultiTrigger (const Expr &e, const std::vector< Expr > &multiTrigger)=0
 Set a single multi-trigger for quantifier instantiation.
 
virtual Expr existsExpr (const std::vector< Expr > &vars, const Expr &body)=0
 Existential quantifier.
 
virtual Op lambdaExpr (const std::vector< Expr > &vars, const Expr &body)=0
 Lambda-expression.
 
virtual Op transClosure (const Op &op)=0
 Transitive closure of a binary predicate.
 
virtual Expr simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0
 Symbolic simulation expression.
 
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).
 
virtual void setTimeLimit (unsigned limit)=0
 Set a time limit in tenth of a second,.
 
virtual void assertFormula (const Expr &e)=0
 Assert a new formula in the current context.
 
virtual void registerAtom (const Expr &e)=0
 Register an atomic formula of interest.
 
virtual Expr getImpliedLiteral ()=0
 Return next literal implied by last assertion. Null Expr if none.
 
virtual Expr simplify (const Expr &e)=0
 Simplify e with respect to the current context.
 
virtual QueryResult query (const Expr &e)=0
 Check validity of e in the current context.
 
virtual QueryResult checkUnsat (const Expr &e)=0
 Check satisfiability of the expr in the current context.
 
virtual QueryResult checkContinue ()=0
 Get the next model.
 
virtual QueryResult restart (const Expr &e)=0
 Restart the most recent query with e as an additional assertion.
 
virtual void returnFromCheck ()=0
 Returns to context immediately before last invalid query.
 
virtual void getUserAssumptions (std::vector< Expr > &assumptions)=0
 Get assumptions made by the user in this and all previous contexts.
 
virtual void getInternalAssumptions (std::vector< Expr > &assumptions)=0
 Get assumptions made internally in this and all previous contexts.
 
virtual void getAssumptions (std::vector< Expr > &assumptions)=0
 Get all assumptions made in this and all previous contexts.
 
virtual void getAssumptionsUsed (std::vector< Expr > &assumptions)=0
 Returns the set of assumptions used in the proof of queried formula.
 
virtual Expr getProofQuery ()=0
 Set the resource limit (0==unlimited, 1==exhausted).
 
virtual void getCounterExample (std::vector< Expr > &assumptions, bool inOrder=true)=0
 Return the internal assumptions that make the queried formula false.
 
virtual void getConcreteModel (ExprMap< Expr > &m)=0
 Will assign concrete values to all user created variables.
 
virtual QueryResult tryModelGeneration ()=0
 
virtual FormulaValue value (const Expr &e)=0
 Set the resource limit (0==unlimited, 1==exhausted).
 
virtual bool inconsistent (std::vector< Expr > &assumptions)=0
 Returns true if the current context is inconsistent.
 
virtual bool inconsistent ()=0
 Returns true if the current context is inconsistent.
 
virtual bool incomplete ()=0
 Returns true if the invalid result from last query() is imprecise.
 
virtual bool incomplete (std::vector< std::string > &reasons)=0
 Returns true if the invalid result from last query() is imprecise.
 
virtual Proof getProof ()=0
 Returns the proof term for the last proven query.
 
virtual Expr getValue (Expr e)=0
 Evaluate an expression and return a concrete value in the model.
 
virtual Expr getAssignment ()=0
 Returns the list of pairs (name value) for each :named attribute.
 
virtual Expr getTCC ()=0
 Returns the TCC of the last assumption or query.
 
virtual void getAssumptionsTCC (std::vector< Expr > &assumptions)=0
 Return the set of assumptions used in the proof of the last TCC.
 
virtual Proof getProofTCC ()=0
 Returns the proof of TCC of the last assumption or query.
 
virtual Expr getClosure ()=0
 After successful query, return its closure |- Gamma => phi.
 
virtual Proof getProofClosure ()=0
 Construct a proof of the query closure |- Gamma => phi.
 
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.
 
virtual void push ()=0
 Checkpoint the current context and increase the scope level.
 
virtual void pop ()=0
 Restore the current context to its state at the last checkpoint.
 
virtual void popto (int stackLevel)=0
 Restore the current context to the given stackLevel.
 
virtual int scopeLevel ()=0
 Returns the current scope level. Initially, the scope level is 1.
 
virtual void pushScope ()=0
 Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing!
 
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!
 
virtual void poptoScope (int scopeLevel)=0
 Restore the current context to the given scopeLevel.
 
virtual ContextgetCurrentContext ()=0
 Get the current context.
 
virtual void reset ()=0
 Destroy and recreate validity checker: resets everything except for flags.
 
virtual void logAnnotation (const Expr &annot)=0
 Add an annotation to the current script - prints annot when translating.
 
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)
 
virtual void loadFile (std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0
 Read and execute the commands from a stream.
 
Reporting Statistics

Methods for collecting and reporting run-time statistics

virtual StatisticsgetStatistics ()=0
 Get statistics object.
 
virtual void printStatistics ()=0
 Print collected statistics to stdout.
 

Static Public Member Functions

static CLFlags createFlags ()
 Create the set of command line flags with default values;.
 
static ValidityCheckercreate (const CLFlags &flags)
 Create an instance of ValidityChecker.
 
static ValidityCheckercreate ()
 Create an instance of ValidityChecker using default flag values.
 

Detailed Description

Generic API for a validity checker.

Author: Clark Barrett

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.

Definition at line 92 of file vc.h.

Constructor & Destructor Documentation

CVC3::ValidityChecker::ValidityChecker ( )
inline

Constructor.

Definition at line 96 of file vc.h.

virtual CVC3::ValidityChecker::~ValidityChecker ( )
inlinevirtual

Destructor.

Definition at line 98 of file vc.h.

Member Function Documentation

virtual CLFlags& CVC3::ValidityChecker::getFlags ( ) const
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().

virtual void CVC3::ValidityChecker::reprocessFlags ( )
pure virtual

Force reprocessing of all flags.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

CLFlags ValidityChecker::createFlags ( )
static

Create the set of command line flags with default values;.

Returns
the set of flags by value

Definition at line 69 of file vcl.cpp.

References CVC3::CLFlags::addFlag(), and IF_DEBUG.

ValidityChecker * ValidityChecker::create ( const CLFlags flags)
static

Create an instance of ValidityChecker.

Parameters
flagsis the set of command line flags.

Definition at line 63 of file vcl.cpp.

ValidityChecker * ValidityChecker::create ( )
static

Create an instance of ValidityChecker using default flag values.

Definition at line 300 of file vcl.cpp.

virtual Type CVC3::ValidityChecker::boolType ( )
pure virtual

Create type BOOLEAN.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::realType ( )
pure virtual

Create type REAL.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::intType ( )
pure virtual

Create type INT.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::subrangeType ( const Expr l,
const Expr r 
)
pure virtual

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.

virtual Type CVC3::ValidityChecker::subtypeType ( const Expr pred,
const Expr witness 
)
pure virtual

Creates a subtype defined by the given predicate.

Parameters
predis 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).
witnessis an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove $\exists x. pred(x))$. if the witness check fails, a TypecheckException is thrown.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::tupleType ( const Type type0,
const Type type1 
)
pure virtual

2-element tuple

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::tupleType ( const Type type0,
const Type type1,
const Type type2 
)
pure virtual

3-element tuple

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::tupleType ( const std::vector< Type > &  types)
pure virtual

n-element tuple (from a vector of types)

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::recordType ( const std::string &  field,
const Type type 
)
pure virtual

1-element record

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::recordType ( const std::string &  field0,
const Type type0,
const std::string &  field1,
const Type type1 
)
pure virtual

2-element record

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::recordType ( const std::string &  field0,
const Type type0,
const std::string &  field1,
const Type type1,
const std::string &  field2,
const Type type2 
)
pure virtual

3-element record

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::recordType ( const std::vector< std::string > &  fields,
const std::vector< Type > &  types 
)
pure virtual

n-element record (fields and types must be of the same length)

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::dataType ( const std::string &  name,
const std::string &  constructor,
const std::vector< std::string > &  selectors,
const std::vector< Expr > &  types 
)
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().

virtual Type CVC3::ValidityChecker::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 
)
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.

virtual void CVC3::ValidityChecker::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 
)
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.

virtual Type CVC3::ValidityChecker::arrayType ( const Type typeIndex,
const Type typeData 
)
pure virtual

Create an array type (ARRAY typeIndex OF typeData)

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::bitvecType ( int  n)
pure virtual

Create a bitvector type of length n.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::funType ( const Type typeDom,
const Type typeRan 
)
pure virtual

Create a function type typeDom -> typeRan.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::funType ( const std::vector< Type > &  typeDom,
const Type typeRan 
)
pure virtual

Create a function type (t1,t2,...,tn) -> typeRan.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::createType ( const std::string &  typeName)
pure virtual

Create named user-defined uninterpreted type.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Type CVC3::ValidityChecker::createType ( const std::string &  typeName,
const Type def 
)
pure virtual

Create named user-defined interpreted type (type abbreviation)

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::lookupType ( const std::string &  typeName)
pure virtual

Lookup a user-defined (uninterpreted) type by name. Returns Null if none.

Implemented in CVC3::VCL.

virtual ExprManager* CVC3::ValidityChecker::getEM ( )
pure virtual
virtual Expr CVC3::ValidityChecker::varExpr ( const std::string &  name,
const Type type 
)
pure virtual

Create a variable with a given name and type.

Parameters
nameis the name of the variable
typeis its type. The type cannot be a function type.
Returns
an Expr representation of a new variable

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Expr CVC3::ValidityChecker::varExpr ( const std::string &  name,
const Type type,
const Expr def 
)
pure virtual

Create a variable with a given name, type, and value.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::lookupVar ( const std::string &  name,
Type type 
)
pure virtual

Get the variable associated with a name, and its type.

Parameters
nameis the variable name
typeis where the type value is returned
Returns
a variable by the name. If there is no such Expr, a NULL \ Expr is returned.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::getType ( const Expr e)
pure virtual

Get the type of the Expr.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::getBaseType ( const Expr e)
pure virtual

Get the largest supertype of the Expr.

Implemented in CVC3::VCL.

virtual Type CVC3::ValidityChecker::getBaseType ( const Type t)
pure virtual

Get the largest supertype of the Type.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::getTypePred ( const Type t,
const Expr e 
)
pure virtual

Get the subtype predicate.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::stringExpr ( const std::string &  str)
pure virtual

Create a string Expr.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::idExpr ( const std::string &  name)
pure virtual

Create an ID Expr.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const std::vector< Expr > &  kids)
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().

virtual Expr CVC3::ValidityChecker::listExpr ( const Expr e1)
pure virtual

Overloaded version of listExpr with one argument.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const Expr e1,
const Expr e2 
)
pure virtual

Overloaded version of listExpr with two arguments.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const Expr e1,
const Expr e2,
const Expr e3 
)
pure virtual

Overloaded version of listExpr with three arguments.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const std::string &  op,
const std::vector< Expr > &  kids 
)
pure virtual

Overloaded version of listExpr with string operator and many arguments.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const std::string &  op,
const Expr e1 
)
pure virtual

Overloaded version of listExpr with string operator and one argument.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const std::string &  op,
const Expr e1,
const Expr e2 
)
pure virtual

Overloaded version of listExpr with string operator and two arguments.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::listExpr ( const std::string &  op,
const Expr e1,
const Expr e2,
const Expr e3 
)
pure virtual

Overloaded version of listExpr with string operator and three arguments.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::printExpr ( const Expr e)
pure virtual

Prints e to the standard output.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual void CVC3::ValidityChecker::printExpr ( const Expr e,
std::ostream &  os 
)
pure virtual

Prints e to the given ostream.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::parseExpr ( const Expr e)
pure virtual

Parse an expression using a Theory-specific parser.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Type CVC3::ValidityChecker::parseType ( const Expr e)
pure virtual

Parse a type expression using a Theory-specific parser.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::importExpr ( const Expr e)
pure virtual

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.

virtual Type CVC3::ValidityChecker::importType ( const Type t)
pure virtual

Import the Type from another instance of ValidityChecker.

See Also
getType()

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::cmdsFromString ( const std::string &  s,
InputLanguage  lang = PRESENTATION_LANG 
)
pure virtual

Parse a sequence of commands from a presentation language string.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::exprFromString ( const std::string &  e)
pure virtual

Parse an expression from a presentation language string.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::trueExpr ( )
pure virtual

Return TRUE Expr.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Expr CVC3::ValidityChecker::falseExpr ( )
pure virtual

Return FALSE Expr.

Implemented in CVC3::VCL.

Referenced by SAT::CNF_Manager::cons().

virtual Expr CVC3::ValidityChecker::notExpr ( const Expr child)
pure virtual

Create negation.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::andExpr ( const Expr left,
const Expr right 
)
pure virtual

Create 2-element conjunction.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::andExpr ( const std::vector< Expr > &  children)
pure virtual

Create n-element conjunction.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::orExpr ( const Expr left,
const Expr right 
)
pure virtual

Create 2-element disjunction.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::orExpr ( const std::vector< Expr > &  children)
pure virtual

Create n-element disjunction.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::impliesExpr ( const Expr hyp,
const Expr conc 
)
pure virtual

Create Boolean implication.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::iffExpr ( const Expr left,
const Expr right 
)
pure virtual

Create left IFF right (boolean equivalence)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::eqExpr ( const Expr child0,
const Expr child1 
)
pure virtual

Create an equality expression.

The two children must have the same type, and cannot be of type Boolean.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::iteExpr ( const Expr ifpart,
const Expr thenpart,
const Expr elsepart 
)
pure virtual

Create IF ifpart THEN thenpart ELSE elsepart ENDIF.

Parameters
ifpartmust be of type Boolean.
thenpartand
elsepartmust have the same type, which will also be the type of the ite expression.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::distinctExpr ( const std::vector< Expr > &  children)
pure virtual

Create an expression asserting that all the children are different.

Parameters
childrenthe children to be asserted different

Implemented in CVC3::VCL.

virtual Op CVC3::ValidityChecker::createOp ( const std::string &  name,
const Type type 
)
pure virtual

Create a named uninterpreted function with a given type.

Parameters
nameis the new function's name (as ID Expr)
typeis a function type ( [range -> domain] )

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Op CVC3::ValidityChecker::createOp ( const std::string &  name,
const Type type,
const Expr def 
)
pure virtual

Create a named user-defined function with a given type.

Implemented in CVC3::VCL.

virtual Op CVC3::ValidityChecker::lookupOp ( const std::string &  name,
Type type 
)
pure virtual

Get the Op associated with a name, and its type.

Parameters
nameis the operator name
typeis where the type value is returned
Returns
an Op by the name. If there is no such Op, a NULL \ Op is returned.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::funExpr ( const Op op,
const Expr child 
)
pure virtual

Unary function application (op must be of function type)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::funExpr ( const Op op,
const Expr left,
const Expr right 
)
pure virtual

Binary function application (op must be of function type)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::funExpr ( const Op op,
const Expr child0,
const Expr child1,
const Expr child2 
)
pure virtual

Ternary function application (op must be of function type)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::funExpr ( const Op op,
const std::vector< Expr > &  children 
)
pure virtual

n-ary function application (op must be of function type)

Implemented in CVC3::VCL.

virtual bool CVC3::ValidityChecker::addPairToArithOrder ( const Expr smaller,
const Expr bigger 
)
pure virtual

Add the pair of variables to the variable ordering for aritmetic solving. Terms that are not arithmetic will be ignored.

Parameters
smallerthe smaller variable
biggerthe bigger variable

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Expr CVC3::ValidityChecker::ratExpr ( int  n,
int  d = 1 
)
pure virtual

Create a rational number with numerator n and denominator d.

Parameters
nthe numerator
dthe denominator, cannot be 0.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::ratExpr ( const std::string &  n,
const std::string &  d,
int  base 
)
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.

virtual Expr CVC3::ValidityChecker::ratExpr ( const std::string &  n,
int  base = 10 
)
pure virtual

Create a rational from a single string.

Parameters
ncan be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format.
baseis the base in which to interpret the string.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::uminusExpr ( const Expr child)
pure virtual

Unary minus.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::plusExpr ( const Expr left,
const Expr right 
)
pure virtual

Create 2-element sum (left + right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::plusExpr ( const std::vector< Expr > &  children)
pure virtual

Create n-element sum.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::minusExpr ( const Expr left,
const Expr right 
)
pure virtual

Make a difference (left - right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::multExpr ( const Expr left,
const Expr right 
)
pure virtual

Create a product (left * right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::powExpr ( const Expr x,
const Expr n 
)
pure virtual

Create a power expression (x ^ n); n must be integer.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::divideExpr ( const Expr numerator,
const Expr denominator 
)
pure virtual

Create expression x / y.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::ltExpr ( const Expr left,
const Expr right 
)
pure virtual

Create (left < right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::leExpr ( const Expr left,
const Expr right 
)
pure virtual

Create (left <= right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::gtExpr ( const Expr left,
const Expr right 
)
pure virtual

Create (left > right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::geExpr ( const Expr left,
const Expr right 
)
pure virtual

Create (left >= right)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recordExpr ( const std::string &  field,
const Expr expr 
)
pure virtual

Create a 1-element record value (# field := expr #)

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recordExpr ( const std::string &  field0,
const Expr expr0,
const std::string &  field1,
const Expr expr1 
)
pure virtual

Create a 2-element record value (# field0 := expr0, field1 := expr1 #)

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recordExpr ( const std::string &  field0,
const Expr expr0,
const std::string &  field1,
const Expr expr1,
const std::string &  field2,
const Expr expr2 
)
pure virtual

Create a 3-element record value (# field_i := expr_i #)

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recordExpr ( const std::vector< std::string > &  fields,
const std::vector< Expr > &  exprs 
)
pure virtual

Create an n-element record value (# field_i := expr_i #)

Parameters
fields
exprsmust be the same length as fields

Fields will be sorted automatically

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recSelectExpr ( const Expr record,
const std::string &  field 
)
pure virtual

Create record.field (field selection)

Create an expression representing the selection of a field from a record.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::recUpdateExpr ( const Expr record,
const std::string &  field,
const Expr newValue 
)
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.

virtual Expr CVC3::ValidityChecker::readExpr ( const Expr array,
const Expr index 
)
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.

virtual Expr CVC3::ValidityChecker::writeExpr ( const Expr array,
const Expr index,
const Expr newValue 
)
pure virtual

Array update; equivalent to "array WITH index := newValue".

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVConstExpr ( const std::string &  s,
int  base = 2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVConstExpr ( const std::vector< bool > &  bits)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVConstExpr ( const Rational r,
int  len = 0 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newConcatExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newConcatExpr ( const std::vector< Expr > &  kids)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVExtractExpr ( const Expr e,
int  hi,
int  low 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVNegExpr ( const Expr t1)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVAndExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVAndExpr ( const std::vector< Expr > &  kids)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVOrExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVOrExpr ( const std::vector< Expr > &  kids)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVXorExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVXorExpr ( const std::vector< Expr > &  kids)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVXnorExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVXnorExpr ( const std::vector< Expr > &  kids)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVNandExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVNorExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVCompExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVLTExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVLEExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSLTExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSLEExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newSXExpr ( const Expr t1,
int  len 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVUminusExpr ( const Expr t1)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSubExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVPlusExpr ( int  numbits,
const std::vector< Expr > &  k 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVPlusExpr ( int  numbits,
const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVMultExpr ( int  numbits,
const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVUDivExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVURemExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSDivExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSRemExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSModExpr ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newFixedLeftShiftExpr ( const Expr t1,
int  r 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newFixedConstWidthLeftShiftExpr ( const Expr t1,
int  r 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newFixedRightShiftExpr ( const Expr t1,
int  r 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVSHL ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVLSHR ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::newBVASHR ( const Expr t1,
const Expr t2 
)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Rational CVC3::ValidityChecker::computeBVConst ( const Expr e)
pure virtual

'numbits' is the number of bits in the result

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::tupleExpr ( const std::vector< Expr > &  exprs)
pure virtual

Tuple expression.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::tupleSelectExpr ( const Expr tuple,
int  index 
)
pure virtual

Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::tupleUpdateExpr ( const Expr tuple,
int  index,
const Expr newValue 
)
pure virtual

Tuple update; equivalent to "tuple WITH index := newValue".

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::datatypeConsExpr ( const std::string &  constructor,
const std::vector< Expr > &  args 
)
pure virtual

Datatype constructor expression.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::datatypeSelExpr ( const std::string &  selector,
const Expr arg 
)
pure virtual

Datatype selector expression.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::datatypeTestExpr ( const std::string &  constructor,
const Expr arg 
)
pure virtual

Datatype tester expression.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::boundVarExpr ( const std::string &  name,
const std::string &  uid,
const Type type 
)
pure virtual

Create a bound variable with a given name, unique ID (uid) and type.

Parameters
nameis the name of the variable
uidis the unique ID (a string), which must be unique for each variable
typeis its type. The type cannot be a function type.
Returns
an Expr representation of a new variable

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::forallExpr ( const std::vector< Expr > &  vars,
const Expr body 
)
pure virtual

Universal quantifier.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::forallExpr ( const std::vector< Expr > &  vars,
const Expr body,
const Expr trigger 
)
pure virtual

Universal quantifier with a trigger.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::forallExpr ( const std::vector< Expr > &  vars,
const Expr body,
const std::vector< Expr > &  triggers 
)
pure virtual

Universal quantifier with a set of triggers.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::forallExpr ( const std::vector< Expr > &  vars,
const Expr body,
const std::vector< std::vector< Expr > > &  triggers 
)
pure virtual

Universal quantifier with a set of multi-triggers.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::setTriggers ( const Expr e,
const std::vector< std::vector< Expr > > &  triggers 
)
pure virtual

Set triggers for quantifier instantiation.

Parameters
ethe expression for which triggers are being set.
triggersEach 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.

virtual void CVC3::ValidityChecker::setTriggers ( const Expr e,
const std::vector< Expr > &  triggers 
)
pure virtual

Set triggers for quantifier instantiation (no multi-triggers)

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::setTrigger ( const Expr e,
const Expr trigger 
)
pure virtual

Set a single trigger for quantifier instantiation.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::setMultiTrigger ( const Expr e,
const std::vector< Expr > &  multiTrigger 
)
pure virtual

Set a single multi-trigger for quantifier instantiation.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::existsExpr ( const std::vector< Expr > &  vars,
const Expr body 
)
pure virtual

Existential quantifier.

Implemented in CVC3::VCL.

virtual Op CVC3::ValidityChecker::lambdaExpr ( const std::vector< Expr > &  vars,
const Expr body 
)
pure virtual

Lambda-expression.

Implemented in CVC3::VCL.

virtual Op CVC3::ValidityChecker::transClosure ( const Op op)
pure virtual

Transitive closure of a binary predicate.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::simulateExpr ( const Expr f,
const Expr s0,
const std::vector< Expr > &  inputs,
const Expr n 
)
pure virtual

Symbolic simulation expression.

Parameters
fis the next state function (LAMBDA-expression)
s0is the initial state
inputsis the vector of LAMBDA-expressions representing the sequences of inputs to f
nis a constant, the number of cycles to run the simulation.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::setResourceLimit ( unsigned  limit)
pure virtual

Set the resource limit (0==unlimited, 1==exhausted).

Currently, the limit is the total number of processed facts.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::setTimeLimit ( unsigned  limit)
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.

virtual void CVC3::ValidityChecker::assertFormula ( const Expr e)
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().

virtual void CVC3::ValidityChecker::registerAtom ( const Expr e)
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.

virtual Expr CVC3::ValidityChecker::getImpliedLiteral ( )
pure virtual

Return next literal implied by last assertion. Null Expr if none.

Returned literals are either registered atomic formulas or their negation

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::simplify ( const Expr e)
pure virtual

Simplify e with respect to the current context.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual QueryResult CVC3::ValidityChecker::query ( const Expr e)
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.

Parameters
eis the queried formula

Implemented in CVC3::VCL.

Referenced by SAT::CNF_Manager::cons(), and CVC3::VCCmd::evaluateCommand().

virtual QueryResult CVC3::ValidityChecker::checkUnsat ( const Expr e)
pure virtual

Check satisfiability of the expr in the current context.

Equivalent to query(!e)

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual QueryResult CVC3::ValidityChecker::checkContinue ( )
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().

virtual QueryResult CVC3::ValidityChecker::restart ( const Expr e)
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().

virtual void CVC3::ValidityChecker::returnFromCheck ( )
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.

virtual void CVC3::ValidityChecker::getUserAssumptions ( std::vector< Expr > &  assumptions)
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.

Parameters
assumptionsshould be empty on entry.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::getInternalAssumptions ( std::vector< Expr > &  assumptions)
pure virtual

Get assumptions made internally in this and all previous contexts.

Internal assumptions are literals assumed by the sat solver.

Parameters
assumptionsshould be empty on entry.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::getAssumptions ( std::vector< Expr > &  assumptions)
pure virtual

Get all assumptions made in this and all previous contexts.

Parameters
assumptionsshould be empty on entry.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual void CVC3::ValidityChecker::getAssumptionsUsed ( std::vector< Expr > &  assumptions)
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

Parameters
assumptionsshould be empty on entry.

Implemented in CVC3::VCL.

virtual Expr CVC3::ValidityChecker::getProofQuery ( )
pure virtual

Set the resource limit (0==unlimited, 1==exhausted).

Currently, the limit is the total number of processed facts.

Implemented in CVC3::VCL.

virtual void CVC3::ValidityChecker::getCounterExample ( std::vector< Expr > &  assumptions,
bool  inOrder = true 
)
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.

Parameters
assumptionsshould be empty on entry.
inOrderif 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().

virtual void CVC3::ValidityChecker::getConcreteModel ( ExprMap< Expr > &  m)
pure virtual

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().

virtual QueryResult CVC3::ValidityChecker::tryModelGeneration ( )
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().

virtual FormulaValue CVC3::ValidityChecker::value ( const Expr e)
pure virtual

Set the resource limit (0==unlimited, 1==exhausted).

Currently, the limit is the total number of processed facts.

Implemented in CVC3::VCL.

virtual bool CVC3::ValidityChecker::inconsistent ( std::vector< Expr > &  assumptions)
pure virtual

Returns true if the current context is inconsistent.

Also returns a minimal set of assertions used to determine the inconsistency.

Parameters
assumptionsshould be empty on entry.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual bool CVC3::ValidityChecker::inconsistent ( )
pure virtual

Returns true if the current context is inconsistent.

Implemented in CVC3::VCL.

virtual bool CVC3::ValidityChecker::incomplete ( )
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().

virtual bool CVC3::ValidityChecker::incomplete ( std::vector< std::string > &  reasons)
pure virtual

Returns true if the invalid result from last query() is imprecise.

See Also
incomplete()

The argument is filled with the reasons for incompleteness (they are intended to be shown to the end user).

Implemented in CVC3::VCL.

virtual Proof CVC3::ValidityChecker::getProof ( )
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().

virtual Expr CVC3::ValidityChecker::getValue ( Expr  e)
pure virtual

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().

virtual Expr CVC3::ValidityChecker::getAssignment ( )
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().

virtual Expr CVC3::ValidityChecker::getTCC ( )
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().

virtual void CVC3::ValidityChecker::getAssumptionsTCC ( std::vector< Expr > &  assumptions)
pure virtual

Return the set of assumptions used in the proof of the last TCC.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual Proof CVC3::ValidityChecker::getProofTCC ( )
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().

virtual Expr CVC3::ValidityChecker::getClosure ( )
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().

virtual Proof CVC3::ValidityChecker::getProofClosure ( )
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().

virtual int CVC3::ValidityChecker::stackLevel ( )
pure virtual

Returns the current stack level. Initial level is 0.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual void CVC3::ValidityChecker::push ( )
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().

virtual void CVC3::ValidityChecker::pop ( )
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().

virtual void CVC3::ValidityChecker::popto ( int  stackLevel)
pure virtual

Restore the current context to the given stackLevel.

Parameters
stackLevelshould 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().

virtual int CVC3::ValidityChecker::scopeLevel ( )
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().

virtual void CVC3::ValidityChecker::pushScope ( )
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().

virtual void CVC3::ValidityChecker::popScope ( )
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().

virtual void CVC3::ValidityChecker::poptoScope ( int  scopeLevel)
pure virtual

Restore the current context to the given scopeLevel.

Parameters
scopeLevelshould 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().

virtual Context* CVC3::ValidityChecker::getCurrentContext ( )
pure virtual

Get the current context.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::VCCmd().

virtual void CVC3::ValidityChecker::reset ( )
pure virtual

Destroy and recreate validity checker: resets everything except for flags.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::processCommands().

virtual void CVC3::ValidityChecker::logAnnotation ( const Expr annot)
pure virtual

Add an annotation to the current script - prints annot when translating.

Implemented in CVC3::VCL.

Referenced by CVC3::VCCmd::evaluateCommand().

virtual void CVC3::ValidityChecker::loadFile ( const std::string &  fileName,
InputLanguage  lang = PRESENTATION_LANG,
bool  interactive = false,
bool  calledFromParser = false 
)
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().

virtual void CVC3::ValidityChecker::loadFile ( std::istream &  is,
InputLanguage  lang = PRESENTATION_LANG,
bool  interactive = false 
)
pure virtual

Read and execute the commands from a stream.

Implemented in CVC3::VCL.

virtual Statistics& CVC3::ValidityChecker::getStatistics ( )
pure virtual

Get statistics object.

Implemented in CVC3::VCL.

Referenced by sighandler().

virtual void CVC3::ValidityChecker::printStatistics ( )
pure virtual

Print collected statistics to stdout.

Implemented in CVC3::VCL.

Referenced by main().


The documentation for this class was generated from the following files: