CVC3::DecisionEngineDFS Class Reference
[Decision Engine]

Decision Engine for use with the Search Engine. More...

#include <decision_engine_dfs.h>

Inheritance diagram for CVC3::DecisionEngineDFS:

Inheritance graph
[legend]
Collaboration diagram for CVC3::DecisionEngineDFS:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions


Detailed Description

Decision Engine for use with the Search Engine.

Author: Clark Barrett

Created: Fri Jul 11 16:34:22 2003

Definition at line 41 of file decision_engine_dfs.h.


Constructor & Destructor Documentation

DecisionEngineDFS::DecisionEngineDFS ( TheoryCore core,
SearchImplBase se 
)

Constructor.

Function: DecisionEngineDFS::DecisionEngineDFS

Author: Clark Barrett

Created: Sun Jul 13 22:52:51 2003

Constructor

Definition at line 49 of file decision_engine_dfs.cpp.

virtual CVC3::DecisionEngineDFS::~DecisionEngineDFS (  )  [inline, virtual]

Definition at line 49 of file decision_engine_dfs.h.


Member Function Documentation

bool DecisionEngineDFS::isBetter ( const Expr e1,
const Expr e2 
) [protected, virtual]

Implements CVC3::DecisionEngine.

Definition at line 32 of file decision_engine_dfs.cpp.

Expr DecisionEngineDFS::findSplitter ( const Expr e  )  [virtual]

Find the next splitter.

Returns:
Null Expr if no splitter is found.

Implements CVC3::DecisionEngine.

Definition at line 67 of file decision_engine_dfs.cpp.

References CVC3::ExprMap< Data >::clear(), CVC3::DecisionEngine::d_visited, CVC3::DecisionEngine::findSplitterRec(), IF_DEBUG, CVC3::Expr::isNull(), and CVC3::TRACE.

void DecisionEngineDFS::goalSatisfied (  )  [virtual]

Search should call this when it derives 'false'.

Implements CVC3::DecisionEngine.

Definition at line 88 of file decision_engine_dfs.cpp.


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:17:46 2009 for CVC3 by  doxygen 1.5.2