From d4564e7ef8eb277fcfc42c3130a3180165594b58 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 28 Sep 2020 17:38:59 -0300 Subject: [proof-new] Adds a proof manager for the SAT solver (#5140) Tracks the refutation proof built by Minisat. See the header for extensive explanations. This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links). --- src/CMakeLists.txt | 2 + src/expr/lazy_proof_chain.cpp | 14 + src/expr/lazy_proof_chain.h | 4 + src/prop/minisat/core/Solver.h | 2 + src/prop/sat_proof_manager.cpp | 722 +++++++++++++++++++++++++++++++++++++++++ src/prop/sat_proof_manager.h | 587 +++++++++++++++++++++++++++++++++ src/prop/theory_proxy.cpp | 2 + src/prop/theory_proxy.h | 5 +- 8 files changed, 1336 insertions(+), 2 deletions(-) create mode 100644 src/prop/sat_proof_manager.cpp create mode 100644 src/prop/sat_proof_manager.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 74dcc39b3..620bcc352 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -190,6 +190,8 @@ libcvc4_add_sources( prop/sat_solver_factory.cpp prop/sat_solver_factory.h prop/bv_sat_solver_notify.h + prop/sat_proof_manager.cpp + prop/sat_proof_manager.h prop/sat_solver_types.cpp prop/sat_solver_types.h prop/theory_proxy.cpp diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index a01d541eb..95704d82a 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -29,6 +29,20 @@ LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm, LazyCDProofChain::~LazyCDProofChain() {} +const std::map> LazyCDProofChain::getLinks() + const +{ + std::map> links; + for (const std::pair& link : d_gens) + { + Assert(link.second); + std::shared_ptr pfn = link.second->getProofFor(link.first); + Assert(pfn); + links[link.first] = pfn; + } + return links; +} + std::shared_ptr LazyCDProofChain::getProofFor(Node fact) { Trace("lazy-cdproofchain") diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 7fa49bccc..a58cc5c7d 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -119,6 +119,10 @@ class LazyCDProofChain : public ProofGenerator /** identify */ std::string identify() const override; + /** Retrieve, for each fact in d_gens, it mapped to the proof node generated + * by its generator in d_gens. */ + const std::map> getLinks() const; + private: /** The proof manager, used for allocating new ProofNode objects */ ProofNodeManager* d_manager; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 0630df1b7..f3bcfb67e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -33,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Heap.h" #include "prop/minisat/mtl/Vec.h" #include "prop/minisat/utils/Options.h" +#include "prop/sat_proof_manager.h" #include "theory/theory.h" @@ -55,6 +56,7 @@ class Solver { /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::TheoryProxy; + friend class CVC4::prop::SatProofManager; friend class CVC4::TSatProof; public: diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp new file mode 100644 index 000000000..36913fda8 --- /dev/null +++ b/src/prop/sat_proof_manager.cpp @@ -0,0 +1,722 @@ +/********************* */ +/*! \file sat_proof_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the proof manager for Minisat + **/ + +#include "prop/sat_proof_manager.h" + +#include "expr/proof_node_algorithm.h" +#include "options/smt_options.h" +#include "prop/cnf_stream.h" +#include "prop/minisat/minisat.h" +#include "theory/theory_proof_step_buffer.h" + +namespace CVC4 { +namespace prop { + +SatProofManager::SatProofManager(Minisat::Solver* solver, + CnfStream* cnfStream, + context::UserContext* userContext, + ProofNodeManager* pnm) + : d_solver(solver), + d_cnfStream(cnfStream), + d_pnm(pnm), + d_resChains(pnm, true, userContext), + d_resChainPg(userContext, pnm), + d_assumptions(userContext), + d_conflictLit(undefSatVariable) +{ + d_false = NodeManager::currentNM()->mkConst(false); +} + +void SatProofManager::printClause(const Minisat::Clause& clause) +{ + for (unsigned i = 0, size = clause.size(); i < size; ++i) + { + SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); + Trace("sat-proof") << satLit << " "; + } +} + +Node SatProofManager::getClauseNode(SatLiteral satLit) +{ + Assert(d_cnfStream->getNodeCache().find(satLit) + != d_cnfStream->getNodeCache().end()) + << "SatProofManager::getClauseNode: literal " << satLit + << " undefined.\n"; + return d_cnfStream->getNodeCache()[satLit]; +} + +Node SatProofManager::getClauseNode(const Minisat::Clause& clause) +{ + std::vector clauseNodes; + for (unsigned i = 0, size = clause.size(); i < size; ++i) + { + SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); + Assert(d_cnfStream->getNodeCache().find(satLit) + != d_cnfStream->getNodeCache().end()) + << "SatProofManager::getClauseNode: literal " << satLit + << " undefined\n"; + clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]); + } + // order children by node id + std::sort(clauseNodes.begin(), clauseNodes.end()); + return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes); +} + +void SatProofManager::startResChain(const Minisat::Clause& start) +{ + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "SatProofManager::startResChain: "; + printClause(start); + Trace("sat-proof") << "\n"; + } + d_resLinks.push_back( + std::pair(getClauseNode(start), Node::null())); +} + +void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant) +{ + SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); + if (!redundant) + { + Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit + << "] " << ~satLit << "\n"; + d_resLinks.push_back( + std::pair(d_cnfStream->getNodeCache()[~satLit], + d_cnfStream->getNodeCache()[satLit])); + } + else + { + Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit " + << satLit << " stored\n"; + d_redundantLits.push_back(satLit); + } +} + +void SatProofManager::addResolutionStep(const Minisat::Clause& clause, + Minisat::Lit lit) +{ + // the given clause is supposed to be the second in a resolution, with the + // given literal as the pivot occurring positive in the first and negatively + // in the second clause. Thus, we store its negation + SatLiteral satLit = MinisatSatSolver::toSatLiteral(~lit); + Node clauseNode = getClauseNode(clause); + d_resLinks.push_back( + std::pair(clauseNode, d_cnfStream->getNodeCache()[satLit])); + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit + << "] "; + printClause(clause); + Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t" + << clauseNode << "\n"; + } +} + +void SatProofManager::endResChain(Minisat::Lit lit) +{ + SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); + Trace("sat-proof") << "SatProofManager::endResChain: chain_res for " + << satLit; + endResChain(getClauseNode(satLit), {satLit}); +} + +void SatProofManager::endResChain(const Minisat::Clause& clause) +{ + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "; + printClause(clause); + } + std::set clauseLits; + for (unsigned i = 0, size = clause.size(); i < size; ++i) + { + clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i])); + } + endResChain(getClauseNode(clause), clauseLits); +} + +void SatProofManager::endResChain(Node conclusion, + const std::set& conclusionLits) +{ + Trace("sat-proof") << ", " << conclusion << "\n"; + // first process redundant literals + std::set visited; + unsigned pos = d_resLinks.size(); + for (SatLiteral satLit : d_redundantLits) + { + processRedundantLit(satLit, conclusionLits, visited, pos); + } + d_redundantLits.clear(); + // build resolution chain + std::vector children, args; + for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i) + { + children.push_back(d_resLinks[i].first); + Trace("sat-proof") << "SatProofManager::endResChain: "; + if (i > 0) + { + Trace("sat-proof") + << "[" << d_cnfStream->getTranslationCache()[d_resLinks[i].second] + << "] "; + } + // special case for clause (or l1 ... ln) being a single literal + // corresponding itself to a clause, which is indicated by the pivot being + // of the form (not (or l1 ... ln)) + if (d_resLinks[i].first.getKind() == kind::OR + && !(d_resLinks[i].second.getKind() == kind::NOT + && d_resLinks[i].second[0].getKind() == kind::OR + && d_resLinks[i].second[0] == d_resLinks[i].first)) + { + for (unsigned j = 0, sizeJ = d_resLinks[i].first.getNumChildren(); + j < sizeJ; + ++j) + { + Trace("sat-proof") + << d_cnfStream->getTranslationCache()[d_resLinks[i].first[j]]; + if (j < sizeJ - 1) + { + Trace("sat-proof") << ", "; + } + } + } + else + { + Assert(d_cnfStream->getTranslationCache().find(d_resLinks[i].first) + != d_cnfStream->getTranslationCache().end()) + << "clause node " << d_resLinks[i].first + << " treated as unit has no literal. Pivot is " + << d_resLinks[i].second << "\n"; + Trace("sat-proof") + << d_cnfStream->getTranslationCache()[d_resLinks[i].first]; + } + Trace("sat-proof") << " : "; + if (i > 0) + { + args.push_back(d_resLinks[i].second); + Trace("sat-proof") << "[" << d_resLinks[i].second << "] "; + } + Trace("sat-proof") << d_resLinks[i].first << "\n"; + } + // clearing + d_resLinks.clear(); + // whether no-op + if (children.size() == 1) + { + Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion " + << conclusion << " is set-equal to premise " + << children[0] << "\n"; + return; + } + if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion)) + { + Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of " + << conclusion << "\n"; + } + // since the conclusion can be both reordered and without duplicates and the + // SAT solver does not record this information, we must recompute it here so + // the proper CHAIN_RESOLUTION step can be created + // compute chain resolution conclusion + Node chainConclusion = d_pnm->getChecker()->checkDebug( + PfRule::CHAIN_RESOLUTION, children, args, Node::null(), ""); + Trace("sat-proof") + << "SatProofManager::endResChain: creating step for computed conclusion " + << chainConclusion << "\n"; + // buffer steps + theory::TheoryProofStepBuffer psb; + psb.addStep(PfRule::CHAIN_RESOLUTION, children, args, chainConclusion); + if (chainConclusion != conclusion) + { + // if this happens that chainConclusion needs to be factored and/or + // reordered, which in either case can be done only if it's not a unit + // clause. + CVC4_UNUSED Node reducedChainConclusion = + psb.factorReorderElimDoubleNeg(chainConclusion); + Assert(reducedChainConclusion == conclusion) + << "original conclusion " << conclusion + << "\nis different from computed conclusion " << chainConclusion + << "\nafter factorReorderElimDoubleNeg " << reducedChainConclusion; + } + // buffer the steps in the resolution chain proof generator + const std::vector>& steps = psb.getSteps(); + for (const std::pair& step : steps) + { + Trace("sat-proof") << "SatProofManager::endResChain: adding for " + << step.first << " step " << step.second << "\n"; + d_resChainPg.addStep(step.first, step.second); + // the premises of this resolution may not have been justified yet, so we do + // not pass assumptions to check closedness + d_resChains.addLazyStep(step.first, &d_resChainPg); + } +} + +void SatProofManager::processRedundantLit( + SatLiteral lit, + const std::set& conclusionLits, + std::set& visited, + unsigned pos) +{ + Trace("sat-proof") << push + << "SatProofManager::processRedundantLit: Lit: " << lit + << "\n"; + if (visited.count(lit)) + { + Trace("sat-proof") << "already visited\n" << pop; + return; + } + Minisat::Solver::TCRef reasonRef = + d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit))); + if (reasonRef == Minisat::Solver::TCRef_Undef) + { + Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos + << "\n" + << pop; + visited.insert(lit); + d_resLinks.insert(d_resLinks.begin() + pos, + std::pair(d_cnfStream->getNodeCache()[~lit], + d_cnfStream->getNodeCache()[lit])); + return; + } + Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size()) + << "reasonRef " << reasonRef << " and d_satSolver->ca.size() " + << d_solver->ca.size() << "\n"; + const Minisat::Clause& reason = d_solver->ca[reasonRef]; + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "reason: "; + printClause(reason); + Trace("sat-proof") << "\n"; + } + // check if redundant literals in the reason. The first literal is the one we + // will be eliminating, so we check the others + for (unsigned i = 1, size = reason.size(); i < size; ++i) + { + SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]); + // if literal does not occur in the conclusion we process it as well + if (!conclusionLits.count(satLit)) + { + processRedundantLit(satLit, conclusionLits, visited, pos); + } + } + Assert(!visited.count(lit)); + visited.insert(lit); + Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos + << "\n" + << pop; + // add the step before steps for children. Note that the step is with the + // reason, not only with ~lit, since the learned clause is built under the + // assumption that the redundant literal is removed via the resolution with + // the explanation of its negation + Node clauseNode = getClauseNode(reason); + d_resLinks.insert( + d_resLinks.begin() + pos, + std::pair(clauseNode, d_cnfStream->getNodeCache()[lit])); +} + +void SatProofManager::explainLit( + SatLiteral lit, std::unordered_set& premises) +{ + Node litNode = getClauseNode(lit); + Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit + << " [" << litNode << "]\n"; + Minisat::Solver::TCRef reasonRef = + d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit))); + if (reasonRef == Minisat::Solver::TCRef_Undef) + { + Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop; + return; + } + Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size()) + << "reasonRef " << reasonRef << " and d_satSolver->ca.size() " + << d_solver->ca.size() << "\n"; + const Minisat::Clause& reason = d_solver->ca[reasonRef]; + unsigned size = reason.size(); + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "SatProofManager::explainLit: with clause: "; + printClause(reason); + Trace("sat-proof") << "\n"; + } + // pedantically check that the negation of the literal to explain *does not* + // occur in the reason, otherwise we will loop forever + for (unsigned i = 0; i < size; ++i) + { + AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit) + << "cyclic justification\n"; + } + // add the reason clause first + std::vector children{getClauseNode(reason)}, args; + // save in the premises + premises.insert(children.back()); + Trace("sat-proof") << push; + for (unsigned i = 0; i < size; ++i) + { + SatLiteral curr_lit = MinisatSatSolver::toSatLiteral(reason[i]); + // ignore the lit we are trying to explain... + if (curr_lit == lit) + { + continue; + } + std::unordered_set childPremises; + explainLit(~curr_lit, childPremises); + // save to resolution chain premises / arguments + Assert(d_cnfStream->getNodeCache().find(curr_lit) + != d_cnfStream->getNodeCache().end()); + children.push_back(d_cnfStream->getNodeCache()[~curr_lit]); + args.push_back(d_cnfStream->getNodeCache()[curr_lit]); + // add child premises and the child itself + premises.insert(childPremises.begin(), childPremises.end()); + premises.insert(d_cnfStream->getNodeCache()[~curr_lit]); + } + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for " + << lit << ", " << litNode << " with clauses:\n"; + for (unsigned i = 0, csize = children.size(); i < csize; ++i) + { + Trace("sat-proof") << "SatProofManager::explainLit: " << children[i]; + if (i > 0) + { + Trace("sat-proof") << " [" << args[i - 1] << "]"; + } + Trace("sat-proof") << "\n"; + } + } + // if justification of children contains the expected conclusion, avoid the + // cyclic proof by aborting. + if (premises.count(litNode)) + { + Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit + << " [" << litNode << "], ABORT\n" + << pop; + return; + } + Trace("sat-proof") << pop; + // create step + ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args); + d_resChainPg.addStep(litNode, ps); + // the premises in the limit of the justification may correspond to other + // links in the chain which have, themselves, literals yet to be justified. So + // we are not ready yet to check closedness w.r.t. CNF transformation of the + // preprocessed assertions + d_resChains.addLazyStep(litNode, &d_resChainPg); +} + +void SatProofManager::finalizeProof(Node inConflictNode, + const std::vector& inConflict) +{ + Trace("sat-proof") + << "SatProofManager::finalizeProof: conflicting clause node: " + << inConflictNode << "\n"; + // nothing to do + if (inConflictNode == d_false) + { + return; + } + if (Trace.isOn("sat-proof-debug2")) + { + Trace("sat-proof-debug2") + << push << "SatProofManager::finalizeProof: saved proofs in chain:\n"; + std::map> links = d_resChains.getLinks(); + std::unordered_set skip; + for (const std::pair>& link : links) + { + if (skip.count(link.first)) + { + continue; + } + auto it = d_cnfStream->getTranslationCache().find(link.first); + if (it != d_cnfStream->getTranslationCache().end()) + { + Trace("sat-proof-debug2") + << "SatProofManager::finalizeProof: " << it->second; + } + // a refl step added due to double elim negation, ignore + else if (link.second->getRule() == PfRule::REFL) + { + continue; + } + // a clause + else + { + Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:"; + Assert(link.first.getKind() == kind::OR) << link.first; + for (const Node& n : link.first) + { + it = d_cnfStream->getTranslationCache().find(n); + Assert(it != d_cnfStream->getTranslationCache().end()); + Trace("sat-proof-debug2") << it->second << " "; + } + } + Trace("sat-proof-debug2") << "\n"; + Trace("sat-proof-debug2") + << "SatProofManager::finalizeProof: " << link.first << "\n"; + // get resolution + Node cur = link.first; + std::shared_ptr pfn = link.second; + while (pfn->getRule() != PfRule::CHAIN_RESOLUTION) + { + Assert(pfn->getChildren().size() == 1 + && pfn->getChildren()[0]->getRule() == PfRule::ASSUME) + << *link.second.get() << "\n" + << *pfn.get(); + cur = pfn->getChildren()[0]->getResult(); + // retrieve justification of assumption in the links + Assert(links.find(cur) != links.end()); + pfn = links[cur]; + // ignore it in the rest of the outside loop + skip.insert(cur); + } + std::vector fassumps; + expr::getFreeAssumptions(pfn.get(), fassumps); + Trace("sat-proof-debug2") << push; + for (const Node& fa : fassumps) + { + Trace("sat-proof-debug2") << "SatProofManager::finalizeProof: - "; + it = d_cnfStream->getTranslationCache().find(fa); + if (it != d_cnfStream->getTranslationCache().end()) + { + Trace("sat-proof-debug2") << it->second << "\n"; + continue; + } + // then it's a clause + Assert(fa.getKind() == kind::OR); + for (const Node& n : fa) + { + it = d_cnfStream->getTranslationCache().find(n); + Assert(it != d_cnfStream->getTranslationCache().end()); + Trace("sat-proof-debug2") << it->second << " "; + } + Trace("sat-proof-debug2") << "\n"; + } + Trace("sat-proof-debug2") << pop; + Trace("sat-proof-debug2") + << "SatProofManager::finalizeProof: " << *pfn.get() << "\n=======\n"; + ; + } + Trace("sat-proof-debug2") << pop; + } + // We will resolve away of the literals l_1...l_n in inConflict. At this point + // each ~l_i must be either explainable, the result of a previously saved + // resolution chain, or an input. In account of it possibly being the first, + // we call explainLit on each ~l_i while accumulating the children and + // arguments for the resolution step to conclude false. + std::vector children{inConflictNode}, args; + std::unordered_set premises; + for (unsigned i = 0, size = inConflict.size(); i < size; ++i) + { + Assert(d_cnfStream->getNodeCache().find(inConflict[i]) + != d_cnfStream->getNodeCache().end()); + std::unordered_set childPremises; + explainLit(~inConflict[i], childPremises); + Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]]; + // save to resolution chain premises / arguments + children.push_back(negatedLitNode); + args.push_back(d_cnfStream->getNodeCache()[inConflict[i]]); + // add child premises and the child itself + premises.insert(childPremises.begin(), childPremises.end()); + premises.insert(negatedLitNode); + Trace("sat-proof") << "===========\n"; + } + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false " + "with clauses:\n"; + for (unsigned i = 0, size = children.size(); i < size; ++i) + { + Trace("sat-proof") << "SatProofManager::finalizeProof: " << children[i]; + if (i > 0) + { + Trace("sat-proof") << " [" << args[i - 1] << "]"; + } + Trace("sat-proof") << "\n"; + } + } + // create step + ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args); + d_resChainPg.addStep(d_false, ps); + // not yet ready to check closedness because maybe only now we will justify + // literals used in resolutions + d_resChains.addLazyStep(d_false, &d_resChainPg); + // Fix point justification of literals in leaves of the proof of false + bool expanded; + do + { + expanded = false; + Trace("sat-proof") << "expand assumptions to prove false\n"; + std::shared_ptr pfn = d_resChains.getProofFor(d_false); + Assert(pfn); + Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n"; + std::vector fassumps; + expr::getFreeAssumptions(pfn.get(), fassumps); + if (Trace.isOn("sat-proof")) + { + for (const Node& fa : fassumps) + { + Trace("sat-proof") << "- "; + auto it = d_cnfStream->getTranslationCache().find(fa); + if (it != d_cnfStream->getTranslationCache().end()) + { + Trace("sat-proof") << it->second << "\n"; + Trace("sat-proof") << "- " << fa << "\n"; + continue; + } + // then it's a clause + Assert(fa.getKind() == kind::OR); + for (const Node& n : fa) + { + it = d_cnfStream->getTranslationCache().find(n); + Assert(it != d_cnfStream->getTranslationCache().end()); + Trace("sat-proof") << it->second << " "; + } + Trace("sat-proof") << "\n"; + Trace("sat-proof") << "- " << fa << "\n"; + } + } + + // for each assumption, see if it has a reason + for (const Node& fa : fassumps) + { + // ignore already processed assumptions + if (premises.count(fa)) + { + Trace("sat-proof") << "already processed assumption " << fa << "\n"; + continue; + } + // ignore input assumptions. This is necessary to avoid rare collisions + // between input clauses and literals that are equivalent at the node + // level. In trying to justify the literal below if, it was previously + // propagated (say, in a previous check-sat call that survived the + // user-context changes) but no longer holds, then we may introduce a + // bogus proof for it, rather than keeping it as an input. + if (d_assumptions.contains(fa)) + { + Trace("sat-proof") << "input assumption " << fa << "\n"; + continue; + } + // ignore non-literals + auto it = d_cnfStream->getTranslationCache().find(fa); + if (it == d_cnfStream->getTranslationCache().end()) + { + Trace("sat-proof") << "no lit assumption " << fa << "\n"; + premises.insert(fa); + continue; + } + Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa + << "\n"; + // mark another iteration for the loop, as some resolution link may be + // connected because of the new justifications + expanded = true; + std::unordered_set childPremises; + explainLit(it->second, childPremises); + // add the premises used in the justification. We know they will have + // been as expanded as possible + premises.insert(childPremises.begin(), childPremises.end()); + // add free assumption itself + premises.insert(fa); + } + } while (expanded); + // now we should be able to close it + if (options::proofNewEagerChecking()) + { + std::vector assumptionsVec; + for (const Node& a : d_assumptions) + { + assumptionsVec.push_back(a); + } + d_resChains.addLazyStep(d_false, &d_resChainPg, assumptionsVec); + } +} + +void SatProofManager::storeUnitConflict(Minisat::Lit inConflict) +{ + Assert(d_conflictLit == undefSatVariable); + d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict); +} + +void SatProofManager::finalizeProof() +{ + Assert(d_conflictLit != undefSatVariable); + Trace("sat-proof") + << "SatProofManager::finalizeProof: conflicting (lazy) satLit: " + << d_conflictLit << "\n"; + finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit}); +} + +void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding) +{ + SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict); + Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: " + << satLit << "\n"; + Node clauseNode = getClauseNode(satLit); + if (adding) + { + registerSatAssumptions({clauseNode}); + } + finalizeProof(clauseNode, {satLit}); +} + +void SatProofManager::finalizeProof(const Minisat::Clause& inConflict, + bool adding) +{ + if (Trace.isOn("sat-proof")) + { + Trace("sat-proof") + << "SatProofManager::finalizeProof: conflicting clause: "; + printClause(inConflict); + Trace("sat-proof") << "\n"; + } + std::vector clause; + for (unsigned i = 0, size = inConflict.size(); i < size; ++i) + { + clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i])); + } + Node clauseNode = getClauseNode(inConflict); + if (adding) + { + registerSatAssumptions({clauseNode}); + } + finalizeProof(clauseNode, clause); +} + +std::shared_ptr SatProofManager::getProof() +{ + std::shared_ptr pfn = d_resChains.getProofFor(d_false); + if (!pfn) + { + pfn = d_pnm->mkAssume(d_false); + } + return pfn; +} + +void SatProofManager::registerSatLitAssumption(Minisat::Lit lit) +{ + Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - " + << getClauseNode(MinisatSatSolver::toSatLiteral(lit)) + << "\n"; + d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit))); +} + +void SatProofManager::registerSatAssumptions(const std::vector& assumps) +{ + for (const Node& a : assumps) + { + Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a + << "\n"; + d_assumptions.insert(a); + } +} + +} // namespace prop +} // namespace CVC4 diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h new file mode 100644 index 000000000..da67f0c1e --- /dev/null +++ b/src/prop/sat_proof_manager.h @@ -0,0 +1,587 @@ +/********************* */ +/*! \file sat_proof_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The proof manager for Minisat + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SAT_PROOF_MANAGER_H +#define CVC4__SAT_PROOF_MANAGER_H + +#include "context/cdhashset.h" +#include "expr/buffered_proof_generator.h" +#include "expr/expr.h" +#include "expr/lazy_proof_chain.h" +#include "expr/node.h" +#include "expr/proof.h" +#include "expr/proof_node_manager.h" +#include "prop/minisat/core/SolverTypes.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_types.h" + +namespace Minisat { +class Solver; +} + +namespace CVC4 { +namespace prop { + +/** + * This class is responsible for managing the proof production of the SAT + * solver. It tracks resolutions produced during solving and stores them, + * independently, with the connection of the resolutions only made when the + * empty clause is produced and the refutation is complete. The expected + * assumptions of the refutation are the clausified preprocessed assertions and + * lemmas. + * + * These resolutions are stored in a LazyCDProofChain, a user-context-dependent + * proof that takes lazy steps and can connect them when generating a proof for + * a given fact. Its use in this proof manager is so that, assuming the + * following lazy steps are saved in the LazyCDProofChain: + * + * --- S0: (l4, PG0) + * --- S1: ((or l3 l4), PG1) + * --- S2: ((or l1 ~l3), PG2) + * --- S3: (false, PG3) + * --- S4: (~l2, PG4) + * --- S5: (~l3, PG5) + * --- S6: (~l5, PG6) + * + * when requesting the proof of false, assuming that the proof generators have + * the following expansions: + * + * --- PG0 -> (CHAIN_RES ((or l4 l1) ~l1)) + * --- PG1 -> (CHAIN_RES ((or l3 l5 l6 l7) ~l5 (or ~l6 l7) (or l4 ~l7))) + * --- PG2 -> (CHAIN_RES ((or l1 ~l3 l5) ~l5)) + * --- PG3 -> (CHAIN_RES ((or l1 l2) ~l1 ~l2)) + * --- PG4 -> (CHAIN_RES ((or l3 ~l2) ~l3)) + * --- PG5 -> (CHAIN_RES ((or l1 ~l3) ~l1)) + * --- PG6 -> (CHAIN_RES ((or l1 ~l5) ~l1)) + * + * will connect the independent resolutions and yield the following refutation + * + * (or l1 ~l5) ~l1 + * ---------------- CHAIN_RES + * (or l1 ~l3 l5) ~l5 + * ---------------------- CHAIN_RES + * (or l1 ~l3) ~l1 + * ----------------------------- CHAIN_RES + * (or l3 ~l2) ~l3 + * -------------------- CHAIN_RES + * (or l1 l2) ~l1 ~l2 + * --------------------------- CHAIN_RES + * false + * + * where note that the steps S0 and S1, for l4 and (or l3 l4), respectively, + * were ignored, since they were not part of the chain starting with + * false. Moreover there is no requirement that the steps are registered + * chronologically in the LazyCDProofChain. The chain started on step S3 and + * proceeded to steps S4, S5, S2, and finally S6. + * + * To track the reasoning of the SAT solver and produce the steps above this + * class does three main things: + * (1) Register the resolutions for learned clauses as they are learned. + * (2) Register the resolutions for propagated literals when necessary. + * (3) Register the *full* resolution proof for the empty clause. + * + * Case (1) covers the learned clauses during backjumping. The only information + * saved is that, from clauses C1 to Cn, a given learned clause C is derived via + * chain resolution (and possibly factoring, reordering and double negation + * elimination in its literals), i.e., we do not recursively prove C1 to Cn at + * this moment. + * + * Not explaining C1 to Cn eagerly is beneficial because: + * - we might be wasting resources in fully explanaining it now, since C may not + * be necessary for the derivation of the empty clause, and + * - in explaining clauses lazily we might have shorter explanations, which has + * been observed empirically to be often the case. + * + * The latter case is a result of the SAT solver possibly changing the + * explanation of each of C, C1 to Cn, or the components of their + * explanations. This is because the set of propagated literals that may be used + * in these explanations can change in different SAT contexts, with the same + * clause being derived several times, each from a different set of clauses. + * + * Therefore we only fully explain a clause when absolutely necessary, i.e., + * when we are done (see case (3)) or when we'd not be able to do it afterwards + * (see case (2)). In the example above, step S2 is generated from case (1), + * with the shallow proof + * + * (or l1 ~l3 l5) ~l5 + * ------------------------- CHAIN_RES + * (or l1 ~l3) + * + * explaining the learned clause (or l1 ~l3). Its full proof would only be + * produced if it were part of the final refutation, as it indeed is. Note that + * in the example above the refutation proof contains the resolution proof of + * ~l5. + * + * Case (2) covers: + * (2.1) propagated literals explained by clauses being deleted + * (2.2) propagated literals whose negation occurs in a learned clause, which + * are then deleted for being redundant. + * + * Case (2.1) only happens for the so-called "locked clauses", which are clauses + * C = l1 v ... v ln that propagate their first literal, l1. When a locked + * clause C is deleted we save a chain resolution proof of l1 because we'd not + * be able to retrieve C afterwards, since it is deleted. The proof is a chain + * resolution step between C and ~l2, ..., ~ln, concluding l1. In the example + * above, step S0 is generated from case (2.1), with the locked clause (or l4 + * l1) being deleted and requiring the registration in the LazyCDPRoofChain of a + * lazy step for + * + * (or l4 l1) ~l1 + * ------------------------- CHAIN_RES + * l4 + * + * Case (2.2) requires that, when a redundant literal (i.e., a literal whose + * negation is propagated) is deleted from a learned clause, we add the + * explanation of its negation to the chain resolution proof of the learned + * clause. This justifies the deletion of the redundant literal. However, the + * explanation for the propagated literal (the SAT solver maintains a map from + * propagated literals to the clauses that propagate them in the current + * context, i.e., their explanations, clauses in which all literals but the + * propagated one have their negation propagated) may also contain literals that + * were in the learned clause and were deleted for being redundant. Therefore + * eliminating a redundant literal requires recursively explaining the + * propagated literals in its explanation as long as they are, themselves, + * redundant literals in the learned clause. + * + * In the above example step S1, concluding (or l3 l4), is generated from the + * resolutions + * + * (or l3 l5 l6 l7) ~l5 + * -------------------------- CHAIN_RES + * (or l3 l6 l7) (or ~l6 l7) (or l4 ~l7) + * ---------------------------------------------------------------- CHAIN_RES + * (or l3 l4) + * + * as l6 and l7 are redundant, which leads to (or l3 l6 l7) being resolved with + * l6's explanation, (or ~l6 l7). The literals in the explanation of l7 are + * recursively explained if they are also redundant, which is the case for l7, + * so its explanation is also added as premise for the resolution. Since l4 is + * not redundant, it is not recursively explained. + * + * Note that the actual proof generated does not have the intermediary step + * before removing redundant literals. It's all done in one fell swoop: + * + * (or l3 l5 l6 l7) ~l5 (or ~l6 l7) (or l4 ~l7) + * --------------------------------------------------- CHAIN_RES + * (or l3 l4) + * + * Finally, case (3) happens when the SAT solver derives the empty clause and + * it's not possible to backjump. The empty clause is learned from a conflict + * clause: a clause whose every literal has its negation propagated in the + * current context. Thus the proof of the empty clause is generated, at first, + * in the same way as case (1): a resolution chain betweeen the conflict clause + * and its negated literals. However, since we are now done, we recursively + * explain the propagated literals, starting from the negated literals from the + * conflict clause and progressing to all propagated literals ocurring in a + * given explanation. + * + * In the above example this happens as: step S3 + * + * (or l1 l2) ~l1 ~l2 + * --------------------------- CHAIN_RES + * false + * + * is added for a conflict clause (or l1 l2). Then we attempt to explain ~l1 and + * ~l2. The former has no explanation (i.e., it's an input), while the latter + * has explanation (or l3 ~l2). This leads to step S4 + * + * (or l3 ~l2) ~l3 + * -------------------- CHAIN_RES + * ~l2 + * + * being added to the LazyCDProofChain. In explaining ~l3 the step S5 + * + * (or l1 ~l3) ~l1 + * --------------------- CHAIN_RES + * ~l3 + * + * is added. Since ~l1 has no explanation, the process halts. Note that at this + * point the step S6 has not been added to the LazyCDProofChain. This is because + * to explain ~l5 we need to look at the literal premises in the proofs of + * learned clauses. + * + * The last thing done then in case (3), after the resolution on the conflict + * clause and an initial recursive explanation of propagated literals, is to + * connect the refutation proof and then recursively its propagated literal + * leaves, repeating until a fix point. + * + * In the above example the first connection yields + * + * (or l1 ~l3 l5) ~l5 + * ---------------------- CHAIN_RES + * (or l1 ~l3) ~l1 + * ----------------------------- CHAIN_RES + * (or l3 ~l2) ~l3 + * -------------------- CHAIN_RES + * (or l1 l2) ~l1 ~l2 + * --------------------------- CHAIN_RES + * false + * + * whose literal leaves are ~l1 and ~l5. The former has no explanation, but the + * latter is explained by (or l1 ~l5), thus leading to step S6 + * + * (or l1 ~l5) ~l1 + * --------------------- CHAIN_RES + * ~l5 + * + * then the final connection + * + * (or l1 ~l5) ~l1 + * ---------------- CHAIN_RES + * (or l1 ~l3 l5) ~l5 + * ---------------------- CHAIN_RES + * (or l1 ~l3) ~l1 + * ----------------------------- CHAIN_RES + * (or l3 ~l2) ~l3 + * -------------------- CHAIN_RES + * (or l1 l2) ~l1 ~l2 + * --------------------------- CHAIN_RES + * false + * + * which has no more explainable literals as leaves. + * + * The interfaces below provide ways for the SAT solver to register its + * assumptions (clausified assertions and lemmas) for the SAT proof + * (registerSatAssumption), register resolution steps (startResChain / + * addResolutionStep / endResChain), build the final refutation proof + * (finalizeProof) and retrieve the refutation proof (getProof). So in a given + * run of the SAT solver these interfaces are expected to be used in the + * following order: + * + * (registerSatAssumptions | (startResChain (addResolutionStep)+ endResChain)*)* + * finalizeProof + * getProof + * + */ +class SatProofManager +{ + public: + SatProofManager(Minisat::Solver* solver, + CnfStream* cnfStream, + context::UserContext* userContext, + ProofNodeManager* pnm); + + /** Marks the start of a resolution chain. + * + * This call is followed by *at least one* call to addResolution step and one + * call to endResChain. + * + * The given clause, at the node level, is registered in d_resLinks with a + * null pivot, since this is the first link in the chain. + * + * @param start a SAT solver clause (list of literals) that will be the first + * clause in a resolution chain. + */ + void startResChain(const Minisat::Clause& start); + /** Adds a resolution step with a clause + * + * There must have been a call to startResChain before any call to + * addResolution step. After following calls to addResolution step there is + * one call to endResChain. + * + * The resolution step is added to d_resLinks with the clause, at the node + * level, and the literal, at the node level, as the pivot. + * + * @param clause the clause being resolved against + * @param lit the pivot of the resolution step + */ + void addResolutionStep(const Minisat::Clause& clause, Minisat::Lit lit); + /** Adds a resolution step with a unit clause + * + * The resolution step is added to d_resLinks such that lit, at the node + * level, is the pivot and and the unit clause is ~lit, at the node level. + * + * If the literal is marked as redundant, then a step is *not* is added to + * d_resLinks. It is rather saved to d_redundandLits, whose components we will + * be handled in a special manner when the resolution chain is finished. This + * is because the steps corresponding to the removal of redundant literals + * have to be done in a specific order. See proccessRedundantLits below. + * + * @param lit the literal being resolved against + * @param redundant whether lit is redundant + */ + void addResolutionStep(Minisat::Lit lit, bool redundant = false); + /** Ends resolution chain concluding a unit clause + * + * This call must have been preceded by one call to startResChain and at least + * one call to addResolutionStep. + * + * This and the version below both call the node version of this method, + * described further below, which actually does the necessary processing. + */ + void endResChain(Minisat::Lit lit); + /** Ends resolution chain concluding a clause */ + void endResChain(const Minisat::Clause& clause); + /** Build refutation proof starting from conflict clause + * + * This method (or its variations) is only called when the SAT solver has + * reached an unsatisfiable state. + * + * This and the versions below call the node version of this method, described + * further below, which actually does the necessary processing. + * + * @param adding whether the conflict is coming from a freshly added clause + */ + void finalizeProof(const Minisat::Clause& inConflict, bool adding = false); + /** Build refutation proof starting from conflict unit clause + * + * @param adding whether the conflict is coming from a freshly added clause + */ + void finalizeProof(Minisat::Lit inConflict, bool adding = false); + /** As above, but uses the unit conflict clause saved in d_conflictLit. */ + void finalizeProof(); + /** Set the unit conflict clause d_conflictLit. */ + void storeUnitConflict(Minisat::Lit inConflict); + + /** Retrive the refutation proof + * + * If there is no chain for false in d_resChains, meaning that this call was + * made before finalizeProof, an assumption proof node is produced. + */ + std::shared_ptr getProof(); + + /** Register a unit clause input, converted to its node representation. */ + void registerSatLitAssumption(Minisat::Lit lit); + /** Register a set clause inputs. */ + void registerSatAssumptions(const std::vector& assumps); + + private: + /** Ends resolution chain concluding clause + * + * This method builds the proof of conclusion from the resolution chain + * currently saved in d_resLinks. + * + * First each saved redundant literals in d_redundantLits is processed via + * processRedundantLit. The literals in the resolution chain's conclusion are + * used to verifynig which literals in the computed explanations are + * redundant, i.e., don't occur in conclusionLits. The nessary resolution + * steps will be added to d_resLinks. + * + * The proof to be built will be a CHAIN_RESOLUTION step, whose children and + * arguments will be retrieved from traversing d_resLinks. Consider the + * following d_resLinks (where each [~]li is its node equivalent): + * + * - <(or l3 l5 l6 l7), null> + * - <~l5, l5> + * - <(or ~l6 l7), l6> + * - <(or l4 ~l7), l7> + * + * The resulting children and arguments for the CHAIN_RESOLUTION proof step would be: + * - [(or l3 l5 l6 l7), ~l5, (or ~l6 l7), (or l4 ~l7)] + * - [l5, l6, l7] + * and the proof step + * + * (or l3 l5 l6 l7) ~l5 (or ~l6 l7) (or l4 ~l7) + * --------------------------------------------------- CHAIN_RES_{l5,l6,l7} + * (or l3 l4) + * + * The conclusion of the CHAIN_RES proof step is *not* the given conclusion of + * this method. This is because conclusion is the node equivalent of the + * clause in the SAT solver, which is kept modulo duplicates, reordering, and + * double negation elimination. Therefore we generate the above step in the + * correct way for the semantics of CHAIN_RES, based on its children and + * arguments, via the d_pnm's proof checker. The resulting node n is fed into + * the clause normalization in TheoryProofStepBuffer, which reduces n to + * conclusion. + * + * All the proof steps generated to conclude conclusion from the premises in + * d_resLinks are saved into d_resChainPg, which is saved as the proof + * generator for lazy step added to d_resChains for the conclusion. + * + * @param conclusion the node-level conclusion of the resolution chain + * @param conclusionLits the set of literals in the conclusion + */ + void endResChain(Node conclusion, const std::set& conclusionLits); + + /** Explain redundant literal and generate corresponding resolution steps + * + * If the redundant literal has a reason, we add a resolution step with that + * clause, otherwise with the negation of the redundant literal as the unit + * clause. The redundant literal is the resolvent in both cases. The steps + * are always added as the *first* link after last resolution step added + * *before* processing redundant literals began, i.e., at d_resLinks.begin() + + * pos. This is to guarantee that the links are in the correct order for the + * chain resolution, see below. + * + * If the reason contains literals that do not occur in conclusionLits, they + * are redundant and recursively processed by this method. This recursive + * processing happens *before* the resolution step for lit is added. Since + * steps are always added in position pos, pushing steps after that 1 + * position, this guarantees that a step with a clause will occur before the + * steps that eliminate its redundant literals. + * + * Consider d_resLinks with 3 links before the first processRedundantLit call, + * i.e., pos = 3, and d_redundantLits = {l1}, with reason(l1) = (or l1 ~l2), + * with ~l2 redundant. Assume ~l2 has no explanation. By processing ~l2 first, + * the link <~l2, l2> will be added at position 3. Then by coming back to the + * processing of l1 the link <(or l1 ~l2), l1> will also be added position 3, + * with <~l2, l2> pushed to position 4. If this these links had the reverse + * order the literal ~l2 would, erroneously, occur in the chain resolution + * conclusion, as it is introduced by (or l1 ~l2). + * + * After a resolution step for a redundant literal is added, it is marked as + * visited, thus avoiding adding redundunt resolution steps to the chain if + * that literal occurs again in another redundant literal's reason. + * + * @param lit the redundant literal + * @param conclusionLits the literals in the clause from which redundant + * literals have been removed + * @param visited cache of literals already processed + * @param pos position, in d_resLinks, of last resolution step added *before* + * processing redundant literals + */ + void processRedundantLit(SatLiteral lit, + const std::set& conclusionLits, + std::set& visited, + unsigned pos); + /** Explain literal if it is propagated in the SAT solver + * + * If a literal is propagated, i.e., it has a reason in the SAT solver, that + * clause is retrieved. This method is then called recursively on the negation + * of each of reason's literals (that is not lit). Afterwards a + * CHAIN_RESOLUTION proof step is created to conclude lit from the reason and + * its literals, other than lit, negations. + * + * This method also tracks all the literals and clauses, at the node level, + * that have been used as premises of resolutions steps in the recursive + * explanations. A resolution step is only created if the conclusion does not + * occur in these premises, as this would configure a cyclic proof. + * + * These cyclic proofs, at the node level, are naturally generated by the SAT + * solver because they are so that a literal is derived from a clause (so they + * are different) but both correspond to the *same node*. For example, + * consider the following derivation at the SAT solver level + * + * [l1, l2, l3] ~l2 ~l3 + * -------------------------- CHAIN_RES + * [l0, ~l1] l1 + * ---------------------- CHAIN_RES + * l0 + * + * which has no issues. However, its node equivalent is + * + * (or a b c) (not b) (not c) + * ------------------------------- CHAIN_RES + * (or (or a b c) (not a)) a + * --------------------------------- CHAIN_RES + * (or a b c) + * + * which is cyclic. The issue is that l0 = (or a b c). Only at the SAT level + * are l0 and [l1, l2, l3] different. + * + * If a cyclic proof is identified, the respective node is kept as an + * assumption. + * + * @param lit the literal to explained + * @param premises set of literals and clauses, at the node level, that + * have been used as premises of resolution steps while explaining + * propagations + */ + void explainLit(prop::SatLiteral lit, + std::unordered_set& premises); + + /** Build refutation proof starting from conflict clause + * + * Given a conflict clause, this method handles case (3) described in the + * preamble. Each of the literals in the conflict clause is either + * explainable, the result of a previously saved resolution chain, or an + * input. + * + * First, explainLit is called recursively on the negated literals from + * the conflict clause. + * + * Second, a CHAIN_RESOLUTION proof step is added between + * the conflict clause and its negated literals, concluding false. + * + * Third, until a fix point, the refutation proof is connected, by calling + * d_resChain.getProofFor(d_false), its free assumptions are determined and, + * in case any as a literal that might be explained, we call explainLit. + * + * The latter is called to a fix point because adding an explanation to a + * propagated literal may connect it with a previously saved resolution chain, + * which may have free assumptions that are literals that can be explained and + * so on. + * + * @param inConflictNode node corresponding to conflict clause + * @param inConflict literals in the conflict clause + */ + void finalizeProof(Node inConflictNode, + const std::vector& inConflict); + + /** The SAT solver to which we are managing proofs */ + Minisat::Solver* d_solver; + /** Pointer to the underlying cnf stream. */ + CnfStream* d_cnfStream; + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** Resolution steps (links) accumulator for chain resolution. + * + * Each pair has a clause and the pivot for the resolution step it is involved + * on. The pivot occurs positively in the clause yielded by the resolution up + * to the previous link and negatively in this link. The first link has a null + * pivot. Links are kept at the node level. + * + * This accumulator is reset after each chain resolution. */ + std::vector> d_resLinks; + + /** Redundant literals removed from the resolution chain's conclusion. + * + * This accumulator is reset after each chain resolution. */ + std::vector d_redundantLits; + + /** + * Associates clauses to their local proofs. These proofs are local and + * possibly updated during solving. When the final conclusion is reached, a + * final proof is built based on the proofs saved here. + * + * This chain is initialized so that its getProofFor method, which connects + * the chain, accounts for cyclic proofs. This is so that we avoid the issue + * described in explainLit. + */ + LazyCDProofChain d_resChains; + + /** The proof generator for resolution chains */ + BufferedProofGenerator d_resChainPg; + + /** The false node */ + Node d_false; + + /** All clauses added to the SAT solver, kept in a context-dependent manner. + */ + context::CDHashSet d_assumptions; + + /** + * A placeholder that may be used to store the literal with the final + * conflict. + */ + SatLiteral d_conflictLit; + /** Gets node equivalent to literal */ + Node getClauseNode(SatLiteral satLit); + /** Gets node equivalent to clause. + * + * To avoid generating different nodes for the same clause, modulo ordering, + * an invariant assumed throughout this class, the OR node generated by this + * method always has its children ordered. + */ + Node getClauseNode(const Minisat::Clause& clause); + /** Prints clause, as a sequence of literals, in the "sat-proof" trace. */ + void printClause(const Minisat::Clause& clause); +}; /* class SatProofManager */ + +} // namespace prop +} // namespace CVC4 + +#endif /* CVC4__SAT_PROOF_MANAGER_H */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d1d032af6..65da2fc7c 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -149,5 +149,7 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { return d_decisionEngine->getPolarity(var); } +CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 7a6f16ff0..e16728d0d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -88,6 +88,8 @@ class TheoryProxy SatValue getDecisionPolarity(SatVariable var); + CnfStream* getCnfStream(); + private: /** The prop engine we are using. */ PropEngine* d_propEngine; @@ -109,8 +111,7 @@ class TheoryProxy * all imported and exported lemmas. */ std::unordered_set d_shared; - -}; /* class SatSolver */ +}; /* class TheoryProxy */ }/* CVC4::prop namespace */ -- cgit v1.2.3