CVCL::ValidityChecker Class Reference
[Validity Checker API]

Generic API for a validity checker

. More...

#include <vc.h>

Inheritance diagram for CVCL::ValidityChecker:

[legend]List of all members.

Public Member Functions

• ValidityChecker ()

  Constructor.
  

• virtual ~ValidityChecker ()

  Destructor.
  

• virtual CLFlags & getFlags () const =0

  Return the set of command-line flags.
  

• virtual void reprocessFlags ()=0

  Force reprocessing of all flags.
  

Type-related methods

Methods for creating and looking up types

See also:

class Type

• virtual Type boolType ()=0

  Create type BOOLEAN.
  

• virtual Type realType ()=0

  Create type REAL.
  

• virtual Type intType ()=0

  Create type INT.
  

• virtual Type subrangeType (const Expr &l, const Expr &r)=0

  Create a subrange type [l..r].
  

• virtual Type subtypeType (const Expr &pred)=0

  Creates a subtype defined by the given predicate.
  

• virtual Type tupleType (const Type &type0, const Type &type1)=0

  2-element tuple
  

• virtual Type tupleType (const Type &type0, const Type &type1, const Type &type2)=0

  3-element tuple
  

• virtual Type tupleType (const std::vector< Type > &types)=0

  n-element tuple (from a vector of types)
  

• virtual Type recordType (const std::string &field, const Type &type)=0

  1-element record
  

• virtual Type recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0

  2-element record
  

• virtual Type recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)=0

  3-element record
  

• virtual Type recordType (const std::vector< std::string > &fields, const std::vector< Type > &types)=0

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

• virtual Type dataType (const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)=0

  Single datatype, single constructor.
  

• virtual Type dataType (const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)=0

  Single datatype, multiple constructors.
  

• virtual void dataType (const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes)=0

  Multiple datatypes.
  

• virtual Type arrayType (const Type &typeIndex, const Type &typeData)=0

  Create an array type (ARRAY typeIndex OF typeData).
  

• virtual Type funType (const Type &typeDom, const Type &typeRan)=0

  Create a function type typeDom -> typeRan.
  

• virtual Type funType (const std::vector< Type > &typeDom, const Type &typeRan)=0

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

• virtual Type createType (const std::string &typeName)=0

  Create named user-defined uninterpreted type.
  

• virtual Type createType (const std::string &typeName, const Type &def)=0

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

• virtual Type lookupType (const std::string &typeName)=0

  Lookup a user-defined (uninterpreted) type by name.
  

General Expr methods

See also:

class Expr

class ExprManager

• virtual ExprManager * getEM ()=0

  Return the ExprManager.
  

• virtual Expr varExpr (const std::string &name, const Type &type)=0

  Create a variable with a given name and type.
  

• virtual Expr varExpr (const std::string &name, const Type &type, const Expr &def)=0

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

• virtual Expr boundVarExpr (const std::string &name, const std::string &uid, const Type &type)=0

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

• virtual Expr lookupVar (const std::string &name, Type *type)=0

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

• virtual Type getType (const Expr &e)=0

  Get the type of the Expr.
  

• virtual Type getBaseType (const Expr &e)=0

  Get the largest supertype of the Expr.
  

• virtual Type getBaseType (const Type &t)=0

  Get the largest supertype of the Type.
  

• virtual Expr getTypePred (const Type &t, const Expr &e)=0

  Get the subtype predicate.
  

• virtual Expr stringExpr (const std::string &str)=0

  Create a string Expr.
  

• virtual Expr idExpr (const std::string &name)=0

  Create an ID Expr.
  

• virtual Expr listExpr (const std::vector< Expr > &kids)=0

  Create a list Expr.
  

• virtual Expr listExpr (const Expr &e1)=0

  Overloaded version of listExpr with one argument.
  

• virtual Expr listExpr (const Expr &e1, const Expr &e2)=0

  Overloaded version of listExpr with two arguments.
  

• virtual Expr listExpr (const Expr &e1, const Expr &e2, const Expr &e3)=0

  Overloaded version of listExpr with three arguments.
  

• virtual Expr listExpr (const std::string &op, const std::vector< Expr > &kids)=0

  Overloaded version of listExpr with string operator and many arguments.
  

• virtual Expr listExpr (const std::string &op, const Expr &e1)=0

  Overloaded version of listExpr with string operator and one argument.
  

• virtual Expr listExpr (const std::string &op, const Expr &e1, const Expr &e2)=0

  Overloaded version of listExpr with string operator and two arguments.
  

• virtual Expr listExpr (const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)=0

  Overloaded version of listExpr with string operator and three arguments.
  

• virtual void printExpr (const Expr &e)=0

  Prints e to the standard output.
  

• virtual void printExpr (const Expr &e, std::ostream &os)=0

  Prints e to the given ostream.
  

• virtual Expr parseExpr (const Expr &e)=0

  Parse an expression using a Theory-specific parser.
  

• virtual Type parseType (const Expr &e)=0

  Parse a type expression using a Theory-specific parser.
  

• virtual Expr importExpr (const Expr &e)=0

  Import the Expr from another instance of ValidityChecker.
  

• virtual Type importType (const Type &t)=0

  Import the Type from another instance of ValidityChecker.
  

Core expression methods

Methods for manipulating core expressions

Except for equality and ite, the children provided as arguments must be of type Boolean.

• virtual Expr trueExpr ()=0

  Return TRUE Expr.
  

• virtual Expr falseExpr ()=0

  Return FALSE Expr.
  

• virtual Expr notExpr (const Expr &child)=0

  Create negation.
  

• virtual Expr andExpr (const Expr &left, const Expr &right)=0

  Create 2-element conjunction.
  

• virtual Expr andExpr (const std::vector< Expr > &children)=0

  Create n-element conjunction.
  

• virtual Expr orExpr (const Expr &left, const Expr &right)=0

  Create 2-element disjunction.
  

• virtual Expr orExpr (const std::vector< Expr > &children)=0

  Create n-element disjunction.
  

• virtual Expr impliesExpr (const Expr &hyp, const Expr &conc)=0

  Create Boolean implication.
  

• virtual Expr iffExpr (const Expr &left, const Expr &right)=0

  Create left IFF right (boolean equivalence).
  

• virtual Expr eqExpr (const Expr &child0, const Expr &child1)=0

  Create an equality expression.
  

• virtual Expr iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0

  Create IF ifpart THEN thenpart ELSE elsepart ENDIF.
  

User-defined (uninterpreted) function methods

Methods for manipulating uninterpreted function expressions

• virtual Op createOp (const std::string &name, const Type &type)=0

  Create a named uninterpreted function with a given type.
  

• virtual Op createOp (const std::string &name, const Type &type, const Expr &def)=0

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

• virtual Expr funExpr (const Op &op, const Expr &child)=0

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

• virtual Expr funExpr (const Op &op, const Expr &left, const Expr &right)=0

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

• virtual Expr funExpr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)=0

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

• virtual Expr funExpr (const Op &op, const std::vector< Expr > &children)=0

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

Arithmetic expression methods

Methods for manipulating arithmetic expressions

These functions create arithmetic expressions. The children provided as arguments must be of type Real.

• virtual Expr ratExpr (int n, int d=1)=0

  Create a rational number with numerator n and denominator d.
  

• virtual Expr ratExpr (const std::string &n, const std::string &d, int base)=0

  Create a rational number with numerator n and denominator d.
  

• virtual Expr ratExpr (const std::string &n, int base=10)=0

  Create a rational from a single string.
  

• virtual Expr uminusExpr (const Expr &child)=0

  Unary minus.
  

• virtual Expr plusExpr (const Expr &left, const Expr &right)=0

  Create 2-element sum (left + right).
  

• virtual Expr minusExpr (const Expr &left, const Expr &right)=0

  Make a difference (left - right).
  

• virtual Expr multExpr (const Expr &left, const Expr &right)=0

  Create a product (left * right).
  

• virtual Expr powExpr (const Expr &x, const Expr &n)=0

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

• virtual Expr divideExpr (const Expr &numerator, const Expr &denominator)=0

  Create expression x / y.
  

• virtual Expr ltExpr (const Expr &left, const Expr &right)=0

  Create (left < right).
  

• virtual Expr leExpr (const Expr &left, const Expr &right)=0

  Create (left <= right).
  

• virtual Expr gtExpr (const Expr &left, const Expr &right)=0

  Create (left > right).
  

• virtual Expr geExpr (const Expr &left, const Expr &right)=0

  Create (left >= right).
  

Record expression methods

Methods for manipulating record expressions

• virtual Expr recordExpr (const std::string &field, const Expr &expr)=0

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

• virtual Expr recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)=0

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

• virtual Expr recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)=0

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

• virtual Expr recordExpr (const std::vector< std::string > &fields, const std::vector< Expr > &exprs)=0

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

• virtual Expr recSelectExpr (const Expr &record, const std::string &field)=0

  Create record.field (field selection).
  

• virtual Expr recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue)=0

  Record update; equivalent to "record WITH .field := newValue".
  

Array expression methods

Methods for manipulating array expressions

• virtual Expr readExpr (const Expr &array, const Expr &index)=0

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

• virtual Expr writeExpr (const Expr &array, const Expr &index, const Expr &newValue)=0

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

Other expression methods

Methods for manipulating other kinds of expressions

• virtual Expr tupleExpr (const std::vector< Expr > &exprs)=0

  Tuple expression.
  

• virtual Expr tupleSelectExpr (const Expr &tuple, int index)=0

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

• virtual Expr tupleUpdateExpr (const Expr &tuple, int index, const Expr &newValue)=0

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

• virtual Expr datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args)=0

  Datatype constructor expression.
  

• virtual Expr datatypeSelExpr (const std::string &selector, const Expr &arg)=0

  Datatype selector expression.
  

• virtual Expr datatypeTestExpr (const std::string &constructor, const Expr &arg)=0

  Datatype tester expression.
  

• virtual Expr forallExpr (const std::vector< Expr > &vars, const Expr &body)=0

  Universal quantifier.
  

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

  Existential quantifier.
  

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

  Lambda-expression.
  

• virtual Expr simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0

  Symbolic simulation expression.
  

Validity checking methods

Methods related to validity checking

This group includes methods for asserting formulas, checking validity in the given logical context, manipulating the scope level of the context, etc.

• virtual void setResourceLimit (unsigned limit)=0

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

• virtual void assertFormula (const Expr &e)=0

  Assert a new formula in the current context.
  

• virtual void registerAtom (const Expr &e)=0

  Register an atomic formula of interest.
  

• virtual Expr getImpliedLiteral ()=0

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

• virtual Expr simplify (const Expr &e)=0

  Simplify e with respect to the current context.
  

• virtual Theorem3 simplifyThm (const Expr &e)=0

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

• virtual Theorem simplifyThm2 (const Expr &e)=0

  Simpfy e, ignoring TCCs (assumes total interpretation).
  

• virtual void printV (const Expr &e)=0

  Dump all variables in e.
  

• virtual bool query (const Expr &e, bool tcc=false)=0

  Check validity of e in the current context.
  

• virtual bool checkUnsat (const Expr &e)=0

  Check satisfiability of the expr in the current context.
  

• virtual bool checkContinue ()=0

  Get the next model.
  

• virtual bool restart (const Expr &e)=0

  Restart the most recent query with e as an additional assertion.
  

• virtual void returnFromCheck ()=0

  Returns to context immediately before last invalid query.
  

• virtual void getUserAssumptions (std::vector< Expr > &assumptions)=0

  Get assumptions made by the user in this and all previous contexts.
  

• virtual void getInternalAssumptions (std::vector< Expr > &assumptions)=0

  Get assumptions made internally in this and all previous contexts.
  

• virtual void getAssumptions (std::vector< Expr > &assumptions)=0

  Get all assumptions made in this and all previous contexts.
  

• virtual void getAssumptionsUsed (std::vector< Expr > &assumptions)=0

  Returns the set of assumptions used in the proof of queried formula.
  

• virtual void getCounterExample (std::vector< Expr > &assumptions, bool inOrder=true)=0

  Return the internal assumptions that make the queried formula false.
  

• virtual void getConcreteModel (ExprMap< Expr > &m)=0

  Will assign concrete values to all user created variables.
  

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

  Returns true if the current context is inconsistent.
  

• virtual bool incomplete ()=0

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

• virtual bool incomplete (std::vector< std::string > &reasons)=0

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

• virtual Proof getProof ()=0

  Returns the proof term for the last proven query.
  

• virtual const Expr & getTCC ()=0

  Returns the TCC of the last assumption or query.
  

• virtual void getAssumptionsTCC (std::vector< Expr > &assumptions)=0

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

• virtual const Proof & getProofTCC ()=0

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

• virtual const Expr & getClosure ()=0

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

• virtual const Proof & getProofClosure ()=0

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

Context methods

Methods for manipulating contexts

Contexts support stack-based push and pop. There are two separate notions of the current context stack. stackLevel(), push(), pop(), and popto() work with the user-level notion of the stack.

scopeLevel(), pushScope(), popScope(), and poptoScope() work with the internal stack which is more fine-grained than the user stack.

Do not use the scope methods unless you know what you are doing. *

• virtual int stackLevel ()=0

  Returns the current stack level. Initial level is 0.
  

• virtual void push ()=0

  Checkpoint the current context and increase the scope level.
  

• virtual void pop ()=0

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

• virtual void popto (int stackLevel)=0

  Restore the current context to the given stackLevel.
  

• virtual int scopeLevel ()=0

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

• virtual void pushScope ()=0

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

• virtual void popScope ()=0

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

• virtual void poptoScope (int scopeLevel)=0

  Restore the current context to the given scopeLevel.
  

• virtual Context * getCurrentContext ()=0

  Get the current context.
  

Reading files

Methods for reading external files

• virtual void loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0

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

• virtual void loadFile (std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0

  Read and execute the commands from a stream.
  

Reporting Statistics

Methods for collecting and reporting run-time statistics

• virtual Statistics & getStatistics ()=0

  Get statistics object.
  

• virtual void printStatistics ()=0

  Print collected statistics to stdout.
  

Static Public Member Functions

• static CLFlags createFlags ()

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

• static ValidityChecker * create (const CLFlags &flags)

  Create an instance of ValidityChecker.
  

• static ValidityChecker * create ()

  Create an instance of ValidityChecker using default flag values.
  

---

Detailed Description

Generic API for a validity checker

.

Author: Clark Barrett

Created: Tue Nov 26 18:24:25 2002

All terms and formulas are represented as expressions using the Expr class. The notion of a context is also important. A context is a "background" set of formulas which are assumed to be true or false. Formulas can be added to the context explicitly, using assertFormula, or they may be added as part of processing a query command. At any time, the current set of formulas making up the context can be retrieved using getAssumptions.

Definition at line 92 of file vc.h.

---

Constructor & Destructor Documentation

CVCL::ValidityChecker::ValidityChecker (   )  [inline]

Constructor. Definition at line 96 of file vc.h.

virtual CVCL::ValidityChecker::~ValidityChecker (   )  [inline, virtual]

Destructor. Definition at line 98 of file vc.h.

---

Member Function Documentation

virtual CLFlags& CVCL::ValidityChecker::getFlags (   )  const [pure virtual]

Return the set of command-line flags. The flags are returned by reference, and if modified, will have an immediate effect on the subsequent commands. Note that not all flags will have such an effect; some flags are used only at initialization time (like "sat"), and therefore, will not take effect if modified after ValidityChecker is created. Implemented in CVCL::VCL. Referenced by CVCL::VCCmd::evaluateNext(), main(), CVCL::VCCmd::reportResult(), and sighandler().

virtual void CVCL::ValidityChecker::reprocessFlags (   )  [pure virtual]

Force reprocessing of all flags. Implemented in CVCL::VCL.

CLFlags ValidityChecker::createFlags (   )  [static]

Create the set of command line flags with default values;. Returns: the set of flags by value Definition at line 71 of file vcl.cpp. References CVCL::CLFlags::addFlag(), and IF_DEBUG(). Referenced by create(), and main().

ValidityChecker * ValidityChecker::create (  const CLFlags &  flags  )  [static]

Create an instance of ValidityChecker. Parameters: flags  is the set of command line flags. Definition at line 65 of file vcl.cpp.

ValidityChecker * ValidityChecker::create (   )  [static]

Create an instance of ValidityChecker using default flag values. Definition at line 235 of file vcl.cpp. References createFlags(). Referenced by main().

virtual Type CVCL::ValidityChecker::boolType (   )  [pure virtual]

Create type BOOLEAN. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::realType (   )  [pure virtual]

Create type REAL. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::intType (   )  [pure virtual]

Create type INT. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::subrangeType (  const Expr &  l, const Expr &  r )  [pure virtual]

Create a subrange type [l..r]. l and r can be Null; l=Null represents minus infinity, r=Null is plus infinity. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::subtypeType (  const Expr &  pred  )  [pure 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). Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::tupleType (  const Type &  type0, const Type &  type1 )  [pure virtual]

2-element tuple Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::tupleType (  const Type &  type0, const Type &  type1, const Type &  type2 )  [pure virtual]

3-element tuple Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::tupleType (  const std::vector< Type > &  types  )  [pure virtual]

n-element tuple (from a vector of types) Implemented in CVCL::VCL.

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

1-element record Implemented in CVCL::VCL.

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

2-element record Fields will be sorted automatically Implemented in CVCL::VCL.

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

3-element record Fields will be sorted automatically Implemented in CVCL::VCL.

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

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

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

Single datatype, single constructor. The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::dataType (  const std::string &  name, const std::vector< std::string > &  constructors, const std::vector< std::vector< std::string > > &  selectors, const std::vector< std::vector< Expr > > &  types )  [pure virtual]

Single datatype, multiple constructors. The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::dataType (  const std::vector< std::string > &  names, const std::vector< std::vector< std::string > > &  constructors, const std::vector< std::vector< std::vector< std::string > > > &  selectors, const std::vector< std::vector< std::vector< Expr > > > &  types, std::vector< Type > &  returnTypes )  [pure virtual]

Multiple datatypes. The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::arrayType (  const Type &  typeIndex, const Type &  typeData )  [pure virtual]

Create an array type (ARRAY typeIndex OF typeData). Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::funType (  const Type &  typeDom, const Type &  typeRan )  [pure virtual]

Create a function type typeDom -> typeRan. Implemented in CVCL::VCL.

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

Create a function type (t1,t2,...,tn) -> typeRan. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::createType (  const std::string &  typeName  )  [pure virtual]

Create named user-defined uninterpreted type. Implemented in CVCL::VCL.

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

Create named user-defined interpreted type (type abbreviation). Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::lookupType (  const std::string &  typeName  )  [pure virtual]

Lookup a user-defined (uninterpreted) type by name. Implemented in CVCL::VCL.

virtual ExprManager* CVCL::ValidityChecker::getEM (   )  [pure virtual]

Return the ExprManager. Implemented in CVCL::VCL. Referenced by main().

virtual Expr CVCL::ValidityChecker::varExpr (  const std::string &  name, const Type &  type )  [pure 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 Implemented in CVCL::VCL.

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

Create a variable with a given name, type, and value. Implemented in CVCL::VCL.

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

Create a bound variable with a given name, unique ID (uid) and type. Parameters: 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 Implemented in CVCL::VCL.

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

virtual Type CVCL::ValidityChecker::getType (  const Expr &  e  )  [pure virtual]

Get the type of the Expr. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::getBaseType (  const Expr &  e  )  [pure virtual]

Get the largest supertype of the Expr. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::getBaseType (  const Type &  t  )  [pure virtual]

Get the largest supertype of the Type. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::getTypePred (  const Type &  t, const Expr &  e )  [pure virtual]

Get the subtype predicate. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::stringExpr (  const std::string &  str  )  [pure virtual]

Create a string Expr. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::idExpr (  const std::string &  name  )  [pure virtual]

Create an ID Expr. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::listExpr (  const std::vector< Expr > &  kids  )  [pure virtual]

Create a list Expr. Intermediate representation for DP-specific expressions. Normally, the first element of the list is a string Expr representing an operator, and the rest of the list are the arguments. For example, kids.push_back(vc->stringExpr("PLUS")); kids.push_back(x); // x and y are previously created Exprs kids.push_back(y); Expr lst = vc->listExpr(kids); Or, alternatively (using its overloaded version): Expr lst = vc->listExpr("PLUS", x, y); or vector<Expr> summands; summands.push_back(x); summands.push_back(y); ... Expr lst = vc->listExpr("PLUS", summands); Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::listExpr (  const Expr &  e1  )  [pure virtual]

Overloaded version of listExpr with one argument. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::listExpr (  const Expr &  e1, const Expr &  e2 )  [pure virtual]

Overloaded version of listExpr with two arguments. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::listExpr (  const Expr &  e1, const Expr &  e2, const Expr &  e3 )  [pure virtual]

Overloaded version of listExpr with three arguments. Implemented in CVCL::VCL.

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

Overloaded version of listExpr with string operator and many arguments. Implemented in CVCL::VCL.

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

Overloaded version of listExpr with string operator and one argument. Implemented in CVCL::VCL.

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

Overloaded version of listExpr with string operator and two arguments. Implemented in CVCL::VCL.

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

Overloaded version of listExpr with string operator and three arguments. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::printExpr (  const Expr &  e  )  [pure virtual]

Prints e to the standard output. Implemented in CVCL::VCL.

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

Prints e to the given ostream. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::parseExpr (  const Expr &  e  )  [pure virtual]

Parse an expression using a Theory-specific parser. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::parseType (  const Expr &  e  )  [pure virtual]

Parse a type expression using a Theory-specific parser. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::importExpr (  const Expr &  e  )  [pure virtual]

Import the Expr from another instance of ValidityChecker. When expressions need to be passed among several instances of ValidityChecker, they need to be explicitly imported into the corresponding instance using this method. The return result is an identical expression that belongs to the current instance of ValidityChecker, and can be safely used as part of more complex expressions from the same instance. Implemented in CVCL::VCL.

virtual Type CVCL::ValidityChecker::importType (  const Type &  t  )  [pure virtual]

Import the Type from another instance of ValidityChecker. See also: getType() Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::trueExpr (   )  [pure virtual]

Return TRUE Expr. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::falseExpr (   )  [pure virtual]

Return FALSE Expr. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::notExpr (  const Expr &  child  )  [pure virtual]

Create negation. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::andExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create 2-element conjunction. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::andExpr (  const std::vector< Expr > &  children  )  [pure virtual]

Create n-element conjunction. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::orExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create 2-element disjunction. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::orExpr (  const std::vector< Expr > &  children  )  [pure virtual]

Create n-element disjunction. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::impliesExpr (  const Expr &  hyp, const Expr &  conc )  [pure virtual]

Create Boolean implication. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::iffExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create left IFF right (boolean equivalence). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::eqExpr (  const Expr &  child0, const Expr &  child1 )  [pure virtual]

Create an equality expression. The two children must have the same type, and cannot be of type Boolean. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::iteExpr (  const Expr &  ifpart, const Expr &  thenpart, const Expr &  elsepart )  [pure 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. Implemented in CVCL::VCL.

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

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

Create a named user-defined function with a given type. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::funExpr (  const Op &  op, const Expr &  child )  [pure virtual]

Unary function application (op must be of function type). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::funExpr (  const Op &  op, const Expr &  left, const Expr &  right )  [pure virtual]

Binary function application (op must be of function type). Implemented in CVCL::VCL.

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

Ternary function application (op must be of function type). Implemented in CVCL::VCL.

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

n-ary function application (op must be of function type) Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::ratExpr (  int  n, int  d = 1 )  [pure virtual]

Create a rational number with numerator n and denominator d. Parameters: n  the numerator d  the denominator, cannot be 0. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::ratExpr (  const std::string &  n, const std::string &  d, int  base )  [pure virtual]

Create a rational number with numerator n and denominator d. Here n and d are given as strings. They are converted to arbitrary-precision integers according to the given base. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::ratExpr (  const std::string &  n, int  base = 10 )  [pure 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. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::uminusExpr (  const Expr &  child  )  [pure virtual]

Unary minus. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::plusExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create 2-element sum (left + right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::minusExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Make a difference (left - right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::multExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create a product (left * right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::powExpr (  const Expr &  x, const Expr &  n )  [pure virtual]

Create a power expression (x ^ n); n must be integer. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::divideExpr (  const Expr &  numerator, const Expr &  denominator )  [pure virtual]

Create expression x / y. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::ltExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create (left < right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::leExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create (left <= right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::gtExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create (left > right). Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::geExpr (  const Expr &  left, const Expr &  right )  [pure virtual]

Create (left >= right). Implemented in CVCL::VCL.

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

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

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

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

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

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

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

Create an n-element record value (# field_i := expr_i #). Parameters: fields  exprs  must be the same length as fields Fields will be sorted automatically Implemented in CVCL::VCL.

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

Create record.field (field selection). Create an expression representing the selection of a field from a record. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::recUpdateExpr (  const Expr &  record, const std::string &  field, const Expr &  newValue )  [pure virtual]

Record update; equivalent to "record WITH .field := newValue". Notice the `.' before field in the presentation language (and the comment above); this is to distinguish it from datatype update. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::readExpr (  const Expr &  array, const Expr &  index )  [pure virtual]

Create an expression array[index] (array access). Create an expression for the value of array at the given index Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::writeExpr (  const Expr &  array, const Expr &  index, const Expr &  newValue )  [pure virtual]

Array update; equivalent to "array WITH index := newValue". Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::tupleExpr (  const std::vector< Expr > &  exprs  )  [pure virtual]

Tuple expression. Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::tupleSelectExpr (  const Expr &  tuple, int  index )  [pure virtual]

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

virtual Expr CVCL::ValidityChecker::tupleUpdateExpr (  const Expr &  tuple, int  index, const Expr &  newValue )  [pure virtual]

Tuple update; equivalent to "tuple WITH index := newValue". Implemented in CVCL::VCL.

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

Datatype constructor expression. Implemented in CVCL::VCL.

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

Datatype selector expression. Implemented in CVCL::VCL.

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

Datatype tester expression. Implemented in CVCL::VCL.

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

Universal quantifier. Implemented in CVCL::VCL.

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

Existential quantifier. Implemented in CVCL::VCL.

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

Lambda-expression. Implemented in CVCL::VCL.

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

virtual void CVCL::ValidityChecker::setResourceLimit (  unsigned  limit  )  [pure virtual]

Set the resource limit (0==unlimited, 1==exhausted). Currently, the limit is the total number of processed facts. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::assertFormula (  const Expr &  e  )  [pure virtual]

Assert a new formula in the current context. This creates the assumption e |- e. The formula must have Boolean type. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::registerAtom (  const Expr &  e  )  [pure virtual]

Register an atomic formula of interest. Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::getImpliedLiteral (   )  [pure virtual]

Return next literal implied by last assertion. Null Expr if none. Returned literals are either registered atomic formulas or their negation Implemented in CVCL::VCL.

virtual Expr CVCL::ValidityChecker::simplify (  const Expr &  e  )  [pure virtual]

Simplify e with respect to the current context. Implemented in CVCL::VCL.

virtual Theorem3 CVCL::ValidityChecker::simplifyThm (  const Expr &  e  )  [pure 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]. Implemented in CVCL::VCL.

virtual Theorem CVCL::ValidityChecker::simplifyThm2 (  const Expr &  e  )  [pure virtual]

Simpfy e, ignoring TCCs (assumes total interpretation). Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::printV (  const Expr &  e  )  [pure virtual]

Dump all variables in e. Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::query (  const Expr &  e, bool  tcc = false )  [pure 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) Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::checkUnsat (  const Expr &  e  )  [pure 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 Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::checkContinue (   )  [pure 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. Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::restart (  const Expr &  e  )  [pure virtual]

Restart the most recent query with e as an additional assertion. This method should only be called after a query which returns false. Returns true if the resulting query is valid and false otherwise. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::returnFromCheck (   )  [pure virtual]

Returns to context immediately before last invalid query. This method should only be called after a query which returns false. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getUserAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual]

Get assumptions made by the user in this and all previous contexts. User assumptions are created either by calls to assertFormula or by a call to query. In the latter case, the negated query is added as an assumption. Parameters: assumptions  should be empty on entry. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getInternalAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual]

Get assumptions made internally in this and all previous contexts. Internal assumptions are literals assumed by the sat solver. Parameters: assumptions  should be empty on entry. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual]

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

virtual void CVCL::ValidityChecker::getAssumptionsUsed (  std::vector< Expr > &  assumptions  )  [pure virtual]

Returns the set of assumptions used in the proof of queried formula. It returns a subset of getAssumptions(). If the last query was false or there has not yet been a query, it does nothing. Parameters: assumptions  should be empty on entry. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getCounterExample (  std::vector< Expr > &  assumptions, bool  inOrder = true )  [pure virtual]

Return the internal assumptions that make the queried formula false. This method should only be called after a query which returns false. It will try to return the simplest possible subset of the internal assumptions sufficient to make the queried expression false. Parameters: assumptions  should be empty on entry. inOrder  if true, returns the assumptions in the order they were made. This is slightly more expensive than inOrder = false. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getConcreteModel (  ExprMap< Expr > &  m  )  [pure virtual]

Will assign concrete values to all user created variables. This function should only be called after a query which return false. Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::inconsistent (  std::vector< Expr > &  assumptions  )  [pure virtual]

Returns true if the current context is inconsistent. Also returns a minimal set of assertions used to determine the inconsistency. Parameters: assumptions  should be empty on entry. Implemented in CVCL::VCL.

virtual bool CVCL::ValidityChecker::incomplete (   )  [pure 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. Implemented in CVCL::VCL. Referenced by CVCL::VCCmd::reportResult().

virtual bool CVCL::ValidityChecker::incomplete (  std::vector< std::string > &  reasons  )  [pure virtual]

Returns true if the invalid result from last query() is imprecise. See also: incomplete() The argument is filled with the reasons for incompleteness (they are intended to be shown to the end user). Implemented in CVCL::VCL.

virtual Proof CVCL::ValidityChecker::getProof (   )  [pure virtual]

Returns the proof term for the last proven query. If there has not been a successful query, it should return a NULL proof Implemented in CVCL::VCL.

virtual const Expr& CVCL::ValidityChecker::getTCC (   )  [pure virtual]

Returns the TCC of the last assumption or query. Returns Null if no assumptions or queries were performed. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::getAssumptionsTCC (  std::vector< Expr > &  assumptions  )  [pure virtual]

Return the set of assumptions used in the proof of the last TCC. Implemented in CVCL::VCL.

virtual const Proof& CVCL::ValidityChecker::getProofTCC (   )  [pure virtual]

Returns the proof of TCC of the last assumption or query. Returns Null if no assumptions or queries were performed. Implemented in CVCL::VCL.

virtual const Expr& CVCL::ValidityChecker::getClosure (   )  [pure virtual]

After successful query, return its closure |- Gamma => phi. Turn a valid query Gamma |- phi into an implication |- Gamma => phi. Returns Null if last query was invalid. Implemented in CVCL::VCL.

virtual const Proof& CVCL::ValidityChecker::getProofClosure (   )  [pure virtual]

Construct a proof of the query closure |- Gamma => phi. Returns Null if last query was Invalid. Implemented in CVCL::VCL.

virtual int CVCL::ValidityChecker::stackLevel (   )  [pure virtual]

Returns the current stack level. Initial level is 0. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::push (   )  [pure virtual]

Checkpoint the current context and increase the scope level. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::pop (   )  [pure virtual]

Restore the current context to its state at the last checkpoint. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::popto (  int  stackLevel  )  [pure 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. Implemented in CVCL::VCL.

virtual int CVCL::ValidityChecker::scopeLevel (   )  [pure virtual]

Returns the current scope level. Initially, the scope level is 1. Implemented in CVCL::VCL.

virtual void CVCL::ValidityChecker::pushScope (   )  [pure virtual]

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

virtual void CVCL::ValidityChecker::popScope (   )  [pure virtual]

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

virtual void CVCL::ValidityChecker::poptoScope (  int  scopeLevel  )  [pure 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. Implemented in CVCL::VCL.

virtual Context* CVCL::ValidityChecker::getCurrentContext (   )  [pure virtual]

Get the current context. Implemented in CVCL::VCL. Referenced by CVCL::VCCmd::VCCmd().

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

Read and execute the commands from a file given by name ("" means stdin). Implemented in CVCL::VCL. Referenced by main().

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

Read and execute the commands from a stream. Implemented in CVCL::VCL.

virtual Statistics& CVCL::ValidityChecker::getStatistics (   )  [pure virtual]

Get statistics object. Implemented in CVCL::VCL. Referenced by sighandler().

virtual void CVCL::ValidityChecker::printStatistics (   )  [pure virtual]

Print collected statistics to stdout. Implemented in CVCL::VCL. Referenced by main().

---

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

• vc.h
• vcl.cpp

---