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

5 files changed, 63 insertions, 18 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index de60b5f7d..d7b1e6d99 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -58,13 +58,12 @@ public:
 };
 
 PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
-                       TheoryEngine* te, Context* context)
-: d_inCheckSat(false),
+                       TheoryEngine* te, Context* context) :
+  d_inCheckSat(false),
   d_options(opts),
   d_decisionEngine(de),
   d_theoryEngine(te),
-  d_context(context)
-{
+  d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
   d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
@@ -129,6 +128,9 @@ Result PropEngine::checkSat() {
 
   Debug("prop") << "PropEngine::checkSat() => "
                 << (result ? "true" : "false") << endl;
+  if(result && d_theoryEngine->isIncomplete()) {
+    return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
+  }
   return Result(result ? Result::SAT : Result::UNSAT);
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e3c8c584c..2f2fba848 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -530,7 +530,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
                    n.getMetaKind() == kind::metakind::VARIABLE ), e,
                  "expected variable or defined-function application "
                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
-  if(!d_options->interactive || !d_options->produceAssignments) {
+  if(!d_options->produceAssignments) {
     return false;
   }
   if(d_assignments == NULL) {
@@ -557,6 +557,10 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
     throw ModalException(msg);
   }
 
+  if(d_assignments == NULL) {
+    return SExpr();
+  }
+
   NodeManagerScope nms(d_nodeManager);
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
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.