diff options
Diffstat (limited to 'src/decision/decision_engine.cpp')
-rw-r--r-- | src/decision/decision_engine.cpp | 43 |
1 files changed, 31 insertions, 12 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 63a09ba2c..e12ae6127 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -26,12 +26,12 @@ using namespace std; namespace CVC4 { DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc) - : d_enabledITEStrategies(), + : d_enabledITEStrategy(nullptr), d_needIteSkolemMap(), - d_relevancyStrategy(NULL), + d_relevancyStrategy(nullptr), d_assertions(uc), - d_cnfStream(NULL), - d_satSolver(NULL), + d_cnfStream(nullptr), + d_satSolver(nullptr), d_satContext(sc), d_userContext(uc), d_result(sc, SAT_VALUE_UNKNOWN), @@ -53,9 +53,9 @@ void DecisionEngine::init() if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) { - d_enabledITEStrategies.emplace_back(new decision::JustificationHeuristic( + d_enabledITEStrategy.reset(new decision::JustificationHeuristic( this, d_userContext, d_satContext)); - d_needIteSkolemMap.push_back(d_enabledITEStrategies.back().get()); + d_needIteSkolemMap.push_back(d_enabledITEStrategy.get()); } } @@ -65,18 +65,34 @@ void DecisionEngine::shutdown() Assert(d_engineState == 1); d_engineState = 2; - - d_enabledITEStrategies.clear(); + d_enabledITEStrategy.reset(nullptr); d_needIteSkolemMap.clear(); } +SatLiteral DecisionEngine::getNext(bool& stopSearch) +{ + NodeManager::currentResourceManager()->spendResource( + ResourceManager::Resource::DecisionStep); + Assert(d_cnfStream != nullptr) + << "Forgot to set cnfStream for decision engine?"; + Assert(d_satSolver != nullptr) + << "Forgot to set satSolver for decision engine?"; + + return d_enabledITEStrategy == nullptr + ? undefSatLiteral + : d_enabledITEStrategy->getNext(stopSearch); +} + bool DecisionEngine::isRelevant(SatVariable var) { Debug("decision") << "isRelevant(" << var <<")" << std::endl; - if(d_relevancyStrategy != NULL) { + if (d_relevancyStrategy != nullptr) + { //Assert(d_cnfStream->hasNode(var)); return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) ); - } else { + } + else + { return true; } } @@ -84,10 +100,13 @@ bool DecisionEngine::isRelevant(SatVariable var) SatValue DecisionEngine::getPolarity(SatVariable var) { Debug("decision") << "getPolarity(" << var <<")" << std::endl; - if(d_relevancyStrategy != NULL) { + if (d_relevancyStrategy != nullptr) + { Assert(isRelevant(var)); return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) ); - } else { + } + else + { return SAT_VALUE_UNKNOWN; } } |