fix issue with repeated rewrites breaking assumptions map

HanielB · Aug 9, 2023 · 70d8fc8 · 70d8fc8
1 parent 20e4576
commit 70d8fc8
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 8 deletions.
diff --git a/src/proof/lean/lean_post_processor.cpp b/src/proof/lean/lean_post_processor.cpp
@@ -356,10 +356,15 @@ bool LeanProofPostprocessCallback::update(Node res,
         s.erase(0, 6);
         ss << s;
       }
-      d_newRewriteAssumptions.insert(
-          nm->mkNode(kind::SEXPR,
-                     d_lnc.convert(res),
-                     nm->mkBoundVar(ss.str(), nm->sExprType())));
+      // we will only add if fresh, since when printing the assumptions are
+      // retrieved via node hashing
+      Node assump = d_lnc.convert(res);
+      if (!d_newAssumptionsCollected.count(assump))
+      {
+        d_newRewriteAssumptions.insert(nm->mkNode(
+            kind::SEXPR, assump, nm->mkBoundVar(ss.str(), nm->sExprType())));
+        d_newAssumptionsCollected.insert(assump);
+      }
       // Make this an assumption
       cdp->addStep(res, PfRule::ASSUME, {}, {res}, false, CDPOverwrite::ALWAYS);
       break;
@@ -1428,11 +1433,16 @@ bool LeanProofPostprocessCallback::update(Node res,
         s.erase(0, 6);
         ss << s;
       }
+      // we will only add if fresh, since when printing the assumptions are
+      // retrieved via node hashing
+      Node assump = d_lnc.convert(res);
+      if (!d_newAssumptionsCollected.count(assump))
+      {
+        d_newHoleAssumptions.insert(nm->mkNode(
+            kind::SEXPR, assump, nm->mkBoundVar(ss.str(), nm->sExprType())));
+        d_newAssumptionsCollected.insert(assump);
+      }
       // Make this an assumption
-      d_newHoleAssumptions.insert(
-          nm->mkNode(kind::SEXPR,
-                     d_lnc.convert(res),
-                     nm->mkBoundVar(ss.str(), nm->sExprType())));
       cdp->addStep(res, PfRule::ASSUME, {}, {res}, false, CDPOverwrite::ALWAYS);
       break;
     }

diff --git a/src/proof/lean/lean_post_processor.h b/src/proof/lean/lean_post_processor.h
@@ -65,6 +65,7 @@ class LeanProofPostprocessCallback : public ProofNodeUpdaterCallback
    */
   std::unordered_set<Node> d_newRewriteAssumptions;
   std::unordered_set<Node> d_newHoleAssumptions;
+  std::unordered_set<Node> d_newAssumptionsCollected;
 
  protected:
   /** The node converter */