CVC3
2.4.1
|
Classes | |
class | CVC3::SearchSimple |
Implementation of the simple search engine. More... | |
Functions | |
QueryResult | CVC3::SearchSimple::checkValidRec (Theorem &thm) |
Recursive DPLL algorithm used by checkValid. More... | |
QueryResult | CVC3::SearchSimple::checkValidMain (const Expr &e2) |
Private helper function for checkValid and restart. More... | |
CVC3::SearchSimple::SearchSimple (TheoryCore *core) | |
Constructor. More... | |
CVC3::SearchSimple::~SearchSimple () | |
Destructor. More... | |
const std::string & | CVC3::SearchSimple::getName () |
Name of this search engine. More... | |
QueryResult | CVC3::SearchSimple::checkValidInternal (const Expr &e) |
Checks the validity of a formula in the current context. More... | |
QueryResult | CVC3::SearchSimple::restartInternal (const Expr &e) |
Reruns last check with e as an additional assumption. More... | |
void | CVC3::SearchSimple::addLiteralFact (const Theorem &thm) |
Notify the search engine about a new literal fact. More... | |
void | CVC3::SearchSimple::addNonLiteralFact (const Theorem &thm) |
Notify the search engine about a new non-literal fact. More... | |
Variables | |
std::string | CVC3::SearchSimple::d_name |
Name. More... | |
DecisionEngine * | CVC3::SearchSimple::d_decisionEngine |
Decision Engine. More... | |
CDO< Theorem > | CVC3::SearchSimple::d_goal |
Formula being checked. More... | |
CDO< Theorem > | CVC3::SearchSimple::d_nonLiterals |
Non-literals generated by DP's. More... | |
CDO< Theorem > | CVC3::SearchSimple::d_simplifiedThm |
Theorem which records simplification of the last query. More... | |
This module includes all the components of a very simplistic search engine. It is used mainly for debugging purposes.
|
private |
Recursive DPLL algorithm used by checkValid.
Definition at line 37 of file search_simple.cpp.
References CVC3::ABORT, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::hasFind(), CVC3::Expr::isFalse(), CVC3::Expr::isNull(), CVC3::Expr::isTrue(), SATISFIABLE, TRACE, TRACE_MSG, and UNSATISFIABLE.
Referenced by CVC3::SearchSimple::checkValidMain().
|
private |
Private helper function for checkValid and restart.
Definition at line 126 of file search_simple.cpp.
References CVC3::SearchSimple::checkValidRec(), CVC3::ExprHashMap< Data >::clear(), CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, CVC3::SearchSimple::d_goal, CVC3::SearchImplBase::d_lastCounterExample, CVC3::SearchImplBase::d_lastValid, CVC3::SearchSimple::d_simplifiedThm, DebugAssert, CVC3::TheoryCore::getCM(), CVC3::CommonProofRules::iffContrapositive(), CVC3::CommonProofRules::iffMP(), CVC3::TheoryCore::incomplete(), CVC3::ContextManager::pop(), CVC3::SearchImplBase::processResult(), CVC3::SATISFIABLE, CVC3::CommonProofRules::symmetryRule(), TRACE, TRACE_MSG, CVC3::UNKNOWN, and CVC3::UNSATISFIABLE.
Referenced by CVC3::SearchSimple::checkValidInternal(), and CVC3::SearchSimple::restartInternal().
SearchSimple::SearchSimple | ( | TheoryCore * | core) |
Constructor.
Definition at line 101 of file search_simple.cpp.
References CVC3::SearchEngine::d_commonRules, CVC3::SearchSimple::d_decisionEngine, CVC3::SearchSimple::d_goal, CVC3::SearchSimple::d_nonLiterals, and CVC3::CommonProofRules::trueTheorem().
SearchSimple::~SearchSimple | ( | ) |
Destructor.
Definition at line 120 of file search_simple.cpp.
References CVC3::SearchSimple::d_decisionEngine.
|
inlinevirtual |
Name of this search engine.
Implements CVC3::SearchEngine.
Definition at line 71 of file search_simple.h.
References CVC3::SearchSimple::d_name.
|
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.
Implements CVC3::SearchImplBase.
Definition at line 165 of file search_simple.cpp.
References CVC3::TheoryCore::addFact(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngine::d_core, CVC3::SearchSimple::d_goal, CVC3::SearchSimple::d_nonLiterals, CVC3::SearchSimple::d_simplifiedThm, DebugAssert, CVC3::TheoryCore::getCM(), CVC3::TheoryCore::getExprTrans(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::negate(), CVC3::SearchImplBase::newUserAssumption(), CVC3::ExprTransform::preprocess(), CVC3::ContextManager::push(), CVC3::SearchImplBase::scopeLevel(), CVC3::Type::toString(), CVC3::Expr::toString(), TRACE, and TRACE_MSG.
|
virtual |
Reruns last check with e as an additional assumption.
Implements CVC3::SearchImplBase.
Definition at line 207 of file search_simple.cpp.
References CVC3::TheoryCore::addFact(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngine::d_core, CVC3::SearchSimple::d_simplifiedThm, CVC3::TheoryCore::getCM(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::SearchImplBase::newUserAssumption(), CVC3::ContextManager::popto(), CVC3::Type::toString(), CVC3::Expr::toString(), TRACE, and TRACE_MSG.
|
inlinevirtual |
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.
Implements CVC3::SearchImplBase.
Definition at line 74 of file search_simple.h.
|
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.
Implements CVC3::SearchImplBase.
Definition at line 237 of file search_simple.cpp.
References CVC3::CommonProofRules::andIntro(), CVC3::SearchEngine::d_commonRules, and CVC3::SearchSimple::d_nonLiterals.
|
private |
|
private |
Decision Engine.
Definition at line 50 of file search_simple.h.
Referenced by CVC3::SearchSimple::SearchSimple(), and CVC3::SearchSimple::~SearchSimple().
|
private |
Formula being checked.
Definition at line 53 of file search_simple.h.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), and CVC3::SearchSimple::SearchSimple().
|
private |
Non-literals generated by DP's.
Definition at line 55 of file search_simple.h.
Referenced by CVC3::SearchSimple::addNonLiteralFact(), CVC3::SearchSimple::checkValidInternal(), and CVC3::SearchSimple::SearchSimple().
|
private |
Theorem which records simplification of the last query.
Definition at line 57 of file search_simple.h.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), and CVC3::SearchSimple::restartInternal().