CVC3
Classes | Functions | Variables
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
QueryResult SearchSimple::checkValidMain ( const Expr e2)
private
SearchSimple::SearchSimple ( TheoryCore core)
SearchSimple::~SearchSimple ( )

Destructor.

Definition at line 120 of file search_simple.cpp.

References CVC3::SearchSimple::d_decisionEngine.

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

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
QueryResult SearchSimple::restartInternal ( const Expr e)
virtual
void CVC3::SearchSimple::addLiteralFact ( const Theorem thm)
inlinevirtual

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

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

Name.

Definition at line 47 of file search_simple.h.

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

DecisionEngine* CVC3::SearchSimple::d_decisionEngine
private

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
CDO<Theorem> CVC3::SearchSimple::d_nonLiterals
private

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

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