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).
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
LazyCDProofChain::~LazyCDProofChain() {}
+const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
+ const
+{
+ std::map<Node, std::shared_ptr<ProofNode>> links;
+ for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+ {
+ Assert(link.second);
+ std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
+ Assert(pfn);
+ links[link.first] = pfn;
+ }
+ return links;
+}
+
std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
{
Trace("lazy-cdproofchain")
/** 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<Node, std::shared_ptr<ProofNode>> getLinks() const;
+
private:
/** The proof manager, used for allocating new ProofNode objects */
ProofNodeManager* d_manager;
#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"
/** 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<Minisat::Solver>;
public:
--- /dev/null
+/********************* */
+/*! \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<Node> 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<Node, Node>(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<Node, Node>(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<Node, Node>(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<SatLiteral> 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<SatLiteral>& conclusionLits)
+{
+ Trace("sat-proof") << ", " << conclusion << "\n";
+ // first process redundant literals
+ std::set<SatLiteral> visited;
+ unsigned pos = d_resLinks.size();
+ for (SatLiteral satLit : d_redundantLits)
+ {
+ processRedundantLit(satLit, conclusionLits, visited, pos);
+ }
+ d_redundantLits.clear();
+ // build resolution chain
+ std::vector<Node> 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<std::pair<Node, ProofStep>>& steps = psb.getSteps();
+ for (const std::pair<Node, ProofStep>& 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<SatLiteral>& conclusionLits,
+ std::set<SatLiteral>& 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<Node, Node>(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<Node, Node>(clauseNode, d_cnfStream->getNodeCache()[lit]));
+}
+
+void SatProofManager::explainLit(
+ SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& 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<Node> 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<TNode, TNodeHashFunction> 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<SatLiteral>& 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<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
+ std::unordered_set<Node, NodeHashFunction> skip;
+ for (const std::pair<const Node, std::shared_ptr<ProofNode>>& 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<ProofNode> 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<Node> 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<Node> children{inConflictNode}, args;
+ std::unordered_set<TNode, TNodeHashFunction> 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<TNode, TNodeHashFunction> 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<ProofNode> pfn = d_resChains.getProofFor(d_false);
+ Assert(pfn);
+ Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n";
+ std::vector<Node> 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<TNode, TNodeHashFunction> 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<Node> 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<SatLiteral> 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<ProofNode> SatProofManager::getProof()
+{
+ std::shared_ptr<ProofNode> 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<Node>& assumps)
+{
+ for (const Node& a : assumps)
+ {
+ Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a
+ << "\n";
+ d_assumptions.insert(a);
+ }
+}
+
+} // namespace prop
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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<ProofNode> 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<Node>& 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<SatLiteral>& 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<SatLiteral>& conclusionLits,
+ std::set<SatLiteral>& 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<TNode, TNodeHashFunction>& 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<SatLiteral>& 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<std::pair<Node, Node>> d_resLinks;
+
+ /** Redundant literals removed from the resolution chain's conclusion.
+ *
+ * This accumulator is reset after each chain resolution. */
+ std::vector<SatLiteral> 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<Node, NodeHashFunction> 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 */
return d_decisionEngine->getPolarity(var);
}
+CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
SatValue getDecisionPolarity(SatVariable var);
+ CnfStream* getCnfStream();
+
private:
/** The prop engine we are using. */
PropEngine* d_propEngine;
* all imported and exported lemmas.
*/
std::unordered_set<Node, NodeHashFunction> d_shared;
-
-}; /* class SatSolver */
+}; /* class TheoryProxy */
}/* CVC4::prop namespace */
projects / cvc5.git / commitdiff