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

3 files changed, 52 insertions, 13 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 */
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 29aed8426..4113466d7 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -130,6 +130,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
   d_propEngine(NULL),
   d_theoryOut(this, ctxt),
   d_hasShutDown(false),
+  d_incomplete(ctxt, false),
   d_statistics() {
 
   d_sharedTermManager = new SharedTermManager(this, ctxt);
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.