[proof] Fix open proof issues in SAT proof (#6887)

Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.

So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.

1 files changed, 11 insertions, 6 deletions

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 0f8ad8e69..ad23bedc9 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -162,6 +162,16 @@ void SatProofManager::endResChain(Node conclusion,
                                   const std::set<SatLiteral>& conclusionLits)
 {
   Trace("sat-proof") << ", " << conclusion << "\n";
+  if (d_resChains.hasGenerator(conclusion))
+  {
+    Trace("sat-proof")
+        << "SatProofManager::endResChain: skip repeated proof of " << conclusion
+        << "\n";
+    // clearing
+    d_resLinks.clear();
+    d_redundantLits.clear();
+    return;
+  }
   // first process redundant literals
   std::set<SatLiteral> visited;
   unsigned pos = d_resLinks.size();
@@ -240,11 +250,6 @@ void SatProofManager::endResChain(Node conclusion,
       return;
     }
   }
-  if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
-  {
-    Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "
-                       << conclusion << "\n";
-  }
   // since the conclusion can be both reordered and without duplicates and the
   // SAT solver does not record this information, we use a MACRO_RESOLUTION
   // step, which bypasses these. Note that we could generate a chain resolution
@@ -252,7 +257,7 @@ void SatProofManager::endResChain(Node conclusion,
   // post-processing.
   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
   // note that we must tell the proof generator to overwrite if repeated
-  d_resChainPg.addStep(conclusion, ps, CDPOverwrite::ALWAYS);
+  d_resChainPg.addStep(conclusion, ps);
   // the premises of this resolution may not have been justified yet, so we do
   // not pass assumptions to check closedness
   d_resChains.addLazyStep(conclusion, &d_resChainPg);