diff options
Diffstat (limited to 'src/theory/decision_manager.cpp')
| -rw-r--r-- | src/theory/decision_manager.cpp | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp index 3cc67fe6d..5c43e6159 100644 --- a/src/theory/decision_manager.cpp +++ b/src/theory/decision_manager.cpp @@ -38,7 +38,7 @@ void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds) d_reg_strategy[id].push_back(ds); } -Node DecisionManager::getNextDecisionRequest(unsigned& priority) +Node DecisionManager::getNextDecisionRequest() { Trace("dec-manager-debug") << "DecisionManager: Get next decision..." << std::endl; @@ -51,10 +51,6 @@ Node DecisionManager::getNextDecisionRequest(unsigned& priority) Node lit = ds->getNextDecisionRequest(); if (!lit.isNull()) { - StrategyId sid = rs.first; - priority = sid < STRAT_LAST_M_SOUND - ? 0 - : (sid < STRAT_LAST_FM_COMPLETE ? 1 : 2); Trace("dec-manager") << "DecisionManager: -> literal " << lit << " decided by strategy " << ds->identify() << std::endl; |