[proof-new] Fix explanation of literals in SAT proof manager (#6346)

Prevents exponential behavior in SAT proof generation by not reexplaining previously explained literals. Also fix a potential issue in not previously overwriting rederived resolution chains during solving.

2 files changed, 21 insertions, 0 deletions

diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index b37295c52..2cbbd7e91 100644
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -81,4 +81,23 @@ std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
   return cdp.getProofFor(fact);
 }
 
+bool BufferedProofGenerator::hasProofFor(Node f)
+{
+  NodeProofStepMap::iterator it = d_facts.find(f);
+  if (it == d_facts.end())
+  {
+    Node symFact = CDProof::getSymmFact(f);
+    if (symFact.isNull())
+    {
+      return false;
+    }
+    it = d_facts.find(symFact);
+    if (it == d_facts.end())
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
 }  // namespace cvc5
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 81e2667bf..89e8b196d 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -48,6 +48,8 @@ class BufferedProofGenerator : public ProofGenerator
                CDPOverwrite opolicy = CDPOverwrite::NEVER);
   /** Get proof for. It is robust to (dis)equality symmetry. */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Whether a step has been registered for f. */
+  bool hasProofFor(Node f) override;
   /** identify */
   std::string identify() const override { return "BufferedProofGenerator"; }