Simple Search Engine
[Search Engine]

Collaboration diagram for Simple Search Engine:

Classes

• class CVC3::SearchSimple

  Implementation of the simple search engine. More...
  

Functions

• QueryResult CVC3::SearchSimple::checkValidRec (Theorem &thm)

  Recursive DPLL algorithm used by checkValid.
  

• QueryResult CVC3::SearchSimple::checkValidMain (const Expr &e2)

  Private helper function for checkValid and restart.
  

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

  Constructor.
  

• CVC3::SearchSimple::~SearchSimple ()

  Destructor.
  

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

  Name of this search engine.
  

• QueryResult CVC3::SearchSimple::checkValidInternal (const Expr &e)

  Checks the validity of a formula in the current context.
  

• QueryResult CVC3::SearchSimple::restartInternal (const Expr &e)

  Reruns last check with e as an additional assumption.
  

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

  Notify the search engine about a new literal fact.
  

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

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

Variables

• std::string CVC3::SearchSimple::d_name

  Name.
  

• DecisionEngine * CVC3::SearchSimple::d_decisionEngine

  Decision Engine.
  

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

  Formula being checked.
  

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

  Non-literals generated by DP's.
  

• CDO< Theorem > CVC3::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

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