CVC3: CVC3::DecisionEngineDFS Class Reference

CVC3

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

#include <decision_engine_dfs.h>

Inherits CVC3::DecisionEngine.

Collaboration diagram for CVC3::DecisionEngineDFS:

Collaboration graph

Public Member Functions
	DecisionEngineDFS (TheoryCore core, SearchImplBase se)
	Constructor.

virtual	~DecisionEngineDFS ()

virtual Expr	findSplitter (const Expr &e)
	Find the next splitter.

virtual void	goalSatisfied ()
	Search should call this when it derives 'false'.

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.

void	popDecision ()
	Pop last decision (and context)

void	popTo (int dl)
	Pop to given scope.

Expr	lastSplitter ()
	Return the last known splitter.

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
TheoryCore *	d_core
	Pointer to core theory.

SearchImplBase *	d_se
	Pointer to search engine.

CDList< Expr >	d_splitters
	List of currently active splitters.

StatCounter	d_splitterCount
	Total number of splitters.

ExprMap< Expr >	d_bestByExpr

ExprMap< Expr >	d_visited
	Visited cache for findSplitterRec traversal.

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: