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.)

1 files changed, 1 insertions, 26 deletions

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)