Simple Search Engine
[Search Engine]

Collaboration diagram for Simple Search Engine:

Classes

Functions

Variables


Detailed Description

This module includes all the components of a very simplistic search engine. It is used mainly for debugging purposes.

Function Documentation

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().


Variable Documentation

std::string CVC3::SearchSimple::d_name [private, inherited]

Name.

Definition at line 47 of file search_simple.h.

Referenced by CVC3::SearchSimple::getName().

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().


Generated on Wed Nov 18 16:14:13 2009 for CVC3 by  doxygen 1.5.2