CVC3::DecisionEngineMBTF Class Reference

#include <decision_engine_mbtf.h>

Inherits CVC3::DecisionEngine.

Collaboration diagram for CVC3::DecisionEngineMBTF:

Classes
class	CacheEntry

Public Member Functions
	DecisionEngineMBTF (TheoryCore *core, SearchImplBase *se)
virtual	~DecisionEngineMBTF ()
virtual Expr	findSplitter (const Expr &e)
	Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur.
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)

Private Attributes
int	d_startLevel
int	d_bottomLevel
int	d_topLevel
bool	d_topLevelLock
int	d_height
std::vector< CacheEntry >	d_cache
ExprMap< int >	d_index

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

Definition at line 24 of file decision_engine_mbtf.h.

Constructor & Destructor Documentation

CVC3::DecisionEngineMBTF::DecisionEngineMBTF	(	TheoryCore *	core,
		SearchImplBase *	se
	)

virtual CVC3::DecisionEngineMBTF::~DecisionEngineMBTF ( )

inlinevirtual

Definition at line 50 of file decision_engine_mbtf.h.

Member Function Documentation

virtual bool CVC3::DecisionEngineMBTF::isBetter ( const Expr &  e1, const Expr &  e2  )

protectedvirtual

Implements CVC3::DecisionEngine.

virtual Expr CVC3::DecisionEngineMBTF::findSplitter ( const Expr &  e )

virtual

Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur.

Returns

Null Expr if passed in a Null Expr.

Implements CVC3::DecisionEngine.

virtual void CVC3::DecisionEngineMBTF::goalSatisfied ( )

virtual

Search should call this when it derives 'false'.

Implements CVC3::DecisionEngine.

Member Data Documentation

int CVC3::DecisionEngineMBTF::d_startLevel

private

Definition at line 36 of file decision_engine_mbtf.h.

int CVC3::DecisionEngineMBTF::d_bottomLevel

private

Definition at line 37 of file decision_engine_mbtf.h.

int CVC3::DecisionEngineMBTF::d_topLevel

private

Definition at line 38 of file decision_engine_mbtf.h.

bool CVC3::DecisionEngineMBTF::d_topLevelLock

private

Definition at line 39 of file decision_engine_mbtf.h.

int CVC3::DecisionEngineMBTF::d_height

private

Definition at line 40 of file decision_engine_mbtf.h.

std::vector<CacheEntry> CVC3::DecisionEngineMBTF::d_cache

private

Definition at line 42 of file decision_engine_mbtf.h.

ExprMap<int> CVC3::DecisionEngineMBTF::d_index

private

Definition at line 43 of file decision_engine_mbtf.h.

---

The documentation for this class was generated from the following file:

• decision_engine_mbtf.h