From b53423bcec060d5a49ee2df4d1da55ed289de1d2 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 26 Apr 2013 20:30:41 -0400 Subject: rm decision/relevancy --- src/decision/decision_engine.cpp | 31 ------------------------------- 1 file changed, 31 deletions(-) (limited to 'src/decision/decision_engine.cpp') 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 &assertions) { Assert(false); // doing this so that we revisit what to do @@ -146,15 +126,4 @@ void DecisionEngine::addAssertions(const vector &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 */ -- cgit v1.2.3