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]

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

SearchSimple::SearchSimple ( TheoryCore core  )  [inherited]

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]

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

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]

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

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

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 Thu Oct 15 22:17:16 2009 for CVC3 by  doxygen 1.5.8