[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.

1 files changed, 17 insertions, 9 deletions

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"))
   {