Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

1 files changed, 41 insertions, 4 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 1afe835fb..b1ecabf81 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -18,6 +18,7 @@
 
 #include "decision/decision_engine.h"
 #include "decision/justification_heuristic.h"
+#include "decision/relevancy.h"
 
 #include "expr/node.h"
 #include "util/options.h"
@@ -30,6 +31,7 @@ namespace CVC4 {
                                  context::Context *uc) :
   d_enabledStrategies(),
   d_needIteSkolemMap(),
+  d_relevancyStrategy(NULL),
   d_assertions(),
   d_cnfStream(NULL),
   d_satSolver(NULL),
@@ -49,6 +51,13 @@ namespace CVC4 {
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
   }
+  if(options->decisionMode == Options::DECISION_STRATEGY_RELEVANCY) {
+    RelevancyStrategy* ds = 
+      new decision::Relevancy(this, d_satContext, options->decisionOptions);
+    enableStrategy(ds);
+    d_needIteSkolemMap.push_back(ds);
+    d_relevancyStrategy = ds;
+  }
 }
 
 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
@@ -57,6 +66,35 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds)
 }
 
 
+bool DecisionEngine::isRelevant(SatVariable var)
+{
+  Debug("decision") << "isRelevant(" << var <<")" << std::endl;
+  if(d_relevancyStrategy != NULL) {
+    //Assert(d_cnfStream->hasNode(var));
+    return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
+  } else {
+    return true;
+  }
+}
+
+SatValue DecisionEngine::getPolarity(SatVariable var)
+{
+  Debug("decision") << "getPolariry(" << var <<")" << std::endl;
+  if(d_relevancyStrategy != NULL) {
+    Assert(isRelevant(var));
+    return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
+  } else {
+    return SAT_VALUE_UNKNOWN;
+  }
+}
+
+
+
+
+
+
+
+
 void DecisionEngine::addAssertions(const vector<Node> &assertions)
 {
   Assert(false);  // doing this so that we revisit what to do
@@ -68,10 +106,9 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions)
   //   d_assertions.push_back(assertions[i]); 
 }
 
-void DecisionEngine::addAssertions
-  (const vector<Node> &assertions,
-   unsigned assertionsEnd,
-   IteSkolemMap iteSkolemMap) 
+void DecisionEngine::addAssertions(const vector<Node> &assertions,
+                                   unsigned assertionsEnd,
+                                   IteSkolemMap iteSkolemMap)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;