CVC3
2.4.1
|
This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More...
#include <theory_core.h>
Classes | |
class | CoreNotifyObj |
class | CoreSatAPI |
Interface class for callbacks to SAT from Core. More... | |
Public Member Functions | |
TheoryCore (ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics) | |
Constructor. More... | |
~TheoryCore () | |
Destructor. More... | |
void | getResource () |
Request a unit of resource. More... | |
void | registerCoreSatAPI (CoreSatAPI *coreSatAPI) |
Register a SatAPI for TheoryCore. More... | |
void | addNotifyEq (Theory *t, const Expr &e) |
Register a callback for every equality. More... | |
Theorem | callTheoryPreprocess (const Expr &e) |
Call theory-specific preprocess routines. More... | |
ContextManager * | getCM () const |
TheoremManager * | getTM () const |
const CLFlags & | getFlags () const |
Statistics & | getStatistics () const |
ExprTransform * | getExprTrans () const |
CoreProofRules * | getCoreRules () const |
Translator * | getTranslator () const |
ExprMap< Expr > & | tccCache () |
Access to tcc cache (needed by theory_bitvector) More... | |
const CDList< Expr > & | getTerms () |
Get list of terms. More... | |
int | getCurQuantLevel () |
void | setInPP () |
Set the flag for the preprocessor. More... | |
void | clearInPP () |
Theorem | getTheoremForTerm (const Expr &e) |
Get theorem which was responsible for introducing this term. More... | |
unsigned | getQuantLevelForTerm (const Expr &e) |
Get quantification level at which this term was introduced. More... | |
const CDList< Expr > & | getPredicates () |
Get list of predicates. More... | |
bool | inUpdate () |
Whether updates are being processed. More... | |
bool | okToEnqueue () |
Whether its OK to add new facts (for use in rewrites) More... | |
void | addSharedTerm (const Expr &e) |
void | assertFact (const Theorem &e) |
Assert a new fact to the decision procedure. More... | |
void | checkSat (bool fullEffort) |
Check for satisfiability in the theory. More... | |
Theorem | rewrite (const Expr &e) |
Theory-specific rewrite rules. More... | |
void | setup (const Expr &e) |
void | update (const Theorem &e, const Expr &d) |
Theorem | solve (const Theorem &e) |
Theorem | simplifyOp (const Expr &e) |
Recursive simplification step. More... | |
void | checkType (const Expr &e) |
Check that e is a valid Type expr. More... | |
Cardinality | finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Compute information related to finiteness of types. More... | |
void | computeType (const Expr &e) |
Compute and store the type of e. More... | |
Type | computeBaseType (const Type &t) |
Compute the base type of the top-level operator of an arbitrary type. More... | |
Expr | computeTCC (const Expr &e) |
Compute and cache the TCC of e. More... | |
Expr | computeTypePred (const Type &t, const Expr &e) |
Theory specific computation of the subtyping predicate for type t applied to the expression e. More... | |
Expr | parseExprOp (const Expr &e) |
Theory-specific parsing implemented by the DP. More... | |
ExprStream & | print (ExprStream &os, const Expr &e) |
Theory-specific pretty-printing. More... | |
void | refineCounterExample () |
Calls for other theories to add facts to refine a coutnerexample. More... | |
bool | refineCounterExample (Theorem &thm) |
void | computeModelBasic (const std::vector< Expr > &v) |
Assign concrete values to basic-type variables in v. More... | |
void | addFact (const Theorem &e) |
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure; use enqueueFact(). More... | |
Theorem | simplify (const Expr &e) |
Top-level simplifier. More... | |
bool | inconsistent () |
Check if the current context is inconsistent. More... | |
Theorem | inconsistentThm () |
Get the proof of inconsistency for the current context. More... | |
bool | checkSATCore () |
To be called by SearchEngine when it believes the context is satisfiable. More... | |
bool | incomplete () |
Check if the current decision branch is marked as incomplete. More... | |
bool | incomplete (std::vector< std::string > &reasons) |
Check if the branch is incomplete, and return the reasons (strings) More... | |
void | registerAtom (const Expr &e, const Theorem &thm) |
Register an atomic formula of interest. More... | |
Theorem | getImpliedLiteral (void) |
Return the next implied literal (NULL Theorem if none) More... | |
unsigned | numImpliedLiterals () |
Return total number of implied literals. More... | |
Theorem | getImpliedLiteralByIndex (unsigned index) |
Return an implied literal by index. More... | |
Expr | parseExpr (const Expr &e) |
Parse the generic expression. More... | |
Expr | parseExprTop (const Expr &e) |
Top-level call to parseExpr, clears the bound variable stack. More... | |
void | assignValue (const Expr &t, const Expr &val) |
Assign t a concrete value val. Used in model generation. More... | |
void | assignValue (const Theorem &thm) |
Record a derived assignment to a variable (LHS). More... | |
void | addToVarDB (const Expr &e) |
Adds expression to var database. More... | |
void | collectBasicVars () |
Split compound vars into basic type variables. More... | |
void | buildModel (ExprMap< Expr > &m) |
Calls theory specific computeModel, results are placed in map. More... | |
bool | buildModel (Theorem &thm) |
void | collectModelValues (const Expr &e, ExprMap< Expr > &m) |
Recursively build a compound-type variable assignment for e. More... | |
void | setResourceLimit (unsigned limit) |
Set the resource limit (0==unlimited). More... | |
unsigned | getResourceLimit () |
Get the resource limit. More... | |
bool | outOfResources () |
Return true if resources are exhausted. More... | |
void | initTimeLimit () |
Initialize base time used for !setTimeLimit. More... | |
void | setTimeLimit (unsigned limit) |
Set the time limit in seconds (0==unlimited). More... | |
Theorem | rewriteLiteral (const Expr &e) |
Called by search engine. More... | |
Expr | getAssignment () |
Get the value of all :named terms. More... | |
Expr | getValue (Expr e) |
Get the value of an arbitrary formula or term. More... | |
void | enqueueFact (const Theorem &e) |
Enqueue a new fact. More... | |
void | enqueueSE (const Theorem &thm) |
Check if the current context is inconsistent. More... | |
void | setInconsistent (const Theorem &e) |
void | setupTerm (const Expr &e, Theory *i, const Theorem &thm) |
Setup additional terms within a theory-specific setup(). More... | |
![]() | |
Theory (TheoryCore *theoryCore, const std::string &name) | |
Whether theory has been used (for smtlib translator) More... | |
virtual | ~Theory (void) |
Destructor. More... | |
ExprManager * | getEM () |
Access to ExprManager. More... | |
TheoryCore * | theoryCore () |
Get a pointer to theoryCore. More... | |
CommonProofRules * | getCommonRules () |
Get a pointer to common proof rules. More... | |
const std::string & | getName () const |
Get the name of the theory (for debugging purposes) More... | |
virtual void | setUsed () |
Set the "used" flag on this theory (for smtlib translator) More... | |
virtual bool | theoryUsed () |
Get whether theory has been used (for smtlib translator) More... | |
virtual Theorem | theoryPreprocess (const Expr &e) |
Theory-specific preprocessing. More... | |
virtual void | checkAssertEqInvariant (const Theorem &e) |
A debug check used by the primary solver. More... | |
virtual void | computeModelTerm (const Expr &e, std::vector< Expr > &v) |
Add variables from 'e' to 'v' for constructing a concrete model. More... | |
virtual void | computeModel (const Expr &e, std::vector< Expr > &vars) |
Compute the value of a compound variable from the more primitive ones. More... | |
virtual void | assertTypePred (const Expr &e, const Theorem &pred) |
Receives all the type predicates for the types of the given theory. More... | |
virtual Theorem | rewriteAtomic (const Expr &e) |
Theory-specific rewrites for atomic formulas. More... | |
virtual void | notifyInconsistent (const Theorem &thm) |
Notification of conflict. More... | |
virtual void | registerAtom (const Expr &e) |
Theory-specific registration of atoms. More... | |
Expr | simplifyExpr (const Expr &e) |
Simplify a term e w.r.t. the current context. More... | |
void | registerKinds (Theory *theory, std::vector< int > &kinds) |
Register new kinds with the given theory. More... | |
void | unregisterKinds (Theory *theory, std::vector< int > &kinds) |
Unregister kinds for a theory. More... | |
void | registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false) |
Register a new theory. More... | |
void | unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver) |
Unregister a theory. More... | |
int | getNumTheories () |
Return the number of registered theories. More... | |
bool | hasTheory (int kind) |
Test whether a kind maps to any theory. More... | |
Theory * | theoryOf (int kind) |
Return the theory associated with a kind. More... | |
Theory * | theoryOf (const Type &e) |
Return the theory associated with a type. More... | |
Theory * | theoryOf (const Expr &e) |
Return the theory associated with an Expr. More... | |
Theorem | find (const Expr &e) |
Return the theorem that e is equal to its find. More... | |
const Theorem & | findRef (const Expr &e) |
Return the find as a reference: expr must have a find. More... | |
Theorem | findReduce (const Expr &e) |
Return find-reduced version of e. More... | |
bool | findReduced (const Expr &e) |
Return true iff e is find-reduced. More... | |
Expr | findExpr (const Expr &e) |
Return the find of e, or e if it has no find. More... | |
Expr | getTCC (const Expr &e) |
Compute the TCC of e, or the subtyping predicate, if e is a type. More... | |
Type | getBaseType (const Expr &e) |
Compute (or look up in cache) the base type of e and return the result. More... | |
Type | getBaseType (const Type &tp) |
Compute the base type from an arbitrary type. More... | |
Expr | getTypePred (const Type &t, const Expr &e) |
Calls the correct theory to compute a type predicate. More... | |
Theorem | updateHelper (const Expr &e) |
Update the children of the term e. More... | |
void | setupCC (const Expr &e) |
Setup a term for congruence closure (must have sig and rep attributes) More... | |
void | updateCC (const Theorem &e, const Expr &d) |
Update a term w.r.t. congruence closure (must be setup with setupCC()) More... | |
Theorem | rewriteCC (const Expr &e) |
Rewrite a term w.r.t. congruence closure (must be setup with setupCC()) More... | |
void | getModelTerm (const Expr &e, std::vector< Expr > &v) |
Calls the correct theory to get all of the terms that need to be assigned values in the concrete model. More... | |
Theorem | getModelValue (const Expr &e) |
Fetch the concrete assignment to the variable during model generation. More... | |
void | addSplitter (const Expr &e, int priority=0) |
Suggest a splitter to the SearchEngine. More... | |
void | addGlobalLemma (const Theorem &thm, int priority=0) |
Add a global lemma. More... | |
bool | isLeaf (const Expr &e) |
Test if e is an i-leaf term for the current theory. More... | |
bool | isLeafIn (const Expr &e1, const Expr &e2) |
Test if e1 is an i-leaf in e2. More... | |
bool | leavesAreSimp (const Expr &e) |
Test if all i-leaves of e are simplified. More... | |
Type | boolType () |
Return BOOLEAN type. More... | |
const Expr & | falseExpr () |
Return FALSE Expr. More... | |
const Expr & | trueExpr () |
Return TRUE Expr. More... | |
Expr | newVar (const std::string &name, const Type &type) |
Create a new variable given its name and type. More... | |
Expr | newVar (const std::string &name, const Type &type, const Expr &def) |
Create a new named expression given its name, type, and definition. More... | |
Op | newFunction (const std::string &name, const Type &type, bool computeTransClosure) |
Create a new uninterpreted function. More... | |
Op | lookupFunction (const std::string &name, Type *type) |
Look up a function by name. More... | |
Op | newFunction (const std::string &name, const Type &type, const Expr &def) |
Create a new defined function. More... | |
Expr | addBoundVar (const std::string &name, const Type &type) |
Create and add a new bound variable to the stack, for parseExprOp(). More... | |
Expr | addBoundVar (const std::string &name, const Type &type, const Expr &def) |
Create and add a new bound named def to the stack, for parseExprOp(). More... | |
Expr | lookupVar (const std::string &name, Type *type) |
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet. More... | |
Type | newTypeExpr (const std::string &name) |
Create a new uninterpreted type with the given name. More... | |
Type | lookupTypeExpr (const std::string &name) |
Lookup type by name. Return Null if no such type exists. More... | |
Type | newTypeExpr (const std::string &name, const Type &def) |
Create a new type abbreviation with the given name. More... | |
Type | newSubtypeExpr (const Expr &pred, const Expr &witness) |
Create a new subtype expression. More... | |
Expr | resolveID (const std::string &name) |
Resolve an identifier, for use in parseExprOp() More... | |
void | installID (const std::string &name, const Expr &e) |
Install name as a new identifier associated with Expr e. More... | |
Theorem | typePred (const Expr &e) |
Return BOOLEAN type. More... | |
Theorem | reflexivityRule (const Expr &a) |
==> a == a More... | |
Theorem | symmetryRule (const Theorem &a1_eq_a2) |
a1 == a2 ==> a2 == a1 More... | |
Theorem | transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) |
(a1 == a2) & (a2 == a3) ==> (a1 == a3) More... | |
Theorem | substitutivityRule (const Op &op, const std::vector< Theorem > &thms) |
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n) More... | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t) |
Special case for unary operators. More... | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2) |
Special case for binary operators. More... | |
Theorem | substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) |
Optimized: only positions which changed are included. More... | |
Theorem | substitutivityRule (const Expr &e, int changed, const Theorem &thm) |
Optimized: only a single position changed. More... | |
Theorem | iffMP (const Theorem &e1, const Theorem &e1_iff_e2) |
e1 AND (e1 IFF e2) ==> e2 More... | |
Theorem | rewriteAnd (const Expr &e) |
==> AND(e1,e2) IFF [simplified expr] More... | |
Theorem | rewriteOr (const Expr &e) |
==> OR(e1,...,en) IFF [simplified expr] More... | |
Theorem | rewriteIte (const Expr &e) |
Derived rule for rewriting ITE. More... | |
Theorem | renameExpr (const Expr &e) |
Derived rule to create a new name for an expression. More... | |
Private Types | |
enum | EffortLevel { LOW, NORMAL, FULL } |
Effort level for processFactQueue. More... | |
Private Member Functions | |
CoreProofRules * | createProofRules (TheoremManager *tm) |
Private method to get a new theorem producer. More... | |
bool | processFactQueue (EffortLevel effort=NORMAL) |
A helper function for addFact() More... | |
void | processNotify (const Theorem &e, NotifyList *L) |
Process a notify list triggered as a result of new theorem e. More... | |
Theorem | rewriteCore (const Theorem &e) |
Transitive composition of other rewrites with the above. More... | |
void | setupSubFormulas (const Expr &s, const Expr &e, const Theorem &thm) |
Helper for registerAtom. More... | |
void | processUpdates () |
Process updates recorded by calls to update() More... | |
void | assertFactCore (const Theorem &e) |
The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface function name. More... | |
void | assertFormula (const Theorem &e) |
Process a newly derived formula. More... | |
Theorem | rewriteCore (const Expr &e) |
Check that lhs and rhs of thm have same base type. More... | |
void | setFindLiteral (const Theorem &thm) |
Set the find pointer of an atomic formula and notify SearchEngine. More... | |
Theorem | rewriteLitCore (const Expr &e) |
Core rewrites for literals (NOT and EQ) More... | |
Theorem | getModelValue (const Expr &e) |
Enqueue a fact to be sent to the SearchEngine. More... | |
Expr | processCond (const Expr &e, int i) |
An auxiliary recursive function to process COND expressions into ITE. More... | |
bool | isBasicKind (int kind) |
Return true if no special parsing is required for this kind. More... | |
void | checkEquation (const Theorem &thm) |
Helper check functions for solve. More... | |
void | checkSolved (const Theorem &thm) |
Helper check functions for solve. More... | |
bool | timeLimitReached () |
ExprStream & | printSmtLibShared (ExprStream &os, const Expr &e) |
void | assertEqualities (const Theorem &e) |
Assert a system of equations (1 or more). More... | |
void | setIncomplete (const std::string &reason) |
Mark the branch as incomplete. More... | |
Theorem | typePred (const Expr &e) |
Return a theorem for the type predicate of e. More... | |
Private Attributes | |
ContextManager * | d_cm |
Context manager. More... | |
TheoremManager * | d_tm |
Theorem manager. More... | |
CoreProofRules * | d_rules |
Core proof rules. More... | |
const CLFlags & | d_flags |
Reference to command line flags. More... | |
Statistics & | d_statistics |
Reference to statistics. More... | |
PrettyPrinter * | d_printer |
PrettyPrinter (we own it) More... | |
ExprManager::TypeComputer * | d_typeComputer |
Type Computer. More... | |
ExprTransform * | d_exprTrans |
Expr Transformer. More... | |
Translator * | d_translator |
Translator. More... | |
std::queue< Theorem > | d_queue |
Assertion queue. More... | |
std::vector< Theorem > | d_queueSE |
Queue of facts to be sent to the SearchEngine. More... | |
CDO< bool > | d_inconsistent |
Inconsistent flag. More... | |
CDMap< std::string, bool > | d_incomplete |
The set of reasons for incompleteness (empty when we are complete) More... | |
CDO< Theorem > | d_incThm |
Proof of inconsistent. More... | |
CDList< Expr > | d_terms |
List of all active terms in the system (for quantifier instantiation) More... | |
std::hash_map< Expr, Theorem > | d_termTheorems |
Map from active terms to theorems that introduced those terms. More... | |
CDList< Expr > | d_predicates |
List of all active non-equality atomic formulas in the system (for quantifier instantiation) More... | |
std::vector< Expr > | d_vars |
List of variables that were created up to this point. More... | |
std::map< std::string, Expr > | d_globals |
Database of declared identifiers. More... | |
std::vector< std::pair < std::string, Expr > > | d_boundVarStack |
Bound variable stack: a vector of pairs <name, var> More... | |
std::hash_map< std::string, Expr > | d_boundVarMap |
Map for bound vars. More... | |
ExprMap< Expr > | d_parseCacheTop |
Top-level cache for parser. More... | |
ExprMap< Expr > | d_parseCacheOther |
Alternative cache for parser when not at top-level. More... | |
ExprMap< Expr > * | d_parseCache |
Current cache being used for parser. More... | |
ExprMap< Expr > | d_tccCache |
Cache for tcc's. More... | |
std::vector< Theory * > | d_theories |
Array of registered theories. More... | |
std::hash_map< int, Theory * > | d_theoryMap |
Array mapping kinds to theories. More... | |
Theory * | d_solver |
The theory which has the solver (if any) More... | |
ExprHashMap< std::vector< Expr > > | d_varModelMap |
Mapping of compound type variables to simpler types (model generation) More... | |
ExprHashMap< Theorem > | d_varAssignments |
Mapping of intermediate variables to their values. More... | |
std::vector< Expr > | d_basicModelVars |
List of basic variables (temporary storage for model generation) More... | |
ExprHashMap< Theorem > | d_simplifiedModelVars |
Mapping of basic variables to simplified expressions (temp. storage) More... | |
const bool * | d_simplifyInPlace |
Command line flag whether to simplify in place. More... | |
Theorem(TheoryCore::* | d_currentRecursiveSimplifier )(const Expr &) |
Which recursive simplifier to use. More... | |
unsigned | d_resourceLimit |
Resource limit (0==unlimited, 1==no more resources, >=2 - available). More... | |
unsigned | d_timeBase |
Time limit (0==unlimited, >0==total available cpu time in seconds). More... | |
unsigned | d_timeLimit |
bool | d_inCheckSATCore |
bool | d_inAddFact |
bool | d_inRegisterAtom |
bool | d_inPP |
CoreNotifyObj | d_notifyObj |
CDList< Theorem > | d_impliedLiterals |
List of implied literals, based on registered atomic formulas of interest. More... | |
CDO< unsigned > | d_impliedLiteralsIdx |
Next index in d_impliedLiterals that has not yet been fetched. More... | |
std::vector< Theorem > | d_update_thms |
List of theorems from calls to update() More... | |
std::vector< Expr > | d_update_data |
List of data accompanying above theorems from calls to update() More... | |
NotifyList | d_notifyEq |
Notify list that gets processed on every equality. More... | |
unsigned | d_inUpdate |
Whether we are in the middle of doing updates. More... | |
std::vector< std::pair< Expr, Expr > > | d_assignment |
The set of named expressions to evaluate on a GET_ASSIGNMENT request. More... | |
CoreSatAPI * | d_coreSatAPI |
Friends | |
class | Theory |
class | CoreNotifyObj |
So we get notified every time there's a pop. More... | |
Additional Inherited Members | |
![]() | |
bool | d_theoryUsed |
This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories.
Author: Clark Barrett
Created: Sat Feb 8 14:54:05 2003
Definition at line 53 of file theory_core.h.
|
private |
Effort level for processFactQueue.
LOW means just process facts, don't call theory checkSat methods NORMAL means call theory checkSat methods without full effort FULL means call theory checkSat methods with full effort
Enumerator | |
---|---|
LOW | |
NORMAL | |
FULL |
Definition at line 258 of file theory_core.h.
TheoryCore::TheoryCore | ( | ContextManager * | cm, |
ExprManager * | em, | ||
TheoremManager * | tm, | ||
Translator * | tr, | ||
const CLFlags & | flags, | ||
Statistics & | statistics | ||
) |
Constructor.
Definition at line 698 of file theory_core.cpp.
References AND, AND_R, ANNOTATION, ANY_TYPE, APPLY, ARITH_VAR_ORDER, ASSERT, ASSERTIONS, ASSUMPTIONS, BOOLEAN, BOUND_VAR, CALL, CHECK_TYPE, COND, CONST, CONTEXT, COUNTEREXAMPLE, COUNTERMODEL, createProofRules(), CVC3::Theory::d_commonRules, CVC3::Theory::d_em, d_exprTrans, CVC3::Theory::d_name, d_printer, d_rules, CVC3::Theory::d_theoryCore, CVC3::Theory::d_theoryUsed, d_typeComputer, DBG, DEFUN, DISTINCT, DUMP_ASSUMPTIONS, DUMP_CLOSURE, DUMP_CLOSURE_PROOF, DUMP_PROOF, DUMP_SIG, DUMP_TCC, DUMP_TCC_ASSUMPTIONS, DUMP_TCC_PROOF, ECHO, ELSE, EQ, FALSE_EXPR, FORGET, GET_ASSIGNMENT, GET_CHILD, GET_TYPE, GET_VALUE, CVC3::TheoremManager::getRules(), HELP, ID, IF, IFF, IFF_R, IFTHEN, IMPLIES, ITE, ITE_R, LET, LETDECL, LETDECLS, NEQ, NOT, OPTION, OR, PF_APPLY, PF_HOLE, POP, POP_SCOPE, POPTO, POPTO_SCOPE, PRINT, PUSH, PUSH_SCOPE, QUERY, RAW_LIST, CVC3::ExprManager::registerPrettyPrinter(), CVC3::Theory::registerTheory(), CVC3::ExprManager::registerTypeComputer(), RESET, SEQ, SKOLEM_VAR, STRING_EXPR, SUBSTITUTE, SUBTYPE, THEOREM_KIND, TRACE, TRANSFORM, TRUE_EXPR, TYPE, TYPEDEF, UCONST, UNTRACE, VARDECL, VARDECLS, VARLIST, WHERE, and XOR.
TheoryCore::~TheoryCore | ( | ) |
Destructor.
Definition at line 847 of file theory_core.cpp.
References CVC3::Theory::d_em, d_exprTrans, d_printer, d_rules, d_typeComputer, and CVC3::ExprManager::unregisterPrettyPrinter().
|
private |
Private method to get a new theorem producer.
This method is used ONLY by the TheoryCore constructor. The only reason to have this method is to separate the trusted part of the constructor into a separate .cpp file (Alternative is to make the entire constructer trusted, which is not very safe). Method is implemented in core_theorem_producer.cpp
Definition at line 45 of file core_theorem_producer.cpp.
Referenced by TheoryCore().
|
private |
A helper function for addFact()
Returns true if lemmas were added to search engine, false otherwise
Definition at line 121 of file theory_core.cpp.
Referenced by addFact(), callTheoryPreprocess(), checkSATCore(), and registerAtom().
|
private |
Process a notify list triggered as a result of new theorem e.
Definition at line 173 of file theory_core.cpp.
References DebugAssert, CVC3::NotifyList::getExpr(), CVC3::NotifyList::getTheory(), CVC3::NotifyList::size(), and CVC3::Theory::update().
Referenced by assertEqualities().
Transitive composition of other rewrites with the above.
Definition at line 257 of file theory_core.cpp.
References DebugAssert, CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), and CVC3::Theorem::toString().
Referenced by rewrite().
Helper for registerAtom.
Definition at line 269 of file theory_core.cpp.
References CVC3::Expr::addToNotify(), CVC3::Expr::arity(), CVC3::Expr::isAbsAtomicFormula(), and CVC3::Expr::isAtomic().
Referenced by registerAtom().
|
private |
Process updates recorded by calls to update()
Definition at line 291 of file theory_core.cpp.
References DebugAssert, CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Type::isBool(), and CVC3::Theorem::isRewrite().
|
private |
The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface function name.
Definition at line 321 of file theory_core.cpp.
References CVC3::Expr::arity(), DebugAssert, std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::PRESENTATION_LANG, CVC3::Expr::toString(), and TRACE.
|
private |
Process a newly derived formula.
Definition at line 385 of file theory_core.cpp.
References CVC3::Expr::addToNotify(), CVC3::Theory::assertFact(), DebugAssert, EQ, CVC3::Expr::eqExpr(), EXISTS, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isNot(), NOT, CVC3::PRESENTATION_LANG, CVC3::Theorem::toString(), CVC3::Expr::toString(), and TRACE.
Referenced by assertEqualities().
Check that lhs and rhs of thm have same base type.
Returns phi |= e = rewriteCore(e). "Core" added to avoid conflict with theory interface function name
Definition at line 455 of file theory_core.cpp.
References CVC3::Expr::clearRewriteNormal(), DebugAssert, EQ, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isEq(), CVC3::Theorem::isRefl(), CVC3::Expr::isRewriteNormal(), NOT, CVC3::Expr::setRewriteNormal(), and CVC3::Expr::toString().
|
private |
Set the find pointer of an atomic formula and notify SearchEngine.
thm | is a Theorem(phi) or Theorem(NOT phi), where phi is an atomic formula to get a find pointer to TRUE or FALSE, respectively. |
Definition at line 509 of file theory_core.cpp.
References DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), CVC3::PRESENTATION_LANG, CVC3::Expr::setFind(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::toString(), and TRACE.
Referenced by registerAtom(), and update().
Core rewrites for literals (NOT and EQ)
Definition at line 560 of file theory_core.cpp.
References DebugAssert, EQ, CVC3::Expr::getKind(), NOT, and CVC3::Expr::toString().
Referenced by rewrite().
Enqueue a fact to be sent to the SearchEngine.
Fetch the concrete assignment to the variable during model generation
Definition at line 595 of file theory_core.cpp.
Referenced by collectModelValues(), and CVC3::Theory::getModelValue().
An auxiliary recursive function to process COND expressions into ITE.
Definition at line 605 of file theory_core.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getString(), ID, CVC3::int2string(), CVC3::Expr::iteExpr(), RAW_LIST, and CVC3::Expr::toString().
Referenced by parseExprOp().
|
private |
Return true if no special parsing is required for this kind.
Definition at line 630 of file theory_core.cpp.
References AND, ASSERT, ASSERTIONS, ASSUMPTIONS, CALL, CHECK_TYPE, CHECKSAT, CONTEXT, CONTINUE, COUNTEREXAMPLE, COUNTERMODEL, DBG, DISTINCT, DUMP_ASSUMPTIONS, DUMP_CLOSURE, DUMP_CLOSURE_PROOF, DUMP_PROOF, DUMP_SIG, DUMP_TCC, DUMP_TCC_ASSUMPTIONS, DUMP_TCC_PROOF, ECHO, ELSE, FORGET, GET_ASSIGNMENT, GET_CHILD, GET_TYPE, GET_VALUE, HELP, IFF, IMPLIES, LETDECL, LETDECLS, NOT, OPTION, OR, POP, POP_SCOPE, POPTO, POPTO_SCOPE, PRINT, PUSH, PUSH_SCOPE, QUERY, RESET, RESTART, SEQ, SUBSTITUTE, TRACE, TRANSFORM, TYPEDEF, UNTRACE, VARDECL, VARDECLS, VARLIST, WHERE, and XOR.
Referenced by parseExprOp().
|
private |
Helper check functions for solve.
Definition at line 1195 of file theory_core.cpp.
References d_solver, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::isEq(), CVC3::Theory::solve(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().
Referenced by checkSolved().
|
private |
Helper check functions for solve.
Definition at line 1220 of file theory_core.cpp.
References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), checkEquation(), CVC3::Theory::d_commonRules, CVC3::Theorem::getExpr(), CVC3::Expr::isAnd(), and CVC3::Expr::isBoolConst().
Referenced by solve().
|
private |
Definition at line 4062 of file theory_core.cpp.
References d_timeBase, d_timeLimit, and setIncomplete().
|
private |
Print an expression in the shared subset of SMT-LIB v1/v2 Should only be called if os.lang() is SMTLIB_LANG or SMTLIB_V2_LANG.
Definition at line 1915 of file theory_core.cpp.
References AND, ANY_TYPE, CVC3::Expr::arity(), CVC3::Expr::begin(), BOOLEAN, d_translator, DebugAssert, DISTINCT, CVC3::Expr::end(), EQ, CVC3::Translator::escapeSymbol(), FALSE_EXPR, CVC3::Translator::fixConstName(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::ExprStream::lang(), LETDECL, NOT, OR, PF_APPLY, PF_HOLE, CVC3::pop(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::push(), RAW_LIST, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), STRING_EXPR, SUBTYPE, CVC3::Expr::toString(), TRANSFORM, TRUE_EXPR, TYPEDEF, UCONST, and XOR.
Referenced by print().
|
inline |
Request a unit of resource.
It will be subtracted from the resource limit.
Definition at line 334 of file theory_core.h.
References CVC3::Statistics::counter(), d_resourceLimit, and getStatistics().
Referenced by addFact().
|
inline |
Register a SatAPI for TheoryCore.
Definition at line 340 of file theory_core.h.
References d_coreSatAPI.
Referenced by CVC3::SearchImplBase::SearchImplBase(), and CVC3::SearchSat::SearchSat().
Register a callback for every equality.
Definition at line 343 of file theory_core.h.
References CVC3::NotifyList::add(), and d_notifyEq.
Referenced by CVC3::TheoryQuant::TheoryQuant().
Call theory-specific preprocess routines.
Definition at line 857 of file theory_core.cpp.
References d_theories, CVC3::Theorem::getRHS(), LOW, processFactQueue(), CVC3::Theory::reflexivityRule(), CVC3::Theory::theoryPreprocess(), and CVC3::Theory::transitivityRule().
Referenced by CVC3::ExprTransform::preprocess().
|
inline |
Definition at line 348 of file theory_core.h.
References d_cm.
Referenced by CVC3::TheoryQuant::add_parent(), addFact(), CVC3::SearchEngineFast::addNonLiteralFact(), assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryQuant::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::mapTermsByType(), CVC3::ExprTransform::newPPrec(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchImplBase::pop(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::SearchImplBase::push(), CVC3::TheoryQuant::pushBackList(), CVC3::DecisionEngine::pushDecision(), CVC3::TheoryQuant::pushForwList(), CVC3::TheoryQuant::recursiveMap(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::SearchImplBase::scopeLevel(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchSat::SearchSat(), CVC3::TheoryQuant::synCheckSat(), and CVC3::TheoryQuant::synNewInst().
|
inline |
Definition at line 349 of file theory_core.h.
References d_tm.
Referenced by CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchImplBase::getProof(), CVC3::SearchSat::getProof(), SAT::DPLLTMiniSat::getSatProof(), CVC3::SearchEngine::SearchEngine(), and CVC3::SearchSat::SearchSat().
|
inline |
Definition at line 350 of file theory_core.h.
References d_flags.
Referenced by CVC3::SearchEngineFast::bcp(), CVC3::Translator::finish(), CVC3::Theory::newSubtypeExpr(), CVC3::SearchSat::newUserAssumptionIntHelper(), parseExprOp(), CVC3::ExprTransform::preprocess(), print(), CVC3::Translator::processType(), rewrite(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchSat::SearchSat(), and CVC3::TheoryQuant::TheoryQuant().
|
inline |
Definition at line 351 of file theory_core.h.
References d_statistics.
Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::findInCNFCache(), getResource(), CVC3::SearchSat::SearchSat(), and CVC3::SearchEngineFast::split().
|
inline |
Definition at line 352 of file theory_core.h.
References d_exprTrans.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchImplBase::newUserAssumption(), and CVC3::SearchSat::newUserAssumptionInt().
|
inline |
Definition at line 353 of file theory_core.h.
References d_rules.
Referenced by CVC3::ExprTransform::ExprTransform().
|
inline |
Definition at line 354 of file theory_core.h.
References d_translator.
Referenced by CVC3::TheoryUF::printSmtLibShared().
Access to tcc cache (needed by theory_bitvector)
Definition at line 357 of file theory_core.h.
References d_tccCache.
Referenced by CVC3::TheoryBitvector::computeTCC().
Get list of terms.
Definition at line 360 of file theory_core.h.
References d_terms.
Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::debug(), CVC3::TheoryQuant::naiveCheckSat(), and CVC3::TheoryQuant::synCheckSat().
int CVC3::TheoryCore::getCurQuantLevel | ( | ) |
|
inline |
Set the flag for the preprocessor.
Definition at line 365 of file theory_core.h.
References d_inPP.
Referenced by CVC3::ExprTransform::preprocess().
|
inline |
Definition at line 366 of file theory_core.h.
References d_inPP.
Referenced by CVC3::ExprTransform::preprocess().
Get theorem which was responsible for introducing this term.
Definition at line 868 of file theory_core.cpp.
References d_termTheorems, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), and TRACE.
Referenced by getQuantLevelForTerm().
unsigned TheoryCore::getQuantLevelForTerm | ( | const Expr & | e) |
Get quantification level at which this term was introduced.
Definition at line 904 of file theory_core.cpp.
References CVC3::Expr::getIndex(), getTheoremForTerm(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isIff(), CVC3::Expr::isNot(), CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryQuant::enqueueInst(), and CVC3::TheoryQuant::getExprScore().
Get list of predicates.
Definition at line 373 of file theory_core.h.
References d_predicates.
Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::debug(), and CVC3::TheoryQuant::synCheckSat().
|
inline |
Whether updates are being processed.
Definition at line 375 of file theory_core.h.
References d_inUpdate.
|
inline |
Whether its OK to add new facts (for use in rewrites)
Definition at line 377 of file theory_core.h.
References d_inAddFact, d_inCheckSATCore, d_inPP, and d_inRegisterAtom.
|
inlinevirtual |
Variables of uninterpreted types may be sent here, and they should be ignored.
Reimplemented from CVC3::Theory.
Definition at line 383 of file theory_core.h.
|
virtual |
Assert a new fact to the decision procedure.
Each fact that makes it into the core framework is assigned to exactly one theory: the theory associated with that fact. assertFact is called to inform the theory that a new fact has been assigned to the theory.
Implements CVC3::Theory.
Definition at line 960 of file theory_core.cpp.
References DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), SKOLEM_VAR, CVC3::Theorem::toString(), UCONST, and CVC3::Expr::unnegate().
|
inlinevirtual |
Check for satisfiability in the theory.
fullEffort | when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing. |
If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called.
Implements CVC3::Theory.
Definition at line 385 of file theory_core.h.
Theory-specific rewrite rules.
By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done.
Reimplemented from CVC3::Theory.
Definition at line 968 of file theory_core.cpp.
References AND, AND_R, APPLY, CVC3::Expr::arity(), BOUND_VAR, CVC3::Theory::d_commonRules, d_rules, DebugAssert, DISTINCT, EQ, EXISTS, FALSE_EXPR, CVC3::Theory::find(), FORALL, CVC3::Theorem::getExpr(), getFlags(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), IFF, IFF_R, IMPLIES, CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Theorem::isRefl(), CVC3::Expr::isTrue(), ITE, ITE_R, LAMBDA, LETDECL, NOT, OR, CVC3::CommonProofRules::reflexivityRule(), CVC3::Theory::reflexivityRule(), CVC3::Theory::rewrite(), CVC3::Theory::rewriteAnd(), CVC3::CoreProofRules::rewriteAndSubterms(), rewriteCore(), CVC3::CoreProofRules::rewriteDistinct(), CVC3::CommonProofRules::rewriteIff(), CVC3::CoreProofRules::rewriteImplies(), CVC3::Theory::rewriteIte(), CVC3::CoreProofRules::rewriteIteCond(), CVC3::CoreProofRules::rewriteIteToAnd(), CVC3::CoreProofRules::rewriteIteToIff(), CVC3::CoreProofRules::rewriteIteToImp(), CVC3::CoreProofRules::rewriteIteToNot(), CVC3::CoreProofRules::rewriteIteToOr(), CVC3::CoreProofRules::rewriteLetDecl(), rewriteLitCore(), CVC3::Theory::rewriteOr(), CVC3::CoreProofRules::rewriteOrSubterms(), CVC3::Expr::setRewriteNormal(), simplify(), SKOLEM_VAR, CVC3::Theory::substitutivityRule(), CVC3::Theory::theoryOf(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), TRUE_EXPR, UCONST, XOR, and CVC3::CommonProofRules::xorToIff().
|
inlinevirtual |
Only Boolean constants (TRUE and FALSE) and variables of uninterpreted types should appear here (they come from records and tuples). Just ignore them.
Reimplemented from CVC3::Theory.
Definition at line 390 of file theory_core.h.
We use the update method of theory core to track registered atomic formulas. Updates are recorded and then processed by calling processUpdates once all equalities have been processed.
Reimplemented from CVC3::Theory.
Definition at line 1141 of file theory_core.cpp.
References CVC3::Expr::addToNotify(), CVC3::Theory::d_commonRules, d_update_data, d_update_thms, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::CommonProofRules::iffFalseElim(), CVC3::Theory::iffMP(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), CVC3::CommonProofRules::rewriteUsingSymmetry(), setFindLiteral(), setInconsistent(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Theory::symmetryRule(), and CVC3::Theory::transitivityRule().
Function: TheoryCore::solve
Author: Clark Barrett
Created: Wed Feb 26 16:17:54 2003
This is a generalization of what's in my thesis. The goal is to rewrite e into an equisatisfiable conjunction of equations such that the left-hand side of each equation is a variable which does not appear as an i-leaf of the rhs, where i is the theory of the primary solver. Any solution which satisfies this is fine. "Solvers" from other theories can do whatever they want as long as we eventually reach this form.
Reimplemented from CVC3::Theory.
Definition at line 1248 of file theory_core.cpp.
References checkSolved(), d_solver, DebugAssert, CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), IF_DEBUG, CVC3::Expr::isAnd(), CVC3::Expr::isBoolConst(), CVC3::Expr::isEq(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), CVC3::Theory::solve(), and CVC3::Theory::theoryOf().
Recursive simplification step.
INVARIANT: the result is a Theorem(e=e'), where e' is a fully simplified version of e. To simplify subexpressions recursively, call simplify() function.
This theory-specific method is called when the simplifier descends top-down into the expression. Normally, every kid is simplified recursively, and the results are combined into the new parent with the same operator (Op). This functionality is provided with the default implementation.
However, in some expressions some kids may not matter in the result, and can be skipped. For instance, if the first kid in a long AND simplifies to FALSE, then the entire expression simplifies to FALSE, and the remaining kids do not need to be simplified.
This call is a chance for a DP to provide these types of optimizations during the top-down phase of simplification.
Reimplemented from CVC3::Theory.
Definition at line 1292 of file theory_core.cpp.
References AND, CVC3::Expr::arity(), CVC3::Theory::d_commonRules, d_rules, DebugAssert, EQ, FALSE_EXPR, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), IF_DEBUG, IFF, CVC3::CommonProofRules::iffTrue(), IMPLIES, CVC3::Expr::isBoolConst(), CVC3::Expr::isFalse(), CVC3::Theorem::isRefl(), CVC3::Expr::isTrue(), ITE, NOT, OR, CVC3::Theory::reflexivityRule(), CVC3::Theory::rewriteAnd(), CVC3::CoreProofRules::rewriteImplies(), CVC3::CommonProofRules::rewriteIteSame(), CVC3::Theory::rewriteOr(), simplify(), CVC3::Theory::simplifyOp(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Theory::substitutivityRule(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and TRUE_EXPR.
|
virtual |
Check that e is a valid Type expr.
Reimplemented from CVC3::Theory.
Definition at line 1408 of file theory_core.cpp.
References ANY_TYPE, CVC3::Expr::arity(), BOOLEAN, FatalAssert, CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isFunction(), SUBTYPE, and CVC3::Expr::toString().
|
virtual |
Compute information related to finiteness of types.
Used by the TypeComputer defined in TheoryCore (theories should not call this funtion directly – they should use the methods in Type instead). Each theory should implement this if it contains any types that could be non-infinite.
Reimplemented from CVC3::Theory.
Definition at line 1443 of file theory_core.cpp.
References ANY_TYPE, BOOLEAN, CVC3::CARD_FINITE, CVC3::CARD_INFINITE, CVC3::CARD_UNKNOWN, CVC3::Theory::falseExpr(), FatalAssert, CVC3::Theory::getEM(), CVC3::Expr::getKind(), SUBTYPE, and CVC3::Theory::trueExpr().
|
virtual |
Compute and store the type of e.
e | is the expression whose type is computed. |
This function computes the type of the top-level operator of e, and recurses into children using getType(), if necessary.
Reimplemented from CVC3::Theory.
Definition at line 1471 of file theory_core.cpp.
References AND, AND_R, CVC3::Type::anyType(), APPLY, CVC3::Type::arity(), CVC3::Expr::arity(), CVC3::Theory::boolType(), CVC3::Theory::d_em, DebugAssert, DISTINCT, EQ, CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), IFF, IFF_R, IMPLIES, CVC3::int2string(), CVC3::Expr::isApply(), CVC3::Type::isBool(), CVC3::Type::isFunction(), ITE, ITE_R, LETDECL, NOT, OR, RAW_LIST, CVC3::Expr::setType(), CVC3::Type::toString(), CVC3::Expr::toString(), and XOR.
Compute the base type of the top-level operator of an arbitrary type.
Reimplemented from CVC3::Theory.
Definition at line 1620 of file theory_core.cpp.
References ANY_TYPE, CVC3::Expr::arity(), BOOLEAN, DebugAssert, CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isFunction(), SUBTYPE, CVC3::Type::toString(), CVC3::Expr::toString(), and TYPEDEF.
Compute and cache the TCC of e.
e | is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined. |
This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary.
The default implementation is to compute TCCs recursively for all children, and return their conjunction.
Reimplemented from CVC3::Theory.
Definition at line 1650 of file theory_core.cpp.
References AND, CVC3::andExpr(), APPLY, CVC3::Expr::begin(), CVC3::Theory::computeTCC(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theory::getTCC(), IMPLIES, ITE, NOT, OR, CVC3::orExpr(), CVC3::Theory::rewriteAnd(), CVC3::Theory::rewriteOr(), and CVC3::Theory::theoryOf().
Theory specific computation of the subtyping predicate for type t applied to the expression e.
By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)
Reimplemented from CVC3::Theory.
Definition at line 1704 of file theory_core.cpp.
References CVC3::andExpr(), APPLY, CVC3::Theory::computeTypePred(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Theory::getTypePred(), CVC3::Expr::lookupType(), CVC3::Expr::mkOp(), SUBTYPE, CVC3::Theory::theoryOf(), and CVC3::ExprManager::trueExpr().
Theory-specific parsing implemented by the DP.
Reimplemented from CVC3::Theory.
Definition at line 1724 of file theory_core.cpp.
References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::Expr::begin(), BOOLEAN, CVC3::ExprManager::boolExpr(), CVC3::Theory::boolType(), COND, d_parseCache, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), EQ, CVC3::Expr::eqExpr(), FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::ExprMap< Data >::find(), CVC3::Theory::getEM(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), getFlags(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::Expr::getType(), ID, IF, CVC3::Expr::iffExpr(), isBasicKind(), CVC3::Expr::iteExpr(), LET, NEQ, CVC3::ExprManager::newLeafExpr(), CVC3::Theory::newSubtypeExpr(), NULL_KIND, parseExpr(), processCond(), RAW_LIST, SUBTYPE, CVC3::Expr::toString(), TRACE, TRUE_EXPR, CVC3::ExprManager::trueExpr(), TYPE, TYPEDECL, and TYPEDEF.
|
virtual |
Theory-specific pretty-printing.
By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer.
Reimplemented from CVC3::Theory.
Definition at line 2055 of file theory_core.cpp.
References AND, ANNOTATION, ANY_TYPE, ARITH_VAR_ORDER, CVC3::Expr::arity(), ARROW, ASSERT, ASSERTIONS, ASSUMPTIONS, CVC3::Expr::begin(), BOOLEAN, BOUND_VAR, CVC3::ExprHashMap< Data >::clear(), CONST, contains(), COUNTEREXAMPLE, COUNTERMODEL, CVC3::Theory::d_em, d_translator, DebugAssert, DISTINCT, CVC3::Expr::end(), std::endl(), EQ, CVC3::Translator::escapeSymbol(), FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::Theory::falseExpr(), CVC3::Translator::fixConstName(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), getFlags(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Expr::getString(), CVC3::Expr::getType(), ID, IFF, IMPLIES, CVC3::int2string(), CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::isReal(), CVC3::Expr::isString(), ITE, CVC3::ExprStream::lang(), LET, LETDECL, CVC3::LISP_LANG, CVC3::Expr::negate(), CVC3::nodag(), NOT, CVC3::Expr::notExpr(), OR, PF_APPLY, PF_HOLE, POP, CVC3::pop(), POP_SCOPE, CVC3::popSave(), POPTO, POPTO_SCOPE, CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::Expr::printAST(), printSmtLibShared(), PUSH, CVC3::push(), PUSH_SCOPE, CVC3::pushRestore(), QUERY, CVC3::Translator::quoteAnnotation(), RAW_LIST, RESET, CVC3::SIMPLIFY_LANG, SKOLEM_VAR, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), CVC3::SPASS_LANG, STRING_EXPR, SUBTYPE, CVC3::to_lower(), CVC3::to_upper(), CVC3::Expr::toString(), CVC3::TPTP_LANG, TRANSFORM, TRUE_EXPR, CVC3::ExprManager::trueExpr(), CVC3::Theory::trueExpr(), TYPE, TYPEDEF, UCONST, WHERE, and XOR.
|
virtual |
Calls for other theories to add facts to refine a coutnerexample.
Reimplemented from CVC3::Theory.
Definition at line 3429 of file theory_core.cpp.
References CVC3::Theory::d_em, d_theories, CVC3::Theorem::getLeafAssumptions(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), inconsistent(), inconsistentThm(), RAW_LIST, and CVC3::Expr::toString().
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
bool TheoryCore::refineCounterExample | ( | Theorem & | thm) |
Definition at line 3415 of file theory_core.cpp.
References d_theories, CVC3::Theory::getNumTheories(), inconsistent(), and inconsistentThm().
|
virtual |
Assign concrete values to basic-type variables in v.
Reimplemented from CVC3::Theory.
Definition at line 3449 of file theory_core.cpp.
References assignValue(), CVC3::Theory::d_em, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getRHS(), TRACE, and CVC3::ExprManager::trueExpr().
void TheoryCore::addFact | ( | const Theorem & | e) |
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure; use enqueueFact().
Definition at line 3468 of file theory_core.cpp.
References d_inAddFact, d_inconsistent, d_queue, d_queueSE, d_update_data, d_update_thms, DebugAssert, getCM(), CVC3::Theorem::getExpr(), getResource(), IF_DEBUG, outOfResources(), CVC3::PRESENTATION_LANG, processFactQueue(), setIncomplete(), CVC3::Expr::toString(), and TRACE.
Referenced by assignValue(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::commitFacts(), CVC3::ExprTransform::newPPrec(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::Circuit::propagate(), CVC3::DecisionEngine::pushDecision(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::SearchEngineFast::split().
Top-level simplifier.
Reimplemented from CVC3::Theory.
Definition at line 184 of file theory_core.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getSimpCache(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::int2string(), CVC3::Theorem::isRefl(), CVC3::Expr::isVar(), CVC3::Expr::setSimpCache(), CVC3::Expr::toString(), CVC3::Expr::usesCC(), and CVC3::Expr::validSimpCache().
Referenced by getAssignment(), getValue(), CVC3::ExprTransform::newPPrec(), registerAtom(), rewrite(), setupTerm(), CVC3::SearchImplBase::simplify(), CVC3::Theory::simplify(), CVC3::Theory::simplifyOp(), simplifyOp(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::smartSimplify(), CVC3::ExprTransform::specialSimplify(), and CVC3::SearchEngineFast::split().
|
inlinevirtual |
Check if the current context is inconsistent.
Reimplemented from CVC3::Theory.
Definition at line 422 of file theory_core.h.
References d_inconsistent.
Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::Theory::inconsistent(), refineCounterExample(), and CVC3::SearchEngineFast::split().
|
inline |
Get the proof of inconsistency for the current context.
Definition at line 425 of file theory_core.h.
References d_incThm.
Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::SearchEngine::getConcreteModel(), and refineCounterExample().
bool TheoryCore::checkSATCore | ( | ) |
To be called by SearchEngine when it believes the context is satisfiable.
Definition at line 3507 of file theory_core.cpp.
References d_inCheckSATCore, d_queue, d_queueSE, d_update_data, d_update_thms, DebugAssert, FULL, IF_DEBUG, and processFactQueue().
Referenced by CVC3::SearchEngineFast::split().
|
inline |
Check if the current decision branch is marked as incomplete.
Definition at line 435 of file theory_core.h.
References d_incomplete, and CVC3::CDMap< Key, Data, HashFcn >::size().
Referenced by assertEqualities(), CVC3::SearchEngineFast::checkSAT(), and CVC3::SearchSimple::checkValidMain().
bool TheoryCore::incomplete | ( | std::vector< std::string > & | reasons) |
Check if the branch is incomplete, and return the reasons (strings)
Definition at line 3528 of file theory_core.cpp.
References CVC3::CDMap< Key, Data, HashFcn >::begin(), d_incomplete, CVC3::CDMap< Key, Data, HashFcn >::end(), and CVC3::CDMap< Key, Data, HashFcn >::size().
Register an atomic formula of interest.
If e or its negation is later deduced, we will add the implied literal to d_impliedLiterals
Reimplemented from CVC3::Theory.
Definition at line 3541 of file theory_core.cpp.
References CVC3::Theory::d_commonRules, d_inRegisterAtom, d_termTheorems, DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::iffFalseElim(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), LOW, processFactQueue(), setFindLiteral(), CVC3::Expr::setRegisteredAtom(), setupSubFormulas(), simplify(), and CVC3::Theory::theoryOf().
Referenced by CVC3::SearchSat::registerAtom(), and CVC3::Theory::registerAtom().
Theorem TheoryCore::getImpliedLiteral | ( | void | ) |
Return the next implied literal (NULL Theorem if none)
Definition at line 3571 of file theory_core.cpp.
References d_impliedLiterals, and d_impliedLiteralsIdx.
Referenced by CVC3::SearchImplBase::getImpliedLiteral().
|
inline |
Return total number of implied literals.
Definition at line 448 of file theory_core.h.
References d_impliedLiterals.
Theorem TheoryCore::getImpliedLiteralByIndex | ( | unsigned | index) |
Return an implied literal by index.
Definition at line 3582 of file theory_core.cpp.
References d_impliedLiterals, and DebugAssert.
Referenced by CVC3::SearchSat::getImpliedLiteral().
Parse the generic expression.
This method should be used in parseExprOp() for recursive calls to subexpressions, and is the method called by the command processor.
Reimplemented from CVC3::Theory.
Definition at line 3589 of file theory_core.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::ExprMap< Data >::clear(), d_assignment, d_boundVarMap, d_boundVarStack, d_parseCache, d_parseCacheTop, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::Theory::getEM(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Expr::getString(), CVC3::Expr::getType(), CVC3::Theory::hasTheory(), ID, CVC3::Expr::isApply(), CVC3::Expr::isNull(), LAMBDA, CVC3::Expr::mkOp(), NULL_KIND, CVC3::Theory::parseExprOp(), RAW_LIST, CVC3::Theory::resolveID(), STRING_EXPR, CVC3::Theory::theoryOf(), and CVC3::Expr::toString().
Referenced by CVC3::Theory::parseExpr(), parseExprOp(), and parseExprTop().
Top-level call to parseExpr, clears the bound variable stack.
Use it in VCL instead of parseExpr().
Definition at line 461 of file theory_core.h.
References d_boundVarStack, d_parseCache, d_parseCacheTop, and parseExpr().
Assign t a concrete value val. Used in model generation.
Reimplemented from CVC3::Theory.
Definition at line 3713 of file theory_core.cpp.
References CVC3::TheoryCore::CoreSatAPI::addAssumption(), addFact(), d_coreSatAPI, d_varAssignments, DebugAssert, CVC3::Expr::eqExpr(), CVC3::Theory::find(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::toString(), and CVC3::Theory::transitivityRule().
Referenced by CVC3::Theory::assignValue(), buildModel(), collectModelValues(), and computeModelBasic().
|
virtual |
Record a derived assignment to a variable (LHS).
Reimplemented from CVC3::Theory.
Definition at line 3734 of file theory_core.cpp.
References addFact(), d_varAssignments, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::Theory::symmetryRule(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and CVC3::Theory::transitivityRule().
void TheoryCore::addToVarDB | ( | const Expr & | e) |
Adds expression to var database.
Definition at line 3756 of file theory_core.cpp.
Referenced by CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::Theory::renameExpr().
void TheoryCore::collectBasicVars | ( | ) |
Split compound vars into basic type variables.
The results are saved in d_basicModelVars and d_simplifiedModelVars. Also, add new basic vars as shared terms whenever their type belongs to a different theory than the term itself.
Definition at line 3763 of file theory_core.cpp.
References CVC3::Theory::addSharedTerm(), d_basicModelVars, d_simplifiedModelVars, d_varAssignments, d_varModelMap, d_vars, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Theory::getModelTerm(), CVC3::Theorem::getRHS(), RAW_LIST, CVC3::Theory::theoryOf(), TRACE, and TRACE_MSG.
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
Calls theory specific computeModel, results are placed in map.
Definition at line 3862 of file theory_core.cpp.
References assignValue(), collectModelValues(), d_basicModelVars, CVC3::Theory::d_em, d_simplifiedModelVars, d_theories, d_varAssignments, d_vars, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::getLHS(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), CVC3::Theorem::getRHS(), inconsistent(), inconsistentThm(), CVC3::Theorem::isNull(), RAW_LIST, CVC3::Theory::theoryOf(), CVC3::Expr::toString(), TRACE, TRACE_MSG, and CVC3::Theory::transitivityRule().
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
bool TheoryCore::buildModel | ( | Theorem & | thm) |
Definition at line 3817 of file theory_core.cpp.
References d_basicModelVars, d_simplifiedModelVars, d_theories, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), CVC3::Theorem::getRHS(), inconsistent(), inconsistentThm(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), and TRACE.
Recursively build a compound-type variable assignment for e.
Not all theories may implement aggregation of compound values. If a compound variable is not assigned by a theory, add the more primitive variable assignments to 'm'.
Some variables may simplify to something else (simplifiedVars map). INVARIANT: e is always simplified (it's not in simplifiedVars map). Also, if v simplifies to e, and e is assigned, then v must be assigned.
Definition at line 3954 of file theory_core.cpp.
References assignValue(), CVC3::Theory::computeModel(), d_simplifiedModelVars, d_varAssignments, d_varModelMap, CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), getModelValue(), CVC3::Theory::getName(), CVC3::Theorem::getRHS(), IF_DEBUG, RAW_LIST, CVC3::Theory::reflexivityRule(), CVC3::Theory::theoryOf(), TRACE, and CVC3::Theory::transitivityRule().
Referenced by buildModel().
|
inline |
Set the resource limit (0==unlimited).
Definition at line 488 of file theory_core.h.
References d_resourceLimit.
|
inline |
|
inline |
Return true if resources are exhausted.
Definition at line 492 of file theory_core.h.
References d_resourceLimit.
Referenced by addFact(), and CVC3::SearchEngineFast::checkSAT().
void TheoryCore::initTimeLimit | ( | ) |
Initialize base time used for !setTimeLimit.
Definition at line 4058 of file theory_core.cpp.
References d_timeBase.
Referenced by setTimeLimit().
void TheoryCore::setTimeLimit | ( | unsigned | limit) |
Set the time limit in seconds (0==unlimited).
Definition at line 4053 of file theory_core.cpp.
References d_timeLimit, and initTimeLimit().
Called by search engine.
Definition at line 4029 of file theory_core.cpp.
References CVC3::Theory::d_commonRules, DebugAssert, CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::CommonProofRules::iffContrapositive(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isNot(), CVC3::Theory::rewriteAtomic(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().
Referenced by CVC3::SearchImplBase::replaceITE().
Expr TheoryCore::getAssignment | ( | ) |
Get the value of all :named terms.
Definition at line 4320 of file theory_core.cpp.
References d_assignment, d_exprTrans, CVC3::Theory::d_theoryCore, CVC3::Theory::getEM(), CVC3::Theorem::getRHS(), CVC3::ExprTransform::preprocess(), RAW_LIST, and simplify().
Get the value of an arbitrary formula or term.
Definition at line 4333 of file theory_core.cpp.
References d_exprTrans, CVC3::Theory::d_theoryCore, CVC3::Theorem::getRHS(), CVC3::ExprTransform::preprocess(), and simplify().
|
privatevirtual |
Assert a system of equations (1 or more).
e is either a single equation, or a conjunction of equations
Invariants:
In other words, the entire equality queue is processed "in parallel".
Reimplemented from CVC3::Theory.
Definition at line 4093 of file theory_core.cpp.
References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), assertFormula(), CVC3::Theory::checkAssertEqInvariant(), CVC3::Theory::d_commonRules, CVC3::Theory::d_em, d_inconsistent, d_notifyEq, d_solver, DebugAssert, CVC3::Theory::find(), CVC3::Theory::findReduced(), getCM(), CVC3::Expr::getEqNext(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), IF_DEBUG, incomplete(), CVC3::ExprManager::invalidateSimpCache(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), processNotify(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), setInconsistent(), CVC3::Theory::symmetryRule(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::transitivityRule().
Referenced by CVC3::Theory::assertEqualities().
|
privatevirtual |
Mark the branch as incomplete.
Reimplemented from CVC3::Theory.
Definition at line 4180 of file theory_core.cpp.
References d_incomplete, and CVC3::CDMap< Key, Data, HashFcn >::insert().
Referenced by addFact(), CVC3::Theory::setIncomplete(), and timeLimitReached().
Return a theorem for the type predicate of e.
Note: used only by theory_arith
Definition at line 4186 of file theory_core.cpp.
References d_rules, and CVC3::CoreProofRules::typePred().
Referenced by CVC3::Theory::typePred().
|
virtual |
Enqueue a new fact.
not private because used in search_fast.cpp
Reimplemented from CVC3::Theory.
Referenced by CVC3::SearchImplBase::addCNFFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::commitFacts(), and CVC3::Theory::enqueueFact().
|
virtual |
Check if the current context is inconsistent.
Reimplemented from CVC3::Theory.
Definition at line 588 of file theory_core.cpp.
References DebugAssert.
Referenced by CVC3::Theory::enqueueSE().
|
virtual |
not private because used in search_fast.cpp
Reimplemented from CVC3::Theory.
Definition at line 4245 of file theory_core.cpp.
References d_inconsistent, d_incThm, d_queueSE, d_theories, DebugAssert, CVC3::Theory::falseExpr(), and CVC3::Theorem::getExpr().
Referenced by assertEqualities(), CVC3::SearchEngineFast::setInconsistent(), CVC3::Theory::setInconsistent(), setupTerm(), and update().
Setup additional terms within a theory-specific setup().
not private because used in theory_bitvector.cpp
Definition at line 4260 of file theory_core.cpp.
References CVC3::Theory::addSharedTerm(), CVC3::Expr::arity(), CVC3::Theory::assertTypePred(), d_predicates, d_rules, d_terms, d_termTheorems, DebugAssert, CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getIndex(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::getType(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isFalse(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTerm(), CVC3::Expr::isTrue(), CVC3::CDList< T >::push_back(), CVC3::Theory::reflexivityRule(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), setInconsistent(), CVC3::Expr::setStoredPredicate(), CVC3::Theory::setup(), simplify(), CVC3::Theory::theoryOf(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, and CVC3::CoreProofRules::typePred().
Referenced by CVC3::TheoryRecords::setup(), and CVC3::TheoryArray::setup().
|
friend |
Definition at line 54 of file theory_core.h.
|
friend |
So we get notified every time there's a pop.
Definition at line 175 of file theory_core.h.
|
private |
|
private |
|
private |
Core proof rules.
Definition at line 63 of file theory_core.h.
Referenced by getCoreRules(), rewrite(), setupTerm(), simplifyOp(), TheoryCore(), typePred(), and ~TheoryCore().
|
private |
Reference to command line flags.
Definition at line 66 of file theory_core.h.
Referenced by getFlags().
|
private |
Reference to statistics.
Definition at line 69 of file theory_core.h.
Referenced by getStatistics().
|
private |
PrettyPrinter (we own it)
Definition at line 72 of file theory_core.h.
Referenced by TheoryCore(), and ~TheoryCore().
|
private |
Type Computer.
Definition at line 75 of file theory_core.h.
Referenced by TheoryCore(), and ~TheoryCore().
|
private |
Expr Transformer.
Definition at line 78 of file theory_core.h.
Referenced by getAssignment(), getExprTrans(), getValue(), TheoryCore(), and ~TheoryCore().
|
private |
Definition at line 81 of file theory_core.h.
Referenced by getTranslator(), print(), and printSmtLibShared().
|
private |
Assertion queue.
Definition at line 84 of file theory_core.h.
Referenced by addFact(), and checkSATCore().
|
private |
Queue of facts to be sent to the SearchEngine.
Definition at line 86 of file theory_core.h.
Referenced by addFact(), checkSATCore(), and setInconsistent().
|
private |
Inconsistent flag.
Definition at line 89 of file theory_core.h.
Referenced by addFact(), assertEqualities(), inconsistent(), and setInconsistent().
|
private |
The set of reasons for incompleteness (empty when we are complete)
Definition at line 91 of file theory_core.h.
Referenced by incomplete(), and setIncomplete().
Proof of inconsistent.
Definition at line 94 of file theory_core.h.
Referenced by inconsistentThm(), and setInconsistent().
List of all active terms in the system (for quantifier instantiation)
Definition at line 96 of file theory_core.h.
Referenced by getTerms(), and setupTerm().
|
private |
Map from active terms to theorems that introduced those terms.
Definition at line 99 of file theory_core.h.
Referenced by getTheoremForTerm(), registerAtom(), and setupTerm().
List of all active non-equality atomic formulas in the system (for quantifier instantiation)
Definition at line 103 of file theory_core.h.
Referenced by getPredicates(), and setupTerm().
|
private |
List of variables that were created up to this point.
Definition at line 105 of file theory_core.h.
Referenced by addToVarDB(), buildModel(), and collectBasicVars().
|
private |
Database of declared identifiers.
Definition at line 107 of file theory_core.h.
Referenced by CVC3::Theory::installID(), and CVC3::Theory::resolveID().
|
private |
Bound variable stack: a vector of pairs <name, var>
Definition at line 109 of file theory_core.h.
Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and parseExprTop().
|
private |
Map for bound vars.
Definition at line 111 of file theory_core.h.
Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and CVC3::Theory::resolveID().
Top-level cache for parser.
Definition at line 114 of file theory_core.h.
Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and parseExprTop().
Alternative cache for parser when not at top-level.
Definition at line 118 of file theory_core.h.
Referenced by CVC3::Theory::addBoundVar().
Current cache being used for parser.
Definition at line 120 of file theory_core.h.
Referenced by CVC3::Theory::addBoundVar(), parseExpr(), parseExprOp(), and parseExprTop().
Cache for tcc's.
Definition at line 122 of file theory_core.h.
Referenced by CVC3::Theory::getTCC(), and tccCache().
|
private |
Array of registered theories.
Definition at line 125 of file theory_core.h.
Referenced by buildModel(), callTheoryPreprocess(), CVC3::Theory::getNumTheories(), refineCounterExample(), CVC3::Theory::registerTheory(), setInconsistent(), and CVC3::Theory::unregisterTheory().
|
private |
Array mapping kinds to theories.
Definition at line 128 of file theory_core.h.
Referenced by CVC3::Theory::hasTheory(), CVC3::Theory::registerKinds(), CVC3::Theory::theoryOf(), and CVC3::Theory::unregisterKinds().
|
private |
The theory which has the solver (if any)
Definition at line 131 of file theory_core.h.
Referenced by assertEqualities(), checkEquation(), CVC3::Theory::registerTheory(), solve(), and CVC3::Theory::unregisterTheory().
|
private |
Mapping of compound type variables to simpler types (model generation)
Definition at line 134 of file theory_core.h.
Referenced by collectBasicVars(), and collectModelValues().
|
private |
Mapping of intermediate variables to their values.
Definition at line 136 of file theory_core.h.
Referenced by assignValue(), buildModel(), collectBasicVars(), and collectModelValues().
|
private |
List of basic variables (temporary storage for model generation)
Definition at line 138 of file theory_core.h.
Referenced by buildModel(), and collectBasicVars().
|
private |
Mapping of basic variables to simplified expressions (temp. storage)
There may be some vars which simplify to something else; we save those separately, and keep only those which simplify to themselves. Once the latter vars are assigned, we'll re-simplify the former variables and use the results as concrete values.
Definition at line 145 of file theory_core.h.
Referenced by buildModel(), collectBasicVars(), and collectModelValues().
|
private |
Command line flag whether to simplify in place.
Definition at line 148 of file theory_core.h.
Which recursive simplifier to use.
Definition at line 150 of file theory_core.h.
|
private |
Resource limit (0==unlimited, 1==no more resources, >=2 - available).
Currently, it is the number of enqueued facts. Once the resource is exhausted, the remaining facts will be dropped, and an incomplete flag is set.
Definition at line 157 of file theory_core.h.
Referenced by getResource(), getResourceLimit(), outOfResources(), and setResourceLimit().
|
private |
Time limit (0==unlimited, >0==total available cpu time in seconds).
Currently, if exhausted processFactQueue will not perform any more reasoning with FULL effor and an incomplete flag is set.
Definition at line 163 of file theory_core.h.
Referenced by initTimeLimit(), and timeLimitReached().
|
private |
Definition at line 164 of file theory_core.h.
Referenced by setTimeLimit(), and timeLimitReached().
|
private |
Definition at line 166 of file theory_core.h.
Referenced by checkSATCore(), and okToEnqueue().
|
private |
Definition at line 167 of file theory_core.h.
Referenced by addFact(), and okToEnqueue().
|
private |
Definition at line 168 of file theory_core.h.
Referenced by okToEnqueue(), and registerAtom().
|
private |
Definition at line 169 of file theory_core.h.
Referenced by clearInPP(), okToEnqueue(), and setInPP().
|
private |
Definition at line 183 of file theory_core.h.
List of implied literals, based on registered atomic formulas of interest.
Definition at line 186 of file theory_core.h.
Referenced by getImpliedLiteral(), getImpliedLiteralByIndex(), and numImpliedLiterals().
|
private |
Next index in d_impliedLiterals that has not yet been fetched.
Definition at line 189 of file theory_core.h.
Referenced by getImpliedLiteral().
|
private |
List of theorems from calls to update()
Definition at line 194 of file theory_core.h.
Referenced by addFact(), checkSATCore(), and update().
|
private |
List of data accompanying above theorems from calls to update()
Definition at line 197 of file theory_core.h.
Referenced by addFact(), checkSATCore(), and update().
|
private |
Notify list that gets processed on every equality.
Definition at line 200 of file theory_core.h.
Referenced by addNotifyEq(), and assertEqualities().
|
private |
Whether we are in the middle of doing updates.
Definition at line 203 of file theory_core.h.
Referenced by inUpdate().
The set of named expressions to evaluate on a GET_ASSIGNMENT request.
Definition at line 206 of file theory_core.h.
Referenced by getAssignment(), and parseExpr().
|
private |
Definition at line 240 of file theory_core.h.
Referenced by CVC3::Theory::addGlobalLemma(), CVC3::Theory::addSplitter(), assignValue(), CVC3::Theory::newSubtypeExpr(), and registerCoreSatAPI().