diff options
-rw-r--r-- | src/decision/decision_engine.cpp | 43 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 22 |
2 files changed, 34 insertions, 31 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; } } diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 28b15c9e0..c4eb29284 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -38,7 +38,7 @@ using namespace CVC4::decision; namespace CVC4 { class DecisionEngine { - vector<std::unique_ptr<ITEDecisionStrategy>> d_enabledITEStrategies; + std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; vector <ITEDecisionStrategy* > d_needIteSkolemMap; RelevancyStrategy* d_relevancyStrategy; @@ -85,7 +85,7 @@ public: d_cnfStream = cs; } - /* enables decision stragies based on options */ + /* Enables decision strategy based on options. */ void init(); /** @@ -98,23 +98,7 @@ public: // Interface for External World to use our services /** Gets the next decision based on strategies that are enabled */ - SatLiteral getNext(bool &stopSearch) { - NodeManager::currentResourceManager()->spendResource( - ResourceManager::Resource::DecisionStep); - Assert(d_cnfStream != NULL) - << "Forgot to set cnfStream for decision engine?"; - Assert(d_satSolver != NULL) - << "Forgot to set satSolver for decision engine?"; - - SatLiteral ret = undefSatLiteral; - for (unsigned i = 0; i < d_enabledITEStrategies.size() - and ret == undefSatLiteral and stopSearch == false; - ++i) - { - ret = d_enabledITEStrategies[i]->getNext(stopSearch); - } - return ret; - } + SatLiteral getNext(bool& stopSearch); /** Is a sat variable relevant */ bool isRelevant(SatVariable var); |