CVC3
Classes | Public Member Functions | Private Member Functions | Private Attributes

CVC3::VCL Class Reference

#include <vcl.h>

Inherits CVC3::ValidityChecker.

Collaboration diagram for CVC3::VCL:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 50 of file vcl.h.


Constructor & Destructor Documentation

VCL::VCL ( const CLFlags flags)

Definition at line 408 of file vcl.cpp.

References IF_DEBUG.

VCL::~VCL ( )

Definition at line 608 of file vcl.cpp.

References IF_DEBUG, and TRACE_MSG.


Member Function Documentation

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

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

Definition at line 309 of file vcl.cpp.

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

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

Recursive assumption graph traversal to find user assumptions.

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

Definition at line 352 of file vcl.cpp.

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

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

Get set of user assertions from the set of assumptions.

Definition at line 379 of file vcl.cpp.

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

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

Check the tcc.

Definition at line 1810 of file vcl.cpp.

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

void VCL::init ( void  ) [private]

Initialize everything except flags.

Definition at line 447 of file vcl.cpp.

References DebugAssert.

void VCL::destroy ( void  ) [private]

Destroy everything except flags.

Definition at line 549 of file vcl.cpp.

References TRACE, and TRACE_MSG.

CLFlags& CVC3::VCL::getFlags ( ) const [inline, virtual]

Return the set of command-line flags.

The flags are returned by reference, and if modified, will have an immediate effect on the subsequent commands. Note that not all flags will have such an effect; some flags are used only at initialization time (like "sat"), and therefore, will not take effect if modified after ValidityChecker is created.

Implements CVC3::ValidityChecker.

Definition at line 169 of file vcl.h.

void VCL::reprocessFlags ( ) [virtual]

Force reprocessing of all flags.

Implements CVC3::ValidityChecker.

Definition at line 623 of file vcl.cpp.

References DebugAssert.

TheoryCore * VCL::core ( )

Definition at line 696 of file vcl.cpp.

Type VCL::boolType ( ) [virtual]

Create type BOOLEAN.

Implements CVC3::ValidityChecker.

Definition at line 700 of file vcl.cpp.

Type VCL::realType ( ) [virtual]

Create type REAL.

Implements CVC3::ValidityChecker.

Definition at line 705 of file vcl.cpp.

Type VCL::intType ( ) [virtual]

Create type INT.

Implements CVC3::ValidityChecker.

Definition at line 711 of file vcl.cpp.

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

Create a subrange type [l..r].

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

Implements CVC3::ValidityChecker.

Definition at line 716 of file vcl.cpp.

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

Creates a subtype defined by the given predicate.

Parameters:
predis a predicate taking one argument of type T and returning Boolean. The resulting type is a subtype of T whose elements x are those satisfying the predicate pred(x).
witnessis an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove $\exists x. pred(x))$. if the witness check fails, a TypecheckException is thrown.

Implements CVC3::ValidityChecker.

Definition at line 721 of file vcl.cpp.

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

2-element tuple

Implements CVC3::ValidityChecker.

Definition at line 727 of file vcl.cpp.

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

3-element tuple

Implements CVC3::ValidityChecker.

Definition at line 736 of file vcl.cpp.

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

n-element tuple (from a vector of types)

Implements CVC3::ValidityChecker.

Definition at line 746 of file vcl.cpp.

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

1-element record

Implements CVC3::ValidityChecker.

Definition at line 752 of file vcl.cpp.

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

2-element record

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 762 of file vcl.cpp.

References CVC3::sort2().

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

3-element record

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 775 of file vcl.cpp.

References CVC3::sort2().

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

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 792 of file vcl.cpp.

References DebugAssert, and CVC3::sort2().

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

Single datatype, single constructor.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

Implements CVC3::ValidityChecker.

Definition at line 806 of file vcl.cpp.

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

Single datatype, multiple constructors.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

Implements CVC3::ValidityChecker.

Definition at line 823 of file vcl.cpp.

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

Multiple datatypes.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

Implements CVC3::ValidityChecker.

Definition at line 836 of file vcl.cpp.

References CVC3::Expr::arity().

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

Create an array type (ARRAY typeIndex OF typeData)

Implements CVC3::ValidityChecker.

Definition at line 852 of file vcl.cpp.

References CVC3::arrayType().

Type VCL::bitvecType ( int  n) [virtual]

Create a bitvector type of length n.

Implements CVC3::ValidityChecker.

Definition at line 858 of file vcl.cpp.

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

Create a function type typeDom -> typeRan.

Implements CVC3::ValidityChecker.

Definition at line 864 of file vcl.cpp.

References CVC3::Type::funType().

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

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

Implements CVC3::ValidityChecker.

Definition at line 870 of file vcl.cpp.

References DebugAssert.

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

Create named user-defined uninterpreted type.

Implements CVC3::ValidityChecker.

Definition at line 876 of file vcl.cpp.

References TYPE.

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

Create named user-defined interpreted type (type abbreviation)

Implements CVC3::ValidityChecker.

Definition at line 885 of file vcl.cpp.

References CVC3::Type::getExpr(), and TYPE.

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

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

Implements CVC3::ValidityChecker.

Definition at line 894 of file vcl.cpp.

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

Return the ExprManager.

Implements CVC3::ValidityChecker.

Definition at line 211 of file vcl.h.

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

Create a variable with a given name and type.

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

Implements CVC3::ValidityChecker.

Definition at line 900 of file vcl.cpp.

References CONST, and CVC3::Type::getExpr().

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

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

Implements CVC3::ValidityChecker.

Definition at line 910 of file vcl.cpp.

References CONST, CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::toString(), and TRACE.

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

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

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

Implements CVC3::ValidityChecker.

Definition at line 955 of file vcl.cpp.

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

Get the type of the Expr.

Implements CVC3::ValidityChecker.

Definition at line 961 of file vcl.cpp.

References CVC3::Expr::getType().

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

Get the largest supertype of the Expr.

Implements CVC3::ValidityChecker.

Definition at line 967 of file vcl.cpp.

Type VCL::getBaseType ( const Type t) [virtual]

Get the largest supertype of the Type.

Implements CVC3::ValidityChecker.

Definition at line 973 of file vcl.cpp.

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

Get the subtype predicate.

Implements CVC3::ValidityChecker.

Definition at line 979 of file vcl.cpp.

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

Create a string Expr.

Implements CVC3::ValidityChecker.

Definition at line 985 of file vcl.cpp.

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

Create an ID Expr.

Implements CVC3::ValidityChecker.

Definition at line 990 of file vcl.cpp.

References ID.

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

Create a list Expr.

Intermediate representation for DP-specific expressions. Normally, the first element of the list is a string Expr representing an operator, and the rest of the list are the arguments. For example,

kids.push_back(vc->stringExpr("PLUS")); kids.push_back(x); // x and y are previously created Exprs kids.push_back(y); Expr lst = vc->listExpr(kids);

Or, alternatively (using its overloaded version):

Expr lst = vc->listExpr("PLUS", x, y);

or

vector<Expr> summands; summands.push_back(x); summands.push_back(y); ... Expr lst = vc->listExpr("PLUS", summands);

Implements CVC3::ValidityChecker.

Definition at line 995 of file vcl.cpp.

References RAW_LIST.

Expr VCL::listExpr ( const Expr e1) [virtual]

Overloaded version of listExpr with one argument.

Implements CVC3::ValidityChecker.

Definition at line 1000 of file vcl.cpp.

References RAW_LIST.

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

Overloaded version of listExpr with two arguments.

Implements CVC3::ValidityChecker.

Definition at line 1005 of file vcl.cpp.

References RAW_LIST.

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

Overloaded version of listExpr with three arguments.

Implements CVC3::ValidityChecker.

Definition at line 1010 of file vcl.cpp.

References RAW_LIST.

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

Overloaded version of listExpr with string operator and many arguments.

Implements CVC3::ValidityChecker.

Definition at line 1015 of file vcl.cpp.

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

Overloaded version of listExpr with string operator and one argument.

Implements CVC3::ValidityChecker.

Definition at line 1023 of file vcl.cpp.

References RAW_LIST.

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

Overloaded version of listExpr with string operator and two arguments.

Implements CVC3::ValidityChecker.

Definition at line 1028 of file vcl.cpp.

References RAW_LIST.

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

Overloaded version of listExpr with string operator and three arguments.

Implements CVC3::ValidityChecker.

Definition at line 1034 of file vcl.cpp.

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

Prints e to the standard output.

Implements CVC3::ValidityChecker.

Definition at line 1045 of file vcl.cpp.

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

Prints e to the given ostream.

Implements CVC3::ValidityChecker.

Definition at line 1050 of file vcl.cpp.

References std::endl().

Expr VCL::parseExpr ( const Expr e) [virtual]

Parse an expression using a Theory-specific parser.

Implements CVC3::ValidityChecker.

Definition at line 1055 of file vcl.cpp.

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

Parse a type expression using a Theory-specific parser.

Implements CVC3::ValidityChecker.

Definition at line 1060 of file vcl.cpp.

Expr VCL::importExpr ( const Expr e) [virtual]

Import the Expr from another instance of ValidityChecker.

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

Implements CVC3::ValidityChecker.

Definition at line 1065 of file vcl.cpp.

References CVC3::Expr::rebuild().

Type VCL::importType ( const Type t) [virtual]

Import the Type from another instance of ValidityChecker.

See also:
getType()

Implements CVC3::ValidityChecker.

Definition at line 1071 of file vcl.cpp.

References CVC3::Type::getExpr().

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

Parse a sequence of commands from a presentation language string.

Implements CVC3::ValidityChecker.

Definition at line 1076 of file vcl.cpp.

Expr VCL::exprFromString ( const std::string &  e) [virtual]

Parse an expression from a presentation language string.

Implements CVC3::ValidityChecker.

Definition at line 1082 of file vcl.cpp.

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

Expr VCL::trueExpr ( ) [virtual]

Return TRUE Expr.

Implements CVC3::ValidityChecker.

Definition at line 1095 of file vcl.cpp.

Expr VCL::falseExpr ( ) [virtual]

Return FALSE Expr.

Implements CVC3::ValidityChecker.

Definition at line 1101 of file vcl.cpp.

Expr VCL::notExpr ( const Expr child) [virtual]

Create negation.

Implements CVC3::ValidityChecker.

Definition at line 1107 of file vcl.cpp.

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

Create 2-element conjunction.

Implements CVC3::ValidityChecker.

Definition at line 1113 of file vcl.cpp.

References MiniSat::right().

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

Create n-element conjunction.

Implements CVC3::ValidityChecker.

Definition at line 1119 of file vcl.cpp.

References AND.

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

Create 2-element disjunction.

Implements CVC3::ValidityChecker.

Definition at line 1127 of file vcl.cpp.

References MiniSat::right().

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

Create n-element disjunction.

Implements CVC3::ValidityChecker.

Definition at line 1133 of file vcl.cpp.

References OR.

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

Create Boolean implication.

Implements CVC3::ValidityChecker.

Definition at line 1141 of file vcl.cpp.

References CVC3::Expr::impExpr().

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

Create left IFF right (boolean equivalence)

Implements CVC3::ValidityChecker.

Definition at line 1147 of file vcl.cpp.

References CVC3::Expr::iffExpr().

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

Create an equality expression.

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

Implements CVC3::ValidityChecker.

Definition at line 1153 of file vcl.cpp.

References CVC3::Expr::eqExpr().

Expr VCL::distinctExpr ( const std::vector< Expr > &  children) [virtual]

Create an expression asserting that all the children are different.

Parameters:
childrenthe children to be asserted different

Implements CVC3::ValidityChecker.

Definition at line 1158 of file vcl.cpp.

References DISTINCT.

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

Create IF ifpart THEN thenpart ELSE elsepart ENDIF.

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

Implements CVC3::ValidityChecker.

Definition at line 1163 of file vcl.cpp.

References CVC3::Expr::iteExpr().

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

Create a named uninterpreted function with a given type.

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

Implements CVC3::ValidityChecker.

Definition at line 1169 of file vcl.cpp.

References CONST, CVC3::Type::getExpr(), and CVC3::Type::isFunction().

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

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

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

Implements CVC3::ValidityChecker.

Definition at line 1239 of file vcl.cpp.

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

Unary function application (op must be of function type)

Implements CVC3::ValidityChecker.

Definition at line 1245 of file vcl.cpp.

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

Binary function application (op must be of function type)

Implements CVC3::ValidityChecker.

Definition at line 1251 of file vcl.cpp.

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

Ternary function application (op must be of function type)

Implements CVC3::ValidityChecker.

Definition at line 1257 of file vcl.cpp.

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

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

Implements CVC3::ValidityChecker.

Definition at line 1263 of file vcl.cpp.

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

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

Parameters:
smallerthe smaller variable
biggerthe bigger variable

Implements CVC3::ValidityChecker.

Definition at line 1268 of file vcl.cpp.

References ARITH_VAR_ORDER.

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

Create a rational number with numerator n and denominator d.

Parameters:
nthe numerator
dthe denominator, cannot be 0.

Implements CVC3::ValidityChecker.

Definition at line 1276 of file vcl.cpp.

References DebugAssert.

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

Create a rational number with numerator n and denominator d.

Here n and d are given as strings. They are converted to arbitrary-precision integers according to the given base.

Implements CVC3::ValidityChecker.

Definition at line 1283 of file vcl.cpp.

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

Create a rational from a single string.

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

Implements CVC3::ValidityChecker.

Definition at line 1289 of file vcl.cpp.

References CVC3::pow().

Expr VCL::uminusExpr ( const Expr child) [virtual]

Unary minus.

Implements CVC3::ValidityChecker.

Definition at line 1316 of file vcl.cpp.

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

Create 2-element sum (left + right)

Implements CVC3::ValidityChecker.

Definition at line 1322 of file vcl.cpp.

References MiniSat::right().

Expr VCL::plusExpr ( const std::vector< Expr > &  children) [virtual]

Create n-element sum.

Implements CVC3::ValidityChecker.

Definition at line 1327 of file vcl.cpp.

References CVC3::PLUS.

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

Make a difference (left - right)

Implements CVC3::ValidityChecker.

Definition at line 1333 of file vcl.cpp.

References MiniSat::right().

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

Create a product (left * right)

Implements CVC3::ValidityChecker.

Definition at line 1339 of file vcl.cpp.

References MiniSat::right().

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

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

Implements CVC3::ValidityChecker.

Definition at line 1345 of file vcl.cpp.

References CVC3::powExpr().

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

Create expression x / y.

Implements CVC3::ValidityChecker.

Definition at line 1351 of file vcl.cpp.

References CVC3::divideExpr().

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

Create (left < right)

Implements CVC3::ValidityChecker.

Definition at line 1357 of file vcl.cpp.

References CVC3::ltExpr().

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

Create (left <= right)

Implements CVC3::ValidityChecker.

Definition at line 1363 of file vcl.cpp.

References CVC3::leExpr().

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

Create (left > right)

Implements CVC3::ValidityChecker.

Definition at line 1369 of file vcl.cpp.

References CVC3::gtExpr().

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

Create (left >= right)

Implements CVC3::ValidityChecker.

Definition at line 1375 of file vcl.cpp.

References CVC3::geExpr().

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

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1381 of file vcl.cpp.

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

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1391 of file vcl.cpp.

References CVC3::sort2().

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

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

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1405 of file vcl.cpp.

References CVC3::sort2().

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

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

Parameters:
fields
exprsmust be the same length as fields

Fields will be sorted automatically

Implements CVC3::ValidityChecker.

Definition at line 1422 of file vcl.cpp.

References DebugAssert, and CVC3::sort2().

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

Create record.field (field selection)

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

Implements CVC3::ValidityChecker.

Definition at line 1435 of file vcl.cpp.

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

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

Notice the `.' before field in the presentation language (and the comment above); this is to distinguish it from datatype update.

Implements CVC3::ValidityChecker.

Definition at line 1441 of file vcl.cpp.

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

Create an expression array[index] (array access)

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

Implements CVC3::ValidityChecker.

Definition at line 1448 of file vcl.cpp.

References CVC3::READ.

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

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

Implements CVC3::ValidityChecker.

Definition at line 1454 of file vcl.cpp.

References CVC3::WRITE.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1460 of file vcl.cpp.

Expr VCL::newBVConstExpr ( const std::vector< bool > &  bits) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1466 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1472 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1478 of file vcl.cpp.

Expr VCL::newConcatExpr ( const std::vector< Expr > &  kids) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1484 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1490 of file vcl.cpp.

Expr VCL::newBVNegExpr ( const Expr t1) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1496 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1502 of file vcl.cpp.

Expr VCL::newBVAndExpr ( const std::vector< Expr > &  kids) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1508 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1514 of file vcl.cpp.

Expr VCL::newBVOrExpr ( const std::vector< Expr > &  kids) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1520 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1526 of file vcl.cpp.

Expr VCL::newBVXorExpr ( const std::vector< Expr > &  kids) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1532 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1538 of file vcl.cpp.

Expr VCL::newBVXnorExpr ( const std::vector< Expr > &  kids) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1544 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1550 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1556 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1562 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1568 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1574 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1580 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1586 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1592 of file vcl.cpp.

Expr VCL::newBVUminusExpr ( const Expr t1) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1598 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1604 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1610 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1615 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1624 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1629 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1634 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1639 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1644 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1649 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1655 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1661 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1667 of file vcl.cpp.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1673 of file vcl.cpp.

References CVC3::BVSHL.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1679 of file vcl.cpp.

References CVC3::BVLSHR.

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

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1685 of file vcl.cpp.

References CVC3::BVASHR.

Rational VCL::computeBVConst ( const Expr e) [virtual]

'numbits' is the number of bits in the result

Implements CVC3::ValidityChecker.

Definition at line 1691 of file vcl.cpp.

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

Tuple expression.

Implements CVC3::ValidityChecker.

Definition at line 1697 of file vcl.cpp.

References DebugAssert.

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

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

Implements CVC3::ValidityChecker.

Definition at line 1703 of file vcl.cpp.

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

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

Implements CVC3::ValidityChecker.

Definition at line 1709 of file vcl.cpp.

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

Datatype constructor expression.

Implements CVC3::ValidityChecker.

Definition at line 1715 of file vcl.cpp.

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

Datatype selector expression.

Implements CVC3::ValidityChecker.

Definition at line 1721 of file vcl.cpp.

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

Datatype tester expression.

Implements CVC3::ValidityChecker.

Definition at line 1727 of file vcl.cpp.

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

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

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

Implements CVC3::ValidityChecker.

Definition at line 1733 of file vcl.cpp.

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

Universal quantifier.

Implements CVC3::ValidityChecker.

Definition at line 1739 of file vcl.cpp.

References DebugAssert, and FORALL.

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

Universal quantifier with a trigger.

Implements CVC3::ValidityChecker.

Definition at line 1744 of file vcl.cpp.

References DebugAssert, and FORALL.

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

Universal quantifier with a set of triggers.

Implements CVC3::ValidityChecker.

Definition at line 1750 of file vcl.cpp.

References DebugAssert, and FORALL.

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

Universal quantifier with a set of multi-triggers.

Implements CVC3::ValidityChecker.

Definition at line 1756 of file vcl.cpp.

References DebugAssert, and FORALL.

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

Set triggers for quantifier instantiation.

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

Implements CVC3::ValidityChecker.

Definition at line 1762 of file vcl.cpp.

References CVC3::Expr::setTriggers().

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

Set triggers for quantifier instantiation (no multi-triggers)

Implements CVC3::ValidityChecker.

Definition at line 1766 of file vcl.cpp.

References CVC3::Expr::setTriggers().

void VCL::setTrigger ( const Expr e,
const Expr trigger 
) [virtual]

Set a single trigger for quantifier instantiation.

Implements CVC3::ValidityChecker.

Definition at line 1770 of file vcl.cpp.

References CVC3::Expr::setTrigger().

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

Set a single multi-trigger for quantifier instantiation.

Implements CVC3::ValidityChecker.

Definition at line 1774 of file vcl.cpp.

References CVC3::Expr::setMultiTrigger().

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

Existential quantifier.

Implements CVC3::ValidityChecker.

Definition at line 1778 of file vcl.cpp.

References EXISTS.

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

Lambda-expression.

Implements CVC3::ValidityChecker.

Definition at line 1783 of file vcl.cpp.

References LAMBDA.

Op VCL::transClosure ( const Op op) [virtual]

Transitive closure of a binary predicate.

Implements CVC3::ValidityChecker.

Definition at line 1787 of file vcl.cpp.

References CVC3::Op::getExpr(), CVC3::Expr::getName(), and CVC3::TRANS_CLOSURE.

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

Symbolic simulation expression.

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

Implements CVC3::ValidityChecker.

Definition at line 1793 of file vcl.cpp.

References SIMULATE.

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

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

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

Implements CVC3::ValidityChecker.

Definition at line 1804 of file vcl.cpp.

void VCL::setTimeLimit ( unsigned  limit) [virtual]

Set a time limit in tenth of a second,.

counting the cpu time used by the current process from now on. Currently, when the limit is reached, cvc3 tries to quickly terminate, probably with the status unknown.

Implements CVC3::ValidityChecker.

Definition at line 2418 of file vcl.cpp.

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

Assert a new formula in the current context.

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

Implements CVC3::ValidityChecker.

Definition at line 1848 of file vcl.cpp.

References ASSERT, CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Type::toString(), TRACE, and TRACE_MSG.

void VCL::registerAtom ( const Expr e) [virtual]

Register an atomic formula of interest.

Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function

Implements CVC3::ValidityChecker.

Definition at line 1892 of file vcl.cpp.

Expr VCL::getImpliedLiteral ( ) [virtual]

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

Returned literals are either registered atomic formulas or their negation

Implements CVC3::ValidityChecker.

Definition at line 1899 of file vcl.cpp.

References CVC3::Theorem::getExpr(), and CVC3::Theorem::isNull().

Expr VCL::simplify ( const Expr e) [virtual]

Simplify e with respect to the current context.

Implements CVC3::ValidityChecker.

Definition at line 1908 of file vcl.cpp.

Theorem VCL::simplifyThm ( const Expr e)

Definition at line 1914 of file vcl.cpp.

References CVC3::Theorem::getRHS(), and CVC3::Expr::getType().

QueryResult VCL::query ( const Expr e) [virtual]

Check validity of e in the current context.

If it returns VALID, the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible.

Parameters:
eis the queried formula

Implements CVC3::ValidityChecker.

Definition at line 1924 of file vcl.cpp.

References CVC3::ABORT, AND, CVC3::Expr::getType(), CVC3::Expr::impExpr(), CVC3::INVALID, CVC3::Type::isBool(), QUERY, CVC3::Type::toString(), TRACE, UNKNOWN, and CVC3::VALID.

QueryResult VCL::checkUnsat ( const Expr e) [virtual]

Check satisfiability of the expr in the current context.

Equivalent to query(!e)

Implements CVC3::ValidityChecker.

Definition at line 1993 of file vcl.cpp.

References CVC3::Expr::negate().

QueryResult VCL::checkContinue ( ) [virtual]

Get the next model.

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

Implements CVC3::ValidityChecker.

Definition at line 1999 of file vcl.cpp.

References CVC3::andExpr(), and CONTINUE.

QueryResult VCL::restart ( const Expr e) [virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 2015 of file vcl.cpp.

References RESTART.

void VCL::returnFromCheck ( ) [virtual]

Returns to context immediately before last invalid query.

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

Implements CVC3::ValidityChecker.

Definition at line 2025 of file vcl.cpp.

void VCL::getUserAssumptions ( std::vector< Expr > &  assumptions) [virtual]

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

User assumptions are created either by calls to assertFormula or by a call to query. In the latter case, the negated query is added as an assumption.

Parameters:
assumptionsshould be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2032 of file vcl.cpp.

void VCL::getInternalAssumptions ( std::vector< Expr > &  assumptions) [virtual]

Get assumptions made internally in this and all previous contexts.

Internal assumptions are literals assumed by the sat solver.

Parameters:
assumptionsshould be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2039 of file vcl.cpp.

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

Get all assumptions made in this and all previous contexts.

Parameters:
assumptionsshould be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2046 of file vcl.cpp.

References ASSUMPTIONS.

void VCL::getAssumptionsUsed ( std::vector< Expr > &  assumptions) [virtual]

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

It returns a subset of getAssumptions(). If the last query was false or there has not yet been a query, it does nothing. NOTE: this functionality is not supported yet

Parameters:
assumptionsshould be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2070 of file vcl.cpp.

References DUMP_ASSUMPTIONS, CVC3::Theorem::getLeafAssumptions(), and CVC3::Theorem::isNull().

Expr VCL::getProofQuery ( ) [virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 2056 of file vcl.cpp.

void VCL::getCounterExample ( std::vector< Expr > &  assumptions,
bool  inOrder 
) [virtual]

Return the internal assumptions that make the queried formula false.

This method should only be called after a query which returns false. It will try to return the simplest possible subset of the internal assumptions sufficient to make the queried expression false.

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

Implements CVC3::ValidityChecker.

Definition at line 2082 of file vcl.cpp.

References COUNTEREXAMPLE.

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

Will assign concrete values to all user created variables.

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

Implements CVC3::ValidityChecker.

Definition at line 2092 of file vcl.cpp.

References COUNTERMODEL.

QueryResult VCL::tryModelGeneration ( ) [virtual]

If the result of the last query was UNKNOWN try to actually build the model to verify the result.

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

Implements CVC3::ValidityChecker.

Definition at line 2101 of file vcl.cpp.

References CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::INVALID, CVC3::Expr::isFalse(), CVC3::orExpr(), and UNKNOWN.

FormulaValue VCL::value ( const Expr e) [virtual]

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

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

Implements CVC3::ValidityChecker.

Definition at line 2135 of file vcl.cpp.

References DebugAssert, and CVC3::Expr::isTerm().

bool VCL::inconsistent ( std::vector< Expr > &  assumptions) [virtual]

Returns true if the current context is inconsistent.

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

Parameters:
assumptionsshould be empty on entry.

Implements CVC3::ValidityChecker.

Definition at line 2140 of file vcl.cpp.

bool VCL::inconsistent ( ) [virtual]

Returns true if the current context is inconsistent.

Implements CVC3::ValidityChecker.

Definition at line 2152 of file vcl.cpp.

bool VCL::incomplete ( ) [virtual]

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

Some decision procedures in CVC are incomplete (quantifier elimination, non-linear arithmetic, etc.). If any incomplete features were used during the last query(), and the result is "invalid" (query() returns false), then this result is inconclusive. It means that the system gave up the search for contradiction at some point.

Implements CVC3::ValidityChecker.

Definition at line 2158 of file vcl.cpp.

bool VCL::incomplete ( std::vector< std::string > &  reasons) [virtual]

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

See also:
incomplete()

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

Implements CVC3::ValidityChecker.

Definition at line 2165 of file vcl.cpp.

Proof VCL::getProof ( ) [virtual]

Returns the proof term for the last proven query.

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

Implements CVC3::ValidityChecker.

Definition at line 2172 of file vcl.cpp.

References DUMP_PROOF.

Expr VCL::getTCC ( ) [virtual]

Returns the TCC of the last assumption or query.

Returns Null if no assumptions or queries were performed.

Implements CVC3::ValidityChecker.

Definition at line 2186 of file vcl.cpp.

References DUMP_TCC.

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

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

Implements CVC3::ValidityChecker.

Definition at line 2196 of file vcl.cpp.

References DUMP_TCC_ASSUMPTIONS.

Proof VCL::getProofTCC ( ) [virtual]

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

Returns Null if no assumptions or queries were performed.

Implements CVC3::ValidityChecker.

Definition at line 2209 of file vcl.cpp.

References DUMP_TCC_PROOF.

Expr VCL::getClosure ( ) [virtual]

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

Turn a valid query Gamma |- phi into an implication |- Gamma => phi.

Returns Null if last query was invalid.

Implements CVC3::ValidityChecker.

Definition at line 2219 of file vcl.cpp.

References DUMP_CLOSURE.

Proof VCL::getProofClosure ( ) [virtual]

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

Returns Null if last query was Invalid.

Implements CVC3::ValidityChecker.

Definition at line 2233 of file vcl.cpp.

References DUMP_CLOSURE_PROOF.

int VCL::stackLevel ( ) [virtual]

Returns the current stack level. Initial level is 0.

Implements CVC3::ValidityChecker.

Definition at line 2247 of file vcl.cpp.

void VCL::push ( ) [virtual]

Checkpoint the current context and increase the scope level.

Implements CVC3::ValidityChecker.

Definition at line 2253 of file vcl.cpp.

References CVC3::ExprStream::push, and PUSH.

void VCL::pop ( ) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2263 of file vcl.cpp.

References POP.

void VCL::popto ( int  stackLevel) [virtual]

Restore the current context to the given stackLevel.

Parameters:
stackLevelshould be greater than or equal to 0 and less than or equal to the current scope level.

Implements CVC3::ValidityChecker.

Definition at line 2278 of file vcl.cpp.

References POPTO.

int VCL::scopeLevel ( ) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2291 of file vcl.cpp.

void VCL::pushScope ( ) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2297 of file vcl.cpp.

References IF_DEBUG, and PUSH_SCOPE.

void VCL::popScope ( ) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2309 of file vcl.cpp.

References std::endl(), IF_DEBUG, CVC3::ExprStream::pop, and POP_SCOPE.

void VCL::poptoScope ( int  scopeLevel) [virtual]

Restore the current context to the given scopeLevel.

Parameters:
scopeLevelshould be less than or equal to the current scope level.

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

Implements CVC3::ValidityChecker.

Definition at line 2324 of file vcl.cpp.

References IF_DEBUG, and POPTO_SCOPE.

Context * VCL::getCurrentContext ( ) [virtual]

Get the current context.

Implements CVC3::ValidityChecker.

Definition at line 2340 of file vcl.cpp.

void VCL::reset ( ) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2346 of file vcl.cpp.

void VCL::logAnnotation ( const Expr annot) [virtual]

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

Implements CVC3::ValidityChecker.

Definition at line 2352 of file vcl.cpp.

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

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

Implements CVC3::ValidityChecker.

Definition at line 2359 of file vcl.cpp.

References CVC3::VCCmd::processCommands().

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

Read and execute the commands from a stream.

Implements CVC3::ValidityChecker.

Definition at line 2368 of file vcl.cpp.

References CVC3::VCCmd::processCommands().

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

Get statistics object.

Implements CVC3::ValidityChecker.

Definition at line 412 of file vcl.h.

void CVC3::VCL::printStatistics ( ) [inline, virtual]

Print collected statistics to stdout.

Implements CVC3::ValidityChecker.

Definition at line 413 of file vcl.h.

unsigned long VCL::getMemory ( int  verbosity = 0)

Definition at line 2381 of file vcl.cpp.


Member Data Documentation

Pointers to main system components.

Definition at line 53 of file vcl.h.

Definition at line 54 of file vcl.h.

Definition at line 55 of file vcl.h.

Definition at line 56 of file vcl.h.

Pointers to theories.

Definition at line 59 of file vcl.h.

Definition at line 60 of file vcl.h.

Definition at line 61 of file vcl.h.

Definition at line 62 of file vcl.h.

Definition at line 63 of file vcl.h.

Definition at line 64 of file vcl.h.

Definition at line 65 of file vcl.h.

Definition at line 66 of file vcl.h.

Definition at line 67 of file vcl.h.

Definition at line 68 of file vcl.h.

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

All theories are stored in this common vector.

This includes TheoryCore and TheoryArith.

Definition at line 72 of file vcl.h.

Command line flags.

Definition at line 75 of file vcl.h.

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

User-level view of the scope stack.

Definition at line 78 of file vcl.h.

Run-time statistics.

Definition at line 81 of file vcl.h.

size_t CVC3::VCL::d_nextIdx [private]

Next index for user assertion.

Definition at line 84 of file vcl.h.

Backtracking map of user assertions.

Definition at line 110 of file vcl.h.

Backtracking map of assertions when assertion batching is on.

Definition at line 113 of file vcl.h.

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

Index into batched Assertions.

Definition at line 116 of file vcl.h.

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 121 of file vcl.h.

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

Definition at line 124 of file vcl.h.

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

Definition at line 127 of file vcl.h.

bool CVC3::VCL::d_dump [private]

Whether to dump a trace (or a translated version)

Definition at line 130 of file vcl.h.


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