Merge from decision branch -- partially working justification heuristic

Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
  revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
  unknown and smtEngine queries DE to get the answer
  relevant stat: smt::resultSource
* there are known bugs

Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A

13 files changed, 422 insertions, 193 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index dbdbb83a9..7c8718370 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -26,16 +26,23 @@ using namespace std;
 
 namespace CVC4 {
 
-DecisionEngine::DecisionEngine() :
+DecisionEngine::DecisionEngine(context::Context *c) :
+  d_enabledStrategies(),
   d_needSimplifiedPreITEAssertions(),
+  d_assertions(),
   d_cnfStream(NULL),
-  d_satSolver(NULL)
+  d_satSolver(NULL),
+  d_satContext(c),
+  d_result(SAT_VALUE_UNKNOWN)
 {
   const Options* options = Options::current();
   Trace("decision") << "Creating decision engine" << std::endl;
+
+  if(options->incrementalSolving) return;
+
   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
-    DecisionStrategy* ds = new decision::JustificationHeuristic(this);
+    DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext);
     enableStrategy(ds);
   }
 }
@@ -49,6 +56,7 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds)
 
 void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
 {
+  d_result = SAT_VALUE_UNKNOWN;
   d_assertions.reserve(assertions.size());
   for(unsigned i = 0; i < assertions.size(); ++i)
     d_assertions.push_back(assertions[i]);
@@ -56,4 +64,15 @@ void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assert
     d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
 }
 
+void DecisionEngine::addAssertion(Node n)
+{
+  d_result = SAT_VALUE_UNKNOWN;
+  if(needSimplifiedPreITEAssertions()) {
+    d_assertions.push_back(n);
+  }
+  for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
+    d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+}
+  
+
 }/* CVC4 namespace */
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index d4037acff..1e6e8a64d 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -45,15 +45,21 @@ class DecisionEngine {
   // PropEngine* d_propEngine;
   CnfStream* d_cnfStream;
   DPLLSatSolverInterface* d_satSolver;
+
+  SatValue d_result;
+
+  context::Context* d_satContext;
 public:
   // Necessary functions
 
   /** Constructor, enables decision stragies based on options */
-  DecisionEngine();
+  DecisionEngine(context::Context *c);
 
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
     Trace("decision") << "Destroying decision engine" << std::endl;
+    for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
+      delete d_enabledStrategies[i];
   }
   
   // void setPropEngine(PropEngine* pe) {
@@ -81,15 +87,42 @@ public:
   // Interface for External World to use our services
 
   /** Gets the next decision based on strategies that are enabled */
-  SatLiteral getNext() {
+  SatLiteral getNext(bool &stopSearch) {
     SatLiteral ret = undefSatLiteral;
-    for(unsigned i = 0; i < d_enabledStrategies.size() 
-          and ret == undefSatLiteral; ++i) {
-      ret = d_enabledStrategies[i]->getNext();
+    for(unsigned i = 0; 
+        i < d_enabledStrategies.size() 
+          and ret == undefSatLiteral
+          and stopSearch == false; ++i) {
+      ret = d_enabledStrategies[i]->getNext(stopSearch);
     }
     return ret;
   }
 
+  /** Is the DecisionEngine in a state where it has solved everything? */
+  bool isDone() {
+    Trace("decision") << "DecisionEngine::isDone() returning "
+		      << (d_result != SAT_VALUE_UNKNOWN)
+		      << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
+		      << std::endl;
+    return (d_result != SAT_VALUE_UNKNOWN);
+  }
+
+  /** */
+  Result getResult() {
+    switch(d_result) {
+    case SAT_VALUE_TRUE: return Result(Result::SAT);
+    case SAT_VALUE_FALSE: return Result(Result::UNSAT);
+    case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+    default: Assert(false);
+    }
+    return Result();
+  }
+
+  /** */
+  void setResult(SatValue val) {
+    d_result = val;
+  }
+
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
@@ -109,6 +142,7 @@ public:
   }
   void informSimplifiedPreITEAssertions(const vector<Node> &assertions);
 
+  void addAssertion(Node n);
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index abcbbaace..6746b13cc 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -25,19 +25,23 @@ namespace CVC4 {
 
 class DecisionEngine;
 
+namespace context {
+class Context;
+}
+
 namespace decision {
 
 class DecisionStrategy {
 protected:
    DecisionEngine* d_decisionEngine;
 public:
-  DecisionStrategy(DecisionEngine* de) :
+  DecisionStrategy(DecisionEngine* de, context::Context *c) :
     d_decisionEngine(de) {
   }
 
   virtual ~DecisionStrategy() { }
 
-  virtual prop::SatLiteral getNext() = 0;
+  virtual prop::SatLiteral getNext(bool&) = 0;
   
   virtual bool needSimplifiedPreITEAssertions() { return false; }
   
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 4b017ef45..e86b03258 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -41,6 +41,7 @@
 
 #include "justification_heuristic.h"
 
+#include "expr/kind.h"
 
 /***
 
@@ -59,14 +60,14 @@ CVC3 code <---->  this code
 
 ***/
 
-void JustificationHeuristic::setJustified(SatVariable v)
+void JustificationHeuristic::setJustified(TNode n)
 {
-  d_justified.insert(v);
+  d_justified.insert(n);
 }
 
-bool JustificationHeuristic::checkJustified(SatVariable v)
+bool JustificationHeuristic::checkJustified(TNode n)
 {
-  return d_justified.find(v) != d_justified.end();
+  return d_justified.find(n) != d_justified.end();
 }
 
 SatValue invertValue(SatValue v)
@@ -76,50 +77,53 @@ SatValue invertValue(SatValue v)
   else return SAT_VALUE_TRUE;
 }
 
-bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision)
+bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, SatLiteral* litDecision)
 //bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
 {
-  // if(not ) {
-  //   //    Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
-  //   return false;
-  //   //    Assert(not lit.isNull());
-  // }
-
-  /** 
-   * TODO -- Base case. Way CVC3 seems to handle is that it has
-   * literals correpsonding to true and false. We'll have to take care
-   * somewhere else.
-   */
+  Trace("decision") 
+    << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; 
 
-  // Var v = lit.getVar();
-  SatVariable v = lit.getSatVariable();
-  SatValue litVal =  d_decisionEngine->getSatValue(lit);
+  /* Handle NOT as a special case */
+  if (node.getKind() == kind::NOT) {
+    desiredVal = invertValue(desiredVal);
+    node = node[0];
+  }
 
-  // if (lit.isFalse() || lit.isTrue()) return false;
-  if (v == 0) return false;
+  if (checkJustified(node)) return false;
+
+  SatValue litVal = tryGetSatValue(node);
+  bool litPresent = false;
+  if(d_decisionEngine->hasSatLiteral(node) ) {
+    SatLiteral lit = d_decisionEngine->getSatLiteral(node);
+    litPresent = true;
+
+    SatVariable v = lit.getSatVariable();
+    // if (lit.isFalse() || lit.isTrue()) return false;
+    if (v == 0) {
+      setJustified(node);
+      return false;
+    }
+  } else {
+    Trace("decision") << "no sat literal for this node" << std::endl;
+  }
 
 
   /* You'd better know what you want */
-  // DebugAssert(value != Var::UNKNOWN, "expected known value");
   Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
 
   /* Good luck, hope you can get what you want */
-  // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
-  //             "invariant violated");
   Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, 
          "invariant voilated");
 
+  /* What type of node is this */
+  Kind k = node.getKind();
+  theory::TheoryId tId = theory::kindToTheoryId(k);
 
-  if (checkJustified(v)) return false;
-
-  if (lit.isNegated()) {
-    desiredVal = invertValue(desiredVal);
-  }
-
-  Node node = d_decisionEngine->getNode(lit);
-  Trace("decision") << "lit = " << lit << std::endl;
-  Trace("decision") << node.getKind() << std::endl;
-  Trace("decision") << node << std::endl;
+  /* Some debugging stuff */
+  Trace("findSpitterRec") << "kind = " << k << std::endl;
+  Trace("findSplitterRec") << "theoryId = " << tId << std::endl;
+  Trace("findSplitterRec") << "node = " << node << std::endl;
+  Trace("findSplitterRec") << "litVal = " << litVal << std::endl;
 
   /*
   if (d_cnfManager->numFanins(v) == 0) {
@@ -133,17 +137,32 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
     }
   }
   */
-  if(node.getNumChildren() == 0) {
+
+
+  /**
+   * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
+   * then check if this is something to split-on? 
+   */
+  if(tId != theory::THEORY_BOOL
+     //      && !(k == kind::EQUAL && node[0].getType().isBoolean()) 
+     ) {
     if(litVal != SAT_VALUE_UNKNOWN) {
-      setJustified(v);
+      setJustified(node);
       return false;
     } else {
-      *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE );
+      if(not d_decisionEngine->hasSatLiteral(node))
+        throw GiveUpException();
+      Assert(d_decisionEngine->hasSatLiteral(node));
+      SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
+      *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+      Trace("decision") << "decision " << *litDecision << std::endl;
+      Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
       return true;
     }
   }
 
 
+  /*** TODO: Term ITEs ***/
   /*
   else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
     // This node represents a predicate with embedded ITE's
@@ -208,134 +227,143 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
       return true;
     }
   }
+  */
 
-  int kind = d_cnfManager->concreteVar(v).getKind();
-  Var::Val valHard = Var::FALSE_VAL;
-  switch (kind) {
-    case AND:
-      valHard = Var::TRUE_VAL;
-    case OR:
-      if (value == valHard) {
-        n = d_cnfManager->numFanins(v);
-        for (i=0; i < n; ++i) {
-          litTmp = d_cnfManager->getFanin(v, i);
-          if (findSplitterRec(litTmp, valHard, litDecision)) {
-            return true;
-          }
-        }
-        DebugAssert(getValue(v) == valHard, "Output should be justified");
-        setJustified(v);
-        return false;
-      }
-      else {
-        Var::Val valEasy = Var::invertValue(valHard);
-        n = d_cnfManager->numFanins(v);
-        for (i=0; i < n; ++i) {
-          litTmp = d_cnfManager->getFanin(v, i);
-          if (getValue(litTmp) != valHard) {
-            if (findSplitterRec(litTmp, valEasy, litDecision)) {
-              return true;
-            }
-            DebugAssert(getValue(v) == valEasy, "Output should be justified");
-            setJustified(v);
-            return false;
-          }
-        }
-        DebugAssert(false, "No controlling input found (2)");
-      }
-      break;
-    case IMPLIES:
-      DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins");
-      if (value == Var::FALSE_VAL) {
-        litTmp = d_cnfManager->getFanin(v, 0);
-        if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+  SatValue valHard = SAT_VALUE_FALSE;
+  switch (k) {
+  case kind::AND:
+    valHard = SAT_VALUE_TRUE;
+  case kind::OR:
+    if (desiredVal == valHard) {
+      int n = node.getNumChildren();
+      for(int i = 0; i < n; ++i) {
+        if (findSplitterRec(node[i], valHard, litDecision)) {
           return true;
         }
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
-          return true;
-        }
-        DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified");
-        setJustified(v);
-        return false;
       }
-      else {
-        litTmp = d_cnfManager->getFanin(v, 0);
-        if (getValue(litTmp) != Var::TRUE_VAL) {
-          if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
-            return true;
-          }
-          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
-          setJustified(v);
-          return false;
-        }
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (getValue(litTmp) != Var::FALSE_VAL) {
-          if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+      Assert(litPresent == false || litVal == valHard, "Output should be justified");
+      setJustified(node);
+      return false;
+    }
+    else {
+      SatValue valEasy = invertValue(valHard);
+      int n = node.getNumChildren();
+      for(int i = 0; i < n; ++i) {
+        Trace("findSplitterRec") << " node[i] = " << node[i] << " " << tryGetSatValue(node[i]) << std::endl;
+        if ( tryGetSatValue(node[i]) != valHard) {
+          Trace("findSplitterRec") << "hi"<< std::endl;
+          if (findSplitterRec(node[i], valEasy, litDecision)) {
             return true;
           }
-          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
-          setJustified(v);
+          Assert(litPresent == false || litVal == valEasy, "Output should be justified");
+          setJustified(node);
           return false;
         }
-        DebugAssert(false, "No controlling input found (3)");
       }
-      break;
-    case IFF: {
-      litTmp = d_cnfManager->getFanin(v, 0);
-      Var::Val val = getValue(litTmp);
-      if (val != Var::UNKNOWN) {
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
-        litTmp = d_cnfManager->getFanin(v, 1);
+      Trace("findSplitterRec") << " * ** " << std::endl;
+      Trace("findSplitterRec") << node.getKind() << " " << node << std::endl;
+      for(unsigned i = 0; i < node.getNumChildren(); ++i) 
+        Trace("findSplitterRec") << "child: " << tryGetSatValue(node[i]) << std::endl;
+      Trace("findSplitterRec") << "node: " << tryGetSatValue(node) << std::endl;
+      Assert(false, "No controlling input found (2)");
+    }
+    break;
 
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        DebugAssert(getValue(v) == value, "Output should be justified");
-        setJustified(v);
-        return false;
+  case kind::IMPLIES:
+    //throw GiveUpException();
+    Assert(node.getNumChildren() == 2, "Expected 2 fanins");
+    if (desiredVal == SAT_VALUE_FALSE) {
+      if (findSplitterRec(node[0], SAT_VALUE_TRUE, litDecision)) {
+        return true;
       }
-      else {
-        val = getValue(d_cnfManager->getFanin(v, 1));
-        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
-        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        DebugAssert(false, "Unable to find controlling input (4)");
+      if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) {
+        return true;
       }
-      break;
+      Assert(litPresent == false || litVal == SAT_VALUE_FALSE, "Output should be justified");
+      setJustified(node);
+      return false;
     }
-    case XOR: {
-      litTmp = d_cnfManager->getFanin(v, 0);
-      Var::Val val = getValue(litTmp);
-      if (val != Var::UNKNOWN) {
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (findSplitterRec(litTmp, val, litDecision)) {
+    else {
+      if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
+        if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) {
           return true;
         }
-        DebugAssert(getValue(v) == value, "Output should be justified");
-        setJustified(v);
+        Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+        setJustified(node);
         return false;
       }
-      else {
-        val = getValue(d_cnfManager->getFanin(v, 1));
-        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
-        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
-        if (findSplitterRec(litTmp, val, litDecision)) {
+      if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
+        if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) {
           return true;
         }
-        DebugAssert(false, "Unable to find controlling input (5)");
+        Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+        setJustified(node);
+        return false;
+      }
+      Assert(false, "No controlling input found (3)");
+    }
+    break;
+  case kind::IFF: 
+    //throw GiveUpException();
+    {
+    SatValue val = tryGetSatValue(node[0]);
+    if (val != SAT_VALUE_UNKNOWN) {
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
       }
-      break;
+      if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+
+      if (findSplitterRec(node[1], val, litDecision)) {
+        return true;
+      }
+      Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+      setJustified(node);
+      return false;
     }
+    else {
+      val = tryGetSatValue(node[1]);
+      if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+      if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      Assert(false, "Unable to find controlling input (4)");
+    }
+    break;
+  }
+    
+  case kind::XOR:
+    //throw GiveUpException();
+    {
+    SatValue val = tryGetSatValue(node[0]);
+    if (val != SAT_VALUE_UNKNOWN) {
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+
+      if (findSplitterRec(node[1], val, litDecision)) {
+        return true;
+      }
+      Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+      setJustified(node);
+      return false;
+    }
+    else {
+      SatValue val = tryGetSatValue(node[1]);
+      if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+      if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      Assert(false, "Unable to find controlling input (5)");
+    }
+    break;
+  }
+
+  case kind::ITE:
+    throw GiveUpException();
+    /*
     case ITE: {
       Lit cIf = d_cnfManager->getFanin(v, 0);
       Lit cThen = d_cnfManager->getFanin(v, 1);
@@ -380,14 +408,15 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
       setJustified(v);
       return false;
     }
-    default:
-      DebugAssert(false, "Unexpected Boolean operator");
-      break;
+      */
+  default:
+    Assert(false, "Unexpected Boolean operator");
+    break;
   }
-  FatalAssert(false, "Should be unreachable");
-  ------------------------------------------------  */
-  return false;
 
+  /* Swap order of these two once we handle all cases */
+  return false;
   Unreachable();
 
+
 }/* findRecSplit method */
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index cb2216d6d..0457e6d3c 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -26,48 +26,99 @@
 #include "decision_engine.h"
 #include "decision_strategy.h"
 
-#include "prop/sat_solver_types.h"
+#include "context/cdhashset.h"
 #include "expr/node.h"
-
-using namespace CVC4::prop;
+#include "prop/sat_solver_types.h"
 
 namespace CVC4 {
 
 namespace decision {
 
+class GiveUpException : public Exception {
+public:
+  GiveUpException() : 
+    Exception("justification hueristic: giving up") {
+  }
+};/* class GiveUpException */
+
 class JustificationHeuristic : public DecisionStrategy {
-  set<SatVariable> d_justified;
-  unsigned  d_prvsIndex;
+  context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+  context::CDO<unsigned>  d_prvsIndex;
+  IntStat d_helfulness;
+  IntStat d_giveup;
+  TimerStat d_timestat;
 public:
-  JustificationHeuristic(CVC4::DecisionEngine* de) : 
-    DecisionStrategy(de) {
+  JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
+    DecisionStrategy(de, c),
+    d_justified(c),
+    d_prvsIndex(c, 0),
+    d_helfulness("decision::jh::helpfulness", 0),
+    d_giveup("decision::jh::giveup", 0),
+    d_timestat("decision::jh::time") {
+    StatisticsRegistry::registerStat(&d_helfulness);
+    StatisticsRegistry::registerStat(&d_giveup);
+    StatisticsRegistry::registerStat(&d_timestat);
     Trace("decision") << "Justification heuristic enabled" << std::endl;
   }
-  prop::SatLiteral getNext() {
+  ~JustificationHeuristic() {
+    StatisticsRegistry::unregisterStat(&d_helfulness);
+    StatisticsRegistry::unregisterStat(&d_timestat);
+  }
+  prop::SatLiteral getNext(bool &stopSearch) {
     Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
 
+    TimerStat::CodeTimer codeTimer(d_timestat);
+
     const vector<Node>& assertions = d_decisionEngine->getAssertions();
 
     for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) {
       SatLiteral litDecision;
 
-      /* Make sure there is a literal corresponding to the node  */
-      if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) {
-        //    Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
-        continue;
+      Trace("decision") << assertions[i] << std::endl;
+
+      SatValue desiredVal = SAT_VALUE_UNKNOWN;
+
+      if(d_decisionEngine->hasSatLiteral(assertions[i]) ) {
+        //desiredVal = d_decisionEngine->getSatValue( d_decisionEngine->getSatLiteral(assertions[i]) );
+        Trace("decision") << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
+        //    continue;
         //    Assert(not lit.isNull());
       }
-      
-      SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]);
-      SatValue desiredVal = d_decisionEngine->getSatValue(lit);
+
       if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE;
-      bool ret = findSplitterRec(lit, desiredVal, &litDecision);
+
+      bool ret;
+      try {
+        ret = findSplitterRec(assertions[i], desiredVal, &litDecision);
+      }catch(GiveUpException &e) {
+        return prop::undefSatLiteral;
+      }
       if(ret == true) {
-        d_prvsIndex = i;
+        Trace("decision") << "Yippee!!" << std::endl;
+        //d_prvsIndex = i;
+	++d_helfulness;
         return litDecision;
       }
     }
 
+    Trace("decision") << "Nothing to split on " << std::endl;
+
+    bool alljustified = true;
+    for(unsigned i = 0 ; i < assertions.size() && alljustified ; ++i) {
+      alljustified &= assertions[i].getKind() == kind::NOT ? 
+        checkJustified(assertions[i][0]) : checkJustified(assertions[i]);
+      if(Debug.isOn("decision")) {
+	bool x = assertions[i].getKind() == kind::NOT ? 
+        checkJustified(assertions[i][0]) : checkJustified(assertions[i]);
+	if(x==false)
+	  Debug("decision") << "****** Not justified [i="<<i<<"]: " << assertions[i] << std::endl;
+      }
+    }
+    Assert(alljustified);
+
+    stopSearch = alljustified;
+    d_decisionEngine->setResult(SAT_VALUE_TRUE);
+
     return prop::undefSatLiteral;
   } 
   bool needSimplifiedPreITEAssertions() { return true; }
@@ -77,16 +128,31 @@ public:
                       << std::endl;
     /* clear the justifcation labels -- reconsider if/when to do
        this */
-    d_justified.clear();
-    d_prvsIndex = 0;
+    //d_justified.clear();
+    //d_prvsIndex = 0;
   }
 private:
   /* Do all the hardwork. */ 
-  bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision);
+  bool findSplitterRec(Node node, SatValue value, SatLiteral* litDecision);
 
   /* Helper functions */
-  void setJustified(SatVariable v);
-  bool checkJustified(SatVariable v);
+  void setJustified(TNode);
+  bool checkJustified(TNode);
+  
+  /* If literal exists corresponding to the node return
+     that. Otherwise an UNKNOWN */
+  SatValue tryGetSatValue(Node n)
+  {
+    Debug("decision") << "   "  << n << " has sat value " << " ";
+    if(d_decisionEngine->hasSatLiteral(n) ) {
+      Debug("decision") << d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n)) << std::endl;
+      return d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n));
+    } else {
+      Debug("decision") << "NO SAT LITERAL" << std::endl;
+      return SAT_VALUE_UNKNOWN;
+    }
+  }
+
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c602d8b9c..79893a087 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -370,8 +370,9 @@ Lit Solver::pickBranchLit()
     }
 #endif /* CVC4_REPLAY */
 
-    // Theory requests
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+    // Theory/DE requests
+    bool stopSearch = false;
+    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
@@ -379,7 +380,10 @@ Lit Solver::pickBranchLit()
       } else {
         Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
       }
-      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+    }
+    if(stopSearch) {
+      return lit_Undef;
     }
 
     Var next = var_Undef;
@@ -1020,15 +1024,23 @@ lbool Solver::search(int nof_conflicts)
 
 	    // If this was a final check, we are satisfiable
             if (check_type == CHECK_FINAL) {
+	      bool decisionEngineDone = proxy->isDecisionEngineDone();
               // Unless a lemma has added more stuff to the queues
-              if (!order_heap.empty() || qhead < trail.size()) {
+              if (!decisionEngineDone  &&
+		  (!order_heap.empty() || qhead < trail.size()) ) {
                 check_type = CHECK_WITH_THEORY;
                 continue;
-              } else if (recheck) {
+              } else if (!decisionEngineDone && recheck) {
                 // There some additional stuff added, so we go for another full-check
                 continue;
               } else {
                 // Yes, we're truly satisfiable
+		if(decisionEngineDone) {
+		  // but we might know that only because of decision engine
+		  Trace("decision") << decisionEngineDone << " decision engine stopping us" << std::endl;
+		  interrupt();
+		  return l_Undef;
+		}
                 return l_True;
               }
             }
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index c8d310992..bed30d658 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -94,7 +94,8 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
 
   // Create the solver
   d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
-                                      Options::current()->incrementalSolving);
+                                      Options::current()->incrementalSolving || 
+                                      Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION );
   // Setup the verbosity
   d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 848c63a18..d1eaec231 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -112,6 +112,13 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
     Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
   }
 
+  /* Tell decision engine */
+  if(negated) {
+    NodeBuilder<> nb(kind::NOT);
+    nb << node;
+    d_decisionEngine->addAssertion(nb.constructNode());
+  }
+
   //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, removable, negated);
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index f024dccf3..53afce35e 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -73,7 +73,7 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
   d_theoryEngine->assertFact(literalNode);
 }
 
-SatLiteral TheoryProxy::getNextDecisionRequest() {
+SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   TNode n = d_theoryEngine->getNextDecisionRequest();
   if(not n.isNull())
     return d_cnfStream->getLiteral(n);
@@ -82,7 +82,12 @@ SatLiteral TheoryProxy::getNextDecisionRequest() {
   // may return in undefSatLiteral in which case the sat solver figure
   // it out something
   Assert(d_decisionEngine != NULL);
-  return d_decisionEngine->getNext();
+  Assert(stopSearch != true);
+  SatLiteral ret = d_decisionEngine->getNext(stopSearch);
+  if(stopSearch) {
+    Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
+  }
+  return ret;
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
@@ -178,5 +183,9 @@ void TheoryProxy::checkTime() {
   d_propEngine->checkTime();
 }
 
+bool TheoryProxy::isDecisionEngineDone() {
+  return d_decisionEngine->isDone();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index ceb328d90..f3fe634e2 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -85,7 +85,7 @@ public:
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
-  SatLiteral getNextDecisionRequest();
+  SatLiteral getNextDecisionRequest(bool& stopSearch);
 
   bool theoryNeedCheck() const;
 
@@ -112,6 +112,8 @@ public:
 
   void checkTime();
 
+  bool isDecisionEngineDone();
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a41def821..c95b9d197 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -244,13 +244,15 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_private(new smt::SmtEnginePrivate(*this)),
   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
-  d_staticLearningTime("smt::SmtEngine::staticLearningTime") {
+  d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
+  d_statResultSource("smt::resultSource", "unknown") {
 
   NodeManagerScope nms(d_nodeManager);
 
   StatisticsRegistry::registerStat(&d_definitionExpansionTime);
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::registerStat(&d_staticLearningTime);
+  StatisticsRegistry::registerStat(&d_statResultSource);
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -264,7 +266,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
     d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
   CVC4_FOR_EACH_THEORY;
 
-  d_decisionEngine = new DecisionEngine();
+  d_decisionEngine = new DecisionEngine(d_context);
   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
   // d_decisionEngine->setPropEngine(d_propEngine);
@@ -339,12 +341,15 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+    StatisticsRegistry::unregisterStat(&d_statResultSource);
+
 
     delete d_private;
     delete d_userContext;
 
     delete d_theoryEngine;
     delete d_propEngine;
+    //delete d_decisionEngine;
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
@@ -967,6 +972,7 @@ Result SmtEngine::check() {
 
   Trace("smt") << "SmtEngine::check(): running check" << endl;
   Result result = d_propEngine->checkSat(millis, resource);
+  d_statResultSource.setData("satSolver");
 
   // PropEngine::checkSat() returns the actual amount used in these
   // variables.
@@ -976,6 +982,14 @@ Result SmtEngine::check() {
   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
                  << ", conflicts " << d_cumulativeResourceUsed << endl;
 
+  if(result.isUnknown() and d_decisionEngine != NULL) {
+    Result deResult = d_decisionEngine->getResult();
+    if(not deResult.isUnknown()) {
+      d_statResultSource.setData("decisionEngine");
+      result = deResult;
+    }
+  }
+
   return result;
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index abd07538b..7feaa7e61 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -223,6 +223,9 @@ class CVC4_PUBLIC SmtEngine {
   TimerStat d_nonclausalSimplificationTime;
   /** time spent in static learning */
   TimerStat d_staticLearningTime;
+  /** how the SMT engine got the answer -- SAT solver or DE */
+  BackedStat<std::string> d_statResultSource;
+
 
 public:
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 0bd02f308..4e8bc375b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -172,6 +172,7 @@ Additional CVC4 options:\n\
    --print-expr-types     print types with variables when printing exprs\n\
    --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
+   --decision=MODE        choose decision mode, see --decision=help\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
@@ -225,6 +226,16 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
+static const string decisionHelp = "\
+Decision modes currently supported by the --decision option:\n\
+\n\
+internal (default)\n\
++ Use the internal decision hueristics of the SAT solver\n\
+\n\
+justification\n\
++ An ATGP-inspired justification heuristic\n\
+";
+
 static const string dumpHelp = "\
 Dump modes currently supported by the --dump option:\n\
 \n\
@@ -338,6 +349,7 @@ enum OptionValue {
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
   SIMPLIFICATION_MODE,
+  DECISION_MODE,
   NO_STATIC_LEARNING,
   INTERACTIVE,
   NO_INTERACTIVE,
@@ -426,6 +438,7 @@ static struct option cmdlineOptions[] = {
   { "uf"         , required_argument, NULL, UF_THEORY   },
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
+  { "decision", required_argument, NULL, DECISION_MODE },
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
@@ -696,6 +709,22 @@ throw(OptionException) {
       }
       break;
 
+    case DECISION_MODE:
+      if(!strcmp(optarg, "internal")) {
+        decisionMode = DECISION_STRATEGY_INTERNAL;
+        decisionModeSetByUser = true;
+      } else if(!strcmp(optarg, "justification")) {
+        decisionMode = DECISION_STRATEGY_JUSTIFICATION;
+        decisionModeSetByUser = true;
+      } else if(!strcmp(optarg, "help")) {
+        puts(decisionHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --decision: `") +
+                              optarg + "'.  Try --decision help.");
+      }
+      break;
+
     case NO_STATIC_LEARNING:
       doStaticLearning = false;
       break;