CVC3::DecisionEngineMBTF Class Reference

#include <decision_engine_mbtf.h>

Inheritance diagram for CVC3::DecisionEngineMBTF:

Inheritance graph
[legend]
Collaboration diagram for CVC3::DecisionEngineMBTF:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Private Attributes

Classes


Detailed Description

Definition at line 24 of file decision_engine_mbtf.h.


Constructor & Destructor Documentation

DecisionEngineMBTF::DecisionEngineMBTF ( TheoryCore core,
SearchImplBase se 
)

Definition at line 46 of file decision_engine_mbtf.cpp.

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

Definition at line 50 of file decision_engine_mbtf.h.


Member Function Documentation

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

Implements CVC3::DecisionEngine.

Definition at line 31 of file decision_engine_mbtf.cpp.

References d_cache, d_height, d_index, CVC3::ExprMap< Data >::end(), and CVC3::ExprMap< Data >::find().

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 CVC3::DecisionEngine.

Definition at line 58 of file decision_engine_mbtf.cpp.

References CVC3::Debug::counter(), CVC3::DecisionEngine::d_core, d_height, d_topLevel, d_topLevelLock, CVC3::DecisionEngine::d_visited, DebugAssert, CVC3::debugger, CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryCore::getCM(), IF_DEBUG, CVC3::Expr::isNull(), CVC3::ContextManager::scopeLevel(), CVC3::Expr::toString(), and CVC3::TRACE.

void DecisionEngineMBTF::goalSatisfied (  )  [virtual]

Search should call this when it derives 'false'.

Implements CVC3::DecisionEngine.

Definition at line 84 of file decision_engine_mbtf.cpp.

References CVC3::DecisionEngine::d_bestByExpr, d_bottomLevel, d_cache, CVC3::DecisionEngine::d_core, CVC3::Expr::d_expr, d_index, CVC3::DecisionEngine::d_splitters, d_startLevel, d_topLevel, d_topLevelLock, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::TheoryCore::getCM(), CVC3::Expr::isAbsAtomicFormula(), MiniSat::max(), and CVC3::ContextManager::scopeLevel().


Member Data Documentation

int CVC3::DecisionEngineMBTF::d_startLevel [private]

Definition at line 36 of file decision_engine_mbtf.h.

Referenced by goalSatisfied().

int CVC3::DecisionEngineMBTF::d_bottomLevel [private]

Definition at line 37 of file decision_engine_mbtf.h.

Referenced by goalSatisfied().

int CVC3::DecisionEngineMBTF::d_topLevel [private]

Definition at line 38 of file decision_engine_mbtf.h.

Referenced by findSplitter(), and goalSatisfied().

bool CVC3::DecisionEngineMBTF::d_topLevelLock [private]

Definition at line 39 of file decision_engine_mbtf.h.

Referenced by findSplitter(), and goalSatisfied().

int CVC3::DecisionEngineMBTF::d_height [private]

Definition at line 40 of file decision_engine_mbtf.h.

Referenced by findSplitter(), and isBetter().

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

Definition at line 42 of file decision_engine_mbtf.h.

Referenced by goalSatisfied(), and isBetter().

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

Definition at line 43 of file decision_engine_mbtf.h.

Referenced by goalSatisfied(), and isBetter().


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:40:44 2007 for CVC3 by  doxygen 1.5.1