diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-14 10:31:35 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-14 13:31:35 +0000 |
commit | d1eee40cc8788d38ec7431ea8d7429a5573a101c (patch) | |
tree | f3e994a1b58ce6a3686e73bc9b8e52c2da58175d /src/prop/sat_proof_manager.cpp | |
parent | 340380462989ff06d08567147bb16d0df9ddb1bc (diff) |
[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.
Diffstat (limited to 'src/prop/sat_proof_manager.cpp')
-rw-r--r-- | src/prop/sat_proof_manager.cpp | 26 |
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")) { |