From 895bf2273d3e9baa89d4a6de174e7789f2ab71af Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 4 Apr 2022 11:12:39 -0300 Subject: [PATCH] [proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536) Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof). This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set. There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases. --- src/prop/opt_clauses_manager.cpp | 38 ++++++++++++++++++- src/prop/opt_clauses_manager.h | 20 ++++++++++ src/prop/proof_cnf_stream.cpp | 9 ++++- src/prop/sat_proof_manager.cpp | 10 ++++- src/prop/sat_proof_manager.h | 13 ++++++- test/regress/cli/CMakeLists.txt | 1 + ...sat-assumption-incremental-bookeeping.smt2 | 17 +++++++++ 7 files changed, 104 insertions(+), 4 deletions(-) create mode 100644 test/regress/cli/regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2 diff --git a/src/prop/opt_clauses_manager.cpp b/src/prop/opt_clauses_manager.cpp index e3ae842b5..6f716bcc5 100644 --- a/src/prop/opt_clauses_manager.cpp +++ b/src/prop/opt_clauses_manager.cpp @@ -27,7 +27,9 @@ OptimizedClausesManager::OptimizedClausesManager( : context::ContextNotifyObj(context), d_context(context), d_optProofs(optProofs), - d_parentProof(parentProof) + d_parentProof(parentProof), + d_nodeHashSet(nullptr), + d_nodeLevels(nullptr) { } @@ -78,8 +80,42 @@ void OptimizedClausesManager::contextNotifyPop() } it = d_optProofs.erase(it); } + if (d_nodeHashSet) + { + Assert(d_nodeLevels); + // traverse mapping from context levels to nodes so that we can reinsert the + // nodes that are below the current level being popped. The entries in the + // map at or above this level are deleted. + for (auto it = d_nodeLevels->cbegin(); it != d_nodeLevels->cend();) + { + if (it->first <= newLvl) + { + Trace("sat-proof") << "Should re-add SAT assumptions of [" << it->first + << "]:\n"; + for (const auto& assumption : it->second) + { + Trace("sat-proof") << "\t- " << assumption << "\n"; + // Note that since it's a hash set we do not care about repetitions + d_nodeHashSet->insert(assumption); + } + ++it; + continue; + } + Trace("sat-proof") << "Should remove from map assumptions of [" + << it->first << "]: " << it->second << "\n"; + it = d_nodeLevels->erase(it); + } + } Trace("sat-proof") << pop; } +void OptimizedClausesManager::trackNodeHashSet( + context::CDHashSet* nodeHashSet, + std::map>* nodeLevels) +{ + d_nodeHashSet = nodeHashSet; + d_nodeLevels = nodeLevels; +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/opt_clauses_manager.h b/src/prop/opt_clauses_manager.h index a629f1a3b..505ad7480 100644 --- a/src/prop/opt_clauses_manager.h +++ b/src/prop/opt_clauses_manager.h @@ -19,6 +19,7 @@ #define CVC5__PROP__OPT_CLAUSES_MANAGER_H #include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/node.h" #include "proof/proof.h" @@ -51,6 +52,21 @@ class OptimizedClausesManager : context::ContextNotifyObj CDProof* parentProof, std::map>>& optProofs); + /** Adds a hash set of nodes to be tracked and updated when popping + * + * This method can be used when it is necessary to track, in a + * context-dependent manner, other information, in a node hash set, beyond the + * proofs associated with given clauses. For example, the SAT proof manager + * needs to bookeep the current assumptions of the SAT solver, which are + * stored in a node hash set. + * + * @param nodeHashSet the node hash set to be updated when context pops + * @param nodeLevels a mapping from context levels to nodes to be reinserted + * at these levels + */ + void trackNodeHashSet(context::CDHashSet* nodeHashSet, + std::map>* nodeLevels); + private: /** Event triggered by the tracked contexting popping * @@ -66,6 +82,10 @@ class OptimizedClausesManager : context::ContextNotifyObj std::map>>& d_optProofs; /** Proof to be updated when context pops. */ CDProof* d_parentProof; + /** Node hash set to be updated when context pops, if such a set is tracked */ + context::CDHashSet* d_nodeHashSet; + /** Map from levels to proof nodes. */ + std::map>* d_nodeLevels; }; } // namespace prop diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 511f3db79..ac70a0cd4 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -636,7 +636,11 @@ void ProofCnfStream::notifyCurrPropagationInsertedAtLevel(int explLevel) Trace("cnf-debug") << "\t..saved pf {" << currPropagationProcPf << "} " << *currPropagationProcPf.get() << "\n"; d_optClausesPfs[explLevel + 1].push_back(currPropagationProcPf); - + // Notify SAT proof manager that the propagation (which is a SAT assumption) + // had its level optimized + d_satPM->notifyAssumptionInsertedAtLevel(explLevel, + d_currPropagationProccessed); + // Reset d_currPropagationProccessed = Node::null(); } @@ -654,6 +658,9 @@ void ProofCnfStream::notifyClauseInsertedAtLevel(const SatClause& clause, d_env.getProofNodeManager()->clone(d_proof.getProofFor(clauseNode)); Assert(clauseCnfPf->getRule() != PfRule::ASSUME); d_optClausesPfs[clLevel + 1].push_back(clauseCnfPf); + // Notify SAT proof manager that the propagation (which is a SAT assumption) + // had its level optimized + d_satPM->notifyAssumptionInsertedAtLevel(clLevel, clauseNode); } Node ProofCnfStream::getClauseNode(const SatClause& clause) diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 61d8719df..d2704ae73 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -39,6 +39,7 @@ SatProofManager::SatProofManager(Env& env, { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + d_optResManager.trackNodeHashSet(&d_assumptions, &d_assumptionLevels); } void SatProofManager::printClause(const Minisat::Clause& clause) @@ -796,6 +797,13 @@ void SatProofManager::registerSatAssumptions(const std::vector& assumps) } } +void SatProofManager::notifyAssumptionInsertedAtLevel(int level, + Node assumption) +{ + Assert(d_assumptions.contains(assumption)); + d_assumptionLevels[level].push_back(assumption); +} + void SatProofManager::notifyPop() { for (context::CDHashMap::const_iterator it = @@ -804,7 +812,7 @@ void SatProofManager::notifyPop() ++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 + // proof node saved to be restored of suffering unintended updates. This is // *necessary*. std::shared_ptr clauseResPf = d_env.getProofNodeManager()->clone(d_resChains.getProofFor(it->first)); diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index e68db690d..8058daccb 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -364,6 +364,10 @@ class SatProofManager : protected EnvObj /** Notify this proof manager that the SAT solver has user-context popped. */ void notifyPop(); + /** Notify this proof manager that a SAT assumption has had its level + * optmized. */ + void notifyAssumptionInsertedAtLevel(int level, Node assumption); + private: /** Ends resolution chain concluding clause * @@ -385,7 +389,8 @@ class SatProofManager : protected EnvObj * - <(or ~l6 l7), l6> * - <(or l4 ~l7), l7> * - * The resulting children and arguments for the CHAIN_RESOLUTION proof step would be: + * 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 @@ -598,6 +603,12 @@ class SatProofManager : protected EnvObj * manager when the context pops. */ std::map>> d_optResProofs; + /** Maps assertion level to assumptions + * + * As above, used by d_optResManager to update the assumption set as the + * context pops, so that we track the correct current SAT assumptions. + */ + std::map> d_assumptionLevels; /** Manager for optimized resolution conclusions inserted at assertion levels * below the current user level. */ OptimizedClausesManager d_optResManager; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index e40ee670e..71d412596 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -973,6 +973,7 @@ set(regress_0_tests regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 regress0/proofs/scope.smt2 + regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 diff --git a/test/regress/cli/regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2 b/test/regress/cli/regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2 new file mode 100644 index 000000000..288488792 --- /dev/null +++ b/test/regress/cli/regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: -i --produce-proofs --proof-check=eager +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_UFLIA) +(declare-fun x (Int) Bool) +(declare-fun y (Int) Bool) +(declare-fun z (Int) Int) +(declare-fun _z (Int) Int) +(assert (= (x 0) (not (y 0)))) +(assert (= (y 0) (> 0 (z 0)))) +(assert (= (z 0) (_z 0))) +(assert (= 0 (_z 0))) +(push) +(check-sat) +(pop) +(assert (not (x 0))) +(check-sat) -- 2.30.2