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, 7 insertions, 0 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 96bd02b5a..aaf47425b 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -41,6 +41,7 @@ namespace theory {
 enum OutputChannelCallType {
   CONFLICT,
   PROPAGATE,
+  PROPAGATE_AS_DECISION,
   AUG_LEMMA,
   LEMMA,
   EXPLANATION
@@ -52,6 +53,7 @@ inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType
   switch(type) {
   case theory::CONFLICT: return out << "CONFLICT";
   case theory::PROPAGATE: return out << "PROPAGATE";
+  case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
   case theory::AUG_LEMMA: return out << "AUG_LEMMA";
   case theory::LEMMA: return out << "LEMMA";
   case theory::EXPLANATION: return out << "EXPLANATION";
@@ -81,6 +83,11 @@ public:
     push(PROPAGATE, n);
   }
 
+  void propagateAsDecision(TNode n)
+    throw(AssertionException) {
+    push(PROPAGATE_AS_DECISION, n);
+  }
+
   LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);