CVCL::VCL Class Reference

#include <vcl.h>

Inheritance diagram for CVCL::VCL:

[legend]Collaboration diagram for CVCL::VCL:

[legend]List of all members.

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.
  

• CLFlags & getFlags () const

  Return the set of command-line flags.
  

• void reprocessFlags ()

  Force reprocessing of all flags.
  

• 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)

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

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

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

• 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)
  

• 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 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 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 forallExpr (const std::vector< Expr > &vars, const Expr &body)

  Universal quantifier.
  

• Expr existsExpr (const std::vector< Expr > &vars, const Expr &body)

  Existential quantifier.
  

• Op lambdaExpr (const std::vector< Expr > &vars, const Expr &body)

  Lambda-expression.
  

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

• Theorem3 simplifyThm (const Expr &e)

  Simplify e into e', and return the Theorem3 object for e = e'.
  

• Theorem simplifyThm2 (const Expr &e)

  Simpfy e, ignoring TCCs (assumes total interpretation).
  

• void printV (const Expr &e)

  Dump all variables in e.
  

• bool query (const Expr &e, bool isTCC=false)

  Check validity of e in the current context.
  

• bool checkUnsat (const Expr &e)

  Check satisfiability of the expr in the current context.
  

• bool checkContinue ()

  Get the next model.
  

• bool 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.
  

• void getCounterExample (std::vector< Expr > &assertions, 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.
  

• bool inconsistent (std::vector< Expr > &assumptions)

  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.
  

• const 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.
  

• const Proof & getProofTCC ()

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

• const Expr & getClosure ()

  After successful query, return its closure |- Gamma => phi.
  

• const 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 loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=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.
  

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.
  

• std::vector< int > d_scopeStack

  User-level view of the scope stack.
  

• Str_To_Expr d_vars

  Cache for printV method.
  

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

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

• std::ostream * d_osdump

  The log file for top-level API calls in the CVCL input language.
  

• std::ostream * d_osdumpTranslate
• std::ofstream d_osdumpFile
• std::ofstream d_osdumpTranslateFile
• std::ifstream d_tmpFile
• const bool & d_translate
• bool d_dump
• bool d_dumpFileOpen
• bool d_translateFileOpen
• IF_DEBUG(void dumpTrace(int
  scope);) publi ~VCL )()

Classes

• class UserAssertion

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

---

Detailed Description

Definition at line 58 of file vcl.h.

---

Member Function Documentation

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

Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi". Definition at line 246 of file vcl.cpp. References CVCL::Assumptions::begin(), d_theoryCore, CVCL::Assumptions::empty(), CVCL::Assumptions::end(), CVCL::Theorem3::getAssumptions(), getAssumptionsRec(), getFlags(), and CVCL::TheoryCore::implIntro3(). Referenced by getClosure(), and getProofClosure().

void CVCL::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. Referenced by deriveClosure().

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

Get set of user assertions from the set of assumptions.

CLFlags& CVCL::VCL::getFlags (   )  const [inline, private, 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 CVCL::ValidityChecker. Definition at line 171 of file vcl.h. References d_flags. Referenced by assertFormula(), deriveClosure(), query(), simplify(), and simplifyThm().

void VCL::reprocessFlags (   )  [private, virtual]

Force reprocessing of all flags. Implements CVCL::ValidityChecker. Definition at line 661 of file vcl.cpp. References d_flags, d_se, CVCL::SearchEngine::getName(), and CVCL::CLFlags::setFlag().

Type VCL::boolType (   )  [private, virtual]

Create type BOOLEAN. Implements CVCL::ValidityChecker. Definition at line 684 of file vcl.cpp.

Type VCL::realType (   )  [private, virtual]

Create type REAL. Implements CVCL::ValidityChecker. Definition at line 689 of file vcl.cpp. References d_theoryArith, and CVCL::TheoryArith::realType().

Type VCL::intType (   )  [private, virtual]

Create type INT. Implements CVCL::ValidityChecker. Definition at line 695 of file vcl.cpp. References d_theoryArith, and CVCL::TheoryArith::intType().

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

Create a subrange type [l..r]. l and r can be Null; l=Null represents minus infinity, r=Null is plus infinity. Implements CVCL::ValidityChecker. Definition at line 700 of file vcl.cpp. References d_theoryArith, and CVCL::TheoryArith::subrangeType().

Type VCL::subtypeType (  const Expr &  pred  )  [private, 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). Implements CVCL::ValidityChecker. Definition at line 705 of file vcl.cpp. References d_cm, forallExpr(), CVCL::Expr::getBody(), CVCL::Expr::getType(), CVCL::Expr::getVars(), CVCL::Type::isBool(), CVCL::Type::isFunction(), CVCL::Expr::isLambda(), CVCL::ContextManager::popto(), CVCL::ContextManager::push(), query(), scopeLevel(), simplify(), CVCL::SUBTYPE, CVCL::Expr::toString(), and CVCL::Type::toString().

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

2-element tuple Implements CVCL::ValidityChecker. Definition at line 745 of file vcl.cpp. References d_theoryRecords, and CVCL::TheoryRecords::tupleType().

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

3-element tuple Implements CVCL::ValidityChecker. Definition at line 754 of file vcl.cpp. References d_theoryRecords, and CVCL::TheoryRecords::tupleType().

Type CVCL::VCL::tupleType (  const std::vector< Type > &  types  )  [private, virtual]

n-element tuple (from a vector of types) Implements CVCL::ValidityChecker.

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

1-element record Implements CVCL::ValidityChecker.

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

2-element record Fields will be sorted automatically Implements CVCL::ValidityChecker.

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

3-element record Fields will be sorted automatically Implements CVCL::ValidityChecker.

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

n-element record (fields and types must be of the same length) Fields will be sorted automatically Implements CVCL::ValidityChecker.

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

Type CVCL::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 )  [private, 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 CVCL::ValidityChecker.

void CVCL::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 )  [private, 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 CVCL::ValidityChecker.

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

Create an array type (ARRAY typeIndex OF typeData). Implements CVCL::ValidityChecker. Definition at line 860 of file vcl.cpp. References CVCL::arrayType().

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

Create a function type typeDom -> typeRan. Implements CVCL::ValidityChecker. Definition at line 866 of file vcl.cpp. References CVCL::Type::funType().

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

Create a function type (t1,t2,...,tn) -> typeRan. Implements CVCL::ValidityChecker.

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

Create named user-defined uninterpreted type. Implements CVCL::ValidityChecker.

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

Create named user-defined interpreted type (type abbreviation). Implements CVCL::ValidityChecker.

Type CVCL::VCL::lookupType (  const std::string &  typeName  )  [private, virtual]

Lookup a user-defined (uninterpreted) type by name. Implements CVCL::ValidityChecker.

ExprManager* CVCL::VCL::getEM (   )  [inline, private, virtual]

Return the ExprManager. Implements CVCL::ValidityChecker. Definition at line 210 of file vcl.h. References d_em.

Expr CVCL::VCL::varExpr (  const std::string &  name, const Type &  type )  [private, 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 CVCL::ValidityChecker. Referenced by CVCL::TheoryArith::TheoryArith().

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

Create a variable with a given name, type, and value. Implements CVCL::ValidityChecker.

Expr CVCL::VCL::boundVarExpr (  const std::string &  name, const std::string &  uid, const Type &  type )  [private, 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 CVCL::ValidityChecker.

Expr CVCL::VCL::lookupVar (  const std::string &  name, Type *  type )  [private, 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 CVCL::ValidityChecker.

Type VCL::getType (  const Expr &  e  )  [private, virtual]

Get the type of the Expr. Implements CVCL::ValidityChecker. Definition at line 974 of file vcl.cpp. References CVCL::Expr::getType().

Type VCL::getBaseType (  const Expr &  e  )  [private, virtual]

Get the largest supertype of the Expr. Implements CVCL::ValidityChecker. Definition at line 980 of file vcl.cpp.

Type VCL::getBaseType (  const Type &  e  )  [private, virtual]

Get the largest supertype of the Type. Implements CVCL::ValidityChecker. Definition at line 986 of file vcl.cpp.

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

Get the subtype predicate. Implements CVCL::ValidityChecker. Definition at line 992 of file vcl.cpp.

Expr CVCL::VCL::stringExpr (  const std::string &  str  )  [private, virtual]

Create a string Expr. Implements CVCL::ValidityChecker.

Expr CVCL::VCL::idExpr (  const std::string &  name  )  [private, virtual]

Create an ID Expr. Implements CVCL::ValidityChecker.

Expr CVCL::VCL::listExpr (  const std::vector< Expr > &  kids  )  [private, 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 CVCL::ValidityChecker.

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

Overloaded version of listExpr with one argument. Implements CVCL::ValidityChecker. Definition at line 1013 of file vcl.cpp. References CVCL::RAW_LIST.

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

Overloaded version of listExpr with two arguments. Implements CVCL::ValidityChecker. Definition at line 1018 of file vcl.cpp. References CVCL::RAW_LIST.

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

Overloaded version of listExpr with three arguments. Implements CVCL::ValidityChecker. Definition at line 1023 of file vcl.cpp. References CVCL::RAW_LIST.

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

Overloaded version of listExpr with string operator and many arguments. Implements CVCL::ValidityChecker.

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

Overloaded version of listExpr with string operator and one argument. Implements CVCL::ValidityChecker.

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

Overloaded version of listExpr with string operator and two arguments. Implements CVCL::ValidityChecker.

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

Overloaded version of listExpr with string operator and three arguments. Implements CVCL::ValidityChecker.

void VCL::printExpr (  const Expr &  e  )  [private, virtual]

Prints e to the standard output. Implements CVCL::ValidityChecker. Definition at line 1058 of file vcl.cpp. Referenced by query().

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

Prints e to the given ostream. Implements CVCL::ValidityChecker.

Expr VCL::parseExpr (  const Expr &  e  )  [private, virtual]

Parse an expression using a Theory-specific parser. Implements CVCL::ValidityChecker. Definition at line 1079 of file vcl.cpp.

Type VCL::parseType (  const Expr &  e  )  [private, virtual]

Parse a type expression using a Theory-specific parser. Implements CVCL::ValidityChecker. Definition at line 1084 of file vcl.cpp.

Expr VCL::importExpr (  const Expr &  e  )  [private, 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 CVCL::ValidityChecker. Definition at line 1089 of file vcl.cpp. References d_em, and CVCL::ExprManager::rebuild().

Type VCL::importType (  const Type &  t  )  [private, virtual]

Import the Type from another instance of ValidityChecker. See also: getType() Implements CVCL::ValidityChecker. Definition at line 1095 of file vcl.cpp. References d_em, CVCL::Type::getExpr(), and CVCL::ExprManager::rebuild().

Expr VCL::trueExpr (   )  [private, virtual]

Return TRUE Expr. Implements CVCL::ValidityChecker. Definition at line 1101 of file vcl.cpp. References d_em, and CVCL::ExprManager::trueExpr().

Expr VCL::falseExpr (   )  [private, virtual]

Return FALSE Expr. Implements CVCL::ValidityChecker. Definition at line 1107 of file vcl.cpp. References d_em, and CVCL::ExprManager::falseExpr(). Referenced by checkContinue().

Expr VCL::notExpr (  const Expr &  child  )  [private, virtual]

Create negation. Implements CVCL::ValidityChecker. Definition at line 1113 of file vcl.cpp.

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

Create 2-element conjunction. Implements CVCL::ValidityChecker. Definition at line 1119 of file vcl.cpp. Referenced by checkContinue().

Expr CVCL::VCL::andExpr (  const std::vector< Expr > &  children  )  [private, virtual]

Create n-element conjunction. Implements CVCL::ValidityChecker.

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

Create 2-element disjunction. Implements CVCL::ValidityChecker. Definition at line 1133 of file vcl.cpp.

Expr CVCL::VCL::orExpr (  const std::vector< Expr > &  children  )  [private, virtual]

Create n-element disjunction. Implements CVCL::ValidityChecker.

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

Create Boolean implication. Implements CVCL::ValidityChecker. Definition at line 1147 of file vcl.cpp. References CVCL::Expr::impExpr().

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

Create left IFF right (boolean equivalence). Implements CVCL::ValidityChecker. Definition at line 1153 of file vcl.cpp. References CVCL::Expr::iffExpr().

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

Create an equality expression. The two children must have the same type, and cannot be of type Boolean. Implements CVCL::ValidityChecker. Definition at line 1159 of file vcl.cpp. References CVCL::Expr::eqExpr().

Expr VCL::iteExpr (  const Expr &  ifpart, const Expr &  thenpart, const Expr &  elsepart )  [private, 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 CVCL::ValidityChecker. Definition at line 1165 of file vcl.cpp. References CVCL::Expr::iteExpr().

Op CVCL::VCL::createOp (  const std::string &  name, const Type &  type )  [private, 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 CVCL::ValidityChecker.

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

Create a named user-defined function with a given type. Implements CVCL::ValidityChecker.

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

Unary function application (op must be of function type). Implements CVCL::ValidityChecker. Definition at line 1228 of file vcl.cpp.

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

Binary function application (op must be of function type). Implements CVCL::ValidityChecker. Definition at line 1234 of file vcl.cpp.

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

Ternary function application (op must be of function type). Implements CVCL::ValidityChecker. Definition at line 1240 of file vcl.cpp.

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

n-ary function application (op must be of function type) Implements CVCL::ValidityChecker.

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

Create a rational number with numerator n and denominator d. Parameters: n  the numerator d  the denominator, cannot be 0. Implements CVCL::ValidityChecker. Definition at line 1252 of file vcl.cpp. References d_em, and CVCL::ExprManager::newRatExpr(). Referenced by popto(), and poptoScope().

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

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

Expr VCL::uminusExpr (  const Expr &  child  )  [private, virtual]

Unary minus. Implements CVCL::ValidityChecker. Definition at line 1271 of file vcl.cpp.

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

Create 2-element sum (left + right). Implements CVCL::ValidityChecker. Definition at line 1277 of file vcl.cpp.

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

Make a difference (left - right). Implements CVCL::ValidityChecker. Definition at line 1283 of file vcl.cpp.

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

Create a product (left * right). Implements CVCL::ValidityChecker. Definition at line 1289 of file vcl.cpp.

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

Create a power expression (x ^ n); n must be integer. Implements CVCL::ValidityChecker. Definition at line 1295 of file vcl.cpp. References CVCL::powExpr().

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

Create expression x / y. Implements CVCL::ValidityChecker. Definition at line 1301 of file vcl.cpp. References CVCL::divideExpr().

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

Create (left < right). Implements CVCL::ValidityChecker. Definition at line 1307 of file vcl.cpp. References CVCL::ltExpr().

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

Create (left <= right). Implements CVCL::ValidityChecker. Definition at line 1313 of file vcl.cpp. References CVCL::leExpr().

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

Create (left > right). Implements CVCL::ValidityChecker. Definition at line 1319 of file vcl.cpp. References CVCL::gtExpr().

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

Create (left >= right). Implements CVCL::ValidityChecker. Definition at line 1325 of file vcl.cpp. References CVCL::geExpr().

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

Create a 1-element record value (# field := expr #). Fields will be sorted automatically Implements CVCL::ValidityChecker.

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

Create a 2-element record value (# field0 := expr0, field1 := expr1 #). Fields will be sorted automatically Implements CVCL::ValidityChecker.

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

Create a 3-element record value (# field_i := expr_i #). Fields will be sorted automatically Implements CVCL::ValidityChecker.

Expr CVCL::VCL::recordExpr (  const std::vector< std::string > &  fields, const std::vector< Expr > &  exprs )  [private, 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 CVCL::ValidityChecker.

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

Create record.field (field selection). Create an expression representing the selection of a field from a record. Implements CVCL::ValidityChecker.

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

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

Create an expression array[index] (array access). Create an expression for the value of array at the given index Implements CVCL::ValidityChecker. Definition at line 1398 of file vcl.cpp. References CVCL::READ.

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

Array update; equivalent to "array WITH index := newValue". Implements CVCL::ValidityChecker. Definition at line 1404 of file vcl.cpp. References CVCL::WRITE.

Expr CVCL::VCL::tupleExpr (  const std::vector< Expr > &  exprs  )  [private, virtual]

Tuple expression. Implements CVCL::ValidityChecker.

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

Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5). Implements CVCL::ValidityChecker. Definition at line 1416 of file vcl.cpp. References d_theoryRecords, and CVCL::TheoryRecords::tupleSelect().

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

Tuple update; equivalent to "tuple WITH index := newValue". Implements CVCL::ValidityChecker. Definition at line 1422 of file vcl.cpp. References d_theoryRecords, and CVCL::TheoryRecords::tupleUpdate().

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

Datatype constructor expression. Implements CVCL::ValidityChecker.

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

Datatype selector expression. Implements CVCL::ValidityChecker.

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

Datatype tester expression. Implements CVCL::ValidityChecker.

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

Universal quantifier. Implements CVCL::ValidityChecker. Referenced by subtypeType().

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

Existential quantifier. Implements CVCL::ValidityChecker.

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

Lambda-expression. Implements CVCL::ValidityChecker.

Expr CVCL::VCL::simulateExpr (  const Expr &  f, const Expr &  s0, const std::vector< Expr > &  inputs, const Expr &  n )  [private, 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 CVCL::ValidityChecker.

void VCL::setResourceLimit (  unsigned  limit  )  [private, virtual]

Set the resource limit (0==unlimited, 1==exhausted). Currently, the limit is the total number of processed facts. Implements CVCL::ValidityChecker. Definition at line 1473 of file vcl.cpp.

void VCL::assertFormula (  const Expr &  e  )  [private, virtual]

Assert a new formula in the current context. This creates the assumption e |- e. The formula must have Boolean type. Implements CVCL::ValidityChecker. Definition at line 1479 of file vcl.cpp. References CVCL::ASSERT, CVCL::SearchEngine::checkValid(), CVCL::CDMap< Key, Data, HashFcn >::count(), d_cm, d_dump, d_em, d_lastQueryTCC, d_nextIdx, d_osdump, d_se, d_translate, d_userAssertions, getFlags(), CVCL::ExprManager::getOutputLang(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Theorem::isNull(), CVCL::SearchEngine::newUserAssumption(), CVCL::ContextManager::popto(), CVCL::ContextManager::push(), scopeLevel(), simplify(), CVCL::SMTLIB_LANG, CVCL::Expr::toString(), CVCL::Type::toString(), and CVCL::TRACE.

void VCL::registerAtom (  const Expr &  e  )  [private, 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 CVCL::ValidityChecker. Definition at line 1534 of file vcl.cpp. References d_se, and CVCL::SearchEngine::registerAtom().

Expr VCL::getImpliedLiteral (   )  [private, virtual]

Return next literal implied by last assertion. Null Expr if none. Returned literals are either registered atomic formulas or their negation Implements CVCL::ValidityChecker. Definition at line 1541 of file vcl.cpp. References d_se, CVCL::Theorem::getExpr(), CVCL::SearchEngine::getImpliedLiteral(), and CVCL::Theorem::isNull().

Expr VCL::simplify (  const Expr &  e  )  [private, virtual]

Simplify e with respect to the current context. Implements CVCL::ValidityChecker. Definition at line 1550 of file vcl.cpp. References getFlags(), CVCL::Theorem::getRHS(), CVCL::Theorem3::getRHS(), simplifyThm(), and simplifyThm2(). Referenced by assertFormula(), and subtypeType().

Theorem3 VCL::simplifyThm (  const Expr &  e  )  [private, virtual]

Simplify e into e', and return the Theorem3 object for e = e'. This function must be called only when +tcc flag is set. The resulting Theorem3 (a 3-valued theorem object) can be used to extract the simplified expression and the proof of its equivalence to the origital expression: thm.getExpr() [to get e=e'], thm.getRHS() [to get just e'], and thm.getProof() [to get a Proof object]. Implements CVCL::ValidityChecker. Definition at line 1559 of file vcl.cpp. References CVCL::SearchEngine::checkValid(), d_cm, d_lastQueryTCC, d_se, CVCL::Theorem::getExpr(), getFlags(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Theorem::isNull(), CVCL::ContextManager::popto(), CVCL::ContextManager::push(), scopeLevel(), CVCL::Expr::toString(), and CVCL::TRANSFORM. Referenced by simplify().

Theorem VCL::simplifyThm2 (  const Expr &  e  )  [private, virtual]

Simpfy e, ignoring TCCs (assumes total interpretation). Implements CVCL::ValidityChecker. Definition at line 1606 of file vcl.cpp. References CVCL::Theorem::getRHS(), and CVCL::Expr::getType(). Referenced by simplify().

void VCL::printV (  const Expr &  e  )  [private, virtual]

Dump all variables in e. Implements CVCL::ValidityChecker. Definition at line 1621 of file vcl.cpp. References CVCL::Expr::arity(), d_vars, CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::UCONST. Referenced by query().

bool VCL::query (  const Expr &  e, bool  isTCC = false )  [private, virtual]

Check validity of e in the current context. If the result is true, then the resulting context is the same as the starting context. If the result is false, then the resulting context is a context in which e is false. e must have Boolean type. Parameters: e  is the queried formula tcc  is a flag indicating that the formula is a TCC, which is assumed to be always defined (so, its TCC is not computed) Implements CVCL::ValidityChecker. Definition at line 1648 of file vcl.cpp. References CVCL::SearchEngine::checkValid(), d_cm, d_dump, d_em, d_lastClosure, d_lastQuery, d_lastQueryTCC, d_osdump, d_osdumpTranslate, d_se, d_translate, d_translator, getFlags(), CVCL::ExprManager::getOutputLang(), CVCL::Expr::getType(), incomplete(), CVCL::Type::isBool(), CVCL::Theorem::isNull(), CVCL::Expr::negate(), CVCL::ContextManager::popto(), CVCL::Translator::preprocess(), printExpr(), printV(), CVCL::ContextManager::push(), CVCL::QUERY, scopeLevel(), CVCL::SMTLIB_LANG, CVCL::Expr::toString(), CVCL::Type::toString(), and CVCL::TRACE. Referenced by checkUnsat(), and subtypeType().

bool VCL::checkUnsat (  const Expr &  e  )  [private, virtual]

Check satisfiability of the expr in the current context. Returns false if the context is satisfiable and true if it is unsatisfiable. Note that this is equivalent to QUERY !e Implements CVCL::ValidityChecker. Definition at line 1731 of file vcl.cpp. References CVCL::Expr::negate(), and query().

bool VCL::checkContinue (   )  [private, virtual]

Get the next model. This method should only be called after a query which returns false. Returns false if another counterexample is found, true otherwise. Implements CVCL::ValidityChecker. Definition at line 1737 of file vcl.cpp. References andExpr(), CVCL::CONTINUE, d_dump, d_em, d_osdump, d_se, falseExpr(), CVCL::SearchEngine::getCounterExample(), CVCL::Theorem::isNull(), CVCL::ExprManager::newLeafExpr(), and CVCL::SearchEngine::restart().

bool VCL::restart (  const Expr &  e  )  [private, virtual]

Restart the most recent query with e as an additional assertion. This method should only be called after a query which returns false. Returns true if the resulting query is valid and false otherwise. Implements CVCL::ValidityChecker. Definition at line 1753 of file vcl.cpp. References d_dump, d_osdump, d_se, CVCL::Theorem::isNull(), CVCL::SearchEngine::restart(), and CVCL::RESTART.

void VCL::returnFromCheck (   )  [private, virtual]

Returns to context immediately before last invalid query. This method should only be called after a query which returns false. Implements CVCL::ValidityChecker. Definition at line 1762 of file vcl.cpp. References d_se, and CVCL::SearchEngine::returnFromCheck().

void CVCL::VCL::getUserAssumptions (  std::vector< Expr > &  assumptions  )  [private, 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 CVCL::ValidityChecker.

void CVCL::VCL::getInternalAssumptions (  std::vector< Expr > &  assumptions  )  [private, 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 CVCL::ValidityChecker.

void CVCL::VCL::getAssumptions (  std::vector< Expr > &  assumptions  )  [private, virtual]

Get all assumptions made in this and all previous contexts. Parameters: assumptions  should be empty on entry. Implements CVCL::ValidityChecker.

void CVCL::VCL::getAssumptionsUsed (  std::vector< Expr > &  assumptions  )  [private, 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. Parameters: assumptions  should be empty on entry. Implements CVCL::ValidityChecker.

void CVCL::VCL::getCounterExample (  std::vector< Expr > &  assertions, bool  inOrder )  [private, 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 CVCL::ValidityChecker.

void VCL::getConcreteModel (  ExprMap< Expr > &  m  )  [private, virtual]

Will assign concrete values to all user created variables. This function should only be called after a query which return false. Implements CVCL::ValidityChecker. Definition at line 1812 of file vcl.cpp. References CVCL::COUNTERMODEL, d_dump, d_em, d_osdump, d_se, CVCL::SearchEngine::getConcreteModel(), and CVCL::ExprManager::newLeafExpr().

bool CVCL::VCL::inconsistent (  std::vector< Expr > &  assumptions  )  [private, 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 CVCL::ValidityChecker.

bool VCL::incomplete (   )  [private, virtual]

Returns true if the invalid result from last query() is imprecise. Some decision procedures in CVC Lite 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 CVCL::ValidityChecker. Definition at line 1834 of file vcl.cpp. References d_lastQuery, and CVCL::Theorem3::isNull(). Referenced by query().

bool CVCL::VCL::incomplete (  std::vector< std::string > &  reasons  )  [private, 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 CVCL::ValidityChecker.

Proof VCL::getProof (   )  [private, 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 CVCL::ValidityChecker. Definition at line 1848 of file vcl.cpp. References d_dump, d_em, d_lastQuery, d_osdump, d_se, CVCL::DUMP_PROOF, CVCL::SearchEngine::getProof(), CVCL::Theorem3::isNull(), and CVCL::ExprManager::newLeafExpr().

const Expr & VCL::getTCC (   )  [private, virtual]

Returns the TCC of the last assumption or query. Returns Null if no assumptions or queries were performed. Implements CVCL::ValidityChecker. Definition at line 1862 of file vcl.cpp. References d_dump, d_em, d_lastQueryTCC, d_osdump, CVCL::DUMP_TCC, CVCL::Theorem::getExpr(), CVCL::Theorem::isNull(), and CVCL::ExprManager::newLeafExpr().

void CVCL::VCL::getAssumptionsTCC (  std::vector< Expr > &  assumptions  )  [private, virtual]

Return the set of assumptions used in the proof of the last TCC. Implements CVCL::ValidityChecker.

const Proof & VCL::getProofTCC (   )  [private, virtual]

Returns the proof of TCC of the last assumption or query. Returns Null if no assumptions or queries were performed. Implements CVCL::ValidityChecker. Definition at line 1885 of file vcl.cpp. References d_dump, d_em, d_lastQueryTCC, d_osdump, CVCL::DUMP_TCC_PROOF, CVCL::Theorem::getProof(), CVCL::Theorem::isNull(), and CVCL::ExprManager::newLeafExpr().

const Expr & VCL::getClosure (   )  [private, 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 CVCL::ValidityChecker. Definition at line 1895 of file vcl.cpp. References d_dump, d_em, d_lastClosure, d_lastQuery, d_osdump, deriveClosure(), CVCL::DUMP_CLOSURE, CVCL::Theorem3::getExpr(), CVCL::Theorem3::isNull(), and CVCL::ExprManager::newLeafExpr().

const Proof & VCL::getProofClosure (   )  [private, virtual]

Construct a proof of the query closure |- Gamma => phi. Returns Null if last query was Invalid. Implements CVCL::ValidityChecker. Definition at line 1909 of file vcl.cpp. References d_dump, d_em, d_lastClosure, d_lastQuery, d_osdump, deriveClosure(), CVCL::DUMP_CLOSURE_PROOF, CVCL::Theorem3::getProof(), CVCL::Theorem3::isNull(), and CVCL::ExprManager::newLeafExpr().

int VCL::stackLevel (   )  [private, virtual]

Returns the current stack level. Initial level is 0. Implements CVCL::ValidityChecker. Definition at line 1923 of file vcl.cpp. References d_scopeStack. Referenced by popto().

void VCL::push (   )  [private, virtual]

Checkpoint the current context and increase the scope level. Implements CVCL::ValidityChecker. Definition at line 1929 of file vcl.cpp. References d_cm, d_dump, d_em, d_osdump, d_scopeStack, CVCL::ExprManager::newLeafExpr(), CVCL::ContextManager::push(), CVCL::PUSH, scopeLevel(), and CVCL::TRACE.

void VCL::pop (   )  [private, virtual]

Restore the current context to its state at the last checkpoint. Implements CVCL::ValidityChecker. Definition at line 1942 of file vcl.cpp. References d_cm, d_dump, d_em, d_osdump, d_scopeStack, CVCL::ExprManager::newLeafExpr(), CVCL::POP, CVCL::ContextManager::popto(), and CVCL::TRACE.

void VCL::popto (  int  stackLevel  )  [private, 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 CVCL::ValidityChecker. Definition at line 1957 of file vcl.cpp. References d_cm, d_dump, d_osdump, d_scopeStack, CVCL::ContextManager::popto(), CVCL::POPTO, ratExpr(), and stackLevel().

int VCL::scopeLevel (   )  [private, virtual]

Returns the current scope level. Initially, the scope level is 1. Implements CVCL::ValidityChecker. Definition at line 1974 of file vcl.cpp. References d_cm, and CVCL::ContextManager::scopeLevel(). Referenced by assertFormula(), popScope(), poptoScope(), push(), pushScope(), query(), simplifyThm(), and subtypeType().

void VCL::pushScope (   )  [private, virtual]

Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing! Implements CVCL::ValidityChecker. Definition at line 1980 of file vcl.cpp. References d_cm, d_dump, d_em, d_flags, d_osdump, IF_DEBUG(), CVCL::ExprManager::newLeafExpr(), CVCL::ContextManager::push(), CVCL::PUSH_SCOPE, and scopeLevel().

void VCL::popScope (   )  [private, virtual]

Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing! Implements CVCL::ValidityChecker. Definition at line 1991 of file vcl.cpp. References d_cm, d_dump, d_em, d_flags, d_osdump, IF_DEBUG(), CVCL::ExprManager::newLeafExpr(), CVCL::ContextManager::pop(), CVCL::POP_SCOPE, and scopeLevel().

void VCL::poptoScope (  int  scopeLevel  )  [private, 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 CVCL::ValidityChecker. Definition at line 2005 of file vcl.cpp. References d_cm, d_dump, d_flags, d_osdump, IF_DEBUG(), CVCL::ContextManager::popto(), CVCL::POPTO_SCOPE, CVCL::ContextManager::push(), ratExpr(), and scopeLevel().

Context * VCL::getCurrentContext (   )  [private, virtual]

Get the current context. Implements CVCL::ValidityChecker. Definition at line 2020 of file vcl.cpp. References d_cm, and CVCL::ContextManager::getCurrentContext().

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

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

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

Read and execute the commands from a stream. Implements CVCL::ValidityChecker.

Statistics& CVCL::VCL::getStatistics (   )  [inline, private, virtual]

Get statistics object. Implements CVCL::ValidityChecker. Definition at line 346 of file vcl.h. References d_statistics.

void CVCL::VCL::printStatistics (   )  [inline, private, virtual]

Print collected statistics to stdout. Implements CVCL::ValidityChecker. Definition at line 347 of file vcl.h. References d_statistics, and std::endl().

---

Member Data Documentation

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

Pointers to main system components. Definition at line 61 of file vcl.h. Referenced by assertFormula(), checkContinue(), falseExpr(), getClosure(), getConcreteModel(), getEM(), getProof(), getProofClosure(), getProofTCC(), getTCC(), importExpr(), importType(), pop(), popScope(), push(), pushScope(), query(), ratExpr(), and trueExpr().

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

Definition at line 62 of file vcl.h. Referenced by assertFormula(), getCurrentContext(), pop(), popScope(), popto(), poptoScope(), push(), pushScope(), query(), scopeLevel(), simplifyThm(), and subtypeType().

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

Definition at line 63 of file vcl.h.

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

Definition at line 64 of file vcl.h. Referenced by assertFormula(), checkContinue(), getConcreteModel(), getImpliedLiteral(), getProof(), query(), registerAtom(), reprocessFlags(), restart(), returnFromCheck(), and simplifyThm().

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

Pointers to theories. Definition at line 67 of file vcl.h. Referenced by deriveClosure().

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

Definition at line 68 of file vcl.h.

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

Definition at line 69 of file vcl.h. Referenced by intType(), realType(), and subrangeType().

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

Definition at line 70 of file vcl.h.

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

Definition at line 71 of file vcl.h.

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

Definition at line 72 of file vcl.h. Referenced by tupleSelectExpr(), tupleType(), and tupleUpdateExpr().

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

Definition at line 73 of file vcl.h.

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

Definition at line 74 of file vcl.h.

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

Definition at line 75 of file vcl.h.

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

Definition at line 76 of file vcl.h. Referenced by query().

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

All theories are stored in this common vector. This includes TheoryCore and TheoryArith. Definition at line 80 of file vcl.h.

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

Command line flags. Definition at line 83 of file vcl.h. Referenced by getFlags(), popScope(), poptoScope(), pushScope(), and reprocessFlags().

std::vector<int> CVCL::VCL::d_scopeStack [private]

User-level view of the scope stack. Definition at line 86 of file vcl.h. Referenced by pop(), popto(), push(), and stackLevel().

Str_To_Expr CVCL::VCL::d_vars [private]

Cache for printV method. Definition at line 89 of file vcl.h. Referenced by printV().

Statistics CVCL::VCL::d_statistics [private]

Run-time statistics. Definition at line 92 of file vcl.h. Referenced by getStatistics(), and printStatistics().

size_t CVCL::VCL::d_nextIdx [private]

Next index for user assertion. Definition at line 95 of file vcl.h. Referenced by assertFormula().

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

Backtracking map of user assertions. Definition at line 121 of file vcl.h. Referenced by assertFormula().

Theorem3 CVCL::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 126 of file vcl.h. Referenced by getClosure(), getProof(), getProofClosure(), incomplete(), and query().

Theorem CVCL::VCL::d_lastQueryTCC [private]

Result of the last query(e, true) (for a TCC). Definition at line 129 of file vcl.h. Referenced by assertFormula(), getProofTCC(), getTCC(), query(), and simplifyThm().

Theorem3 CVCL::VCL::d_lastClosure [private]

Closure of the last query(e): |- Gamma => e. Definition at line 132 of file vcl.h. Referenced by getClosure(), getProofClosure(), and query().

std::ostream* CVCL::VCL::d_osdump [private]

The log file for top-level API calls in the CVCL input language. Definition at line 135 of file vcl.h. Referenced by assertFormula(), checkContinue(), getClosure(), getConcreteModel(), getProof(), getProofClosure(), getProofTCC(), getTCC(), pop(), popScope(), popto(), poptoScope(), push(), pushScope(), query(), and restart().

std::ostream* CVCL::VCL::d_osdumpTranslate [private]

Definition at line 136 of file vcl.h. Referenced by query().

std::ofstream CVCL::VCL::d_osdumpFile [private]

Definition at line 137 of file vcl.h.

std::ofstream CVCL::VCL::d_osdumpTranslateFile [private]

Definition at line 137 of file vcl.h.

std::ifstream CVCL::VCL::d_tmpFile [private]

Definition at line 138 of file vcl.h.

const bool& CVCL::VCL::d_translate [private]

Definition at line 139 of file vcl.h. Referenced by assertFormula(), and query().

bool CVCL::VCL::d_dump [private]

Definition at line 140 of file vcl.h. Referenced by assertFormula(), checkContinue(), getClosure(), getConcreteModel(), getProof(), getProofClosure(), getProofTCC(), getTCC(), pop(), popScope(), popto(), poptoScope(), push(), pushScope(), query(), and restart().

bool CVCL::VCL::d_dumpFileOpen [private]

Definition at line 140 of file vcl.h.

bool CVCL::VCL::d_translateFileOpen [private]

Definition at line 140 of file vcl.h.

VCL::~VCL [private]

Definition at line 513 of file vcl.cpp.

---

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

• vcl.h
• vcl.cpp

---