#include <vcl.h>

Inherits CVC3::ValidityChecker.

Collaboration diagram for CVC3::VCL:

[legend]

List of all members.

Classes

class UserAssertion
Structure to hold user assertions indexed by declaration order. More...

Public Member Functions

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

Private Member Functions

Theorem3 deriveClosure (const Theorem3 &thm)
Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi".
void getAssumptionsRec (const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs)
Recursive assumption graph traversal to find user assumptions.
void getAssumptions (const Assumptions &a, std::vector< Expr > &assumptions)
Get set of user assertions from the set of assumptions.
Theorem checkTCC (const Expr &tcc)
Check the tcc.
void init (void)
Initialize everything except flags.
void destroy (void)
Destroy everything except flags.

Private Attributes

ExprManager * d_em
Pointers to main system components.
ContextManager * d_cm
TheoremManager * d_tm
SearchEngine * d_se
TheoryCore * d_theoryCore
Pointers to theories.
TheoryUF * d_theoryUF
TheoryArith * d_theoryArith
TheoryArray * d_theoryArray
TheoryQuant * d_theoryQuant
TheoryRecords * d_theoryRecords
TheorySimulate * d_theorySimulate
TheoryBitvector * d_theoryBitvector
TheoryDatatype * d_theoryDatatype
Translator * d_translator
std::vector< Theory * > d_theories
All theories are stored in this common vector.
CLFlags * d_flags
Command line flags.
CDO< int > * d_stackLevel
User-level view of the scope stack.
Statistics * d_statistics
Run-time statistics.
size_t d_nextIdx
Next index for user assertion.
CDMap< Expr, UserAssertion > * d_userAssertions
Backtracking map of user assertions.
CDList< Expr > * d_batchedAssertions
Backtracking map of assertions when assertion batching is on.
CDO< unsigned > * d_batchedAssertionsIdx
Index into batched Assertions.
Theorem3 d_lastQuery
Result of the last query()
Theorem d_lastQueryTCC
Result of the last query(e, true) (for a TCC).
Theorem3 d_lastClosure
Closure of the last query(e): |- Gamma => e.
bool d_dump
Whether to dump a trace (or a translated version)

Detailed Description

Definition at line 50 of file vcl.h.

Constructor & Destructor Documentation

VCL::VCL ( const CLFlags & flags )

Definition at line 408 of file vcl.cpp.

References IF_DEBUG.

VCL::~VCL ( )

Definition at line 608 of file vcl.cpp.

References IF_DEBUG, and TRACE_MSG.

Member Function Documentation

Theorem3 VCL::deriveClosure ( const Theorem3 & thm ) [private]

Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi".

Definition at line 309 of file vcl.cpp.

References CVC3::Assumptions::clear(), and CVC3::Theorem3::getAssumptionsRef().

void VCL::getAssumptionsRec	(	const Theorem &	thm,
		std::set< UserAssertion > &	assumptions,
		bool	addTCCs
	)		`[private]`

Recursive assumption graph traversal to find user assumptions.

If an assumption has a TCC, traverse the proof of TCC and add its assumptions to the set recursively.

Definition at line 352 of file vcl.cpp.

References DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theorem::isNull(), CVC3::Theorem::isRefl(), CVC3::Theorem::setFlag(), CVC3::VCL::UserAssertion::tcc(), CVC3::VCL::UserAssertion::thm(), and CVC3::Theorem::toString().

void VCL::getAssumptions	(	const Assumptions &	a,
		std::vector< Expr > &	assumptions
	)		`[private]`

Get set of user assertions from the set of assumptions.

Definition at line 379 of file vcl.cpp.

References CVC3::Assumptions::begin(), CVC3::Assumptions::empty(), and CVC3::Assumptions::end().

Theorem VCL::checkTCC ( const Expr & tcc ) [private]

Check the tcc.

Definition at line 1810 of file vcl.cpp.

References CVC3::ABORT, FatalAssert, CVC3::INVALID, CVC3::Expr::toString(), UNKNOWN, and CVC3::VALID.

void VCL::init ( void ) [private]

Initialize everything except flags.

Definition at line 447 of file vcl.cpp.

References DebugAssert.

void VCL::destroy ( void ) [private]

Destroy everything except flags.

Definition at line 549 of file vcl.cpp.

References TRACE, and TRACE_MSG.

CLFlags& CVC3::VCL::getFlags ( ) const [inline, 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.

Type VCL::subrangeType	(	const Expr &	l,
		const Expr &	r
	)		`[virtual]`

Type VCL::subtypeType	(	const Expr &	pred,
		const Expr &	witness
	)		`[virtual]`

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 $\exists x. pred(x))$ . if the witness check fails, a TypecheckException is thrown.

Type VCL::tupleType	(	const Type &	type0,
		const Type &	type1
	)		`[virtual]`

Type VCL::recordType	(	const std::string &	field,
		const Type &	type
	)		`[virtual]`

Type VCL::recordType	(	const std::string &	field0,
		const Type &	type0,
		const std::string &	field1,
		const Type &	type1
	)		`[virtual]`

Type VCL::recordType	(	const std::vector< std::string > &	fields,
		const std::vector< Type > &	types
	)		`[virtual]`

Type VCL::dataType	(	const std::string &	name,
		const std::string &	constructor,
		const std::vector< std::string > &	selectors,
		const std::vector< Expr > &	types
	)		`[virtual]`

void VCL::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
	)		`[virtual]`

Type VCL::arrayType	(	const Type &	typeIndex,
		const Type &	typeData
	)		`[virtual]`

name	is the name of the variable
type	is its type. The type cannot be a function type.

Type VCL::funType	(	const Type &	typeDom,
		const Type &	typeRan
	)		`[virtual]`

Type VCL::createType	(	const std::string &	typeName,
		const Type &	def
	)		`[virtual]`

Expr VCL::varExpr	(	const std::string &	name,
		const Type &	type
	)		`[virtual]`

Expr VCL::lookupVar	(	const std::string &	name,
		Type *	type
	)		`[virtual]`

name	is the variable name
type	is where the type value is returned

Expr VCL::getTypePred	(	const Type &	t,
		const Expr &	e
	)		`[virtual]`

Expr VCL::listExpr	(	const Expr &	e1,
		const Expr &	e2
	)		`[virtual]`

void VCL::printExpr	(	const Expr &	e,
		std::ostream &	os
	)		`[virtual]`

void VCL::cmdsFromString	(	const std::string &	s,
		InputLanguage	lang
	)		`[virtual]`

Expr VCL::andExpr	(	const Expr &	left,
		const Expr &	right
	)		`[virtual]`

CVC3::VCL Class Reference