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

2 files changed, 18 insertions, 5 deletions

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 57ce0c78e..f0da885c7 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -52,25 +52,35 @@ public:
 
   void safePoint() throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+  void conflict(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+  void propagate(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(PROPAGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+  void lemma(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(LEMMA, n);
   }
-  void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+  void augmentingLemma(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     Unreachable();
   }
 
-  void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+  void explanation(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(EXPLANATION, n);
   }
 
+  void setIncomplete()
+    throw(Interrupted, AssertionException) {
+    Unreachable();
+  }
+
   void clear() {
     d_callHistory.clear();
   }
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 965857684..6adbba207 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -62,6 +62,9 @@ class FakeOutputChannel : public OutputChannel {
   void explanation(TNode n, bool safe) throw(AssertionException) {
     Unimplemented();
   }
+  void setIncomplete() throw(AssertionException) {
+    Unimplemented()
+  }
 };/* class FakeOutputChannel */
 
 class FakeTheory;