Simple Search Engine
[Search Engine]

Collaboration diagram for Simple Search Engine:

Classes

• class CVCL::SearchSimple

  Implementation of the simple search engine. More...
  

Functions

• Theorem CVCL::SearchSimple::checkValidRec ()

  Recursive DPLL algorithm used by checkValid.
  

• bool CVCL::SearchSimple::checkValidMain (const Expr &e2)

  Private helper function for checkValid and restart.
  

• CVCL::SearchSimple::SearchSimple (TheoryCore *core)

  Constructor.
  

• CVCL::SearchSimple::~SearchSimple ()

  Destructor.
  

• const std::string & CVCL::SearchSimple::getName ()

  Name of this search engine.
  

• bool CVCL::SearchSimple::checkValidInternal (const Expr &e)

  Checks the validity of a formula in the current context.
  

• bool CVCL::SearchSimple::restartInternal (const Expr &e)

  Reruns last check with e as an additional assumption.
  

• void CVCL::SearchSimple::addLiteralFact (const Theorem &thm)

  Notify the search engine about a new literal fact.
  

• void CVCL::SearchSimple::addNonLiteralFact (const Theorem &thm)

  Notify the search engine about a new non-literal fact.
  

Variables

• std::string CVCL::SearchSimple::d_name

  Name.
  

• DecisionEngine * CVCL::SearchSimple::d_decisionEngine

  Decision Engine.
  

• CDO< Theorem > CVCL::SearchSimple::d_goal

  Formula being checked.
  

• CDO< Theorem > CVCL::SearchSimple::d_nonLiterals

  Non-literals generated by DP's.
  

• CDO< Theorem > CVCL::SearchSimple::d_simplifiedThm

  Theorem which records simplification of the last query.
  

---

Detailed Description

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

---

Function Documentation

Theorem SearchSimple::checkValidRec (   )  [private, inherited]

Recursive DPLL algorithm used by checkValid. Definition at line 45 of file search_simple.cpp. References CVCL::SearchEngineRules::caseSplit(), CVCL::TheoryCore::checkSATCore(), CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::SearchSimple::d_decisionEngine, CVCL::SearchSimple::d_goal, CVCL::SearchSimple::d_nonLiterals, CVCL::SearchEngine::d_rules, CVCL::Theory::find(), CVCL::DecisionEngine::findSplitter(), CVCL::CDO< T >::get(), CVCL::Theorem::getExpr(), CVCL::DecisionEngine::goalSatisfied(), CVCL::Expr::hasFind(), CVCL::CommonProofRules::iffMP(), CVCL::TheoryCore::inconsistent(), CVCL::TheoryCore::inconsistentThm(), CVCL::Expr::isFalse(), CVCL::Theorem::isNull(), CVCL::Expr::isNull(), CVCL::Expr::isTrue(), CVCL::DecisionEngine::popDecision(), CVCL::DecisionEngine::pushDecision(), CVCL::CDO< T >::set(), CVCL::SearchImplBase::simplify(), and CVCL::TRACE. Referenced by CVCL::SearchSimple::checkValidMain().

bool SearchSimple::checkValidMain (  const Expr &  e2  )  [private, inherited]

Private helper function for checkValid and restart. Definition at line 134 of file search_simple.cpp. References CVCL::SearchSimple::checkValidRec(), CVCL::ExprHashMap< Data >::clear(), CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::SearchSimple::d_goal, CVCL::SearchImplBase::d_lastCounterExample, CVCL::SearchImplBase::d_lastValid, CVCL::SearchSimple::d_simplifiedThm, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLeafAssumptions(), CVCL::CommonProofRules::iffContrapositive(), CVCL::CommonProofRules::iffMP(), CVCL::Theorem::isNull(), CVCL::Expr::isTrue(), CVCL::ContextManager::pop(), CVCL::SearchImplBase::processResult(), CVCL::CommonProofRules::symmetryRule(), and CVCL::TRACE. Referenced by CVCL::SearchSimple::checkValidInternal(), and CVCL::SearchSimple::restartInternal().

SearchSimple::SearchSimple (  TheoryCore *  core  )  [inherited]

Constructor. Definition at line 109 of file search_simple.cpp. References CVCL::SearchEngine::d_commonRules, CVCL::SearchSimple::d_decisionEngine, CVCL::SearchSimple::d_goal, CVCL::SearchSimple::d_nonLiterals, CVCL::TheoryCore::getFlags(), CVCL::CDO< T >::set(), and CVCL::CommonProofRules::trueTheorem().

SearchSimple::~SearchSimple (   )  [inherited]

Destructor. Definition at line 128 of file search_simple.cpp. References CVCL::SearchSimple::d_decisionEngine.

const std::string& CVCL::SearchSimple::getName (   )  [inline, virtual, inherited]

Name of this search engine. Implements CVCL::SearchEngine. Definition at line 79 of file search_simple.h. References CVCL::SearchSimple::d_name.

bool 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 CVCL::SearchImplBase. Definition at line 169 of file search_simple.cpp. References CVCL::TheoryCore::addFact(), CVCL::SearchSimple::checkValidMain(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::SearchImplBase::d_assumptions, CVCL::SearchImplBase::d_bottomScope, CVCL::SearchEngine::d_core, CVCL::SearchSimple::d_goal, CVCL::SearchSimple::d_nonLiterals, CVCL::SearchSimple::d_simplifiedThm, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::getExprTrans(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isTrue(), CVCL::Expr::negate(), CVCL::SearchImplBase::newUserAssumption(), CVCL::ExprTransform::preprocess(), CVCL::ContextManager::push(), CVCL::SearchImplBase::scopeLevel(), CVCL::CDO< T >::set(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

bool SearchSimple::restartInternal (  const Expr &  e  )  [virtual, inherited]

Reruns last check with e as an additional assumption. Implements CVCL::SearchImplBase. Definition at line 211 of file search_simple.cpp. References CVCL::TheoryCore::addFact(), CVCL::SearchSimple::checkValidMain(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::SearchImplBase::d_assumptions, CVCL::SearchImplBase::d_bottomScope, CVCL::SearchEngine::d_core, CVCL::SearchSimple::d_simplifiedThm, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::negate(), CVCL::SearchImplBase::newUserAssumption(), CVCL::ContextManager::popto(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

void CVCL::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 CVCL::SearchImplBase. Definition at line 82 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 CVCL::SearchImplBase. Definition at line 241 of file search_simple.cpp. References CVCL::CommonProofRules::andIntro(), CVCL::SearchEngine::d_commonRules, CVCL::SearchSimple::d_nonLiterals, CVCL::CDO< T >::get(), and CVCL::CDO< T >::set().

---

Variable Documentation

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

Name. Definition at line 55 of file search_simple.h. Referenced by CVCL::SearchSimple::getName().

DecisionEngine* CVCL::SearchSimple::d_decisionEngine [private, inherited]

Decision Engine. Definition at line 58 of file search_simple.h. Referenced by CVCL::SearchSimple::checkValidRec(), CVCL::SearchSimple::SearchSimple(), and CVCL::SearchSimple::~SearchSimple().

CDO<Theorem> CVCL::SearchSimple::d_goal [private, inherited]

Formula being checked. Definition at line 61 of file search_simple.h. Referenced by CVCL::SearchSimple::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchSimple::checkValidRec(), and CVCL::SearchSimple::SearchSimple().

CDO<Theorem> CVCL::SearchSimple::d_nonLiterals [private, inherited]

Non-literals generated by DP's. Definition at line 63 of file search_simple.h. Referenced by CVCL::SearchSimple::addNonLiteralFact(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchSimple::checkValidRec(), and CVCL::SearchSimple::SearchSimple().

CDO<Theorem> CVCL::SearchSimple::d_simplifiedThm [private, inherited]

Theorem which records simplification of the last query. Definition at line 65 of file search_simple.h. Referenced by CVCL::SearchSimple::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), and CVCL::SearchSimple::restartInternal().

---