diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-16 13:10:05 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-16 13:10:05 -0700 |
commit | f4cd63a00f1c8cc9e4d9e42fd171f7cb1a64aaab (patch) | |
tree | 9ef396c241d1435e472ad9b85104c9696b7cd303 /src/decision/decision_engine.h | |
parent | e2ced5d1e84ea1562eae907fd2b245bae4593406 (diff) |
DecisionEngine: Use single unique pointer for ITE strategy . (#4078)
Previously, DecisionEngine maintained a vector of ITE strategies.
However, only one was ever created. This uses a single unique_ptr member
for the ITE strategy instead of a vector.
Diffstat (limited to 'src/decision/decision_engine.h')
-rw-r--r-- | src/decision/decision_engine.h | 22 |
1 files changed, 3 insertions, 19 deletions
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); |