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

1 files changed, 5 insertions, 0 deletions

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();
 }