CVC3::VCL Class Reference

#include <vcl.h>

Inheritance diagram for CVC3::VCL:

[legend]

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
  

• 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 std::vector< std::vector< Expr > > &triggers)

  Universal quantifier with triggers.
  

• void setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers)

  Set triggers 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 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 48 of file vcl.h.

---

Constructor & Destructor Documentation

CVC3::VCL::VCL

(

const CLFlags &

flags

)

VCL::~VCL

(

)

Definition at line 594 of file vcl.cpp.

References d_flags, destroy(), 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 295 of file vcl.cpp.

References d_se, getAssumptionsRec(), CVC3::Theorem3::getAssumptionsRef(), CVC3::SearchEngine::getCommonRules(), getFlags(), and CVC3::CommonProofRules::implIntro3().

Referenced by getClosure(), and getProofClosure().

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 338 of file vcl.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::count(), d_nextIdx, d_userAssertions, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theorem::isNull(), CVC3::Theorem::isRefl(), CVC3::Theorem::setFlag(), CVC3::VCL::VCL::UserAssertion::tcc(), CVC3::VCL::VCL::UserAssertion::thm(), and CVC3::Theorem::toString().

Referenced by deriveClosure(), and getAssumptions().

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

Get set of user assertions from the set of assumptions.

Definition at line 365 of file vcl.cpp.

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

Referenced by getAssumptionsTCC(), and inconsistent().

Theorem VCL::checkTCC

(

const Expr &

tcc

)

[private]

Check the tcc.

Definition at line 1755 of file vcl.cpp.

References CVC3::ABORT, CVC3::SearchEngine::checkValid(), d_lastQueryTCC, d_se, FatalAssert, CVC3::INVALID, CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), simplify(), CVC3::Expr::toString(), CVC3::UNKNOWN, and CVC3::VALID.

Referenced by assertFormula(), createOp(), query(), and varExpr().

void VCL::init

(

void

)

[private]

Initialize everything except flags.

Definition at line 433 of file vcl.cpp.

References d_batchedAssertions, d_batchedAssertionsIdx, d_cm, d_dump, d_em, d_flags, d_nextIdx, d_se, d_stackLevel, d_statistics, d_theories, d_theoryArith, d_theoryArray, d_theoryBitvector, d_theoryCore, d_theoryDatatype, d_theoryQuant, d_theoryRecords, d_theorySimulate, d_theoryUF, d_tm, d_translator, d_userAssertions, DebugAssert, falseExpr(), CVC3::ContextManager::getCurrentContext(), getCurrentContext(), CVC3::TheoryCore::getExprTrans(), CVC3::ContextManager::push(), CVC3::Theory::reflexivityRule(), CVC3::Expr::setFind(), CVC3::TheoryCore::setResourceLimit(), CVC3::Translator::setTheoryArith(), CVC3::ExprTransform::setTheoryArith(), CVC3::Translator::setTheoryArray(), CVC3::Translator::setTheoryBitvector(), CVC3::Translator::setTheoryCore(), CVC3::Translator::setTheoryDatatype(), CVC3::Translator::setTheoryQuant(), CVC3::Translator::setTheoryRecords(), CVC3::Translator::setTheorySimulate(), CVC3::Translator::setTheoryUF(), CVC3::TheoryCore::setTimeLimit(), CVC3::ExprManager::setTM(), CVC3::Translator::start(), and trueExpr().

Referenced by reset().

void VCL::destroy

(

void

)

[private]

Destroy everything except flags.

Definition at line 535 of file vcl.cpp.

References CVC3::TheoremManager::clear(), CVC3::ExprManager::clear(), d_batchedAssertions, d_batchedAssertionsIdx, d_cm, d_em, d_lastClosure, d_lastQuery, d_lastQueryTCC, d_se, d_stackLevel, d_statistics, d_theories, d_tm, d_translator, d_userAssertions, CVC3::Translator::finish(), CVC3::ContextManager::popto(), popto(), CVC3::TRACE, and TRACE_MSG.

Referenced by reset(), and ~VCL().

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.

Implements CVC3::ValidityChecker.

Definition at line 167 of file vcl.h.

Referenced by assertFormula(), createOp(), deriveClosure(), getAssumptions(), query(), and varExpr().

void VCL::reprocessFlags

(

)

[virtual]

Force reprocessing of all flags.

Implements CVC3::ValidityChecker.

Definition at line 609 of file vcl.cpp.

References d_flags, d_se, d_theories, d_theoryArith, d_theoryCore, d_translator, DebugAssert, CVC3::Theory::getName(), CVC3::SearchEngine::getName(), CVC3::CLFlags::setFlag(), and CVC3::Translator::setTheoryArith().

TheoryCore * VCL::core

(

)

Definition at line 682 of file vcl.cpp.

References d_theoryCore.

Type VCL::boolType

(

)

[virtual]

Create type BOOLEAN.

Implements CVC3::ValidityChecker.

Definition at line 686 of file vcl.cpp.

References CVC3::Theory::boolType(), and d_theoryCore.

Type VCL::realType

(

)

[virtual]

Create type REAL.

Implements CVC3::ValidityChecker.

Definition at line 691 of file vcl.cpp.

References d_theoryArith, and CVC3::TheoryArith::realType().

Type VCL::intType

(

)

[virtual]

Create type INT.

Implements CVC3::ValidityChecker.

Definition at line 697 of file vcl.cpp.

References d_theoryArith, and CVC3::TheoryArith::intType().

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

Create a subrange type [l..r].

l and r can be Null; l=Null represents minus infinity, r=Null is plus infinity.

Implements CVC3::ValidityChecker.

Definition at line 702 of file vcl.cpp.

References d_theoryArith, and CVC3::TheoryArith::subrangeType().

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

Creates a subtype defined by the given predicate.

Parameters:

	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 . if the witness check fails, a TypecheckException is thrown.

Implements CVC3::ValidityChecker.

Definition at line 707 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::newSubtypeExpr().

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

2-element tuple

Implements CVC3::ValidityChecker.

Definition at line 713 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::tupleType().

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

3-element tuple

Implements CVC3::ValidityChecker.

Definition at line 722 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::tupleType().

Type VCL::tupleType

(

const std::vector< Type > &

types

)

[virtual]

n-element tuple (from a vector of types)

Implements CVC3::ValidityChecker.

Definition at line 732 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::tupleType().

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

1-element record

Implements CVC3::ValidityChecker.

Definition at line 738 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::recordType().

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

2-element record

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 748 of file vcl.cpp.

References d_theoryRecords, CVC3::TheoryRecords::recordType(), and CVC3::sort2().

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

3-element record

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 761 of file vcl.cpp.

References d_theoryRecords, CVC3::TheoryRecords::recordType(), and CVC3::sort2().

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

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 778 of file vcl.cpp.

References d_theoryRecords, DebugAssert, CVC3::TheoryRecords::recordType(), and CVC3::sort2().

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

Implements CVC3::ValidityChecker.

Definition at line 792 of file vcl.cpp.

Type VCL::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
	)			[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.

Implements CVC3::ValidityChecker.

Definition at line 809 of file vcl.cpp.

References d_dump, d_theoryDatatype, d_translator, CVC3::TheoryDatatype::dataType(), and CVC3::Translator::dump().

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]

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.

Implements CVC3::ValidityChecker.

Definition at line 822 of file vcl.cpp.

References CVC3::Expr::arity(), d_dump, d_theoryDatatype, d_translator, CVC3::TheoryDatatype::dataType(), and CVC3::Translator::dump().

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

Create an array type (ARRAY typeIndex OF typeData).

Implements CVC3::ValidityChecker.

Definition at line 838 of file vcl.cpp.

Type VCL::bitvecType

(

int

n

)

[virtual]

Create a bitvector type of length n.

Implements CVC3::ValidityChecker.

Definition at line 844 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBitvectorType().

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

Create a function type typeDom -> typeRan.

Implements CVC3::ValidityChecker.

Definition at line 850 of file vcl.cpp.

References CVC3::Type::funType().

Referenced by funType().

Type VCL::funType	(	const std::vector< Type > &	typeDom,
		const Type &	typeRan
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 856 of file vcl.cpp.

References DebugAssert, and funType().

Type VCL::createType

(

const std::string &

typeName

)

[virtual]

Create named user-defined uninterpreted type.

Implements CVC3::ValidityChecker.

Definition at line 862 of file vcl.cpp.

References d_dump, d_theoryCore, d_translator, CVC3::Translator::dump(), idExpr(), listExpr(), CVC3::Theory::newTypeExpr(), and CVC3::TYPE.

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

Create named user-defined interpreted type (type abbreviation).

Implements CVC3::ValidityChecker.

Definition at line 871 of file vcl.cpp.

References d_dump, d_theoryCore, d_translator, CVC3::Translator::dump(), CVC3::Type::getExpr(), idExpr(), CVC3::Theory::newTypeExpr(), and CVC3::TYPE.

Type VCL::lookupType

(

const std::string &

typeName

)

[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 880 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::lookupTypeExpr().

ExprManager* CVC3::VCL::getEM

(

)

[inline, virtual]

Return the ExprManager.

Implements CVC3::ValidityChecker.

Definition at line 209 of file vcl.h.

Referenced by listExpr(), and stringExpr().

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

Create a variable with a given name and type.

Parameters:

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

Returns:

an Expr representation of a new variable

Implements CVC3::ValidityChecker.

Definition at line 886 of file vcl.cpp.

References CVC3::CONST, d_dump, d_theoryCore, d_translator, CVC3::Translator::dump(), CVC3::Type::getExpr(), idExpr(), and CVC3::Theory::newVar().

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

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

Implements CVC3::ValidityChecker.

Definition at line 896 of file vcl.cpp.

References boundVarExpr(), checkTCC(), CVC3::CONST, d_dump, d_theoryCore, d_translator, CVC3::Translator::dump(), eqExpr(), forallExpr(), getBaseType(), CVC3::Type::getExpr(), getFlags(), CVC3::Expr::getType(), getTypePred(), idExpr(), CVC3::Theory::newVar(), CVC3::Type::toString(), and CVC3::TRACE.

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

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

Parameters:

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

Returns:

a variable by the name. If there is no such Expr, a NULL \ Expr is returned.

Implements CVC3::ValidityChecker.

Definition at line 941 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::lookupVar().

Type VCL::getType

(

const Expr &

e

)

[virtual]

Get the type of the Expr.

Implements CVC3::ValidityChecker.

Definition at line 947 of file vcl.cpp.

References CVC3::Expr::getType().

Type VCL::getBaseType

(

const Expr &

e

)

[virtual]

Get the largest supertype of the Expr.

Implements CVC3::ValidityChecker.

Definition at line 953 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::getBaseType().

Referenced by createOp(), and varExpr().

Type VCL::getBaseType

(

const Type &

t

)

[virtual]

Get the largest supertype of the Type.

Implements CVC3::ValidityChecker.

Definition at line 959 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::getBaseType().

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

Get the subtype predicate.

Implements CVC3::ValidityChecker.

Definition at line 965 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::getTypePred().

Referenced by createOp(), and varExpr().

Expr VCL::stringExpr

(

const std::string &

str

)

[virtual]

Create a string Expr.

Implements CVC3::ValidityChecker.

Definition at line 971 of file vcl.cpp.

References getEM(), and CVC3::ExprManager::newStringExpr().

Referenced by idExpr().

Expr VCL::idExpr

(

const std::string &

name

)

[virtual]

Create an ID Expr.

Implements CVC3::ValidityChecker.

Definition at line 976 of file vcl.cpp.

References CVC3::ID, and stringExpr().

Referenced by createOp(), createType(), listExpr(), and varExpr().

Expr VCL::listExpr

(

const std::vector< Expr > &

kids

)

[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);

Implements CVC3::ValidityChecker.

Definition at line 981 of file vcl.cpp.

References getEM(), and CVC3::RAW_LIST.

Referenced by createType(), and listExpr().

Expr VCL::listExpr

(

const Expr &

e1

)

[virtual]

Overloaded version of listExpr with one argument.

Implements CVC3::ValidityChecker.

Definition at line 986 of file vcl.cpp.

References CVC3::RAW_LIST.

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

Overloaded version of listExpr with two arguments.

Implements CVC3::ValidityChecker.

Definition at line 991 of file vcl.cpp.

References CVC3::RAW_LIST.

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

Overloaded version of listExpr with three arguments.

Implements CVC3::ValidityChecker.

Definition at line 996 of file vcl.cpp.

References CVC3::RAW_LIST.

Expr VCL::listExpr	(	const std::string &	op,
		const std::vector< Expr > &	kids
	)			[virtual]

Overloaded version of listExpr with string operator and many arguments.

Implements CVC3::ValidityChecker.

Definition at line 1001 of file vcl.cpp.

References idExpr(), and listExpr().

Expr VCL::listExpr	(	const std::string &	op,
		const Expr &	e1
	)			[virtual]

Overloaded version of listExpr with string operator and one argument.

Implements CVC3::ValidityChecker.

Definition at line 1009 of file vcl.cpp.

References idExpr(), and CVC3::RAW_LIST.

Expr VCL::listExpr	(	const std::string &	op,
		const Expr &	e1,
		const Expr &	e2
	)			[virtual]

Overloaded version of listExpr with string operator and two arguments.

Implements CVC3::ValidityChecker.

Definition at line 1014 of file vcl.cpp.

References idExpr(), and CVC3::RAW_LIST.

Expr VCL::listExpr	(	const std::string &	op,
		const Expr &	e1,
		const Expr &	e2,
		const Expr &	e3
	)			[virtual]

Overloaded version of listExpr with string operator and three arguments.

Implements CVC3::ValidityChecker.

Definition at line 1020 of file vcl.cpp.

References idExpr(), and listExpr().

void VCL::printExpr

(

const Expr &

e

)

[virtual]

Prints e to the standard output.

Implements CVC3::ValidityChecker.

Definition at line 1031 of file vcl.cpp.

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

Prints e to the given ostream.

Implements CVC3::ValidityChecker.

Definition at line 1036 of file vcl.cpp.

References std::endl().

Expr VCL::parseExpr

(

const Expr &

e

)

[virtual]

Parse an expression using a Theory-specific parser.

Implements CVC3::ValidityChecker.

Definition at line 1041 of file vcl.cpp.

References d_theoryCore, and CVC3::TheoryCore::parseExprTop().

Referenced by exprFromString().

Type VCL::parseType

(

const Expr &

e

)

[virtual]

Parse a type expression using a Theory-specific parser.

Implements CVC3::ValidityChecker.

Definition at line 1046 of file vcl.cpp.

References d_theoryCore, and CVC3::TheoryCore::parseExpr().

Expr VCL::importExpr

(

const Expr &

e

)

[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.

Implements CVC3::ValidityChecker.

Definition at line 1051 of file vcl.cpp.

References d_em, and CVC3::ExprManager::rebuild().

Type VCL::importType

(

const Type &

t

)

[virtual]

Import the Type from another instance of ValidityChecker.

See also:

getType()

Implements CVC3::ValidityChecker.

Definition at line 1057 of file vcl.cpp.

References d_em, CVC3::Type::getExpr(), and CVC3::ExprManager::rebuild().

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

Parse a sequence of commands from a presentation language string.

Implements CVC3::ValidityChecker.

Definition at line 1062 of file vcl.cpp.

References loadFile().

Expr VCL::exprFromString

(

const std::string &

e

)

[virtual]

Parse an expression from a presentation language string.

Implements CVC3::ValidityChecker.

Definition at line 1068 of file vcl.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::isNull(), CVC3::Parser::next(), parseExpr(), CVC3::PRESENTATION_LANG, and CVC3::RAW_LIST.

Expr VCL::trueExpr

(

)

[virtual]

Return TRUE Expr.

Implements CVC3::ValidityChecker.

Definition at line 1081 of file vcl.cpp.

References d_em, and CVC3::ExprManager::trueExpr().

Referenced by init().

Expr VCL::falseExpr

(

)

[virtual]

Return FALSE Expr.

Implements CVC3::ValidityChecker.

Definition at line 1087 of file vcl.cpp.

References d_em, and CVC3::ExprManager::falseExpr().

Referenced by checkContinue(), and init().

Expr VCL::notExpr

(

const Expr &

child

)

[virtual]

Create negation.

Implements CVC3::ValidityChecker.

Definition at line 1093 of file vcl.cpp.

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

Create 2-element conjunction.

Implements CVC3::ValidityChecker.

Definition at line 1099 of file vcl.cpp.

Referenced by checkContinue().

Expr VCL::andExpr

(

const std::vector< Expr > &

children

)

[virtual]

Create n-element conjunction.

Implements CVC3::ValidityChecker.

Definition at line 1105 of file vcl.cpp.

References CVC3::AND.

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

Create 2-element disjunction.

Implements CVC3::ValidityChecker.

Definition at line 1113 of file vcl.cpp.

Referenced by tryModelGeneration().

Expr VCL::orExpr

(

const std::vector< Expr > &

children

)

[virtual]

Create n-element disjunction.

Implements CVC3::ValidityChecker.

Definition at line 1119 of file vcl.cpp.

References CVC3::OR.

Expr VCL::impliesExpr	(	const Expr &	hyp,
		const Expr &	conc
	)			[virtual]

Create Boolean implication.

Implements CVC3::ValidityChecker.

Definition at line 1127 of file vcl.cpp.

References CVC3::Expr::impExpr().

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

Create left IFF right (boolean equivalence).

Implements CVC3::ValidityChecker.

Definition at line 1133 of file vcl.cpp.

References CVC3::Expr::iffExpr().

Expr VCL::eqExpr	(	const Expr &	child0,
		const Expr &	child1
	)			[virtual]

Create an equality expression.

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

Implements CVC3::ValidityChecker.

Definition at line 1139 of file vcl.cpp.

References CVC3::Expr::eqExpr().

Referenced by varExpr().

Expr VCL::distinctExpr

(

const std::vector< Expr > &

children

)

[virtual]

Create an expression asserting that all the children are different.

Parameters:

children

the children to be asserted different

Implements CVC3::ValidityChecker.

Definition at line 1144 of file vcl.cpp.

References CVC3::DISTINCT.

Expr VCL::iteExpr	(	const Expr &	ifpart,
		const Expr &	thenpart,
		const Expr &	elsepart
	)			[virtual]

Create IF ifpart THEN thenpart ELSE elsepart ENDIF.

Parameters:

	ifpart	must be of type Boolean.
	thenpart	and
	elsepart	must have the same type, which will also be the type of the ite expression.

Implements CVC3::ValidityChecker.

Definition at line 1149 of file vcl.cpp.

References CVC3::Expr::iteExpr().

Op VCL::createOp	(	const std::string &	name,
		const Type &	type
	)			[virtual]

Create a named uninterpreted function with a given type.

Parameters:

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

Implements CVC3::ValidityChecker.

Definition at line 1155 of file vcl.cpp.

References CVC3::CONST, d_dump, d_theoryCore, d_translator, CVC3::Translator::dump(), CVC3::Type::getExpr(), getFlags(), idExpr(), CVC3::Type::isFunction(), and CVC3::Theory::newFunction().

Op VCL::createOp	(	const std::string &	name,
		const Type &	type,
		const Expr &	def
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1167 of file vcl.cpp.

References CVC3::Expr::andExpr(), CVC3::Type::arity(), checkTCC(), CVC3::CONST, d_dump, d_em, d_theoryCore, d_translator, CVC3::Translator::dump(), forallExpr(), getBaseType(), CVC3::Type::getExpr(), getFlags(), CVC3::Theory::getTCC(), CVC3::Expr::getType(), getTypePred(), idExpr(), CVC3::Type::isFunction(), CVC3::Expr::mkOp(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Theory::newFunction(), CVC3::Expr::toString(), and CVC3::Type::toString().

Op VCL::lookupOp	(	const std::string &	name,
		Type *	type
	)			[virtual]

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

Parameters:

	name	is the operator name
	type	is where the type value is returned

Returns:

an Op by the name. If there is no such Op, a NULL \ Op is returned.

Implements CVC3::ValidityChecker.

Definition at line 1225 of file vcl.cpp.

References d_theoryCore, and CVC3::Theory::lookupFunction().

Expr VCL::funExpr	(	const Op &	op,
		const Expr &	child
	)			[virtual]

Unary function application (op must be of function type).

Implements CVC3::ValidityChecker.

Definition at line 1231 of file vcl.cpp.

Expr VCL::funExpr	(	const Op &	op,
		const Expr &	left,
		const Expr &	right
	)			[virtual]

Binary function application (op must be of function type).

Implements CVC3::ValidityChecker.

Definition at line 1237 of file vcl.cpp.

Expr VCL::funExpr	(	const Op &	op,
		const Expr &	child0,
		const Expr &	child1,
		const Expr &	child2
	)			[virtual]

Ternary function application (op must be of function type).

Implements CVC3::ValidityChecker.

Definition at line 1243 of file vcl.cpp.

Expr VCL::funExpr	(	const Op &	op,
		const std::vector< Expr > &	children
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1249 of file vcl.cpp.

bool VCL::addPairToArithOrder	(	const Expr &	smaller,
		const Expr &	bigger
	)			[virtual]

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

Parameters:

	smaller	the smaller variable
	bigger	the bigger variable

Implements CVC3::ValidityChecker.

Definition at line 1254 of file vcl.cpp.

References CVC3::TheoryArith::addPairToArithOrder(), CVC3::ARITH_VAR_ORDER, d_dump, d_theoryArith, d_translator, and CVC3::Translator::dump().

Expr VCL::ratExpr	(	int	n,
		int	d
	)			[virtual]

Create a rational number with numerator n and denominator d.

Parameters:

	n	the numerator
	d	the denominator, cannot be 0.

Implements CVC3::ValidityChecker.

Definition at line 1262 of file vcl.cpp.

References d_em, DebugAssert, and CVC3::ExprManager::newRatExpr().

Referenced by popto(), and poptoScope().

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

Implements CVC3::ValidityChecker.

Definition at line 1269 of file vcl.cpp.

References d_em, and CVC3::ExprManager::newRatExpr().

Expr VCL::ratExpr	(	const std::string &	n,
		int	base
	)			[virtual]

Create a rational from a single string.

Parameters:

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

Implements CVC3::ValidityChecker.

Definition at line 1275 of file vcl.cpp.

References d_em, CVC3::ExprManager::newRatExpr(), and CVC3::pow().

Expr VCL::uminusExpr

(

const Expr &

child

)

[virtual]

Unary minus.

Implements CVC3::ValidityChecker.

Definition at line 1302 of file vcl.cpp.

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

Create 2-element sum (left + right).

Implements CVC3::ValidityChecker.

Definition at line 1308 of file vcl.cpp.

Expr VCL::plusExpr

(

const std::vector< Expr > &

children

)

[virtual]

Create n-element sum.

Implements CVC3::ValidityChecker.

Definition at line 1313 of file vcl.cpp.

References CVC3::PLUS.

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

Make a difference (left - right).

Implements CVC3::ValidityChecker.

Definition at line 1319 of file vcl.cpp.

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

Create a product (left * right).

Implements CVC3::ValidityChecker.

Definition at line 1325 of file vcl.cpp.

Expr VCL::powExpr	(	const Expr &	x,
		const Expr &	n
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1331 of file vcl.cpp.

Expr VCL::divideExpr	(	const Expr &	numerator,
		const Expr &	denominator
	)			[virtual]

Create expression x / y.

Implements CVC3::ValidityChecker.

Definition at line 1337 of file vcl.cpp.

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

Create (left < right).

Implements CVC3::ValidityChecker.

Definition at line 1343 of file vcl.cpp.

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

Create (left <= right).

Implements CVC3::ValidityChecker.

Definition at line 1349 of file vcl.cpp.

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

Create (left > right).

Implements CVC3::ValidityChecker.

Definition at line 1355 of file vcl.cpp.

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

Create (left >= right).

Implements CVC3::ValidityChecker.

Definition at line 1361 of file vcl.cpp.

Expr VCL::recordExpr	(	const std::string &	field,
		const Expr &	expr
	)			[virtual]

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1367 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::recordExpr().

Expr VCL::recordExpr	(	const std::string &	field0,
		const Expr &	expr0,
		const std::string &	field1,
		const Expr &	expr1
	)			[virtual]

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1377 of file vcl.cpp.

References d_theoryRecords, CVC3::TheoryRecords::recordExpr(), and CVC3::sort2().

Expr VCL::recordExpr	(	const std::string &	field0,
		const Expr &	expr0,
		const std::string &	field1,
		const Expr &	expr1,
		const std::string &	field2,
		const Expr &	expr2
	)			[virtual]

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1391 of file vcl.cpp.

References d_theoryRecords, CVC3::TheoryRecords::recordExpr(), and CVC3::sort2().

Expr VCL::recordExpr	(	const std::vector< std::string > &	fields,
		const std::vector< Expr > &	exprs
	)			[virtual]

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

Parameters:

	fields
	exprs	must be the same length as fields

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1408 of file vcl.cpp.

References d_theoryRecords, DebugAssert, CVC3::TheoryRecords::recordExpr(), and CVC3::sort2().

Expr VCL::recSelectExpr	(	const Expr &	record,
		const std::string &	field
	)			[virtual]

Create record.field (field selection).

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

Implements CVC3::ValidityChecker.

Definition at line 1421 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::recordSelect().

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

Implements CVC3::ValidityChecker.

Definition at line 1427 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::recordUpdate().

Expr VCL::readExpr	(	const Expr &	array,
		const Expr &	index
	)			[virtual]

Create an expression array[index] (array access).

Create an expression for the value of array at the given index

Implements CVC3::ValidityChecker.

Definition at line 1434 of file vcl.cpp.

References CVC3::READ.

Expr VCL::writeExpr	(	const Expr &	array,
		const Expr &	index,
		const Expr &	newValue
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1440 of file vcl.cpp.

References CVC3::WRITE.

Expr VCL::newBVConstExpr	(	const std::string &	s,
		int	base
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1446 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVConstExpr().

Expr VCL::newBVConstExpr

(

const std::vector< bool > &

bits

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1452 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVConstExpr().

Expr VCL::newBVConstExpr	(	const Rational &	r,
		int	len
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1458 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVConstExpr().

Expr VCL::newConcatExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1464 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newConcatExpr().

Expr VCL::newConcatExpr

(

const std::vector< Expr > &

kids

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1470 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newConcatExpr().

Expr VCL::newBVExtractExpr	(	const Expr &	e,
		int	hi,
		int	low
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1476 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVExtractExpr().

Expr VCL::newBVNegExpr

(

const Expr &

t1

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1482 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVNegExpr().

Expr VCL::newBVAndExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1488 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVAndExpr().

Expr VCL::newBVAndExpr

(

const std::vector< Expr > &

kids

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1494 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVAndExpr().

Expr VCL::newBVOrExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1500 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVOrExpr().

Expr VCL::newBVOrExpr

(

const std::vector< Expr > &

kids

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1506 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVOrExpr().

Expr VCL::newBVXorExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1512 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVXorExpr().

Expr VCL::newBVXorExpr

(

const std::vector< Expr > &

kids

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1518 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVXorExpr().

Expr VCL::newBVXnorExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1524 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVXnorExpr().

Expr VCL::newBVXnorExpr

(

const std::vector< Expr > &

kids

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1530 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVXnorExpr().

Expr VCL::newBVNandExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1536 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVNandExpr().

Expr VCL::newBVNorExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1542 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVNorExpr().

Expr VCL::newBVCompExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1548 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVCompExpr().

Expr VCL::newBVLTExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1554 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVLTExpr().

Expr VCL::newBVLEExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1560 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVLEExpr().

Expr VCL::newBVSLTExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1566 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSLTExpr().

Expr VCL::newBVSLEExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1572 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSLEExpr().

Expr VCL::newSXExpr	(	const Expr &	t1,
		int	len
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1578 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newSXExpr().

Expr VCL::newBVUminusExpr

(

const Expr &

t1

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1584 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVUminusExpr().

Expr VCL::newBVSubExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1590 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSubExpr().

Expr VCL::newBVPlusExpr	(	int	numbits,
		const std::vector< Expr > &	k
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1596 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVPlusPadExpr().

Referenced by newBVPlusExpr().

Expr VCL::newBVPlusExpr	(	int	numbits,
		const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1601 of file vcl.cpp.

References newBVPlusExpr().

Expr VCL::newBVMultExpr	(	int	numbits,
		const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1610 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVMultPadExpr().

Expr VCL::newBVUDivExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1615 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVUDivExpr().

Expr VCL::newBVURemExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1620 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVURemExpr().

Expr VCL::newBVSDivExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1625 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSDivExpr().

Expr VCL::newBVSRemExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1630 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSRemExpr().

Expr VCL::newBVSModExpr	(	const Expr &	t1,
		const Expr &	t2
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1635 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newBVSModExpr().

Expr VCL::newFixedLeftShiftExpr	(	const Expr &	t1,
		int	r
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1641 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newFixedLeftShiftExpr().

Expr VCL::newFixedConstWidthLeftShiftExpr	(	const Expr &	t1,
		int	r
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1647 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr().

Expr VCL::newFixedRightShiftExpr	(	const Expr &	t1,
		int	r
	)			[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1653 of file vcl.cpp.

References d_theoryBitvector, and CVC3::TheoryBitvector::newFixedRightShiftExpr().

Rational VCL::computeBVConst

(

const Expr &

e

)

[virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1659 of file vcl.cpp.

References CVC3::TheoryBitvector::computeBVConst(), and d_theoryBitvector.

Expr VCL::tupleExpr

(

const std::vector< Expr > &

exprs

)

[virtual]

Tuple expression.

Implements CVC3::ValidityChecker.

Definition at line 1665 of file vcl.cpp.

References d_theoryRecords, DebugAssert, and CVC3::TheoryRecords::tupleExpr().

Expr VCL::tupleSelectExpr	(	const Expr &	tuple,
		int	index
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1671 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::tupleSelect().

Expr VCL::tupleUpdateExpr	(	const Expr &	tuple,
		int	index,
		const Expr &	newValue
	)			[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 1677 of file vcl.cpp.

References d_theoryRecords, and CVC3::TheoryRecords::tupleUpdate().

Expr VCL::datatypeConsExpr	(	const std::string &	constructor,
		const std::vector< Expr > &	args
	)			[virtual]

Datatype constructor expression.

Implements CVC3::ValidityChecker.

Definition at line 1683 of file vcl.cpp.

References d_theoryDatatype, and CVC3::TheoryDatatype::datatypeConsExpr().

Expr VCL::datatypeSelExpr	(	const std::string &	selector,
		const Expr &	arg
	)			[virtual]

Datatype selector expression.

Implements CVC3::ValidityChecker.

Definition at line 1689 of file vcl.cpp.

References d_theoryDatatype, and CVC3::TheoryDatatype::datatypeSelExpr().

Expr VCL::datatypeTestExpr	(	const std::string &	constructor,
		const Expr &	arg
	)			[virtual]

Datatype tester expression.

Implements CVC3::ValidityChecker.

Definition at line 1695 of file vcl.cpp.

References d_theoryDatatype, and CVC3::TheoryDatatype::datatypeTestExpr().

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

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

Parameters:

	name	is the name of the variable
	uid	is the unique ID (a string), which must be unique for each variable
	type	is its type. The type cannot be a function type.

Returns:

an Expr representation of a new variable

Implements CVC3::ValidityChecker.

Definition at line 1701 of file vcl.cpp.

References d_em, and CVC3::ExprManager::newBoundVarExpr().

Referenced by varExpr().

Expr VCL::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)			[virtual]

Universal quantifier.

Implements CVC3::ValidityChecker.

Definition at line 1707 of file vcl.cpp.

References d_em, DebugAssert, CVC3::FORALL, and CVC3::ExprManager::newClosureExpr().

Referenced by createOp(), and varExpr().

Expr VCL::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body,
		const std::vector< std::vector< Expr > > &	triggers
	)			[virtual]

Universal quantifier with triggers.

Implements CVC3::ValidityChecker.

Definition at line 1712 of file vcl.cpp.

References d_em, DebugAssert, CVC3::FORALL, and CVC3::ExprManager::newClosureExpr().

void VCL::setTriggers	(	const Expr &	e,
		const std::vector< std::vector< Expr > > &	triggers
	)			[virtual]

Set triggers for quantifier instantiation.

Parameters:

	e	is the expression for which triggers are being set.
	Each	item in triggers is a vector of Expr containing one or more patterns. A pattern is a term or Atomic predicate sub-expression of e. A vector containing more than one pattern is treated as a multi-trigger. Patterns will be matched in the order they occur in the vector.

Implements CVC3::ValidityChecker.

Definition at line 1718 of file vcl.cpp.

References CVC3::Expr::setTriggers().

Expr VCL::existsExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)			[virtual]

Existential quantifier.

Implements CVC3::ValidityChecker.

Definition at line 1723 of file vcl.cpp.

References d_em, CVC3::EXISTS, and CVC3::ExprManager::newClosureExpr().

Op VCL::lambdaExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)			[virtual]

Lambda-expression.

Implements CVC3::ValidityChecker.

Definition at line 1728 of file vcl.cpp.

References d_em, CVC3::LAMBDA, CVC3::Expr::mkOp(), and CVC3::ExprManager::newClosureExpr().

Op VCL::transClosure

(

const Op &

op

)

[virtual]

Transitive closure of a binary predicate.

Implements CVC3::ValidityChecker.

Definition at line 1732 of file vcl.cpp.

References d_em, CVC3::Op::getExpr(), CVC3::Expr::getName(), CVC3::Expr::mkOp(), CVC3::ExprManager::newSymbolExpr(), and CVC3::TRANS_CLOSURE.

Expr VCL::simulateExpr	(	const Expr &	f,
		const Expr &	s0,
		const std::vector< Expr > &	inputs,
		const Expr &	n
	)			[virtual]

Symbolic simulation expression.

Parameters:

	f	is the next state function (LAMBDA-expression)
	s0	is the initial state
	inputs	is the vector of LAMBDA-expressions representing the sequences of inputs to f
	n	is a constant, the number of cycles to run the simulation.

Implements CVC3::ValidityChecker.

Definition at line 1738 of file vcl.cpp.

References CVC3::SIMULATE.

void VCL::setResourceLimit

(

unsigned

limit

)

[virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 1749 of file vcl.cpp.

References d_theoryCore, and CVC3::TheoryCore::setResourceLimit().

void VCL::setTimeLimit

(

unsigned

limit

)

[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.

Implements CVC3::ValidityChecker.

Definition at line 2356 of file vcl.cpp.

References d_theoryCore, and CVC3::TheoryCore::setTimeLimit().

void VCL::assertFormula

(

const Expr &

e

)

[virtual]

Assert a new formula in the current context.

This creates the assumption e |- e. The formula must have Boolean type.

Implements CVC3::ValidityChecker.

Definition at line 1793 of file vcl.cpp.

References CVC3::ASSERT, checkTCC(), CVC3::CDMap< Key, Data, HashFcn >::count(), d_batchedAssertions, d_dump, d_nextIdx, d_se, d_theoryCore, d_translator, d_userAssertions, CVC3::Translator::dumpAssertion(), getFlags(), CVC3::Theory::getTCC(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::SearchEngine::newUserAssumption(), CVC3::CDList< T >::push_back(), simplify(), CVC3::Type::toString(), CVC3::TRACE, and TRACE_MSG.

void VCL::registerAtom

(

const Expr &

e

)

[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

Implements CVC3::ValidityChecker.

Definition at line 1837 of file vcl.cpp.

References d_se, and CVC3::SearchEngine::registerAtom().

Expr VCL::getImpliedLiteral

(

)

[virtual]

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

Returned literals are either registered atomic formulas or their negation

Implements CVC3::ValidityChecker.

Definition at line 1844 of file vcl.cpp.

References d_se, CVC3::Theorem::getExpr(), CVC3::SearchEngine::getImpliedLiteral(), and CVC3::Theorem::isNull().

Expr VCL::simplify

(

const Expr &

e

)

[virtual]

Simplify e with respect to the current context.

Implements CVC3::ValidityChecker.

Definition at line 1853 of file vcl.cpp.

References CVC3::Theorem::getRHS(), and simplifyThm().

Referenced by assertFormula(), checkTCC(), and query().

Theorem VCL::simplifyThm

(

const Expr &

e

)

Definition at line 1859 of file vcl.cpp.

References d_theoryCore, CVC3::TheoryCore::getExprTrans(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::ExprTransform::preprocess(), CVC3::TheoryCore::simplify(), and CVC3::Theory::transitivityRule().

Referenced by simplify().

QueryResult VCL::query

(

const Expr &

e

)

[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:

e

is the queried formula

Implements CVC3::ValidityChecker.

Definition at line 1869 of file vcl.cpp.

References CVC3::ABORT, CVC3::AND, checkTCC(), CVC3::SearchEngine::checkValid(), d_batchedAssertions, d_batchedAssertionsIdx, d_dump, d_lastClosure, d_lastQuery, d_lastQueryTCC, d_se, d_theoryCore, d_translator, CVC3::Translator::dumpQuery(), CVC3::Translator::dumpQueryResult(), CVC3::SearchEngine::getCommonRules(), getFlags(), CVC3::Theory::getTCC(), CVC3::Expr::getType(), CVC3::Expr::impExpr(), CVC3::INVALID, CVC3::Type::isBool(), CVC3::QUERY, CVC3::CommonProofRules::queryTCC(), simplify(), CVC3::CDList< T >::size(), CVC3::Type::toString(), CVC3::TRACE, CVC3::CommonProofRules::trueTheorem(), CVC3::UNKNOWN, and CVC3::VALID.

Referenced by checkUnsat().

QueryResult VCL::checkUnsat

(

const Expr &

e

)

[virtual]

Check satisfiability of the expr in the current context.

Equivalent to query(!e)

Implements CVC3::ValidityChecker.

Definition at line 1938 of file vcl.cpp.

References CVC3::Expr::negate(), and query().

QueryResult VCL::checkContinue

(

)

[virtual]

Get the next model.

This method should only be called after a query which returns INVALID. Its return values are as for query().

Implements CVC3::ValidityChecker.

Definition at line 1944 of file vcl.cpp.

References andExpr(), CVC3::CONTINUE, d_dump, d_em, d_se, d_translator, CVC3::Translator::dump(), falseExpr(), CVC3::SearchEngine::getCounterExample(), CVC3::ExprManager::newLeafExpr(), and CVC3::SearchEngine::restart().

QueryResult VCL::restart

(

const Expr &

e

)

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

Implements CVC3::ValidityChecker.

Definition at line 1960 of file vcl.cpp.

References d_dump, d_se, d_translator, CVC3::Translator::dump(), CVC3::SearchEngine::restart(), and CVC3::RESTART.

Referenced by tryModelGeneration().

void VCL::returnFromCheck

(

)

[virtual]

Returns to context immediately before last invalid query.

This method should only be called after a query which returns false.

Implements CVC3::ValidityChecker.

Definition at line 1970 of file vcl.cpp.

References d_se, and CVC3::SearchEngine::returnFromCheck().

void VCL::getUserAssumptions

(

std::vector< Expr > &

assumptions

)

[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:

assumptions

should be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 1977 of file vcl.cpp.

References d_se, and CVC3::SearchEngine::getUserAssumptions().

void VCL::getInternalAssumptions

(

std::vector< Expr > &

assumptions

)

[virtual]

Get assumptions made internally in this and all previous contexts.

Internal assumptions are literals assumed by the sat solver.

Parameters:

assumptions

should be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 1984 of file vcl.cpp.

References d_se, and CVC3::SearchEngine::getInternalAssumptions().

void VCL::getAssumptions

(

std::vector< Expr > &

assumptions

)

[virtual]

Get all assumptions made in this and all previous contexts.

Parameters:

assumptions

should be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 1991 of file vcl.cpp.

References CVC3::ASSUMPTIONS, d_dump, d_em, d_se, d_translator, CVC3::Translator::dump(), CVC3::SearchEngine::getAssumptions(), and CVC3::ExprManager::newLeafExpr().

void VCL::getAssumptionsUsed

(

std::vector< Expr > &

assumptions

)

[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:

assumptions

should be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2015 of file vcl.cpp.

References d_dump, d_em, d_se, d_translator, CVC3::Translator::dump(), CVC3::DUMP_ASSUMPTIONS, CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::isNull(), CVC3::SearchEngine::lastThm(), and CVC3::ExprManager::newLeafExpr().

Expr VCL::getProofQuery

(

)

[virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 2001 of file vcl.cpp.

References d_lastQuery, CVC3::Theorem3::getExpr(), and CVC3::Theorem3::isNull().

void VCL::getCounterExample	(	std::vector< Expr > &	assumptions,
		bool	inOrder
	)			[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:

	assumptions	should be empty on entry.
	inOrder	if true, returns the assumptions in the order they were made. This is slightly more expensive than inOrder = false.

Implements CVC3::ValidityChecker.

Definition at line 2027 of file vcl.cpp.

References CVC3::COUNTEREXAMPLE, d_dump, d_em, d_flags, d_se, d_translator, CVC3::Translator::dump(), CVC3::SearchEngine::getCounterExample(), and CVC3::ExprManager::newLeafExpr().

void VCL::getConcreteModel

(

ExprMap< Expr > &

m

)

[virtual]

Will assign concrete values to all user created variables.

This function should only be called after a query which return false.

Implements CVC3::ValidityChecker.

Definition at line 2037 of file vcl.cpp.

References CVC3::COUNTERMODEL, d_dump, d_em, d_flags, d_se, d_translator, CVC3::Translator::dump(), CVC3::SearchEngine::getConcreteModel(), and CVC3::ExprManager::newLeafExpr().

QueryResult VCL::tryModelGeneration

(

)

[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.

Implements CVC3::ValidityChecker.

Definition at line 2046 of file vcl.cpp.

References d_cm, d_se, d_theoryCore, CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::TheoryCore::incomplete(), CVC3::INVALID, CVC3::Expr::isFalse(), orExpr(), CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), restart(), CVC3::ContextManager::scopeLevel(), scopeLevel(), CVC3::SearchEngine::tryModelGeneration(), and CVC3::UNKNOWN.

FormulaValue VCL::value

(

const Expr &

e

)

[virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 2080 of file vcl.cpp.

References d_se, DebugAssert, CVC3::SearchEngine::getValue(), and CVC3::Expr::isTerm().

bool VCL::inconsistent

(

std::vector< Expr > &

assumptions

)

[virtual]

Returns true if the current context is inconsistent.

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

Parameters:

assumptions

should be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2085 of file vcl.cpp.

References d_theoryCore, getAssumptions(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryCore::inconsistent(), and CVC3::TheoryCore::inconsistentThm().

bool VCL::inconsistent

(

)

[virtual]

Returns true if the current context is inconsistent.

Implements CVC3::ValidityChecker.

Definition at line 2097 of file vcl.cpp.

References d_theoryCore, and CVC3::TheoryCore::inconsistent().

bool VCL::incomplete

(

)

[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.

Implements CVC3::ValidityChecker.

Definition at line 2103 of file vcl.cpp.

References d_lastQuery, d_theoryCore, CVC3::TheoryCore::incomplete(), and CVC3::Theorem3::isNull().

bool VCL::incomplete

(

std::vector< std::string > &

reasons

)

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

Implements CVC3::ValidityChecker.

Definition at line 2110 of file vcl.cpp.

References d_lastQuery, d_theoryCore, CVC3::TheoryCore::incomplete(), and CVC3::Theorem3::isNull().

Proof VCL::getProof

(

)

[virtual]

Returns the proof term for the last proven query.

If there has not been a successful query, it should return a NULL proof

Implements CVC3::ValidityChecker.

Definition at line 2117 of file vcl.cpp.

References d_dump, d_em, d_lastQuery, d_se, d_translator, CVC3::Translator::dump(), CVC3::DUMP_PROOF, CVC3::SearchEngine::getProof(), CVC3::Theorem3::isNull(), and CVC3::ExprManager::newLeafExpr().

Expr VCL::getTCC

(

)

[virtual]

Returns the TCC of the last assumption or query.

Returns Null if no assumptions or queries were performed.

Implements CVC3::ValidityChecker.

Definition at line 2131 of file vcl.cpp.

References d_dump, d_em, d_lastQueryTCC, d_translator, CVC3::Translator::dump(), CVC3::DUMP_TCC, CVC3::Theorem::getExpr(), CVC3::Theorem::isNull(), and CVC3::ExprManager::newLeafExpr().

void VCL::getAssumptionsTCC

(

std::vector< Expr > &

assumptions

)

[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2141 of file vcl.cpp.

References d_dump, d_em, d_lastQuery, d_lastQueryTCC, d_translator, CVC3::Translator::dump(), CVC3::DUMP_TCC_ASSUMPTIONS, getAssumptions(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem3::isNull(), and CVC3::ExprManager::newLeafExpr().

Proof VCL::getProofTCC

(

)

[virtual]

Returns the proof of TCC of the last assumption or query.

Returns Null if no assumptions or queries were performed.

Implements CVC3::ValidityChecker.

Definition at line 2154 of file vcl.cpp.

References d_dump, d_em, d_lastQueryTCC, d_translator, CVC3::Translator::dump(), CVC3::DUMP_TCC_PROOF, CVC3::Theorem::getProof(), CVC3::Theorem::isNull(), and CVC3::ExprManager::newLeafExpr().

Expr VCL::getClosure

(

)

[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.

Implements CVC3::ValidityChecker.

Definition at line 2164 of file vcl.cpp.

References d_dump, d_em, d_lastClosure, d_lastQuery, d_translator, deriveClosure(), CVC3::Translator::dump(), CVC3::DUMP_CLOSURE, CVC3::Theorem3::getExpr(), CVC3::Theorem3::isNull(), and CVC3::ExprManager::newLeafExpr().

Proof VCL::getProofClosure

(

)

[virtual]

Construct a proof of the query closure |- Gamma => phi.

Returns Null if last query was Invalid.

Implements CVC3::ValidityChecker.

Definition at line 2178 of file vcl.cpp.

References d_dump, d_em, d_lastClosure, d_lastQuery, d_translator, deriveClosure(), CVC3::Translator::dump(), CVC3::DUMP_CLOSURE_PROOF, CVC3::Theorem3::getProof(), CVC3::Theorem3::isNull(), and CVC3::ExprManager::newLeafExpr().

int VCL::stackLevel

(

)

[virtual]

Returns the current stack level. Initial level is 0.

Implements CVC3::ValidityChecker.

Definition at line 2192 of file vcl.cpp.

References d_stackLevel, and CVC3::CDO< T >::get().

Referenced by pop(), popto(), and push().

void VCL::push

(

)

[virtual]

Checkpoint the current context and increase the scope level.

Implements CVC3::ValidityChecker.

Definition at line 2198 of file vcl.cpp.

References d_dump, d_em, d_se, d_stackLevel, d_translator, CVC3::Translator::dump(), CVC3::ExprManager::newLeafExpr(), CVC3::SearchEngine::push(), CVC3::PUSH, CVC3::CDO< T >::set(), and stackLevel().

void VCL::pop

(

)

[virtual]

Restore the current context to its state at the last checkpoint.

Implements CVC3::ValidityChecker.

Definition at line 2208 of file vcl.cpp.

References d_dump, d_em, d_se, d_translator, CVC3::Translator::dump(), CVC3::ExprManager::newLeafExpr(), CVC3::SearchEngine::pop(), CVC3::POP, and stackLevel().

void VCL::popto

(

int

stackLevel

)

[virtual]

Restore the current context to the given stackLevel.

Parameters:

stackLevel

should be greater than or equal to 0 and less than or equal to the current scope level.

Implements CVC3::ValidityChecker.

Definition at line 2223 of file vcl.cpp.

References d_dump, d_se, d_translator, CVC3::Translator::dump(), CVC3::SearchEngine::pop(), CVC3::POPTO, ratExpr(), and stackLevel().

Referenced by destroy().

int VCL::scopeLevel

(

)

[virtual]

Returns the current scope level. Initially, the scope level is 1.

Implements CVC3::ValidityChecker.

Definition at line 2236 of file vcl.cpp.

References d_cm, and CVC3::ContextManager::scopeLevel().

Referenced by popScope(), poptoScope(), pushScope(), and tryModelGeneration().

void VCL::pushScope

(

)

[virtual]

Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing!

Implements CVC3::ValidityChecker.

Definition at line 2242 of file vcl.cpp.

References d_cm, d_dump, d_em, d_flags, d_translator, CVC3::Translator::dump(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), CVC3::ContextManager::push(), CVC3::PUSH_SCOPE, and scopeLevel().

void VCL::popScope

(

)

[virtual]

Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing!

Implements CVC3::ValidityChecker.

Definition at line 2254 of file vcl.cpp.

References d_cm, d_dump, d_em, d_flags, d_translator, CVC3::Translator::dump(), std::endl(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), CVC3::ContextManager::pop(), CVC3::POP_SCOPE, and scopeLevel().

void VCL::poptoScope

(

int

scopeLevel

)

[virtual]

Restore the current context to the given scopeLevel.

Parameters:

scopeLevel

should be less than or equal to the current scope level.

If scopeLevel is less than 1, then the current context is reset and the scope level is set to 1.

Implements CVC3::ValidityChecker.

Definition at line 2269 of file vcl.cpp.

References d_cm, d_dump, d_flags, d_translator, CVC3::Translator::dump(), IF_DEBUG, CVC3::ContextManager::popto(), CVC3::POPTO_SCOPE, CVC3::ContextManager::push(), ratExpr(), and scopeLevel().

Context * VCL::getCurrentContext

(

)

[virtual]

Get the current context.

Implements CVC3::ValidityChecker.

Definition at line 2285 of file vcl.cpp.

References d_cm, and CVC3::ContextManager::getCurrentContext().

Referenced by init().

void VCL::reset

(

)

[virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2291 of file vcl.cpp.

References destroy(), and init().

void VCL::loadFile	(	const std::string &	fileName,
		InputLanguage	lang = PRESENTATION_LANG,
		bool	interactive = false,
		bool	calledFromParser = false
	)			[virtual]

Read and execute the commands from a file given by name ("" means stdin).

Implements CVC3::ValidityChecker.

Definition at line 2297 of file vcl.cpp.

References CVC3::VCCmd::processCommands().

Referenced by cmdsFromString().

void VCL::loadFile	(	std::istream &	is,
		InputLanguage	lang = PRESENTATION_LANG,
		bool	interactive = false
	)			[virtual]

Read and execute the commands from a stream.

Implements CVC3::ValidityChecker.

Definition at line 2306 of file vcl.cpp.

References CVC3::VCCmd::processCommands().

Statistics& CVC3::VCL::getStatistics

(

)

[inline, virtual]

Get statistics object.

Implements CVC3::ValidityChecker.

Definition at line 398 of file vcl.h.

void CVC3::VCL::printStatistics

(

)

[inline, virtual]

Print collected statistics to stdout.

Implements CVC3::ValidityChecker.

Definition at line 399 of file vcl.h.

References std::endl().

unsigned long VCL::getMemory

(

int

verbosity = 0

)

Definition at line 2319 of file vcl.cpp.

References d_cm, d_em, CVC3::ExprManager::getMemory(), CVC3::ContextManager::getMemory(), and CVC3::MemoryTracker::print().

---

Member Data Documentation

ExprManager* CVC3::VCL::d_em [private]

Pointers to main system components.

Definition at line 51 of file vcl.h.

Referenced by boundVarExpr(), checkContinue(), createOp(), destroy(), existsExpr(), falseExpr(), forallExpr(), getAssumptions(), getAssumptionsTCC(), getAssumptionsUsed(), getClosure(), getConcreteModel(), getCounterExample(), getMemory(), getProof(), getProofClosure(), getProofTCC(), getTCC(), importExpr(), importType(), init(), lambdaExpr(), pop(), popScope(), push(), pushScope(), ratExpr(), transClosure(), and trueExpr().

ContextManager* CVC3::VCL::d_cm [private]

Definition at line 52 of file vcl.h.

Referenced by destroy(), getCurrentContext(), getMemory(), init(), popScope(), poptoScope(), pushScope(), scopeLevel(), and tryModelGeneration().

TheoremManager* CVC3::VCL::d_tm [private]

Definition at line 53 of file vcl.h.

Referenced by destroy(), and init().

SearchEngine* CVC3::VCL::d_se [private]

Definition at line 54 of file vcl.h.

Referenced by assertFormula(), checkContinue(), checkTCC(), deriveClosure(), destroy(), getAssumptions(), getAssumptionsUsed(), getConcreteModel(), getCounterExample(), getImpliedLiteral(), getInternalAssumptions(), getProof(), getUserAssumptions(), init(), pop(), popto(), push(), query(), registerAtom(), reprocessFlags(), restart(), returnFromCheck(), tryModelGeneration(), and value().

TheoryCore* CVC3::VCL::d_theoryCore [private]

Pointers to theories.

Definition at line 57 of file vcl.h.

Referenced by assertFormula(), boolType(), core(), createOp(), createType(), getBaseType(), getTypePred(), incomplete(), inconsistent(), init(), lookupOp(), lookupType(), lookupVar(), parseExpr(), parseType(), query(), reprocessFlags(), setResourceLimit(), setTimeLimit(), simplifyThm(), subtypeType(), tryModelGeneration(), and varExpr().

TheoryUF* CVC3::VCL::d_theoryUF [private]

Definition at line 58 of file vcl.h.

Referenced by init().

TheoryArith* CVC3::VCL::d_theoryArith [private]

Definition at line 59 of file vcl.h.

Referenced by addPairToArithOrder(), init(), intType(), realType(), reprocessFlags(), and subrangeType().

TheoryArray* CVC3::VCL::d_theoryArray [private]

Definition at line 60 of file vcl.h.

Referenced by init().

TheoryQuant* CVC3::VCL::d_theoryQuant [private]

Definition at line 61 of file vcl.h.

Referenced by init().

TheoryRecords* CVC3::VCL::d_theoryRecords [private]

Definition at line 62 of file vcl.h.

Referenced by init(), recordExpr(), recordType(), recSelectExpr(), recUpdateExpr(), tupleExpr(), tupleSelectExpr(), tupleType(), and tupleUpdateExpr().

TheorySimulate* CVC3::VCL::d_theorySimulate [private]

Definition at line 63 of file vcl.h.

Referenced by init().

TheoryBitvector* CVC3::VCL::d_theoryBitvector [private]

Definition at line 64 of file vcl.h.

Referenced by bitvecType(), computeBVConst(), init(), newBVAndExpr(), newBVCompExpr(), newBVConstExpr(), newBVExtractExpr(), newBVLEExpr(), newBVLTExpr(), newBVMultExpr(), newBVNandExpr(), newBVNegExpr(), newBVNorExpr(), newBVOrExpr(), newBVPlusExpr(), newBVSDivExpr(), newBVSLEExpr(), newBVSLTExpr(), newBVSModExpr(), newBVSRemExpr(), newBVSubExpr(), newBVUDivExpr(), newBVUminusExpr(), newBVURemExpr(), newBVXnorExpr(), newBVXorExpr(), newConcatExpr(), newFixedConstWidthLeftShiftExpr(), newFixedLeftShiftExpr(), newFixedRightShiftExpr(), and newSXExpr().

TheoryDatatype* CVC3::VCL::d_theoryDatatype [private]

Definition at line 65 of file vcl.h.

Referenced by dataType(), datatypeConsExpr(), datatypeSelExpr(), datatypeTestExpr(), and init().

Translator* CVC3::VCL::d_translator [private]

Definition at line 66 of file vcl.h.

Referenced by addPairToArithOrder(), assertFormula(), checkContinue(), createOp(), createType(), dataType(), destroy(), getAssumptions(), getAssumptionsTCC(), getAssumptionsUsed(), getClosure(), getConcreteModel(), getCounterExample(), getProof(), getProofClosure(), getProofTCC(), getTCC(), init(), pop(), popScope(), popto(), poptoScope(), push(), pushScope(), query(), reprocessFlags(), restart(), and varExpr().

std::vector<Theory*> CVC3::VCL::d_theories [private]

All theories are stored in this common vector.

This includes TheoryCore and TheoryArith.

Definition at line 70 of file vcl.h.

Referenced by destroy(), init(), and reprocessFlags().

CLFlags* CVC3::VCL::d_flags [private]

Command line flags.

Definition at line 73 of file vcl.h.

Referenced by getConcreteModel(), getCounterExample(), init(), popScope(), poptoScope(), pushScope(), reprocessFlags(), and ~VCL().

CDO<int>* CVC3::VCL::d_stackLevel [private]

User-level view of the scope stack.

Definition at line 76 of file vcl.h.

Referenced by destroy(), init(), push(), and stackLevel().

Statistics* CVC3::VCL::d_statistics [private]

Run-time statistics.

Definition at line 79 of file vcl.h.

Referenced by destroy(), and init().

size_t CVC3::VCL::d_nextIdx [private]

Next index for user assertion.

Definition at line 82 of file vcl.h.

Referenced by assertFormula(), getAssumptionsRec(), and init().

CDMap<Expr,UserAssertion>* CVC3::VCL::d_userAssertions [private]

Backtracking map of user assertions.

Definition at line 108 of file vcl.h.

Referenced by assertFormula(), destroy(), getAssumptionsRec(), and init().

CDList<Expr>* CVC3::VCL::d_batchedAssertions [private]

Backtracking map of assertions when assertion batching is on.

Definition at line 111 of file vcl.h.

Referenced by assertFormula(), destroy(), init(), and query().

CDO<unsigned>* CVC3::VCL::d_batchedAssertionsIdx [private]

Index into batched Assertions.

Definition at line 114 of file vcl.h.

Referenced by destroy(), init(), and query().

Theorem3 CVC3::VCL::d_lastQuery [private]

Result of the last query().

Saved for printing assumptions and proofs. Normally it is Theorem3, but query() on a TCC returns a 2-valued Theorem.

Definition at line 119 of file vcl.h.

Referenced by destroy(), getAssumptionsTCC(), getClosure(), getProof(), getProofClosure(), getProofQuery(), incomplete(), and query().

Theorem CVC3::VCL::d_lastQueryTCC [private]

Result of the last query(e, true) (for a TCC).

Definition at line 122 of file vcl.h.

Referenced by checkTCC(), destroy(), getAssumptionsTCC(), getProofTCC(), getTCC(), and query().

Theorem3 CVC3::VCL::d_lastClosure [private]

Closure of the last query(e): |- Gamma => e.

Definition at line 125 of file vcl.h.

Referenced by destroy(), getClosure(), getProofClosure(), and query().

bool CVC3::VCL::d_dump [private]

Whether to dump a trace (or a translated version).

Definition at line 128 of file vcl.h.

Referenced by addPairToArithOrder(), assertFormula(), checkContinue(), createOp(), createType(), dataType(), getAssumptions(), getAssumptionsTCC(), getAssumptionsUsed(), getClosure(), getConcreteModel(), getCounterExample(), getProof(), getProofClosure(), getProofTCC(), getTCC(), init(), pop(), popScope(), popto(), poptoScope(), push(), pushScope(), query(), restart(), and varExpr().

---

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

• vcl.h
• vcl.cpp