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

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 0e47cd7f2..71bbefb6a 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -107,6 +107,24 @@ public:
   virtual void propagate(TNode n) throw(AssertionException) = 0;
 
   /**
+   * Request that the core make a decision on this atom.  The decision
+   * will be "as soon as possible," but due to other propagation and
+   * conflict-detection work going on internally, the request is queued
+   * up and may be behind other such requests.  The request will be
+   * silently dropped if the atom has a definite value at the point the
+   * request would be serviced.  This request is also context-dependent
+   * on the search context, meaning that it will be dropped completely
+   * if a conflict is found before it is serviced.  Each request will only
+   * be serviced a single time, even though the atom may become undefined
+   * due to backtracking.
+   *
+   * @param atom the atom to decide upon (or the negation of an
+   * atom---the decision will be in the phase provided); must be
+   * associated to a SAT literal.
+   */
+  virtual void propagateAsDecision(TNode n) throw(AssertionException) = 0;
+
+  /**
    * Tell the core that a valid theory lemma at decision level 0 has
    * been detected.  (This requests a split.)
    *