diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-04-26 20:30:41 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-05-08 19:34:15 -0400 |
commit | b53423bcec060d5a49ee2df4d1da55ed289de1d2 (patch) | |
tree | dc8b9a06b7dd3f4221112b93b03c8810cbc9e7dc /src/decision/decision_engine.cpp | |
parent | 75d3b086d2cbcb4508446e405e0599788a3a25a5 (diff) |
rm decision/relevancy
Diffstat (limited to 'src/decision/decision_engine.cpp')
-rw-r--r-- | src/decision/decision_engine.cpp | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index f634a28d9..073a3ff6b 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -16,7 +16,6 @@ #include "decision/decision_engine.h" #include "decision/justification_heuristic.h" -#include "decision/relevancy.h" #include "expr/node.h" #include "decision/options.h" @@ -62,18 +61,6 @@ void DecisionEngine::init() enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } - if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) { - if(options::incrementalSolving()) { - Warning() << "Relevancy decision heuristic and incremental not supported together" - << std::endl; - return; // Currently not supported with incremental - } - RelevancyStrategy* ds = - new decision::Relevancy(this, d_satContext); - enableStrategy(ds); - d_needIteSkolemMap.push_back(ds); - d_relevancyStrategy = ds; - } } @@ -112,13 +99,6 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } - - - - - - - void DecisionEngine::addAssertions(const vector<Node> &assertions) { Assert(false); // doing this so that we revisit what to do @@ -146,15 +126,4 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions, addAssertions(assertions, assertionsEnd, iteSkolemMap); } -// void DecisionEngine::addAssertion(Node n) -// { -// d_result = SAT_VALUE_UNKNOWN; -// if(needIteSkolemMap()) { -// d_assertions.push_back(n); -// } -// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) -// d_needIteSkolemMap[i]->notifyAssertionsAvailable(); -// } - - }/* CVC4 namespace */ |