hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216

1 files changed, 21 insertions, 7 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index cdc1e1cc2..cc51c7a7c 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -76,7 +76,8 @@ public:
    *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+  virtual void conflict(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -85,7 +86,8 @@ public:
    *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+  virtual void propagate(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
@@ -94,16 +96,19 @@ public:
    * @param n - a theory lemma valid at decision level 0
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+  virtual void lemma(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) = 0;
 
   /**
-   * Tell the core to add the following valid lemma as if it were a user assertion.
-   * This should NOT be called during solving, only preprocessing.
+   * Tell the core to add the following valid lemma as if it were a
+   * user assertion.  This should NOT be called during solving, only
+   * preprocessing.
    *
    * @param n - a theory lemma valid to be asserted
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+  virtual void augmentingLemma(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) = 0;
 
   /**
    * Provide an explanation in response to an explanation request.
@@ -111,7 +116,16 @@ public:
    * @param n - an explanation
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+  virtual void explanation(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) = 0;
+
+  /**
+   * Notification from a theory that it realizes it is incomplete at
+   * this context level.  If SAT is later determined by the
+   * TheoryEngine, it should actually return an UNKNOWN result.
+   */
+  virtual void setIncomplete()
+    throw(Interrupted, AssertionException) = 0;
 
 };/* class OutputChannel */