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, 30 insertions, 6 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 85e6d2cfc..ca39001fe 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,8 +83,10 @@ class TheoryEngine {
 
     void newFact(TNode n);
 
-    void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
-      Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
+    void conflict(TNode conflictNode, bool safe)
+      throw(theory::Interrupted, AssertionException) {
+      Debug("theory") << "EngineOutputChannel::conflict("
+                      << conflictNode << ")" << std::endl;
       d_conflictNode = conflictNode;
       ++(d_engine->d_statistics.d_statConflicts);
       if(safe) {
@@ -92,23 +94,32 @@ class TheoryEngine {
       }
     }
 
-    void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) {
+    void propagate(TNode lit, bool)
+      throw(theory::Interrupted, AssertionException) {
       d_propagatedLiterals.push_back(lit);
       ++(d_engine->d_statistics.d_statPropagate);
     }
 
-    void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+    void lemma(TNode node, bool)
+      throw(theory::Interrupted, AssertionException) {
       ++(d_engine->d_statistics.d_statLemma);
       d_engine->newLemma(node);
     }
-    void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+    void augmentingLemma(TNode node, bool)
+      throw(theory::Interrupted, AssertionException) {
       ++(d_engine->d_statistics.d_statAugLemma);
       d_engine->newAugmentingLemma(node);
     }
-    void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) {
+    void explanation(TNode explanationNode, bool)
+      throw(theory::Interrupted, AssertionException) {
       d_explanationNode = explanationNode;
       ++(d_engine->d_statistics.d_statExplanation);
     }
+
+    void setIncomplete()
+      throw(theory::Interrupted, AssertionException) {
+      d_engine->d_incomplete = true;
+    }
   };/* class EngineOutputChannel */
 
   EngineOutputChannel d_theoryOut;
@@ -130,6 +141,12 @@ class TheoryEngine {
   bool d_hasShutDown;
 
   /**
+   * True if a theory has notified us of incompleteness (at this
+   * context level or below).
+   */
+  context::CDO<bool> d_incomplete;
+
+  /**
    * Check whether a node is in the pre-rewrite cache or not.
    */
   static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
@@ -206,6 +223,13 @@ public:
   }
 
   /**
+   * Return whether or not we are incomplete (in the current context).
+   */
+  bool isIncomplete() {
+    return d_incomplete;
+  }
+
+  /**
    * This is called at shutdown time by the SmtEngine, just before
    * destruction.  It is important because there are destruction
    * ordering issues between PropEngine and Theory.