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

5 files changed, 40 insertions, 9 deletions

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. */