CVC3
2.4.1
|
Modules | |
Fast Search Engine | |
Simple Search Engine | |
Decision Engine | |
Decision Engine, used by Search Engine. | |
Proof Rules for the Search Engines | |
Classes | |
class | CVC3::SearchEngine |
API to to a generic proof search engine. More... | |
class | CVC3::SearchImplBase |
API to to a generic proof search engine (a.k.a. SAT solver) More... | |
class | CVC3::SearchImplBase::Splitter |
Representation of a DP-suggested splitter. More... | |
class | CVC3::SearchSat |
Search engine that connects to a generic SAT reasoning module. More... | |
Functions | |
SearchEngineRules * | CVC3::SearchEngine::createRules () |
Create the trusted component. More... | |
SearchEngineRules * | CVC3::SearchEngine::createRules (SearchEngine *s_eng) |
CVC3::SearchEngine::SearchEngine (TheoryCore *core) | |
Constructor. More... | |
virtual | CVC3::SearchEngine::~SearchEngine () |
Destructor. More... | |
virtual const std::string & | CVC3::SearchEngine::getName ()=0 |
Name of this search engine. More... | |
CommonProofRules * | CVC3::SearchEngine::getCommonRules () |
Accessor for common rules. More... | |
TheoryCore * | CVC3::SearchEngine::theoryCore () |
Accessor for TheoryCore. More... | |
virtual void | CVC3::SearchEngine::registerAtom (const Expr &e)=0 |
Register an atomic formula of interest. More... | |
virtual Theorem | CVC3::SearchEngine::getImpliedLiteral ()=0 |
Return next literal implied by last assertion. Null Expr if none. More... | |
virtual void | CVC3::SearchEngine::push ()=0 |
Push a checkpoint. More... | |
virtual void | CVC3::SearchEngine::pop ()=0 |
Restore last checkpoint. More... | |
virtual QueryResult | CVC3::SearchEngine::checkValid (const Expr &e, Theorem &result)=0 |
Checks the validity of a formula in the current context. More... | |
virtual QueryResult | CVC3::SearchEngine::restart (const Expr &e, Theorem &result)=0 |
Reruns last check with e as an additional assumption. More... | |
virtual void | CVC3::SearchEngine::returnFromCheck ()=0 |
Returns to context immediately before last call to checkValid. More... | |
virtual Theorem | CVC3::SearchEngine::lastThm ()=0 |
Returns the result of the most recent valid theorem. More... | |
virtual Theorem | CVC3::SearchEngine::newUserAssumption (const Expr &e)=0 |
Generate and add an assumption to the set of assumptions in the current context. More... | |
virtual void | CVC3::SearchEngine::getUserAssumptions (std::vector< Expr > &assumptions)=0 |
Get all user assumptions made in this and all previous contexts. More... | |
virtual void | CVC3::SearchEngine::getInternalAssumptions (std::vector< Expr > &assumptions)=0 |
Get assumptions made internally in this and all previous contexts. More... | |
virtual void | CVC3::SearchEngine::getAssumptions (std::vector< Expr > &assumptions)=0 |
Get all assumptions made in this and all previous contexts. More... | |
virtual bool | CVC3::SearchEngine::isAssumption (const Expr &e)=0 |
Check if the formula has already been assumed previously. More... | |
virtual void | CVC3::SearchEngine::getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)=0 |
Will return the set of assertions which make the queried formula false. More... | |
virtual Proof | CVC3::SearchEngine::getProof ()=0 |
Returns the proof term for the last proven query. More... | |
void | CVC3::SearchEngine::getConcreteModel (ExprMap< Expr > &m) |
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. More... | |
bool | CVC3::SearchEngine::tryModelGeneration (Theorem &thm) |
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. More... | |
virtual FormulaValue | CVC3::SearchEngine::getValue (const CVC3::Expr &e)=0 |
Literal | CVC3::SearchImplBase::newLiteral (const Expr &e) |
Construct a Literal out of an Expr or return an existing one. More... | |
Theorem | CVC3::SearchImplBase::simplify (const Theorem &e) |
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e') More... | |
virtual void | CVC3::SearchImplBase::addLiteralFact (const Theorem &thm)=0 |
Notify the search engine about a new literal fact. More... | |
virtual void | CVC3::SearchImplBase::addNonLiteralFact (const Theorem &thm)=0 |
Notify the search engine about a new non-literal fact. More... | |
void | CVC3::SearchImplBase::addCNFFact (const Theorem &thm, bool fromCore=false) |
Add a new fact to the search engine bypassing CNF converter. More... | |
int | CVC3::SearchImplBase::getBottomScope () |
bool | CVC3::SearchImplBase::isClause (const Expr &e) |
Check if e is a clause (a literal, or a disjunction of literals) More... | |
bool | CVC3::SearchImplBase::isPropClause (const Expr &e) |
Check if e is a propositional clause. More... | |
bool | CVC3::SearchImplBase::isCNFVar (const Expr &e) |
Check whether e is a fresh variable introduced by the CNF converter. More... | |
bool | CVC3::SearchImplBase::isGoodSplitter (const Expr &e) |
Check if a splitter is required for completeness. More... | |
void | CVC3::SearchImplBase::enqueueCNF (const Theorem &theta) |
Translate theta to CNF and enqueue the new clauses. More... | |
void | CVC3::SearchImplBase::enqueueCNFrec (const Theorem &theta) |
Recursive version of enqueueCNF() More... | |
void | CVC3::SearchImplBase::applyCNFRules (const Theorem &e) |
FIXME: write a comment. More... | |
void | CVC3::SearchImplBase::addToCNFCache (const Theorem &thm) |
Cache a theorem phi <=> v by phi, where v is a literal. More... | |
Theorem | CVC3::SearchImplBase::findInCNFCache (const Expr &e) |
Find a theorem phi <=> v by phi, where v is a literal. More... | |
Theorem | CVC3::SearchImplBase::replaceITE (const Expr &e) |
Replaces ITE subexpressions in e with variables. More... | |
int | CVC3::SearchImplBase::scopeLevel () |
Return the current scope level (for convenience) More... | |
CVC3::SearchImplBase::SearchImplBase (TheoryCore *core) | |
Constructor. More... | |
virtual | CVC3::SearchImplBase::~SearchImplBase () |
Destructor. More... | |
virtual void | CVC3::SearchImplBase::registerAtom (const Expr &e) |
Register an atomic formula of interest. More... | |
virtual Theorem | CVC3::SearchImplBase::getImpliedLiteral () |
Return next literal implied by last assertion. Null Expr if none. More... | |
virtual void | CVC3::SearchImplBase::push () |
Push a checkpoint. More... | |
virtual void | CVC3::SearchImplBase::pop () |
Restore last checkpoint. More... | |
virtual QueryResult | CVC3::SearchImplBase::checkValidInternal (const Expr &e)=0 |
Checks the validity of a formula in the current context. More... | |
virtual QueryResult | CVC3::SearchImplBase::checkValid (const Expr &e, Theorem &result) |
Similar to checkValidInternal(), only returns Theorem(e) or Null. More... | |
virtual QueryResult | CVC3::SearchImplBase::restartInternal (const Expr &e)=0 |
Reruns last check with e as an additional assumption. More... | |
virtual QueryResult | CVC3::SearchImplBase::restart (const Expr &e, Theorem &result) |
Reruns last check with e as an additional assumption. More... | |
void | CVC3::SearchImplBase::returnFromCheck () |
Returns to context immediately before last call to checkValid. More... | |
virtual Theorem | CVC3::SearchImplBase::lastThm () |
Returns the result of the most recent valid theorem. More... | |
Theorem | CVC3::SearchImplBase::newUserAssumption (const Expr &e) |
Generate and add a new assertion to the set of assertions in the current context. This should only be used by class VCL in assertFormula(). More... | |
virtual Theorem | CVC3::SearchImplBase::newIntAssumption (const Expr &e) |
Add a new internal asserion. More... | |
void | CVC3::SearchImplBase::newIntAssumption (const Theorem &thm) |
Helper for above function. More... | |
void | CVC3::SearchImplBase::getUserAssumptions (std::vector< Expr > &assumptions) |
Get all assumptions made in this and all previous contexts. More... | |
void | CVC3::SearchImplBase::getInternalAssumptions (std::vector< Expr > &assumptions) |
Get assumptions made internally in this and all previous contexts. More... | |
virtual void | CVC3::SearchImplBase::getAssumptions (std::vector< Expr > &assumptions) |
Get all assumptions made in this and all previous contexts. More... | |
virtual bool | CVC3::SearchImplBase::isAssumption (const Expr &e) |
Check if the formula has been assumed. More... | |
void | CVC3::SearchImplBase::addFact (const Theorem &thm) |
Add a new fact to the search engine from the core. More... | |
virtual void | CVC3::SearchImplBase::addSplitter (const Expr &e, int priority) |
Suggest a splitter to the SearchEngine. More... | |
virtual void | CVC3::SearchImplBase::getCounterExample (std::vector< Expr > &assertions, bool inOrder=true) |
Will return the set of assertions which make the queried formula false. More... | |
virtual Proof | CVC3::SearchImplBase::getProof () |
Returns the proof term for the last proven query. More... | |
virtual const Assumptions & | CVC3::SearchImplBase::getAssumptionsUsed () |
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions(). More... | |
void | CVC3::SearchImplBase::processResult (const Theorem &res, const Expr &e) |
Process result of checkValid. More... | |
virtual FormulaValue | CVC3::SearchImplBase::getValue (const CVC3::Expr &e) |
Variables | |
TheoryCore * | CVC3::SearchEngine::d_core |
Access to theory reasoning. More... | |
CommonProofRules * | CVC3::SearchEngine::d_commonRules |
Common proof rules. More... | |
SearchEngineRules * | CVC3::SearchEngine::d_rules |
Proof rules for the search engine. More... | |
VariableManager * | CVC3::SearchImplBase::d_vm |
Variable manager for classes Variable and Literal. More... | |
CDO< int > | CVC3::SearchImplBase::d_bottomScope |
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). More... | |
TheoryCore::CoreSatAPI * | CVC3::SearchImplBase::d_coreSatAPI_implBase |
CDList< Splitter > | CVC3::SearchImplBase::d_dpSplitters |
Backtracking ordered set of DP-suggested splitters. More... | |
Theorem | CVC3::SearchImplBase::d_lastValid |
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. More... | |
ExprHashMap< bool > | CVC3::SearchImplBase::d_lastCounterExample |
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample. More... | |
CDMap< Expr, Theorem > | CVC3::SearchImplBase::d_assumptions |
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions(). More... | |
CDMap< Expr, Theorem > | CVC3::SearchImplBase::d_cnfCache |
Backtracking cache for the CNF generator. More... | |
CDMap< Expr, bool > | CVC3::SearchImplBase::d_cnfVars |
Backtracking set of new variables generated by CNF translator. More... | |
const bool * | CVC3::SearchImplBase::d_cnfOption |
Command line flag whether to convert to CNF. More... | |
const bool * | CVC3::SearchImplBase::d_ifLiftOption |
Flag: whether to convert term ITEs into CNF. More... | |
const bool * | CVC3::SearchImplBase::d_ignoreCnfVarsOption |
Flag: ignore auxiliary CNF variables when searching for a splitter. More... | |
const bool * | CVC3::SearchImplBase::d_origFormulaOption |
Flag: Preserve the original formula with +cnf (for splitter heuristics) More... | |
CNF Caches | |
These caches are for subexpressions of the translated formula phi, to avoid expanding phi into a tree. We cannot use d_cnfCache for that, since it is effectively non-backtracking, and we do not know if a subexpression of phi was translated at the current level, or at some other (inactive) branch of the decision tree. | |
CDMap< Expr, bool > | CVC3::SearchImplBase::d_enqueueCNFCache |
Cache for enqueueCNF() More... | |
CDMap< Expr, bool > | CVC3::SearchImplBase::d_applyCNFRulesCache |
Cache for applyCNFRules() More... | |
CDMap< Expr, Theorem > | CVC3::SearchImplBase::d_replaceITECache |
Cache for replaceITE() More... | |
The search engine includes Boolean reasoning and coordinates with theory reasoning. It consists of a generic abstract API (class SearchEngine) and subclasses implementing concrete instances of search engines.
|
protected |
Create the trusted component.
This function is defined in search_theorem_producer.cpp
Definition at line 46 of file search_theorem_producer.cpp.
Referenced by CVC3::SearchEngine::SearchEngine().
|
protected |
Definition at line 56 of file search_theorem_producer.cpp.
References search_engine.
SearchEngine::SearchEngine | ( | TheoryCore * | core) |
Constructor.
Definition at line 35 of file search.cpp.
References CVC3::SearchEngine::createRules(), CVC3::SearchEngine::d_rules, CVC3::TheoremManager::getFlags(), and CVC3::TheoryCore::getTM().
|
virtual |
|
pure virtual |
Name of this search engine.
Implemented in CVC3::SearchEngineFast, CVC3::SearchSat, and CVC3::SearchSimple.
|
inline |
Accessor for common rules.
Definition at line 84 of file search.h.
References CVC3::SearchEngine::d_commonRules.
|
inline |
Accessor for TheoryCore.
Definition at line 87 of file search.h.
References CVC3::SearchEngine::d_core.
Referenced by CVC3::SearchImplBase::newIntAssumption().
|
pure virtual |
Register an atomic formula of interest.
Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Return next literal implied by last assertion. Null Expr if none.
Returned literals are either registered atomic formulas or their negation
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Push a checkpoint.
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
|
pure virtual |
Restore last checkpoint.
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
|
pure virtual |
Checks the validity of a formula in the current context.
If the query is valid, it returns VALID, the result parameter contains the corresponding theorem, and 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 | the formula to check. |
result | the resulting theorem, if the formula is valid. |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
Reruns last check with e as an additional assumption.
This method should only be called after a query which is invalid.
e | the additional assumption |
result | the resulting theorem, if the query is valid. |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Returns to context immediately before last call to checkValid.
This method should only be called after a query which returns something other than VALID.
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Returns the result of the most recent valid theorem.
Returns Null Theorem if last call was not valid
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().
|
pure virtual |
Generate and add an assumption to the set of assumptions in the current context.
By default, the assumption is added at the current scope. The default can be overridden by specifying the scope parameter.
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Get all user assumptions made in this and all previous contexts.
User assumptions are created either by calls to newUserAssumption or a call to checkValid. In the latter case, the negated query is added as an assumption.
assumptions | should be empty on entry. |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngineTheoremProducer::satProof().
|
pure 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. |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be an empty vector which will be filled \ with the assumptions |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Referenced by CVC3::SearchEngine::getConcreteModel().
|
pure virtual |
Check if the formula has already been assumed previously.
Implemented in CVC3::SearchEngineFast, CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Will return the set of assertions which make the queried formula false.
This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false.
assertions | should be empty on entry. |
inOrder | if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false. |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
pure virtual |
Returns the proof term for the last proven query.
It should be called only after a query which returns VALID. In any other case, it returns Null.
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID.
Definition at line 91 of file search.cpp.
References CVC3::TheoryCore::buildModel(), CVC3::SearchEngine::checkValid(), CVC3::TheoryCore::collectBasicVars(), CVC3::SearchEngine::d_core, CVC3::Theory::falseExpr(), CVC3::SearchEngine::getAssumptions(), CVC3::Theory::getEM(), CVC3::Theorem::getLeafAssumptions(), CVC3::TheoryCore::inconsistentThm(), CVC3::SearchEngine::lastThm(), CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), RAW_LIST, CVC3::TheoryCore::refineCounterExample(), CVC3::Expr::toString(), TRACE, and CVC3::VALID.
bool SearchEngine::tryModelGeneration | ( | Theorem & | thm) |
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent.
Definition at line 57 of file search.cpp.
References CVC3::TheoryCore::buildModel(), CVC3::SearchEngine::checkValid(), CVC3::TheoryCore::collectBasicVars(), CVC3::SearchEngine::d_core, CVC3::Theory::falseExpr(), CVC3::SearchEngine::lastThm(), CVC3::SearchEngine::pop(), CVC3::SearchEngine::push(), CVC3::TheoryCore::refineCounterExample(), and CVC3::VALID.
|
pure virtual |
Implemented in CVC3::SearchSat, and CVC3::SearchImplBase.
|
inlineprotected |
Construct a Literal out of an Expr or return an existing one.
Definition at line 120 of file search_impl_base.h.
References CVC3::SearchImplBase::d_vm.
Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::traceConflict(), and CVC3::SearchEngineFast::unitPropagation().
|
inlineprotected |
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e')
Definition at line 124 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::Theorem::getExpr(), CVC3::Theory::iffMP(), and CVC3::TheoryCore::simplify().
Referenced by CVC3::SearchEngineFast::bcp(), and CVC3::SearchEngineFast::checkValidMain().
|
protectedpure virtual |
Notify the search engine about a new literal fact.
It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of SearchEngine.
IMPORTANT: do not call addFact() from this function; use enqueueFact() or setInconsistent() instead.
Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.
Referenced by CVC3::SearchImplBase::addCNFFact(), and CVC3::DecisionEngine::pushDecision().
|
protectedpure virtual |
Notify the search engine about a new non-literal fact.
It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of SearchEngine.
IMPORTANT: do not call addFact() from this function; use enqueueFact() or setInconsistent() instead.
Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.
Referenced by CVC3::SearchImplBase::addCNFFact().
|
protected |
Add a new fact to the search engine bypassing CNF converter.
Calls either addLiteralFact() or addNonLiteralFact() appropriately, and converts to CNF when d_cnfOption is set. If fromCore==true, this fact already comes from the core, and doesn't need to be reported back to the core.
Definition at line 218 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addLiteralFact(), CVC3::SearchImplBase::addNonLiteralFact(), CVC3::SearchEngine::d_core, CVC3::TheoryCore::enqueueFact(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAbsLiteral(), TRACE, and TRACE_MSG.
Referenced by CVC3::SearchImplBase::addFact(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNF(), and CVC3::SearchImplBase::enqueueCNFrec().
|
inline |
Definition at line 153 of file search_impl_base.h.
References CVC3::SearchImplBase::d_bottomScope.
bool SearchImplBase::isClause | ( | const Expr & | e) |
Check if e is a clause (a literal, or a disjunction of literals)
Definition at line 687 of file search_impl_base.cpp.
References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::isAbsLiteral(), and CVC3::Expr::isOr().
bool SearchImplBase::isPropClause | ( | const Expr & | e) |
Check if e is a propositional clause.
Definition at line 699 of file search_impl_base.cpp.
References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::isOr(), and CVC3::Expr::isPropLiteral().
|
inline |
Check whether e is a fresh variable introduced by the CNF converter.
Search engines do not need to split on those variables in order to be complete
Definition at line 165 of file search_impl_base.h.
References CVC3::SearchImplBase::d_cnfVars.
Referenced by CVC3::SearchImplBase::isGoodSplitter().
bool SearchImplBase::isGoodSplitter | ( | const Expr & | e) |
Check if a splitter is required for completeness.
Currently, it checks that 'e' is not an auxiliary CNF variable
Definition at line 711 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_ignoreCnfVarsOption, CVC3::SearchImplBase::isCNFVar(), CVC3::Expr::isNot(), and TRACE.
Referenced by CVC3::SearchEngineFast::findSplitter(), and CVC3::DecisionEngine::findSplitterRec().
|
private |
Translate theta to CNF and enqueue the new clauses.
Definition at line 360 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::d_origFormulaOption, CVC3::SearchImplBase::enqueueCNFrec(), TRACE, and TRACE_MSG.
Referenced by CVC3::SearchImplBase::addFact().
|
private |
Recursive version of enqueueCNF()
Definition at line 371 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addToCNFCache(), AND, CVC3::CommonProofRules::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::Expr::arity(), CVC3::SearchImplBase::d_cnfVars, CVC3::SearchEngine::d_commonRules, CVC3::SearchImplBase::d_enqueueCNFCache, CVC3::SearchImplBase::d_ifLiftOption, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::getScope(), IFF, CVC3::CommonProofRules::iffMP(), CVC3::int2string(), CVC3::Theorem::isAbsLiteral(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), ITE, CVC3::SearchEngineRules::iteToClauses(), CVC3::CommonProofRules::notNotElim(), OR, CVC3::SearchImplBase::replaceITE(), CVC3::SearchImplBase::scopeLevel(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, TRACE_MSG, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().
Referenced by CVC3::SearchImplBase::enqueueCNF().
|
private |
FIXME: write a comment.
thm | is the input of the form phi <=> v |
Definition at line 563 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addToCNFCache(), AND, CVC3::SearchEngineRules::andCNFRule(), CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), CVC3::SearchImplBase::d_applyCNFRulesCache, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), IFF, CVC3::SearchEngineRules::iffCNFRule(), CVC3::CommonProofRules::iffContrapositive(), CVC3::SearchEngineRules::iffToClauses(), CVC3::SearchEngineRules::impCNFRule(), IMPLIES, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), ITE, CVC3::SearchEngineRules::iteCNFRule(), OR, CVC3::SearchEngineRules::orCNFRule(), CVC3::SearchImplBase::replaceITE(), CVC3::CommonProofRules::substitutivityRule(), CVC3::CommonProofRules::symmetryRule(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, TRACE_MSG, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().
Referenced by CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().
|
private |
Cache a theorem phi <=> v by phi, where v is a literal.
Definition at line 723 of file search_impl_base.cpp.
References CVC3::Statistics::counter(), CVC3::SearchImplBase::d_bottomScope, CVC3::SearchImplBase::d_cnfCache, CVC3::SearchImplBase::d_cnfVars, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::TheoryCore::getStatistics(), CVC3::CommonProofRules::iffContrapositive(), CVC3::Expr::isNot(), CVC3::Theorem::isRewrite(), CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().
Find a theorem phi <=> v by phi, where v is a literal.
Definition at line 750 of file search_impl_base.cpp.
References CVC3::Statistics::counter(), CVC3::SearchImplBase::d_cnfCache, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::TheoryCore::getStatistics(), CVC3::CommonProofRules::iffContrapositive(), CVC3::int2string(), CVC3::Expr::isNot(), CVC3::Theorem::isRewrite(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::Expr::toString(), TRACE, TRACE_MSG, and CVC3::CommonProofRules::transitivityRule().
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::replaceITE().
Replaces ITE subexpressions in e with variables.
Strategy:
For a given atomic formula phi(ite(c, t1, t2)) which depends on a term ITE, generate an equisatisfiable formula:
phi(x) & ite(c, t1=x, t2=x),
where x is a new variable.
The phi(x) part will be generated by the caller, and our job is to assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem phi(ite(c, t1, t2)) <=> phi(x).
Definition at line 804 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, CVC3::SearchImplBase::d_replaceITECache, CVC3::SearchImplBase::findInCNFCache(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::iffMP(), CVC3::Expr::isAbsLiteral(), CVC3::Theorem::isNull(), CVC3::Expr::isPropLiteral(), CVC3::Theorem::isRewrite(), CVC3::CommonProofRules::reflexivityRule(), CVC3::TheoryCore::rewriteLiteral(), TRACE, CVC3::CommonProofRules::transitivityRule(), and CVC3::CommonProofRules::varIntroSkolem().
Referenced by CVC3::SearchImplBase::applyCNFRules(), and CVC3::SearchImplBase::enqueueCNFrec().
|
inlineprotected |
Return the current scope level (for convenience)
Definition at line 192 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::scopeLevel().
Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), and CVC3::SearchEngineFast::traceConflict().
SearchImplBase::SearchImplBase | ( | TheoryCore * | core) |
Constructor.
Definition at line 107 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_coreSatAPI_implBase, CVC3::SearchEngine::d_rules, CVC3::SearchImplBase::d_vm, CVC3::TheoryCore::getCM(), CVC3::TheoryCore::getFlags(), IF_DEBUG, and CVC3::TheoryCore::registerCoreSatAPI().
|
virtual |
Destructor.
Definition at line 132 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_coreSatAPI_implBase, and CVC3::SearchImplBase::d_vm.
|
inlinevirtual |
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::SearchEngine.
Definition at line 200 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::Theory::registerAtom(), and CVC3::Theory::theoryOf().
|
inlinevirtual |
Return next literal implied by last assertion. Null Expr if none.
Returned literals are either registered atomic formulas or their negation
Implements CVC3::SearchEngine.
Definition at line 202 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, and CVC3::TheoryCore::getImpliedLiteral().
|
inlinevirtual |
Push a checkpoint.
Implements CVC3::SearchEngine.
Definition at line 203 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::push().
|
inlinevirtual |
Restore last checkpoint.
Implements CVC3::SearchEngine.
Definition at line 204 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::pop().
|
pure virtual |
Checks the validity of a formula in the current context.
The method that actually calls the SAT solver (implemented in a subclass). It should maintain d_assumptions (add all asserted splitters to it), and set d_lastValid and d_lastCounterExample appropriately before exiting.
Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.
Referenced by CVC3::SearchImplBase::checkValid().
|
virtual |
Similar to checkValidInternal(), only returns Theorem(e) or Null.
Implements CVC3::SearchEngine.
Definition at line 344 of file search_impl_base.cpp.
References CVC3::SearchImplBase::checkValidInternal(), CVC3::CommonProofRules::clearSkolemAxioms(), CVC3::SearchEngine::d_commonRules, and CVC3::SearchImplBase::d_lastValid.
|
pure virtual |
Reruns last check with e as an additional assumption.
Implemented in CVC3::SearchEngineFast, and CVC3::SearchSimple.
Referenced by CVC3::SearchImplBase::restart().
|
virtual |
Reruns last check with e as an additional assumption.
Implements CVC3::SearchEngine.
Definition at line 352 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_lastValid, and CVC3::SearchImplBase::restartInternal().
Referenced by CVC3::SearchImplBase::returnFromCheck().
|
inlinevirtual |
Returns to context immediately before last call to checkValid.
This method should only be called after a query which returns something other than VALID.
Implements CVC3::SearchEngine.
Definition at line 222 of file search_impl_base.h.
References CVC3::SearchEngine::d_core, CVC3::Theory::falseExpr(), and CVC3::SearchImplBase::restart().
|
inlinevirtual |
Returns the result of the most recent valid theorem.
Returns Null Theorem if last call was not valid
Implements CVC3::SearchEngine.
Definition at line 224 of file search_impl_base.h.
References CVC3::SearchImplBase::d_lastValid.
Generate and add a new assertion to the set of assertions in the current context. This should only be used by class VCL in assertFormula().
Implements CVC3::SearchEngine.
Definition at line 141 of file search_impl_base.cpp.
References CVC3::TheoryCore::addFact(), CVC3::CommonProofRules::assumpRule(), CVC3::SearchImplBase::d_assumptions, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, std::endl(), CVC3::TheoryCore::getExprTrans(), IF_DEBUG, CVC3::Theorem::isNull(), CVC3::ExprTransform::preprocess(), CVC3::Expr::setUserAssumption(), and TRACE.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::restartInternal(), and CVC3::SearchEngineFast::restartInternal().
Add a new internal asserion.
Reimplemented in CVC3::SearchEngineFast.
Definition at line 170 of file search_impl_base.cpp.
References CVC3::CommonProofRules::assumpRule(), CVC3::SearchEngine::d_commonRules, CVC3::Expr::isNot(), CVC3::Theorem::setQuantLevel(), and CVC3::SearchEngine::theoryCore().
Referenced by CVC3::SearchEngineFast::newIntAssumption(), and CVC3::DecisionEngine::pushDecision().
void SearchImplBase::newIntAssumption | ( | const Theorem & | thm) |
Helper for above function.
Definition at line 179 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::setIntAssumption(), CVC3::Expr::toString(), and TRACE.
|
virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be an empty vector which will be filled \ with the assumptions |
Implements CVC3::SearchEngine.
Definition at line 189 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions.
|
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::SearchEngine.
Definition at line 197 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions.
Referenced by CVC3::SearchImplBase::getCounterExample().
|
virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be an empty vector which will be filled \ with the assumptions |
Implements CVC3::SearchEngine.
Definition at line 205 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions.
Referenced by CVC3::SearchEngineFast::getCounterExample().
|
virtual |
Check if the formula has been assumed.
Implements CVC3::SearchEngine.
Reimplemented in CVC3::SearchEngineFast.
Definition at line 213 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_assumptions.
Referenced by CVC3::SearchEngineFast::isAssumption().
void SearchImplBase::addFact | ( | const Theorem & | thm) |
Add a new fact to the search engine from the core.
It should be called by TheoryCore::assertFactCore().
Definition at line 231 of file search_impl_base.cpp.
References CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::d_cnfOption, CVC3::SearchImplBase::enqueueCNF(), CVC3::Theorem::getExpr(), TRACE, and TRACE_MSG.
|
virtual |
Suggest a splitter to the SearchEngine.
The higher is the priority, the sooner the SAT solver will split on it. It can be positive or negative (default is 0).
The set of suggested splitters is backtracking; that is, a splitter is "forgotten" once the scope is backtracked.
This method can be used either to change the priority of existing splitters, or to introduce new splitters that DPs consider relevant, even though they do not appear in existing formulas.
Reimplemented in CVC3::SearchEngineFast.
Definition at line 241 of file search_impl_base.cpp.
References CVC3::SearchImplBase::d_dpSplitters, DebugAssert, CVC3::Expr::isAbsLiteral(), CVC3::SearchImplBase::newLiteral(), and CVC3::Expr::toString().
|
virtual |
Will return the set of assertions which make the queried formula false.
This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false.
assertions | should be empty on entry. |
inOrder | if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false. |
Implements CVC3::SearchEngine.
Definition at line 247 of file search_impl_base.cpp.
References CVC3::SearchEngine::d_core, CVC3::SearchImplBase::d_lastValid, CVC3::SearchImplBase::getInternalAssumptions(), CVC3::TheoryCore::getTM(), CVC3::Theorem::isNull(), and CVC3::TheoremManager::withAssumptions().
Referenced by CVC3::SearchEngineFast::getCounterExample().
|
virtual |
Returns the proof term for the last proven query.
It should be called only after a checkValid which returns true. In any other case, it returns Null.
Implements CVC3::SearchEngine.
Definition at line 282 of file search_impl_base.cpp.
References CVC3::SearchEngine::d_core, CVC3::SearchImplBase::d_lastValid, CVC3::Theorem::getProof(), CVC3::TheoryCore::getTM(), CVC3::Theorem::isNull(), and CVC3::TheoremManager::withProof().
|
virtual |
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
It should be called only after a checkValid which returns true. In any other case, it returns Null.
Definition at line 297 of file search_impl_base.cpp.
References CVC3::SearchEngine::d_core, CVC3::SearchImplBase::d_lastValid, CVC3::Assumptions::emptyAssump(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoryCore::getTM(), CVC3::Theorem::isNull(), and CVC3::TheoremManager::withAssumptions().
Process result of checkValid.
Given a proof of FALSE ('res') from an assumption 'e', derive the proof of the inverse of e.
res | is a proof of FALSE |
e | is the assumption used in the above proof |
Definition at line 317 of file search_impl_base.cpp.
References CVC3::ExprHashMap< Data >::clear(), CVC3::SearchEngine::d_commonRules, CVC3::SearchImplBase::d_lastCounterExample, CVC3::SearchImplBase::d_lastValid, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::SearchEngineRules::eliminateSkolemAxioms(), CVC3::ExprHashMap< Data >::erase(), CVC3::Theorem::getExpr(), CVC3::CommonProofRules::getSkolemAxioms(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Theorem::isNull(), CVC3::SearchEngineRules::negIntro(), CVC3::SearchEngineRules::proofByContradiction(), and CVC3::Theorem::toString().
Referenced by CVC3::SearchSimple::checkValidMain(), and CVC3::SearchEngineFast::checkValidMain().
|
inlinevirtual |
Implements CVC3::SearchEngine.
Definition at line 286 of file search_impl_base.h.
References FatalAssert, and CVC3::UNKNOWN_VAL.
|
protected |
Access to theory reasoning.
Definition at line 58 of file search.h.
Referenced by CVC3::SearchImplBase::addCNFFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkSAT(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::commitFacts(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchEngine::getConcreteModel(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchImplBase::getImpliedLiteral(), CVC3::SearchSat::getImpliedLiteral(), CVC3::SearchImplBase::getProof(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::SearchImplBase::pop(), CVC3::Circuit::propagate(), CVC3::SearchImplBase::push(), CVC3::SearchImplBase::registerAtom(), CVC3::SearchSat::registerAtom(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::SearchImplBase::returnFromCheck(), CVC3::SearchImplBase::scopeLevel(), CVC3::SearchEngineFast::setInconsistent(), CVC3::SearchImplBase::simplify(), CVC3::SearchEngineFast::split(), CVC3::SearchEngine::theoryCore(), and CVC3::SearchEngine::tryModelGeneration().
|
protected |
Common proof rules.
Definition at line 61 of file search.h.
Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchSimple::addNonLiteralFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchEngineFast::bcp(), CVC3::SearchImplBase::checkValid(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngine::getCommonRules(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::SearchImplBase::processResult(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchImplBase::replaceITE(), CVC3::SearchSimple::SearchSimple(), and CVC3::SearchEngineFast::split().
|
protected |
Proof rules for the search engine.
Definition at line 64 of file search.h.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::processResult(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngine::SearchEngine(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchEngineFast::unitPropagation(), and CVC3::SearchEngine::~SearchEngine().
|
protected |
Variable manager for classes Variable and Literal.
Definition at line 44 of file search_impl_base.h.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::Circuit::Circuit(), CVC3::SearchImplBase::newLiteral(), CVC3::SearchImplBase::SearchImplBase(), and CVC3::SearchImplBase::~SearchImplBase().
|
protected |
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid).
Definition at line 49 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchImplBase::getBottomScope(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::SearchEngineFast::traceConflict().
|
protected |
Definition at line 51 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::SearchImplBase(), and CVC3::SearchImplBase::~SearchImplBase().
|
protected |
Backtracking ordered set of DP-suggested splitters.
Definition at line 74 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::addSplitter(), and CVC3::SearchEngineFast::addSplitter().
|
protected |
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
Definition at line 78 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::checkValid(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchImplBase::getProof(), CVC3::SearchImplBase::lastThm(), CVC3::SearchImplBase::processResult(), and CVC3::SearchImplBase::restart().
|
protected |
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
Definition at line 81 of file search_impl_base.h.
Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), and CVC3::SearchImplBase::processResult().
|
protected |
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
Definition at line 84 of file search_impl_base.h.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::getAssumptions(), CVC3::SearchImplBase::getInternalAssumptions(), CVC3::SearchImplBase::getUserAssumptions(), CVC3::SearchImplBase::isAssumption(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::SearchImplBase::SearchImplBase().
|
protected |
Backtracking cache for the CNF generator.
Definition at line 87 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::addToCNFCache(), and CVC3::SearchImplBase::findInCNFCache().
|
protected |
Backtracking set of new variables generated by CNF translator.
Specific search engines do not have to split on these variables
Definition at line 90 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchImplBase::isCNFVar().
|
protected |
Command line flag whether to convert to CNF.
Definition at line 92 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::addFact().
|
protected |
Flag: whether to convert term ITEs into CNF.
Definition at line 94 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::enqueueCNFrec().
|
protected |
Flag: ignore auxiliary CNF variables when searching for a splitter.
Definition at line 96 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::isGoodSplitter().
|
protected |
Flag: Preserve the original formula with +cnf (for splitter heuristics)
Definition at line 98 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::enqueueCNF().
|
protected |
Cache for enqueueCNF()
Definition at line 112 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::enqueueCNFrec().
|
protected |
Cache for applyCNFRules()
Definition at line 114 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::applyCNFRules().
|
protected |
Cache for replaceITE()
Definition at line 116 of file search_impl_base.h.
Referenced by CVC3::SearchImplBase::replaceITE().