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;