CVC3  2.4.1
Public Member Functions | Protected Member Functions | List of all members
CVC3::DecisionEngineDFS Class Reference

Decision Engine for use with the Search EngineAuthor: Clark Barrett. More...

#include <decision_engine_dfs.h>

Inheritance diagram for CVC3::DecisionEngineDFS:
CVC3::DecisionEngine

Public Member Functions

 DecisionEngineDFS (TheoryCore *core, SearchImplBase *se)
 Constructor. More...
 
virtual ~DecisionEngineDFS ()
 
virtual Expr findSplitter (const Expr &e)
 Find the next splitter. More...
 
virtual void goalSatisfied ()
 Search should call this when it derives 'false'. More...
 
- Public Member Functions inherited from CVC3::DecisionEngine
 DecisionEngine (TheoryCore *core, SearchImplBase *se)
 
virtual ~DecisionEngine ()
 
void pushDecision (Expr splitter, bool whichCase=true)
 Push context and record the splitter. More...
 
void popDecision ()
 Pop last decision (and context) More...
 
void popTo (int dl)
 Pop to given scope. More...
 
Expr lastSplitter ()
 Return the last known splitter. More...
 

Protected Member Functions

virtual bool isBetter (const Expr &e1, const Expr &e2)
 
- Protected Member Functions inherited from CVC3::DecisionEngine
Expr findSplitterRec (const Expr &e)
 

Additional Inherited Members

- Protected Attributes inherited from CVC3::DecisionEngine
TheoryCored_core
 Pointer to core theory. More...
 
SearchImplBased_se
 Pointer to search engine. More...
 
CDList< Exprd_splitters
 List of currently active splitters. More...
 
StatCounter d_splitterCount
 Total number of splitters. More...
 
ExprMap< Exprd_bestByExpr
 
ExprMap< Exprd_visited
 Visited cache for findSplitterRec traversal. More...
 

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

Definition at line 49 of file decision_engine_dfs.h.

Member Function Documentation

bool DecisionEngineDFS::isBetter ( const Expr e1,
const Expr e2 
)
protectedvirtual

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.

Function: DecisionEngineDFS::findSplitter

Author: Clark Barrett

Created: Sun Jul 13 22:53:18 2003

Main function to choose the next splitter.

Returns
NULL if all known splitters are assigned.

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 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: