hooked up "we are incomplete" flag after conversation with Tim (a theory notifies...

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index de60b5f7d7ca2be7e89a47ff7c5171961d0ded4f..d7b1e6d99afc49d0760783eb1256a0c6511e3c90 100644 (file)
--- 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 e3c8c584cfd7aedb7ab06a175859aefc52e9bdfb..2f2fba848c0fd562965f37ffe9d086d3c708c05b 100644 (file)
--- 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 cdc1e1cc20cf06129a3b027767bf16bb63b2804d..cc51c7a7c4dafe11084f23fbfd6282559d14845e 100644 (file)
--- 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 29aed8426b0d2be45c970c472e3b313c5126dd48..4113466d7ed11501587c8971e2df2185daa166b9 100644 (file)
--- 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 85e6d2cfc908b17deb67b7b61edd24d3dae15914..ca39001fe1491f0334b2095f59eb34d9774e73e4 100644 (file)
--- 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;
@@ -129,6 +140,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.
    */
@@ -205,6 +222,13 @@ public:
     d_propEngine = propEngine;
   }
 
+  /**
+   * 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

diff --git a/test/regress/regress0/bug216.smt2 b/test/regress/regress0/bug216.smt2
new file mode 100644 (file)
index 0000000..78e0f71
--- /dev/null
+++ b/test/regress/regress0/bug216.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (=> x y))
+(check-sat) ; returns sat
+(assert (=> y x))
+(assert (and x (not y)))
+(check-sat) ; returns sat --> ERROR

diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 5627a9db50c4523295b1dea01250e07c9d796b2b..4e7c198eeb037c152ab188fe6c8c53614282069b 100644 (file)
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -71,6 +71,7 @@ public:
     TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
     TS_ASSERT(i == x_and_y.end());
     TS_ASSERT(j == x_and_y.end());
+
     i = x_and_y.begin();
     TS_ASSERT(i != x_and_y.end());
     TS_ASSERT(*i == x);

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 57ce0c78ec73bb090b95a03980f5ed6335cc2421..f0da885c7b8b8b5c6fd21425ae02f8758cda2bba 100644 (file)
--- 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 96585768429b0ffe058b4a94fc10af59d3f3e187..6adbba207fd2831f85f8f606301dd3e06e0a37b0 100644 (file)
--- 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;