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

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