From 795563e54baf80404037ed9b6f169750e3dabc60 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 24 Mar 2022 17:14:12 -0300 Subject: [PATCH] [proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389) The SAT solver may associate, to the result of a resolution, a lower assertion level than the current one. To be able to produce proofs to such clauses, we extend the SAT proof manager to track which resolution results were optimized. Then, when the SAT solver pops, the manager is notified and stores the proofs for these optimized clauses, so that they can be reinserted when the user context is popped. The latter is handled by the SAT proof manager's OptClauseManager attribute. --- src/prop/minisat/core/Solver.cc | 3 +- src/prop/sat_proof_manager.cpp | 58 +++++++++++++++++++++++++-------- src/prop/sat_proof_manager.h | 29 ++++++++++++++--- 3 files changed, 70 insertions(+), 20 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 75e1d831f..1294b9d33 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -213,8 +213,7 @@ Solver::Solver(Env& env, { if (pnm) { - d_pfManager.reset( - new SatProofManager(this, proxy->getCnfStream(), userContext, pnm)); + d_pfManager.reset(new SatProofManager(env, this, proxy->getCnfStream())); } // Create the constant variables diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 582aa5253..d31b1273a 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -24,17 +24,18 @@ namespace cvc5 { namespace prop { -SatProofManager::SatProofManager(Minisat::Solver* solver, - CnfStream* cnfStream, - context::UserContext* userContext, - ProofNodeManager* pnm) - : d_solver(solver), +SatProofManager::SatProofManager(Env& env, + Minisat::Solver* solver, + CnfStream* cnfStream) + : EnvObj(env), + 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_resChains(d_env.getProofNodeManager(), true, userContext()), + d_resChainPg(userContext(), d_env.getProofNodeManager()), + d_assumptions(userContext()), + d_conflictLit(undefSatVariable), + d_optResLevels(userContext()), + d_optResManager(userContext(), &d_resChains, d_optResProofs) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -118,13 +119,15 @@ void SatProofManager::addResolutionStep(const Minisat::Clause& clause, << satLit.isNegated() << "} [" << ~satLit << "] "; printClause(clause); Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t" - << clauseNode << "\n"; + << clauseNode << " - lvl " << clause.level() + 1 << "\n"; } } void SatProofManager::endResChain(Minisat::Lit lit) { SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); + Trace("sat-proof") << "SatProofManager::endResChain: curr user level: " + << userContext()->getLevel() << "\n"; Trace("sat-proof") << "SatProofManager::endResChain: chain_res for " << satLit; endResChain(d_cnfStream->getNode(satLit), {satLit}); @@ -134,6 +137,8 @@ void SatProofManager::endResChain(const Minisat::Clause& clause) { if (TraceIsOn("sat-proof")) { + Trace("sat-proof") << "SatProofManager::endResChain: curr user level: " + << userContext()->getLevel() << "\n"; Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "; printClause(clause); } @@ -142,7 +147,17 @@ void SatProofManager::endResChain(const Minisat::Clause& clause) { clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i])); } - endResChain(getClauseNode(clause), clauseLits); + Node conclusion = getClauseNode(clause); + int clauseLevel = clause.level() + 1; + if (clauseLevel < userContext()->getLevel()) + { + Assert(!d_optResLevels.count(conclusion)); + d_optResLevels[conclusion] = clauseLevel; + Trace("sat-proof") << "SatProofManager::endResChain: ..clause's lvl " + << clause.level() + 1 << " below curr user level " + << userContext()->getLevel() << "\n"; + } + endResChain(conclusion, clauseLits); } void SatProofManager::endResChain(Node conclusion, @@ -756,7 +771,7 @@ std::shared_ptr SatProofManager::getProof() std::shared_ptr pfn = d_resChains.getProofFor(d_false); if (!pfn) { - pfn = d_pnm->mkAssume(d_false); + pfn = d_env.getProofNodeManager()->mkAssume(d_false); } return pfn; } @@ -781,5 +796,22 @@ void SatProofManager::registerSatAssumptions(const std::vector& assumps) } } +void SatProofManager::notifyPop() +{ + for (context::CDHashMap::const_iterator it = + d_optResLevels.begin(); + it != d_optResLevels.end(); + ++it) + { + // Save into map the proof of the resolution chain. We copy to prevent the + // proof node saved to be restored to suffering unintended updates. This is + // *necessary*. + std::shared_ptr clauseResPf = + d_env.getProofNodeManager()->clone(d_resChains.getProofFor(it->first)); + Assert(clauseResPf && clauseResPf->getRule() != PfRule::ASSUME); + d_optResProofs[it->second].push_back(clauseResPf); + } +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 98d125591..d62905792 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -18,12 +18,15 @@ #ifndef CVC5__SAT_PROOF_MANAGER_H #define CVC5__SAT_PROOF_MANAGER_H +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "expr/node.h" #include "proof/buffered_proof_generator.h" #include "proof/lazy_proof_chain.h" #include "prop/minisat/core/SolverTypes.h" +#include "prop/opt_clauses_manager.h" #include "prop/sat_solver_types.h" +#include "smt/env_obj.h" namespace Minisat { class Solver; @@ -268,13 +271,10 @@ class CnfStream; * getProof * */ -class SatProofManager +class SatProofManager : protected EnvObj { public: - SatProofManager(Minisat::Solver* solver, - CnfStream* cnfStream, - context::UserContext* userContext, - ProofNodeManager* pnm); + SatProofManager(Env& env, Minisat::Solver* solver, CnfStream* cnfStream); /** Marks the start of a resolution chain. * @@ -361,6 +361,9 @@ class SatProofManager /** Register a set clause inputs. */ void registerSatAssumptions(const std::vector& assumps); + /** Notify this proof manager that the SAT solver has user-context popped. */ + void notifyPop(); + private: /** Ends resolution chain concluding clause * @@ -582,6 +585,22 @@ class SatProofManager Node getClauseNode(const Minisat::Clause& clause); /** Prints clause, as a sequence of literals, in the "sat-proof" trace. */ void printClause(const Minisat::Clause& clause); + + /** The user context */ + context::UserContext* d_userContext; + + /** User-context dependent map from resolution conclusions to their assertion + level. */ + context::CDHashMap d_optResLevels; + /** Maps assertion level to proof nodes. + * + * This map is used by d_optResManager to update the internal proof of this + * manager when the context pops. + */ + std::map>> d_optResProofs; + /** Manager for optimized resolution conclusions inserted at assertion levels + * below the current user level. */ + OptimizedClausesManager d_optResManager; }; /* class SatProofManager */ } // namespace prop -- 2.30.2