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, 13 insertions, 2 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 75c64654d..c4a8dc591 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -55,6 +55,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_logic(""),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
+  d_decisionRequests(context),
+  d_decisionRequestsIndex(context, 0),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms)
 {
@@ -665,13 +667,22 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   }
 }
 
+void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
+  Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl;
+
+  d_propEngine->checkTime();
+
+  Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)");
+
+  d_decisionRequests.push_back(literal);
+}
+
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType() == b.getType());
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
-Node TheoryEngine::getExplanation(TNode node)
-{
+Node TheoryEngine::getExplanation(TNode node) {
   Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
 
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;