rm decision/relevancy

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 */