Make difficulty manager only consider lemmas at full effort (#7685)

Fixes cvc5/cvc5-projects#350

3 files changed, 27 insertions, 9 deletions

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index a83167591..6b19f2146 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -29,6 +29,7 @@ RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val)
     : d_val(val),
       d_input(lemContext),
       d_computed(false),
+      d_inFullEffortCheck(false),
       d_success(false),
       d_trackRSetExp(false),
       d_miniscopeTopLevel(true)
@@ -100,11 +101,14 @@ void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
   }
 }
 
-void RelevanceManager::resetRound()
+void RelevanceManager::beginRound()
 {
   d_computed = false;
+  d_inFullEffortCheck = true;
 }
 
+void RelevanceManager::endRound() { d_inFullEffortCheck = false; }
+
 void RelevanceManager::computeRelevance()
 {
   d_computed = true;
@@ -351,7 +355,9 @@ const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
 
 void RelevanceManager::notifyLemma(Node n)
 {
-  if (d_dman != nullptr)
+  // only consider lemmas that were sent at full effort, when we have a
+  // complete SAT assignment.
+  if (d_dman != nullptr && d_inFullEffortCheck)
   {
     // ensure we know which literals are relevant, and why
     computeRelevance();
diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h
index 287694445..7d6434c6b 100644
--- a/src/theory/relevance_manager.h
+++ b/src/theory/relevance_manager.h
@@ -90,10 +90,12 @@ class RelevanceManager
   /** Singleton version of above */
   void notifyPreprocessedAssertion(Node n);
   /**
-   * Reset round, called at the beginning of a full effort check in
+   * Begin round, called at the beginning of a full effort check in
    * TheoryEngine.
    */
-  void resetRound();
+  void beginRound();
+  /** End round, called at the end of a full effort check in TheoryEngine. */
+  void endRound();
   /**
    * Is lit part of the current relevant selection? This computes the set of
    * relevant assertions if not already done so. This call is valid during a
@@ -165,6 +167,8 @@ class RelevanceManager
   std::unordered_set<TNode> d_rset;
   /** Have we computed the relevant selection this round? */
   bool d_computed;
+  /** Are we in a full effort check? */
+  bool d_inFullEffortCheck;
   /**
    * Did we succeed in computing the relevant selection? If this is false, there
    * was a syncronization issue between the input formula and the satisfying
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8622c86aa..ea1209b47 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -391,7 +391,7 @@ void TheoryEngine::check(Theory::Effort effort) {
       // to indicate that its information must be recomputed.
       if (d_relManager != nullptr)
       {
-        d_relManager->resetRound();
+        d_relManager->beginRound();
       }
       d_tc->resetRound();
     }
@@ -486,10 +486,18 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
-    if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
-      // Do post-processing of model from the theories (e.g. used for THEORY_SEP
-      // to construct heap model)
-      d_tc->postProcessModel(d_incomplete.get());
+    if (Theory::fullEffort(effort))
+    {
+      if (d_relManager != nullptr)
+      {
+        d_relManager->endRound();
+      }
+      if (!d_inConflict && !needCheck())
+      {
+        // Do post-processing of model from the theories (e.g. used for
+        // THEORY_SEP to construct heap model)
+        d_tc->postProcessModel(d_incomplete.get());
+      }
     }
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;