From 95dcbc6781cd8e62f8436f0cfe944b21dfd60ec0 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 27 Nov 2012 19:02:50 +0000
Subject: [PATCH] Simplify --help=decision with only currently supported
 options

Add notice/warning when using incremental-mode + decision (it was
already disabled)

Some other minor cleanup

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/decision/decision_engine.cpp         | 14 ++++++++++--
 src/decision/justification_heuristic.cpp | 27 +-----------------------
 src/decision/justification_heuristic.h   |  8 +------
 src/decision/options_handlers.h          |  5 ++++-
 4 files changed, 18 insertions(+), 36 deletions(-)

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index d5c819ace..22c70eb6d 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -50,8 +50,18 @@ void DecisionEngine::init()
   d_engineState = 1;
 
   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
-  if(options::incrementalSolving()) return;
-
+  if(options::incrementalSolving()) {
+    if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) {
+      if(options::decisionMode.wasSetByUser()) {
+        Warning() << "Ignorning decision option since using incremental mode (currently not supported together)"
+                  << std::endl;
+      } else {
+        Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)"
+                 << std::endl;
+      }
+    }
+    return;
+  }
   Trace("decision-init") << " * options->decisionMode: " 
                          << options::decisionMode() << std:: endl;
   Trace("decision-init") << " * options->decisionStopOnly: "
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c588c2d92..ba8ab91b7 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -11,8 +11,7 @@
  **
  ** \brief Justification heuristic for decision making
  **
- ** A ATGP-inspired justification-based decision heuristic. See
- ** [insert reference] for more details. This code is, or not, based
+ ** A ATGP-inspired justification-based decision heuristic. This code is based
  ** on the CVC3 implementation of the same heuristic -- note below.
  **
  ** It needs access to the simplified but non-clausal formula.
@@ -44,30 +43,6 @@
 #include "theory/rewriter.h"
 #include "util/ite_removal.h"
 
-/***
-Here's the main idea
-
-   Given a boolean formula "node", the goal is to try to make it
-evaluate to "desiredVal" (true/false). for instance if "node" is a AND
-formula we want to make it evaluate to true, we'd like one of the
-children to be true. this is done recursively.
-
-***/
-
-/*
-
-CVC3 code <---->  this code
- 
- value            desiredVal
- getValue(lit)    litVal
-
-***/
-
-
-// Local helper functions for just this file
-
-
-
 // JustificationHeuristic stuff
 
 void JustificationHeuristic::setJustified(TNode n)
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 5669ae79d..a3b05b1bb 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -130,7 +130,7 @@ public:
 
     Trace("decision") << "jh: Nothing to split on " << std::endl;
 
-#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
+#if defined CVC4_DEBUG
     bool alljustified = true;
     for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
       TNode curass = d_assertions[i];
@@ -176,10 +176,6 @@ public:
     }
   }
 
-  /* Compute justified */
-  /*bool computeJustified() {
-    
-  }*/
 private:
   SatLiteral findSplitter(TNode node, SatValue desiredVal)
   {
@@ -188,7 +184,6 @@ private:
     ret = findSplitterRec(node, desiredVal, &litDecision);
     if(ret == true) {
       Debug("decision") << "Yippee!!" << std::endl;
-      //d_prvsIndex = i;
       ++d_helfulness;
       return litDecision;
     } else {
@@ -198,7 +193,6 @@ private:
   
   /** 
    * Do all the hard work. 
-   * @param findFirst returns
    */ 
   bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
 
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index fd05a0c9f..826bd8acb 100644
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -36,6 +36,9 @@ justification\n\
 \n\
 justification-stoponly\n\
 + Use the justification heuristic only to stop early, not for decisions\n\
+";
+/** Under-development options, commenting out from help for the release */
+/*
 \n\
 relevancy\n\
 + Under development may-relevancy\n\
@@ -52,7 +55,7 @@ justification-rel\n\
 justification-must\n\
 + Start deciding on literals close to root instead of those\n\
 + near leaves (don't expect it to work well) [Unimplemented]\n\
-";
+";*/
 
 inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   options::decisionRelevancyLeaves.set(false);
-- 
2.30.2