#include <decision_engine_mbtf.h>
Inheritance diagram for CVC3::DecisionEngineMBTF:
Definition at line 24 of file decision_engine_mbtf.h.
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.
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().
Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur.
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().
int CVC3::DecisionEngineMBTF::d_startLevel [private] |
int CVC3::DecisionEngineMBTF::d_bottomLevel [private] |
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] |
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().