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: [PATCH] [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 ++
 src/prop/sat_proof_manager.cpp        | 26 +++++++++++++++++---------
 3 files changed, 38 insertions(+), 9 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"; }
 
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 00abb0b8f..5fdc0eb79 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -251,7 +251,8 @@ void SatProofManager::endResChain(Node conclusion,
   // rule here by explicitly computing the detailed steps, but leave this for
   // post-processing.
   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
-  d_resChainPg.addStep(conclusion, ps);
+  // note that we must tell the proof generator to overwrite if repeated
+  d_resChainPg.addStep(conclusion, ps, CDPOverwrite::ALWAYS);
   // 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);
@@ -335,6 +336,13 @@ void SatProofManager::explainLit(
   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
   Node litNode = getClauseNode(lit);
   Trace("sat-proof") << " [" << litNode << "]\n";
+  if (d_resChainPg.hasProofFor(litNode))
+  {
+    Trace("sat-proof") << "SatProofManager::explainLit: already justified "
+                       << lit << ", ABORT\n"
+                       << pop;
+    return;
+  }
   Minisat::Solver::TCRef reasonRef =
       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
   if (reasonRef == Minisat::Solver::TCRef_Undef)
@@ -379,20 +387,20 @@ void SatProofManager::explainLit(
     AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
     AlwaysAssert(children[0] == getClauseNode(reloadedReason));
 #endif
-    SatLiteral curr_lit = d_cnfStream->getTranslationCache()[toExplain[i]];
+    SatLiteral currLit = d_cnfStream->getTranslationCache()[toExplain[i]];
     // ignore the lit we are trying to explain...
-    if (curr_lit == lit)
+    if (currLit == lit)
     {
       continue;
     }
     std::unordered_set<TNode, TNodeHashFunction> childPremises;
-    explainLit(~curr_lit, childPremises);
+    explainLit(~currLit, childPremises);
     // save to resolution chain premises / arguments
-    Assert(d_cnfStream->getNodeCache().find(curr_lit)
+    Assert(d_cnfStream->getNodeCache().find(currLit)
            != d_cnfStream->getNodeCache().end());
-    children.push_back(d_cnfStream->getNodeCache()[~curr_lit]);
-    Node currLitNode = d_cnfStream->getNodeCache()[curr_lit];
-    bool negated = curr_lit.isNegated();
+    children.push_back(d_cnfStream->getNodeCache()[~currLit]);
+    Node currLitNode = d_cnfStream->getNodeCache()[currLit];
+    bool negated = currLit.isNegated();
     Assert(!negated || currLitNode.getKind() == kind::NOT);
     // note this is the opposite of what is done in addResolutionStep. This is
     // because here the clause, which contains the literal being analyzed, is
@@ -401,7 +409,7 @@ void SatProofManager::explainLit(
     args.push_back(negated ? currLitNode[0] : currLitNode);
     // add child premises and the child itself
     premises.insert(childPremises.begin(), childPremises.end());
-    premises.insert(d_cnfStream->getNodeCache()[~curr_lit]);
+    premises.insert(d_cnfStream->getNodeCache()[~currLit]);
   }
   if (Trace.isOn("sat-proof"))
   {
-- 
2.30.2