CVC3
2.4.1
|
#include <vcl.h>
Classes | |
class | UserAssertion |
Structure to hold user assertions indexed by declaration order. More... |
Public Member Functions | |
VCL (const CLFlags &flags) | |
~VCL () | |
CLFlags & | getFlags () const |
Return the set of command-line flags. | |
void | reprocessFlags () |
Force reprocessing of all flags. | |
TheoryCore * | core () |
Type | boolType () |
Create type BOOLEAN. | |
Type | realType () |
Create type REAL. | |
Type | intType () |
Create type INT. | |
Type | subrangeType (const Expr &l, const Expr &r) |
Create a subrange type [l..r]. | |
Type | subtypeType (const Expr &pred, const Expr &witness) |
Creates a subtype defined by the given predicate. | |
Type | tupleType (const Type &type0, const Type &type1) |
2-element tuple | |
Type | tupleType (const Type &type0, const Type &type1, const Type &type2) |
3-element tuple | |
Type | tupleType (const std::vector< Type > &types) |
n-element tuple (from a vector of types) | |
Type | recordType (const std::string &field, const Type &type) |
1-element record | |
Type | recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1) |
2-element record | |
Type | recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2) |
3-element record | |
Type | recordType (const std::vector< std::string > &fields, const std::vector< Type > &types) |
n-element record (fields and types must be of the same length) | |
Type | dataType (const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types) |
Single datatype, single constructor. | |
Type | dataType (const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types) |
Single datatype, multiple constructors. | |
void | dataType (const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes) |
Multiple datatypes. | |
Type | arrayType (const Type &typeIndex, const Type &typeData) |
Create an array type (ARRAY typeIndex OF typeData) | |
Type | bitvecType (int n) |
Create a bitvector type of length n. | |
Type | funType (const Type &typeDom, const Type &typeRan) |
Create a function type typeDom -> typeRan. | |
Type | funType (const std::vector< Type > &typeDom, const Type &typeRan) |
Create a function type (t1,t2,...,tn) -> typeRan. | |
Type | createType (const std::string &typeName) |
Create named user-defined uninterpreted type. | |
Type | createType (const std::string &typeName, const Type &def) |
Create named user-defined interpreted type (type abbreviation) | |
Type | lookupType (const std::string &typeName) |
Lookup a user-defined (uninterpreted) type by name. Returns Null if none. | |
ExprManager * | getEM () |
Return the ExprManager. | |
Expr | varExpr (const std::string &name, const Type &type) |
Create a variable with a given name and type. | |
Expr | varExpr (const std::string &name, const Type &type, const Expr &def) |
Create a variable with a given name, type, and value. | |
Expr | lookupVar (const std::string &name, Type *type) |
Get the variable associated with a name, and its type. | |
Type | getType (const Expr &e) |
Get the type of the Expr. | |
Type | getBaseType (const Expr &e) |
Get the largest supertype of the Expr. | |
Type | getBaseType (const Type &e) |
Get the largest supertype of the Type. | |
Expr | getTypePred (const Type &t, const Expr &e) |
Get the subtype predicate. | |
Expr | stringExpr (const std::string &str) |
Create a string Expr. | |
Expr | idExpr (const std::string &name) |
Create an ID Expr. | |
Expr | listExpr (const std::vector< Expr > &kids) |
Create a list Expr. | |
Expr | listExpr (const Expr &e1) |
Overloaded version of listExpr with one argument. | |
Expr | listExpr (const Expr &e1, const Expr &e2) |
Overloaded version of listExpr with two arguments. | |
Expr | listExpr (const Expr &e1, const Expr &e2, const Expr &e3) |
Overloaded version of listExpr with three arguments. | |
Expr | listExpr (const std::string &op, const std::vector< Expr > &kids) |
Overloaded version of listExpr with string operator and many arguments. | |
Expr | listExpr (const std::string &op, const Expr &e1) |
Overloaded version of listExpr with string operator and one argument. | |
Expr | listExpr (const std::string &op, const Expr &e1, const Expr &e2) |
Overloaded version of listExpr with string operator and two arguments. | |
Expr | listExpr (const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3) |
Overloaded version of listExpr with string operator and three arguments. | |
void | printExpr (const Expr &e) |
Prints e to the standard output. | |
void | printExpr (const Expr &e, std::ostream &os) |
Prints e to the given ostream. | |
Expr | parseExpr (const Expr &e) |
Parse an expression using a Theory-specific parser. | |
Type | parseType (const Expr &e) |
Parse a type expression using a Theory-specific parser. | |
Expr | importExpr (const Expr &e) |
Import the Expr from another instance of ValidityChecker. | |
Type | importType (const Type &t) |
Import the Type from another instance of ValidityChecker. | |
void | cmdsFromString (const std::string &s, InputLanguage lang) |
Parse a sequence of commands from a presentation language string. | |
Expr | exprFromString (const std::string &s) |
Parse an expression from a presentation language string. | |
Expr | trueExpr () |
Return TRUE Expr. | |
Expr | falseExpr () |
Return FALSE Expr. | |
Expr | notExpr (const Expr &child) |
Create negation. | |
Expr | andExpr (const Expr &left, const Expr &right) |
Create 2-element conjunction. | |
Expr | andExpr (const std::vector< Expr > &children) |
Create n-element conjunction. | |
Expr | orExpr (const Expr &left, const Expr &right) |
Create 2-element disjunction. | |
Expr | orExpr (const std::vector< Expr > &children) |
Create n-element disjunction. | |
Expr | impliesExpr (const Expr &hyp, const Expr &conc) |
Create Boolean implication. | |
Expr | iffExpr (const Expr &left, const Expr &right) |
Create left IFF right (boolean equivalence) | |
Expr | eqExpr (const Expr &child0, const Expr &child1) |
Create an equality expression. | |
Expr | distinctExpr (const std::vector< Expr > &children) |
Expr | iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart) |
Create IF ifpart THEN thenpart ELSE elsepart ENDIF. | |
Op | createOp (const std::string &name, const Type &type) |
Create a named uninterpreted function with a given type. | |
Op | createOp (const std::string &name, const Type &type, const Expr &def) |
Create a named user-defined function with a given type. | |
Op | lookupOp (const std::string &name, Type *type) |
Get the Op associated with a name, and its type. | |
Expr | funExpr (const Op &op, const Expr &child) |
Unary function application (op must be of function type) | |
Expr | funExpr (const Op &op, const Expr &left, const Expr &right) |
Binary function application (op must be of function type) | |
Expr | funExpr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) |
Ternary function application (op must be of function type) | |
Expr | funExpr (const Op &op, const std::vector< Expr > &children) |
n-ary function application (op must be of function type) | |
bool | addPairToArithOrder (const Expr &smaller, const Expr &bigger) |
Expr | ratExpr (int n, int d) |
Create a rational number with numerator n and denominator d. | |
Expr | ratExpr (const std::string &n, const std::string &d, int base) |
Create a rational number with numerator n and denominator d. | |
Expr | ratExpr (const std::string &n, int base) |
Create a rational from a single string. | |
Expr | uminusExpr (const Expr &child) |
Unary minus. | |
Expr | plusExpr (const Expr &left, const Expr &right) |
Create 2-element sum (left + right) | |
Expr | plusExpr (const std::vector< Expr > &children) |
Create n-element sum. | |
Expr | minusExpr (const Expr &left, const Expr &right) |
Make a difference (left - right) | |
Expr | multExpr (const Expr &left, const Expr &right) |
Create a product (left * right) | |
Expr | powExpr (const Expr &x, const Expr &n) |
Create a power expression (x ^ n); n must be integer. | |
Expr | divideExpr (const Expr &left, const Expr &right) |
Create expression x / y. | |
Expr | ltExpr (const Expr &left, const Expr &right) |
Create (left < right) | |
Expr | leExpr (const Expr &left, const Expr &right) |
Create (left <= right) | |
Expr | gtExpr (const Expr &left, const Expr &right) |
Create (left > right) | |
Expr | geExpr (const Expr &left, const Expr &right) |
Create (left >= right) | |
Expr | recordExpr (const std::string &field, const Expr &expr) |
Create a 1-element record value (# field := expr #) | |
Expr | recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1) |
Create a 2-element record value (# field0 := expr0, field1 := expr1 #) | |
Expr | recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2) |
Create a 3-element record value (# field_i := expr_i #) | |
Expr | recordExpr (const std::vector< std::string > &fields, const std::vector< Expr > &exprs) |
Create an n-element record value (# field_i := expr_i #) | |
Expr | recSelectExpr (const Expr &record, const std::string &field) |
Create record.field (field selection) | |
Expr | recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue) |
Record update; equivalent to "record WITH .field := newValue". | |
Expr | readExpr (const Expr &array, const Expr &index) |
Create an expression array[index] (array access) | |
Expr | writeExpr (const Expr &array, const Expr &index, const Expr &newValue) |
Array update; equivalent to "array WITH index := newValue". | |
Expr | newBVConstExpr (const std::string &s, int base) |
'numbits' is the number of bits in the result | |
Expr | newBVConstExpr (const std::vector< bool > &bits) |
'numbits' is the number of bits in the result | |
Expr | newBVConstExpr (const Rational &r, int len) |
'numbits' is the number of bits in the result | |
Expr | newConcatExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newConcatExpr (const std::vector< Expr > &kids) |
'numbits' is the number of bits in the result | |
Expr | newBVExtractExpr (const Expr &e, int hi, int low) |
'numbits' is the number of bits in the result | |
Expr | newBVNegExpr (const Expr &t1) |
'numbits' is the number of bits in the result | |
Expr | newBVAndExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVAndExpr (const std::vector< Expr > &kids) |
'numbits' is the number of bits in the result | |
Expr | newBVOrExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVOrExpr (const std::vector< Expr > &kids) |
'numbits' is the number of bits in the result | |
Expr | newBVXorExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVXorExpr (const std::vector< Expr > &kids) |
'numbits' is the number of bits in the result | |
Expr | newBVXnorExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVXnorExpr (const std::vector< Expr > &kids) |
'numbits' is the number of bits in the result | |
Expr | newBVNandExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVNorExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVCompExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVLTExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVLEExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVSLTExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVSLEExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newSXExpr (const Expr &t1, int len) |
'numbits' is the number of bits in the result | |
Expr | newBVUminusExpr (const Expr &t1) |
'numbits' is the number of bits in the result | |
Expr | newBVSubExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVPlusExpr (int numbits, const std::vector< Expr > &k) |
'numbits' is the number of bits in the result | |
Expr | newBVPlusExpr (int numbits, const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVMultExpr (int numbits, const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVUDivExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVURemExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVSDivExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVSRemExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVSModExpr (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newFixedLeftShiftExpr (const Expr &t1, int r) |
'numbits' is the number of bits in the result | |
Expr | newFixedConstWidthLeftShiftExpr (const Expr &t1, int r) |
'numbits' is the number of bits in the result | |
Expr | newFixedRightShiftExpr (const Expr &t1, int r) |
'numbits' is the number of bits in the result | |
Expr | newBVSHL (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVLSHR (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Expr | newBVASHR (const Expr &t1, const Expr &t2) |
'numbits' is the number of bits in the result | |
Rational | computeBVConst (const Expr &e) |
'numbits' is the number of bits in the result | |
Expr | tupleExpr (const std::vector< Expr > &exprs) |
Tuple expression. | |
Expr | tupleSelectExpr (const Expr &tuple, int index) |
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) | |
Expr | tupleUpdateExpr (const Expr &tuple, int index, const Expr &newValue) |
Tuple update; equivalent to "tuple WITH index := newValue". | |
Expr | datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args) |
Datatype constructor expression. | |
Expr | datatypeSelExpr (const std::string &selector, const Expr &arg) |
Datatype selector expression. | |
Expr | datatypeTestExpr (const std::string &constructor, const Expr &arg) |
Datatype tester expression. | |
Expr | boundVarExpr (const std::string &name, const std::string &uid, const Type &type) |
Create a bound variable with a given name, unique ID (uid) and type. | |
Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body) |
Universal quantifier. | |
Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const Expr &trigger) |
Universal quantifier with a trigger. | |
Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) |
Universal quantifier with a set of triggers. | |
Expr | forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) |
Universal quantifier with a set of multi-triggers. | |
void | setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers) |
Set triggers for quantifier instantiation. | |
void | setTriggers (const Expr &e, const std::vector< Expr > &triggers) |
Set triggers for quantifier instantiation (no multi-triggers) | |
void | setTrigger (const Expr &e, const Expr &trigger) |
Set a single trigger for quantifier instantiation. | |
void | setMultiTrigger (const Expr &e, const std::vector< Expr > &multiTrigger) |
Set a single multi-trigger for quantifier instantiation. | |
Expr | existsExpr (const std::vector< Expr > &vars, const Expr &body) |
Existential quantifier. | |
Op | lambdaExpr (const std::vector< Expr > &vars, const Expr &body) |
Lambda-expression. | |
Op | transClosure (const Op &op) |
Transitive closure of a binary predicate. | |
Expr | simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n) |
Symbolic simulation expression. | |
void | setResourceLimit (unsigned limit) |
Set the resource limit (0==unlimited, 1==exhausted). | |
void | setTimeLimit (unsigned limit) |
Set a time limit in tenth of a second,. | |
void | assertFormula (const Expr &e) |
Assert a new formula in the current context. | |
void | registerAtom (const Expr &e) |
Register an atomic formula of interest. | |
Expr | getImpliedLiteral () |
Return next literal implied by last assertion. Null Expr if none. | |
Expr | simplify (const Expr &e) |
Simplify e with respect to the current context. | |
Theorem | simplifyThm (const Expr &e) |
QueryResult | query (const Expr &e) |
Check validity of e in the current context. | |
QueryResult | checkUnsat (const Expr &e) |
Check satisfiability of the expr in the current context. | |
QueryResult | checkContinue () |
Get the next model. | |
QueryResult | restart (const Expr &e) |
Restart the most recent query with e as an additional assertion. | |
void | returnFromCheck () |
Returns to context immediately before last invalid query. | |
void | getUserAssumptions (std::vector< Expr > &assumptions) |
Get assumptions made by the user in this and all previous contexts. | |
void | getInternalAssumptions (std::vector< Expr > &assumptions) |
Get assumptions made internally in this and all previous contexts. | |
void | getAssumptions (std::vector< Expr > &assumptions) |
Get all assumptions made in this and all previous contexts. | |
void | getAssumptionsUsed (std::vector< Expr > &assumptions) |
Returns the set of assumptions used in the proof of queried formula. | |
Expr | getProofQuery () |
Set the resource limit (0==unlimited, 1==exhausted). | |
void | getCounterExample (std::vector< Expr > &assumptions, bool inOrder) |
Return the internal assumptions that make the queried formula false. | |
void | getConcreteModel (ExprMap< Expr > &m) |
Will assign concrete values to all user created variables. | |
QueryResult | tryModelGeneration () |
FormulaValue | value (const Expr &e) |
Set the resource limit (0==unlimited, 1==exhausted). | |
bool | inconsistent (std::vector< Expr > &assumptions) |
Returns true if the current context is inconsistent. | |
bool | inconsistent () |
Returns true if the current context is inconsistent. | |
bool | incomplete () |
Returns true if the invalid result from last query() is imprecise. | |
bool | incomplete (std::vector< std::string > &reasons) |
Returns true if the invalid result from last query() is imprecise. | |
Proof | getProof () |
Returns the proof term for the last proven query. | |
Expr | getAssignment () |
Returns the list of pairs (name value) for each :named attribute. | |
Expr | getValue (Expr e) |
Evaluate an expression and return a concrete value in the model. | |
Expr | getTCC () |
Returns the TCC of the last assumption or query. | |
void | getAssumptionsTCC (std::vector< Expr > &assumptions) |
Return the set of assumptions used in the proof of the last TCC. | |
Proof | getProofTCC () |
Returns the proof of TCC of the last assumption or query. | |
Expr | getClosure () |
After successful query, return its closure |- Gamma => phi. | |
Proof | getProofClosure () |
Construct a proof of the query closure |- Gamma => phi. | |
int | stackLevel () |
Returns the current stack level. Initial level is 0. | |
void | push () |
Checkpoint the current context and increase the scope level. | |
void | pop () |
Restore the current context to its state at the last checkpoint. | |
void | popto (int stackLevel) |
Restore the current context to the given stackLevel. | |
int | scopeLevel () |
Returns the current scope level. Initially, the scope level is 1. | |
void | pushScope () |
Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing! | |
void | popScope () |
Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing! | |
void | poptoScope (int scopeLevel) |
Restore the current context to the given scopeLevel. | |
Context * | getCurrentContext () |
Get the current context. | |
void | reset () |
Destroy and recreate validity checker: resets everything except for flags. | |
void | logAnnotation (const Expr &annot) |
Add an annotation to the current script - prints annot when translating. | |
void | loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false) |
Read and execute the commands from a file given by name ("" means stdin) | |
void | loadFile (std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) |
Read and execute the commands from a stream. | |
Statistics & | getStatistics () |
Get statistics object. | |
void | printStatistics () |
Print collected statistics to stdout. | |
unsigned long | getMemory (int verbosity=0) |
![]() | |
ValidityChecker () | |
Constructor. | |
virtual | ~ValidityChecker () |
Destructor. |
Private Member Functions | |
Theorem3 | deriveClosure (const Theorem3 &thm) |
Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi". | |
void | getAssumptionsRec (const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs) |
Recursive assumption graph traversal to find user assumptions. | |
void | getAssumptions (const Assumptions &a, std::vector< Expr > &assumptions) |
Get set of user assertions from the set of assumptions. | |
Theorem | checkTCC (const Expr &tcc) |
Check the tcc. | |
void | init (void) |
Initialize everything except flags. | |
void | destroy (void) |
Destroy everything except flags. |
Private Attributes | |
ExprManager * | d_em |
Pointers to main system components. | |
ContextManager * | d_cm |
TheoremManager * | d_tm |
SearchEngine * | d_se |
TheoryCore * | d_theoryCore |
Pointers to theories. | |
TheoryUF * | d_theoryUF |
TheoryArith * | d_theoryArith |
TheoryArray * | d_theoryArray |
TheoryQuant * | d_theoryQuant |
TheoryRecords * | d_theoryRecords |
TheorySimulate * | d_theorySimulate |
TheoryBitvector * | d_theoryBitvector |
TheoryDatatype * | d_theoryDatatype |
Translator * | d_translator |
std::vector< Theory * > | d_theories |
All theories are stored in this common vector. | |
CLFlags * | d_flags |
Command line flags. | |
CDO< int > * | d_stackLevel |
User-level view of the scope stack. | |
bool | d_modelStackPushed |
True iff we've pushed the stack artificially to avoid polluting context. | |
Statistics * | d_statistics |
Run-time statistics. | |
size_t | d_nextIdx |
Next index for user assertion. | |
CDMap< Expr, UserAssertion > * | d_userAssertions |
Backtracking map of user assertions. | |
CDList< Expr > * | d_batchedAssertions |
Backtracking map of assertions when assertion batching is on. | |
CDO< unsigned > * | d_batchedAssertionsIdx |
Index into batched Assertions. | |
Theorem3 | d_lastQuery |
Result of the last query() | |
Theorem | d_lastQueryTCC |
Result of the last query(e, true) (for a TCC). | |
Theorem3 | d_lastClosure |
Closure of the last query(e): |- Gamma => e. | |
bool | d_dump |
Whether to dump a trace (or a translated version) |
Additional Inherited Members | |
![]() | |
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. |
CVC3::VCL::VCL | ( | const CLFlags & | flags | ) |
Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi".
Definition at line 311 of file vcl.cpp.
References CVC3::Theorem::clearAllFlags(), CVC3::Theorem3::getAssumptionsRef(), CVC3::TheoremValue::getExpr(), and CVC3::Theorem::thm().
|
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 354 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().
|
private |
Get set of user assertions from the set of assumptions.
Definition at line 381 of file vcl.cpp.
References CVC3::Assumptions::begin(), CVC3::Theorem::clearAllFlags(), CVC3::Assumptions::empty(), CVC3::Assumptions::end(), CVC3::TheoremValue::getExpr(), and CVC3::Theorem::thm().
Check the tcc.
Definition at line 1810 of file vcl.cpp.
References CVC3::ABORT, FatalAssert, CVC3::INVALID, CVC3::Expr::toString(), UNKNOWN, and CVC3::VALID.
|
private |
|
private |
|
inlinevirtual |
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.
|
virtual |
Force reprocessing of all flags.
Implements CVC3::ValidityChecker.
Definition at line 623 of file vcl.cpp.
References DebugAssert.
TheoryCore * VCL::core | ( | ) |
|
virtual |
|
virtual |
|
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.
Creates a subtype defined by the given predicate.
pred | is a predicate taking one argument of type T and returning Boolean. The resulting type is a subtype of T whose elements x are those satisfying the predicate pred(x). |
witness | is an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove ![]() |
Implements CVC3::ValidityChecker.
n-element tuple (from a vector of types)
Implements CVC3::ValidityChecker.
|
virtual |
2-element record
Fields will be sorted automatically
Implements CVC3::ValidityChecker.
Definition at line 762 of file vcl.cpp.
References CVC3::sort2().
|
virtual |
3-element record
Fields will be sorted automatically
Implements CVC3::ValidityChecker.
Definition at line 775 of file vcl.cpp.
References CVC3::sort2().
|
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().
|
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.
|
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.
|
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().
Create an array type (ARRAY typeIndex OF typeData)
Implements CVC3::ValidityChecker.
Definition at line 852 of file vcl.cpp.
References CVC3::arrayType().
|
virtual |
Create a bitvector type of length n.
Implements CVC3::ValidityChecker.
Create a function type typeDom -> typeRan.
Implements CVC3::ValidityChecker.
Definition at line 864 of file vcl.cpp.
References CVC3::Type::funType().
Create a function type (t1,t2,...,tn) -> typeRan.
Implements CVC3::ValidityChecker.
Definition at line 870 of file vcl.cpp.
References DebugAssert.
|
virtual |
Create named user-defined uninterpreted type.
Implements CVC3::ValidityChecker.
Definition at line 876 of file vcl.cpp.
References TYPE.
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.
|
virtual |
Lookup a user-defined (uninterpreted) type by name. Returns Null if none.
Implements CVC3::ValidityChecker.
|
inlinevirtual |
Create a variable with a given name and type.
name | is the name of the variable |
type | is its type. The type cannot be a function type. |
Implements CVC3::ValidityChecker.
Definition at line 900 of file vcl.cpp.
References CONST, and CVC3::Type::getExpr().
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.
Get the variable associated with a name, and its type.
name | is the variable name |
type | is where the type value is returned |
Implements CVC3::ValidityChecker.
Get the type of the Expr.
Implements CVC3::ValidityChecker.
Definition at line 961 of file vcl.cpp.
References CVC3::Expr::getType().
Get the largest supertype of the Expr.
Implements CVC3::ValidityChecker.
Get the largest supertype of the Type.
Implements CVC3::ValidityChecker.
Get the subtype predicate.
Implements CVC3::ValidityChecker.
|
virtual |
|
virtual |
Create an ID Expr.
Implements CVC3::ValidityChecker.
Definition at line 990 of file vcl.cpp.
References ID.
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.
Overloaded version of listExpr with one argument.
Implements CVC3::ValidityChecker.
Definition at line 1000 of file vcl.cpp.
References RAW_LIST.
Overloaded version of listExpr with two arguments.
Implements CVC3::ValidityChecker.
Definition at line 1005 of file vcl.cpp.
References RAW_LIST.
Overloaded version of listExpr with three arguments.
Implements CVC3::ValidityChecker.
Definition at line 1010 of file vcl.cpp.
References RAW_LIST.
Overloaded version of listExpr with string operator and many arguments.
Implements CVC3::ValidityChecker.
Overloaded version of listExpr with string operator and one argument.
Implements CVC3::ValidityChecker.
Definition at line 1023 of file vcl.cpp.
References RAW_LIST.
Overloaded version of listExpr with string operator and two arguments.
Implements CVC3::ValidityChecker.
Definition at line 1028 of file vcl.cpp.
References RAW_LIST.
|
virtual |
Overloaded version of listExpr with string operator and three arguments.
Implements CVC3::ValidityChecker.
|
virtual |
Prints e to the standard output.
Implements CVC3::ValidityChecker.
|
virtual |
Prints e to the given ostream.
Implements CVC3::ValidityChecker.
Definition at line 1050 of file vcl.cpp.
References std::endl().
Parse an expression using a Theory-specific parser.
Implements CVC3::ValidityChecker.
Parse a type expression using a Theory-specific parser.
Implements CVC3::ValidityChecker.
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().
Import the Type from another instance of ValidityChecker.
Implements CVC3::ValidityChecker.
Definition at line 1071 of file vcl.cpp.
References CVC3::Type::getExpr().
|
virtual |
Parse a sequence of commands from a presentation language string.
Implements CVC3::ValidityChecker.
|
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.
|
virtual |
|
virtual |
Create 2-element conjunction.
Implements CVC3::ValidityChecker.
Definition at line 1113 of file vcl.cpp.
References MiniSat::right().
Create n-element conjunction.
Implements CVC3::ValidityChecker.
Definition at line 1119 of file vcl.cpp.
References AND.
Create 2-element disjunction.
Implements CVC3::ValidityChecker.
Definition at line 1127 of file vcl.cpp.
References MiniSat::right().
Create n-element disjunction.
Implements CVC3::ValidityChecker.
Definition at line 1133 of file vcl.cpp.
References OR.
Create Boolean implication.
Implements CVC3::ValidityChecker.
Definition at line 1141 of file vcl.cpp.
References CVC3::Expr::impExpr().
Create left IFF right (boolean equivalence)
Implements CVC3::ValidityChecker.
Definition at line 1147 of file vcl.cpp.
References CVC3::Expr::iffExpr().
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().
Create an expression asserting that all the children are different.
children | the children to be asserted different |
Implements CVC3::ValidityChecker.
Definition at line 1158 of file vcl.cpp.
References DISTINCT.
Create IF ifpart THEN thenpart ELSE elsepart ENDIF.
ifpart | must be of type Boolean. |
thenpart | and |
elsepart | must have the same type, which will also be the type of the ite expression. |
Implements CVC3::ValidityChecker.
Definition at line 1163 of file vcl.cpp.
References CVC3::Expr::iteExpr().
Create a named uninterpreted function with a given type.
name | is the new function's name (as ID Expr) |
type | is 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().
Create a named user-defined function with a given type.
Implements CVC3::ValidityChecker.
Definition at line 1181 of file vcl.cpp.
References CVC3::Expr::andExpr(), CVC3::Type::arity(), CONST, CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isFunction(), CVC3::Expr::mkOp(), CVC3::Type::toString(), and CVC3::Expr::toString().
Unary function application (op must be of function type)
Implements CVC3::ValidityChecker.
Binary function application (op must be of function type)
Implements CVC3::ValidityChecker.
|
virtual |
Ternary function application (op must be of function type)
Implements CVC3::ValidityChecker.
n-ary function application (op must be of function type)
Implements CVC3::ValidityChecker.
Add the pair of variables to the variable ordering for aritmetic solving. Terms that are not arithmetic will be ignored.
smaller | the smaller variable |
bigger | the bigger variable |
Implements CVC3::ValidityChecker.
Definition at line 1268 of file vcl.cpp.
References ARITH_VAR_ORDER.
|
virtual |
Create a rational number with numerator n and denominator d.
n | the numerator |
d | the denominator, cannot be 0. |
Implements CVC3::ValidityChecker.
Definition at line 1276 of file vcl.cpp.
References DebugAssert.
|
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.
|
virtual |
Create a rational from a single string.
n | can be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format. |
base | is the base in which to interpret the string. |
Implements CVC3::ValidityChecker.
Definition at line 1289 of file vcl.cpp.
References CVC3::pow().
Create 2-element sum (left + right)
Implements CVC3::ValidityChecker.
Definition at line 1322 of file vcl.cpp.
References MiniSat::right().
Create n-element sum.
Implements CVC3::ValidityChecker.
Definition at line 1327 of file vcl.cpp.
References CVC3::PLUS.
Make a difference (left - right)
Implements CVC3::ValidityChecker.
Definition at line 1333 of file vcl.cpp.
References MiniSat::right().
Create a product (left * right)
Implements CVC3::ValidityChecker.
Definition at line 1339 of file vcl.cpp.
References MiniSat::right().
Create a power expression (x ^ n); n must be integer.
Implements CVC3::ValidityChecker.
Definition at line 1345 of file vcl.cpp.
References CVC3::powExpr().
Create expression x / y.
Implements CVC3::ValidityChecker.
Definition at line 1351 of file vcl.cpp.
References CVC3::divideExpr().
Create (left < right)
Implements CVC3::ValidityChecker.
Definition at line 1357 of file vcl.cpp.
References CVC3::ltExpr().
Create (left <= right)
Implements CVC3::ValidityChecker.
Definition at line 1363 of file vcl.cpp.
References CVC3::leExpr().
Create (left > right)
Implements CVC3::ValidityChecker.
Definition at line 1369 of file vcl.cpp.
References CVC3::gtExpr().
Create (left >= right)
Implements CVC3::ValidityChecker.
Definition at line 1375 of file vcl.cpp.
References CVC3::geExpr().
Create a 1-element record value (# field := expr #)
Fields will be sorted automatically
Implements CVC3::ValidityChecker.
|
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().
|
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().
|
virtual |
Create an n-element record value (# field_i := expr_i #)
fields | |
exprs | must 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().
Create record.field (field selection)
Create an expression representing the selection of a field from a record.
Implements CVC3::ValidityChecker.
|
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.
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.
Array update; equivalent to "array WITH index := newValue".
Implements CVC3::ValidityChecker.
Definition at line 1454 of file vcl.cpp.
References CVC3::WRITE.
|
virtual |
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
|
virtual |
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
Definition at line 1673 of file vcl.cpp.
References CVC3::BVSHL.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
Definition at line 1679 of file vcl.cpp.
References CVC3::BVLSHR.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
Definition at line 1685 of file vcl.cpp.
References CVC3::BVASHR.
'numbits' is the number of bits in the result
Implements CVC3::ValidityChecker.
Tuple expression.
Implements CVC3::ValidityChecker.
Definition at line 1697 of file vcl.cpp.
References DebugAssert.
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
Implements CVC3::ValidityChecker.
Tuple update; equivalent to "tuple WITH index := newValue".
Implements CVC3::ValidityChecker.
|
virtual |
Datatype constructor expression.
Implements CVC3::ValidityChecker.
Datatype selector expression.
Implements CVC3::ValidityChecker.
Datatype tester expression.
Implements CVC3::ValidityChecker.
|
virtual |
Create a bound variable with a given name, unique ID (uid) and type.
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. |
Implements CVC3::ValidityChecker.
Universal quantifier.
Implements CVC3::ValidityChecker.
Definition at line 1739 of file vcl.cpp.
References DebugAssert, and FORALL.
|
virtual |
Universal quantifier with a trigger.
Implements CVC3::ValidityChecker.
Definition at line 1744 of file vcl.cpp.
References DebugAssert, and FORALL.
|
virtual |
Universal quantifier with a set of triggers.
Implements CVC3::ValidityChecker.
Definition at line 1750 of file vcl.cpp.
References DebugAssert, and FORALL.
|
virtual |
Universal quantifier with a set of multi-triggers.
Implements CVC3::ValidityChecker.
Definition at line 1756 of file vcl.cpp.
References DebugAssert, and FORALL.
|
virtual |
Set triggers for quantifier instantiation.
e | the expression for which triggers are being set. |
triggers | Each item in triggers is a vector of Expr containing one or more patterns. A pattern is a term or Atomic predicate sub-expression of e. A vector containing more than one pattern is treated as a multi-trigger. Patterns will be matched in the order they occur in the vector. |
Implements CVC3::ValidityChecker.
Definition at line 1762 of file vcl.cpp.
References CVC3::Expr::setTriggers().
Set triggers for quantifier instantiation (no multi-triggers)
Implements CVC3::ValidityChecker.
Definition at line 1766 of file vcl.cpp.
References CVC3::Expr::setTriggers().
Set a single trigger for quantifier instantiation.
Implements CVC3::ValidityChecker.
Definition at line 1770 of file vcl.cpp.
References CVC3::Expr::setTrigger().
Set a single multi-trigger for quantifier instantiation.
Implements CVC3::ValidityChecker.
Definition at line 1774 of file vcl.cpp.
References CVC3::Expr::setMultiTrigger().
Existential quantifier.
Implements CVC3::ValidityChecker.
Definition at line 1778 of file vcl.cpp.
References EXISTS.
Lambda-expression.
Implements CVC3::ValidityChecker.
Definition at line 1783 of file vcl.cpp.
References LAMBDA.
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.
|
virtual |
Symbolic simulation expression.
f | is the next state function (LAMBDA-expression) |
s0 | is the initial state |
inputs | is the vector of LAMBDA-expressions representing the sequences of inputs to f |
n | is a constant, the number of cycles to run the simulation. |
Implements CVC3::ValidityChecker.
Definition at line 1793 of file vcl.cpp.
References SIMULATE.
|
virtual |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
Implements CVC3::ValidityChecker.
|
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.
|
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::pop(), CVC3::Type::toString(), TRACE, and TRACE_MSG.
|
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.
|
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 1904 of file vcl.cpp.
References CVC3::Theorem::getExpr(), and CVC3::Theorem::isNull().
Simplify e with respect to the current context.
Implements CVC3::ValidityChecker.
Definition at line 1919 of file vcl.cpp.
References CVC3::Theorem::getRHS(), and CVC3::Expr::getType().
|
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.
e | is the queried formula |
Implements CVC3::ValidityChecker.
Definition at line 1929 of file vcl.cpp.
References CVC3::ABORT, AND, CVC3::Expr::getType(), CVC3::Expr::impExpr(), CVC3::INVALID, CVC3::Type::isBool(), CVC3::pop(), CVC3::push(), QUERY, CVC3::Type::toString(), TRACE, UNKNOWN, and CVC3::VALID.
|
virtual |
Check satisfiability of the expr in the current context.
Equivalent to query(!e)
Implements CVC3::ValidityChecker.
Definition at line 2008 of file vcl.cpp.
References CVC3::Expr::negate().
|
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 2014 of file vcl.cpp.
References CVC3::andExpr(), and CONTINUE.
|
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 2030 of file vcl.cpp.
References RESTART.
|
virtual |
Returns to context immediately before last invalid query.
This method should only be called after a query which returns false.
Implements CVC3::ValidityChecker.
|
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.
assumptions | should be empty on entry. |
Implements CVC3::ValidityChecker.
|
virtual |
Get assumptions made internally in this and all previous contexts.
Internal assumptions are literals assumed by the sat solver.
assumptions | should be empty on entry. |
Implements CVC3::ValidityChecker.
|
virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be empty on entry. |
Implements CVC3::ValidityChecker.
Definition at line 2061 of file vcl.cpp.
References 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
assumptions | should be empty on entry. |
Implements CVC3::ValidityChecker.
Definition at line 2085 of file vcl.cpp.
References DUMP_ASSUMPTIONS, CVC3::Theorem::getLeafAssumptions(), and CVC3::Theorem::isNull().
|
virtual |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
Implements CVC3::ValidityChecker.
|
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.
assumptions | should be empty on entry. |
inOrder | if true, returns the assumptions in the order they were made. This is slightly more expensive than inOrder = false. |
Implements CVC3::ValidityChecker.
Definition at line 2097 of file vcl.cpp.
References COUNTEREXAMPLE.
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 2107 of file vcl.cpp.
References COUNTERMODEL.
|
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 2116 of file vcl.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::INVALID, CVC3::Expr::isFalse(), CVC3::orExpr(), and UNKNOWN.
|
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 2150 of file vcl.cpp.
References DebugAssert, and CVC3::Expr::isTerm().
|
virtual |
Returns true if the current context is inconsistent.
Also returns a minimal set of assertions used to determine the inconsistency.
assumptions | should be empty on entry. |
Implements CVC3::ValidityChecker.
|
virtual |
Returns true if the current context is inconsistent.
Implements CVC3::ValidityChecker.
|
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.
|
virtual |
Returns true if the invalid result from last query() is imprecise.
The argument is filled with the reasons for incompleteness (they are intended to be shown to the end user).
Implements CVC3::ValidityChecker.
|
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 2187 of file vcl.cpp.
References DUMP_PROOF.
|
virtual |
Returns the list of pairs (name value) for each :named attribute.
If the last query was not invalid, should return NULL expr
Implements CVC3::ValidityChecker.
Definition at line 2200 of file vcl.cpp.
References GET_ASSIGNMENT.
Evaluate an expression and return a concrete value in the model.
If the last query was not invalid, should return NULL expr
Implements CVC3::ValidityChecker.
Definition at line 2207 of file vcl.cpp.
References GET_VALUE.
|
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 2214 of file vcl.cpp.
References DUMP_TCC.
|
virtual |
Return the set of assumptions used in the proof of the last TCC.
Implements CVC3::ValidityChecker.
Definition at line 2224 of file vcl.cpp.
References DUMP_TCC_ASSUMPTIONS.
|
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 2237 of file vcl.cpp.
References DUMP_TCC_PROOF.
|
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 2247 of file vcl.cpp.
References DUMP_CLOSURE.
|
virtual |
Construct a proof of the query closure |- Gamma => phi.
Returns Null if last query was Invalid.
Implements CVC3::ValidityChecker.
Definition at line 2261 of file vcl.cpp.
References DUMP_CLOSURE_PROOF.
|
virtual |
Returns the current stack level. Initial level is 0.
Implements CVC3::ValidityChecker.
|
virtual |
Checkpoint the current context and increase the scope level.
Implements CVC3::ValidityChecker.
Definition at line 2281 of file vcl.cpp.
References CVC3::pop(), and PUSH.
|
virtual |
Restore the current context to its state at the last checkpoint.
Implements CVC3::ValidityChecker.
Definition at line 2294 of file vcl.cpp.
References POP, and CVC3::pop().
|
virtual |
Restore the current context to the given stackLevel.
stackLevel | should be greater than or equal to 0 and less than or equal to the current scope level. |
Implements CVC3::ValidityChecker.
Definition at line 2312 of file vcl.cpp.
References POPTO.
|
virtual |
Returns the current scope level. Initially, the scope level is 1.
Implements CVC3::ValidityChecker.
|
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 2331 of file vcl.cpp.
References IF_DEBUG, and PUSH_SCOPE.
|
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 2343 of file vcl.cpp.
References std::endl(), IF_DEBUG, CVC3::ExprStream::pop, and POP_SCOPE.
|
virtual |
Restore the current context to the given scopeLevel.
scopeLevel | should be less than or equal to the current scope level. |
If scopeLevel is less than 1, then the current context is reset and the scope level is set to 1.
Implements CVC3::ValidityChecker.
Definition at line 2358 of file vcl.cpp.
References IF_DEBUG, and POPTO_SCOPE.
|
virtual |
|
virtual |
Destroy and recreate validity checker: resets everything except for flags.
Implements CVC3::ValidityChecker.
|
virtual |
Add an annotation to the current script - prints annot when translating.
Implements CVC3::ValidityChecker.
|
virtual |
Read and execute the commands from a file given by name ("" means stdin)
Implements CVC3::ValidityChecker.
Definition at line 2393 of file vcl.cpp.
References CVC3::VCCmd::processCommands().
|
virtual |
Read and execute the commands from a stream.
Implements CVC3::ValidityChecker.
Definition at line 2402 of file vcl.cpp.
References CVC3::VCCmd::processCommands().
|
inlinevirtual |
|
inlinevirtual |
Print collected statistics to stdout.
Implements CVC3::ValidityChecker.
Definition at line 416 of file vcl.h.
References std::endl().
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
All theories are stored in this common vector.
This includes TheoryCore and TheoryArith.
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |