Added OutputChannel::propagateAsDecision() functionality, allowing a theory

to request a decision on a literal.  All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision.  Requests that don't have a SAT literal give an assert-fail.  Requests
for literals that already have an assignment are silently ignored.

Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).

Performance impact: none to negligible for theories that don't use it
  See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0

3 files changed, 24 insertions, 1 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e1a8ded8e..cdab47163 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -355,13 +355,27 @@ void Solver::popTrail() {
 
 Lit Solver::pickBranchLit()
 {
+    Lit nextLit;
+
 #ifdef CVC4_REPLAY
-    Lit nextLit = proxy->getNextReplayDecision();
+    nextLit = proxy->getNextReplayDecision();
     if (nextLit != lit_Undef) {
       return nextLit;
     }
 #endif /* CVC4_REPLAY */
 
+    // Theory requests
+    nextLit = proxy->getNextDecisionRequest();
+    while (nextLit != lit_Undef) {
+      if(value(var(nextLit)) == l_Undef) {
+        Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
+        return nextLit;
+      } else {
+        Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
+      }
+      nextLit = proxy->getNextDecisionRequest();
+    }
+
     Var next = var_Undef;
 
     // Random decision:
@@ -699,6 +713,7 @@ void Solver::propagateTheory() {
   std::vector<Lit> propagatedLiterals;
   proxy->theoryPropagate(propagatedLiterals);
   int oldTrailSize = trail.size();
+  Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
   for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
     Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
     // multiple theories can propagate the same literal
@@ -707,6 +722,7 @@ void Solver::propagateTheory() {
       uncheckedEnqueue(p, CRef_Lazy);
     } else {
       // but we check that this is the case and that they agree
+      Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl;
       Assert(trail_index(var(p)) >= oldTrailSize);
       Assert(value(p) == lbool(!sign(p)));
     }
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 7df7535dd..559467922 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -71,6 +71,11 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   d_theoryEngine->assertFact(literalNode);
 }
 
+SatLiteral SatSolver::getNextDecisionRequest() {
+  TNode n = d_theoryEngine->getNextDecisionRequest();
+  return n.isNull() ? Minisat::lit_Undef : d_cnfStream->getLiteral(n);
+}
+
 bool SatSolver::theoryNeedCheck() const {
   return d_theoryEngine->needCheck();
 }
diff --git a/src/prop/sat.h b/src/prop/sat.h
index e86443827..3f3166c14 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -236,6 +236,8 @@ public:
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
+  SatLiteral getNextDecisionRequest();
+
   bool theoryNeedCheck() const;
 
   void setCnfStream(CnfStream* cnfStream);