From d1eee40cc8788d38ec7431ea8d7429a5573a101c Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Apr 2021 10:31:35 -0300
Subject: [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.
---
 src/expr/buffered_proof_generator.cpp | 19 +++++++++++++++++++
 src/expr/buffered_proof_generator.h   |  2 ++
 2 files changed, 21 insertions(+)

(limited to 'src/expr')

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"; }
 
-- 
cgit v1.2.3