CVCL::DecisionEngineMBTF Class Reference

#include <decision_engine_mbtf.h>

Inheritance diagram for CVCL::DecisionEngineMBTF:

[legend]Collaboration diagram for CVCL::DecisionEngineMBTF:

[legend]List of all members.

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

Classes

• class CacheEntry

---

Detailed Description

Definition at line 32 of file decision_engine_mbtf.h.

---

Constructor & Destructor Documentation

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

Definition at line 54 of file decision_engine_mbtf.cpp.

virtual CVCL::DecisionEngineMBTF::~DecisionEngineMBTF (   )  [inline, virtual]

Definition at line 58 of file decision_engine_mbtf.h.

---

Member Function Documentation

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

Implements CVCL::DecisionEngine. Definition at line 39 of file decision_engine_mbtf.cpp. References d_cache, d_height, d_index, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), and CVCL::Expr::getSimpFrom().

Expr 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 CVCL::DecisionEngine. Definition at line 66 of file decision_engine_mbtf.cpp. References CVCL::ExprMap< Data >::clear(), CVCL::Debug::counter(), CVCL::DecisionEngine::d_core, d_height, d_topLevel, d_topLevelLock, CVCL::DecisionEngine::d_visited, CVCL::debugger, CVCL::DecisionEngine::findSplitterRec(), CVCL::TheoryCore::getCM(), CVCL::Expr::getHeight(), IF_DEBUG(), CVCL::Expr::isNull(), CVCL::ContextManager::scopeLevel(), CVCL::Expr::toString(), and CVCL::TRACE.

void DecisionEngineMBTF::goalSatisfied (   )  [virtual]

Search should call this when it derives 'false'. Implements CVCL::DecisionEngine. Definition at line 92 of file decision_engine_mbtf.cpp. References CVCL::ExprMap< Data >::clear(), CVCL::DecisionEngine::d_bestByExpr, d_bottomLevel, d_cache, CVCL::DecisionEngine::d_core, CVCL::Expr::d_expr, d_index, CVCL::DecisionEngine::d_splitters, d_startLevel, d_topLevel, d_topLevelLock, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::TheoryCore::getCM(), CVCL::Expr::getSimpFrom(), CVCL::Expr::isAbsAtomicFormula(), CVCL::max(), CVCL::ContextManager::scopeLevel(), and CVCL::CDList< T >::size().

---

Member Data Documentation

int CVCL::DecisionEngineMBTF::d_startLevel [private]

Definition at line 44 of file decision_engine_mbtf.h. Referenced by goalSatisfied().

int CVCL::DecisionEngineMBTF::d_bottomLevel [private]

Definition at line 45 of file decision_engine_mbtf.h. Referenced by goalSatisfied().

int CVCL::DecisionEngineMBTF::d_topLevel [private]

Definition at line 46 of file decision_engine_mbtf.h. Referenced by findSplitter(), and goalSatisfied().

bool CVCL::DecisionEngineMBTF::d_topLevelLock [private]

Definition at line 47 of file decision_engine_mbtf.h. Referenced by findSplitter(), and goalSatisfied().

int CVCL::DecisionEngineMBTF::d_height [private]

Definition at line 48 of file decision_engine_mbtf.h. Referenced by findSplitter(), and isBetter().

std::vector<CacheEntry> CVCL::DecisionEngineMBTF::d_cache [private]

Definition at line 50 of file decision_engine_mbtf.h. Referenced by goalSatisfied(), and isBetter().

ExprMap<int> CVCL::DecisionEngineMBTF::d_index [private]

Definition at line 51 of file decision_engine_mbtf.h. Referenced by goalSatisfied(), and isBetter().

---

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

• decision_engine_mbtf.h
• decision_engine_mbtf.cpp

---