|
Collaboration diagram for Simple Search Engine:
|
|
| QueryResult SearchSimple::checkValidRec | ( | Theorem & | thm | ) | [private, inherited] |
Recursive DPLL algorithm used by checkValid.
Definition at line 37 of file search_simple.cpp.
References CVC3::ABORT, CVC3::SearchEngineRules::caseSplit(), CVC3::TheoryCore::checkSATCore(), CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, CVC3::SearchSimple::d_decisionEngine, CVC3::SearchSimple::d_goal, CVC3::SearchSimple::d_nonLiterals, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::Theory::find(), CVC3::DecisionEngine::findSplitter(), CVC3::CDO< T >::get(), CVC3::Theorem::getExpr(), CVC3::DecisionEngine::goalSatisfied(), CVC3::Expr::hasFind(), CVC3::CommonProofRules::iffMP(), CVC3::TheoryCore::inconsistent(), CVC3::TheoryCore::inconsistentThm(), CVC3::Expr::isFalse(), CVC3::Expr::isNull(), CVC3::Expr::isTrue(), CVC3::TheoryCore::outOfResources(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::pushDecision(), CVC3::SATISFIABLE, CVC3::CDO< T >::set(), CVC3::SearchImplBase::simplify(), CVC3::TRACE, TRACE_MSG, and CVC3::UNSATISFIABLE.
Referenced by CVC3::SearchSimple::checkValidMain().
| QueryResult SearchSimple::checkValidMain | ( | const Expr & | e2 | ) | [private, inherited] |
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::CDO< T >::get(), CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::CommonProofRules::iffContrapositive(), CVC3::CommonProofRules::iffMP(), CVC3::TheoryCore::incomplete(), CVC3::Expr::isTrue(), CVC3::ContextManager::pop(), CVC3::SearchImplBase::processResult(), CVC3::SATISFIABLE, CVC3::CommonProofRules::symmetryRule(), CVC3::TRACE, TRACE_MSG, CVC3::UNKNOWN, and CVC3::UNSATISFIABLE.
Referenced by CVC3::SearchSimple::checkValidInternal(), and CVC3::SearchSimple::restartInternal().
| SearchSimple::SearchSimple | ( | TheoryCore * | core | ) | [inherited] |
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, CVC3::CDO< T >::set(), and CVC3::CommonProofRules::trueTheorem().
| SearchSimple::~SearchSimple | ( | ) | [inherited] |
Destructor.
Definition at line 120 of file search_simple.cpp.
References CVC3::SearchSimple::d_decisionEngine.
| const std::string& CVC3::SearchSimple::getName | ( | ) | [inline, virtual, inherited] |
Name of this search engine.
Implements CVC3::SearchEngine.
Definition at line 71 of file search_simple.h.
References CVC3::SearchSimple::d_name.
| QueryResult SearchSimple::checkValidInternal | ( | const Expr & | e | ) | [virtual, inherited] |
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::CDMap< Key, Data, HashFcn >::count(), 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::CDO< T >::get(), CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getExprTrans(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isTrue(), CVC3::Expr::negate(), CVC3::SearchImplBase::newUserAssumption(), CVC3::ExprTransform::preprocess(), CVC3::ContextManager::push(), CVC3::SearchImplBase::scopeLevel(), CVC3::CDO< T >::set(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::TRACE, and TRACE_MSG.
| QueryResult SearchSimple::restartInternal | ( | const Expr & | e | ) | [virtual, inherited] |
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::CDMap< Key, Data, HashFcn >::count(), CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngine::d_core, CVC3::SearchSimple::d_simplifiedThm, CVC3::CDO< T >::get(), CVC3::TheoryCore::getCM(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::negate(), CVC3::SearchImplBase::newUserAssumption(), CVC3::ContextManager::popto(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::TRACE, and TRACE_MSG.
| void CVC3::SearchSimple::addLiteralFact | ( | const Theorem & | thm | ) | [inline, virtual, inherited] |
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.
| void SearchSimple::addNonLiteralFact | ( | const Theorem & | thm | ) | [virtual, inherited] |
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, CVC3::SearchSimple::d_nonLiterals, CVC3::CDO< T >::get(), and CVC3::CDO< T >::set().
std::string CVC3::SearchSimple::d_name [private, inherited] |
DecisionEngine* CVC3::SearchSimple::d_decisionEngine [private, inherited] |
Decision Engine.
Definition at line 50 of file search_simple.h.
Referenced by CVC3::SearchSimple::checkValidRec(), CVC3::SearchSimple::SearchSimple(), and CVC3::SearchSimple::~SearchSimple().
CDO<Theorem> CVC3::SearchSimple::d_goal [private, inherited] |
Formula being checked.
Definition at line 53 of file search_simple.h.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchSimple::checkValidRec(), and CVC3::SearchSimple::SearchSimple().
CDO<Theorem> CVC3::SearchSimple::d_nonLiterals [private, inherited] |
Non-literals generated by DP's.
Definition at line 55 of file search_simple.h.
Referenced by CVC3::SearchSimple::addNonLiteralFact(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchSimple::checkValidRec(), and CVC3::SearchSimple::SearchSimple().
CDO<Theorem> CVC3::SearchSimple::d_simplifiedThm [private, inherited] |
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().
1.5.2