From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 2 Nov 2011 01:48:41 +0000 (+0000)
Subject: fully implement the always-check-again-after-the-output-channel-is-used fix for bug... 
X-Git-Tag: cvc5-1.0.0~8391
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=161bf31cfa76271542790ec9a2c052e35d6bb1cb;p=cvc5.git

fully implement the always-check-again-after-the-output-channel-is-used fix for bug #275.  will finally close #275.
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 961ef85c5..8a883b1cb 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -654,6 +654,7 @@ CRef Solver::propagate(TheoryCheckType type)
         recheck = true;
         return updateLemmas();
       } else {
+        recheck = proxy->theoryNeedCheck();
         return confl;
       }
     }
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 5d53bf100..36f411df4 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -70,6 +70,10 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   d_theoryEngine->assertFact(literalNode);
 }
 
+bool SatSolver::theoryNeedCheck() const {
+  return d_theoryEngine->needCheck();
+}
+
 void SatSolver::setCnfStream(CnfStream* cnfStream) {
   d_cnfStream = cnfStream;
 }
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 026193eae..13b32f18d 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -230,6 +230,8 @@ public:
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
+  bool theoryNeedCheck() const;
+
   void setCnfStream(CnfStream* cnfStream);
 
   /** Call value() during the search.*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e09e9f47f..386b8bbd4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -125,6 +125,10 @@ void TheoryEngine::check(Theory::Effort effort) {
     // Mark the lemmas flag (no lemmas added)
     d_lemmasAdded = false;
 
+    // Mark the output channel unused (if this is FULL_EFFORT, and nothing
+    // is done by the theories, no additional check will be needed)
+    d_outputChannelUsed = false;
+
     while (true) {
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 09bb6963e..0d9500996 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -191,18 +191,21 @@ class TheoryEngine {
     void conflict(TNode conflictNode) throw(AssertionException) {
       Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
       ++ d_statistics.conflicts;
+      d_engine->d_outputChannelUsed = true;
       d_engine->conflict(conflictNode, d_theory);
     }
 
     void propagate(TNode literal) throw(AssertionException) {
       Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
       ++ d_statistics.propagations;
+      d_engine->d_outputChannelUsed = true;
       d_engine->propagate(literal, d_theory);
     }
 
     unsigned lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
       Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
+      d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable);
     }
 
@@ -343,6 +346,15 @@ class TheoryEngine {
    */
   bool d_lemmasAdded;
 
+  /**
+   * A variable to mark if the OutputChannel was "used" by any theory
+   * since the start of the last check.  If it has been, we require
+   * a FULL_EFFORT check before exiting and reporting SAT.
+   *
+   * See the documentation for the needCheck() function, below.
+   */
+  bool d_outputChannelUsed;
+
   /**
    * Adds a new lemma
    */
@@ -414,18 +426,38 @@ public:
   }
 
   /**
-   * Runs theory specific preprocesssing on the non-Boolean parts of the formula.
-   * This is only called on input assertions, after ITEs have been removed.
+   * Runs theory specific preprocesssing on the non-Boolean parts of
+   * the formula.  This is only called on input assertions, after ITEs
+   * have been removed.
    */
   Node preprocess(TNode node);
 
   /**
    * Return whether or not we are incomplete (in the current context).
    */
-  inline bool isIncomplete() {
+  inline bool isIncomplete() const {
     return d_incomplete;
   }
 
+  /**
+   * Returns true if we need another round of checking.  If this
+   * returns true, check(FULL_EFFORT) _must_ be called by the
+   * propositional layer before reporting SAT.
+   *
+   * This is especially necessary for incomplete theories that lazily
+   * output some lemmas on FULL_EFFORT check (e.g. quantifier reasoning
+   * outputing quantifier instantiations).  In such a case, a lemma can
+   * be asserted that is simplified away (perhaps it's already true).
+   * However, we must maintain the invariant that, if a theory uses the
+   * OutputChannel, it implicitly requests that another check(FULL_EFFORT)
+   * be performed before exit, even if no new facts are on its fact queue,
+   * as it might decide to further instantiate some lemmas, precluding
+   * a SAT response.
+   */
+  inline bool needCheck() const {
+    return d_outputChannelUsed || d_lemmasAdded;
+  }
+
   /**
    * This is called at shutdown time by the SmtEngine, just before
    * destruction.  It is important because there are destruction