#include <decision_engine_caching.h>
Inheritance diagram for CVC3::DecisionEngineCaching:
Definition at line 24 of file decision_engine_caching.h.
DecisionEngineCaching::DecisionEngineCaching | ( | TheoryCore * | core, | |
SearchImplBase * | se | |||
) |
Definition at line 47 of file decision_engine_caching.cpp.
virtual CVC3::DecisionEngineCaching::~DecisionEngineCaching | ( | ) | [inline, virtual] |
Definition at line 50 of file decision_engine_caching.h.
Implements CVC3::DecisionEngine.
Definition at line 31 of file decision_engine_caching.cpp.
References BASE_TRUST_LEVEL, 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 59 of file decision_engine_caching.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 DecisionEngineCaching::goalSatisfied | ( | ) | [virtual] |
Search should call this when it derives 'false'.
Implements CVC3::DecisionEngine.
Definition at line 85 of file decision_engine_caching.cpp.
References CACHE_SIZE, CVC3::ExprMap< Data >::count(), 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::min(), CVC3::ContextManager::scopeLevel(), and TURNOVER_RATE.
int CVC3::DecisionEngineCaching::d_startLevel [private] |
int CVC3::DecisionEngineCaching::d_bottomLevel [private] |
int CVC3::DecisionEngineCaching::d_topLevel [private] |
Definition at line 38 of file decision_engine_caching.h.
Referenced by findSplitter(), and goalSatisfied().
bool CVC3::DecisionEngineCaching::d_topLevelLock [private] |
Definition at line 39 of file decision_engine_caching.h.
Referenced by findSplitter(), and goalSatisfied().
int CVC3::DecisionEngineCaching::d_height [private] |
Definition at line 40 of file decision_engine_caching.h.
Referenced by findSplitter(), and isBetter().
std::vector<CacheEntry> CVC3::DecisionEngineCaching::d_cache [private] |
Definition at line 42 of file decision_engine_caching.h.
Referenced by goalSatisfied(), and isBetter().
ExprMap<int> CVC3::DecisionEngineCaching::d_index [private] |
Definition at line 43 of file decision_engine_caching.h.
Referenced by goalSatisfied(), and isBetter().