CVC3::DecisionEngineMBTF Class Reference

#include <decision_engine_mbtf.h>

Inherits CVC3::DecisionEngine.

Collaboration diagram for CVC3::DecisionEngineMBTF:

List of all members.

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'.
  

Protected Member Functions

• virtual bool isBetter (const Expr &e1, const Expr &e2)

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

---

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

(

)

[inline, virtual]

Definition at line 50 of file decision_engine_mbtf.h.

---

Member Function Documentation

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

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