Improvements for get-difficulty (#7720)

This makes 2 improvements for get-difficulty:
(1) Ensures that we recompute relevance info for lemmas sent at STANDARD effort.
(2) An open proof error was reported by Certora using --produce-difficulty.
This makes get-difficulty more robust by ensuring that lemmas are not marked as having a difficulty. It also minimizes the cases where we mark lemmas as having a difficulty internally.

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 4b42910758b33e5e4c9cba59291da2201d96a8b7..4cb9d5bf98908442f364bccf10b9794ec133992b 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -227,11 +227,20 @@ void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
   std::map<Node, Node> dmapp = dmap;
   dmap.clear();
   std::vector<Node> ppAsserts;
+  std::vector<Node> asserts;
+  getAssertions(as, asserts);
   for (const std::pair<const Node, Node>& ppa : dmapp)
   {
     Trace("difficulty") << "  preprocess difficulty: " << ppa.second << " for "
                         << ppa.first << std::endl;
-    ppAsserts.push_back(ppa.first);
+    // Ensure that only input assertions are marked as having a difficulty.
+    // In some cases, a lemma may be marked as having a difficulty
+    // internally, e.g. for lemmas that require justification, which we should
+    // skip or otherwise we end up with an open proof below.
+    if (std::find(asserts.begin(), asserts.end(), ppa.first) != asserts.end())
+    {
+      ppAsserts.push_back(ppa.first);
+    }
   }
   // assume a SAT refutation from all input assertions that were marked
   // as having a difficulty

diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp
index c0912077170f41af90bb9b399390a7b2b7217acb..0a9eba60d7e69a6f0f4cfd043933e780db2d43da 100644 (file)
--- a/src/theory/difficulty_manager.cpp
+++ b/src/theory/difficulty_manager.cpp
@@ -69,6 +69,9 @@ void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n)
     bool pol = nc.getKind() != kind::NOT;
     TNode atom = pol ? nc : nc[0];
     it = rse.find(atom);
+    Trace("diff-man-debug")
+        << "Check literal: " << atom << ", has reason = " << (it != rse.end())
+        << std::endl;
     if (it != rse.end())
     {
       incrementDifficulty(it->second);

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 6b19f214694eefa64209df0972f0d6aa6d790389..972a2918c2c2a5ac68eadd23251101663452eea8 100644 (file)
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -29,7 +29,6 @@ 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)
@@ -104,11 +103,8 @@ void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
 void RelevanceManager::beginRound()
 {
   d_computed = false;
-  d_inFullEffortCheck = true;
 }
 
-void RelevanceManager::endRound() { d_inFullEffortCheck = false; }
-
 void RelevanceManager::computeRelevance()
 {
   d_computed = true;
@@ -116,24 +112,35 @@ void RelevanceManager::computeRelevance()
   d_rsetExp.clear();
   Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
   std::unordered_map<TNode, int> cache;
+  d_success = true;
   for (const Node& node: d_input)
   {
     TNode n = node;
     int val = justify(n, cache);
     if (val != 1)
     {
-      std::stringstream serr;
-      serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
-           << n;
-      Trace("rel-manager") << serr.str() << std::endl;
-      Assert(false) << serr.str();
+      if (Trace.isOn("rel-manager"))
+      {
+        std::stringstream serr;
+        serr
+            << "RelevanceManager::computeRelevance: WARNING: failed to justify "
+            << n;
+        Trace("rel-manager") << serr.str() << std::endl;
+      }
       d_success = false;
-      d_rset.clear();
-      return;
+      // If we fail to justify an assertion, we set success to false and
+      // continue to try to justify the remaining assertions. This is important
+      // for cases where the difficulty manager is measuring based on lemmas
+      // that are being sent at STANDARD effort, before all assertions are
+      // satisfied.
     }
   }
+  if (!d_success)
+  {
+    d_rset.clear();
+    return;
+  }
   Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
-  d_success = true;
 }
 
 bool RelevanceManager::isBooleanConnective(TNode cur)
@@ -357,7 +364,7 @@ void RelevanceManager::notifyLemma(Node n)
 {
   // only consider lemmas that were sent at full effort, when we have a
   // complete SAT assignment.
-  if (d_dman != nullptr && d_inFullEffortCheck)
+  if (d_dman != nullptr)
   {
     // 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 7d6434c6be2d107f38a1be24131c35570ab6ecab..fbc50801c675a66b4d19f32717e82e893b11fa36 100644 (file)
--- a/src/theory/relevance_manager.h
+++ b/src/theory/relevance_manager.h
@@ -90,12 +90,9 @@ class RelevanceManager
   /** Singleton version of above */
   void notifyPreprocessedAssertion(Node n);
   /**
-   * Begin round, called at the beginning of a full effort check in
-   * TheoryEngine.
+   * Begin round, called at the beginning of a check in TheoryEngine.
    */
   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

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ea1209b47c5f992fcb3fe9b5f9c1b56ca29ead1f..1b2ad3358fd54641cd376f8a0f139fb870d1c0c2 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -384,15 +384,15 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
 
+    // Reset round for the relevance manager, which notice only sets a flag
+    // to indicate that its information must be recomputed.
+    if (d_relManager != nullptr)
+    {
+      d_relManager->beginRound();
+    }
     // If in full effort, we have a fake new assertion just to jumpstart the checking
     if (Theory::fullEffort(effort)) {
       d_factsAsserted = true;
-      // Reset round for the relevance manager, which notice only sets a flag
-      // to indicate that its information must be recomputed.
-      if (d_relManager != nullptr)
-      {
-        d_relManager->beginRound();
-      }
       d_tc->resetRound();
     }
 
@@ -488,10 +488,6 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     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
@@ -1319,7 +1315,7 @@ void TheoryEngine::lemma(TrustNode tlemma,
     std::vector<Node> sks;
     Node retLemma =
         d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
-    if (isLemmaPropertyNeedsJustify(p))
+    if (options().theory.relevanceFilter && isLemmaPropertyNeedsJustify(p))
     {
       d_relManager->notifyPreprocessedAssertion(retLemma);
       d_relManager->notifyPreprocessedAssertions(skAsserts);