From: Haniel Barbosa Date: Fri, 25 Mar 2022 17:41:56 +0000 (-0300) Subject: [proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the... X-Git-Tag: cvc5-1.0.0~175 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b6013aea173981f1efc47c57ca0130b36fdaf20;p=cvc5.git [proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the ProofCnfStream (#8388) Adds functionality for the TheoryProxy and ProofCnfStream modules to be notified of clauses that were asserted in lower levels than the current one. These clauses have their proofs tracked in the ProofCnfStream via an OptimizedClausesManager object. Since the SAT solver may optimize the assertion level of propagation explanations and of added clauses, we need to be able to maintain proofs across context-popping. Not doing this can lead to open proofs. To do this the Proof cnf stream uses an OptClausesManager to re-add proofs of facts inserted at optimized levels. Future PRs will change the SAT solver to use these notifications. --- diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 11d669a18..f6fa0dbb5 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -33,7 +33,8 @@ ProofCnfStream::ProofCnfStream(Env& env, nullptr, userContext(), "ProofCnfStream::LazyCDProof"), - d_blocked(userContext()) + d_blocked(userContext()), + d_optClausesManager(userContext(), &d_proof, d_optClausesPfs) { } @@ -80,7 +81,8 @@ void ProofCnfStream::convertAndAssert(TNode node, { Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") - << ", removable = " << (removable ? "true" : "false") << ")\n"; + << ", removable = " << (removable ? "true" : "false") + << "), level " << userContext()->getLevel() << "\n"; d_cnfStream.d_removable = removable; if (pg) { @@ -593,7 +595,7 @@ void ProofCnfStream::convertPropagation(TrustNode trn) { clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); } - normalizeAndRegister(clauseExp); + d_currPropagationProccessed = normalizeAndRegister(clauseExp); // consume steps if clausification being recorded. If we are not logging it, // we need to add the clause as a closed step to the proof so that the SAT // proof does not have non-input formulas as assumptions. @@ -612,6 +614,47 @@ void ProofCnfStream::convertPropagation(TrustNode trn) } } +void ProofCnfStream::notifyCurrPropagationInsertedAtLevel(int explLevel) +{ + Assert(explLevel < (userContext()->getLevel() - 1)); + Assert(!d_currPropagationProccessed.isNull()); + Trace("cnf") << "Need to save curr propagation " + << d_currPropagationProccessed << "'s proof in level " + << explLevel + 1 << " despite being currently in level " + << userContext()->getLevel() << "\n"; + // Save into map the proof of the processed propagation. Note that + // propagations must be explained eagerly, since their justification depends + // on the theory engine and may be different if we only get its proof when the + // SAT solver pops the user context. Not doing this may lead to open proofs. + // + // It's also necessary to copy the proof node, so we prevent unintended + // updates to the saved proof. Not doing this may also lead to open proofs. + std::shared_ptr currPropagationProcPf = + d_env.getProofNodeManager()->clone( + d_proof.getProofFor(d_currPropagationProccessed)); + Assert(currPropagationProcPf->getRule() != PfRule::ASSUME); + Trace("cnf-debug") << "\t..saved pf {" << currPropagationProcPf << "} " + << *currPropagationProcPf.get() << "\n"; + d_optClausesPfs[explLevel + 1].push_back(currPropagationProcPf); + + d_currPropagationProccessed = Node::null(); +} + +void ProofCnfStream::notifyClauseInsertedAtLevel(const SatClause& clause, + int clLevel) +{ + Trace("cnf") << "Need to save clause " << clause << " in level " + << clLevel + 1 << " despite being currently in level " + << userContext()->getLevel() << "\n"; + Node clauseNode = getClauseNode(clause); + Trace("cnf") << "Node equivalent: " << clauseNode << "\n"; + Assert(clLevel < (userContext()->getLevel() - 1)); + // As above, also justify eagerly. + std::shared_ptr clauseCnfPf = + d_env.getProofNodeManager()->clone(d_proof.getProofFor(clauseNode)); + Assert(clauseCnfPf->getRule() != PfRule::ASSUME); + d_optClausesPfs[clLevel + 1].push_back(clauseCnfPf); +} Node ProofCnfStream::getClauseNode(const SatClause& clause) { diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 1f47203bf..9e43cc643 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -26,6 +26,7 @@ #include "proof/proof_node_manager.h" #include "proof/theory_proof_step_buffer.h" #include "prop/cnf_stream.h" +#include "prop/opt_clauses_manager.h" #include "prop/sat_proof_manager.h" #include "smt/env_obj.h" @@ -101,6 +102,19 @@ class ProofCnfStream : protected EnvObj, public ProofGenerator * generator. */ bool isBlocked(std::shared_ptr pfn); + /** Notify that current propagation inserted at lower level than current. + * + * The proof of the current propagation (d_currPropagationProccessed) will be + * saved in d_optClausesPfs, so that it is not potentially lost when the user + * context is popped. + */ + void notifyCurrPropagationInsertedAtLevel(int explLevel); + /** Notify that added clause was inserted at lower level than current. + * + * As above, the proof of this clause is saved in d_optClausesPfs. + */ + void notifyClauseInsertedAtLevel(const SatClause& clause, int clLevel); + private: /** * Same as above, except that uses the saved d_removable flag. It calls the @@ -174,6 +188,18 @@ class ProofCnfStream : protected EnvObj, public ProofGenerator * These are proof nodes added to this class by external generators. */ context::CDHashSet, ProofNodeHashFunction> d_blocked; + + /** The current propagation being processed via this class. */ + Node d_currPropagationProccessed; + /** User-context-dependent map assertion level to proof nodes. + * + * This map is used to update the internal proof of this class when the + * context pops. + */ + std::map>> d_optClausesPfs; + /** Manager for optimized propagations and added clauses inserted at assertion + * levels below the current user level. */ + OptimizedClausesManager d_optClausesManager; }; } // namespace prop diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index e89d43e07..59790ed7a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -198,6 +198,19 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { } } +void TheoryProxy::notifyCurrPropagationInsertedAtLevel(int explLevel) +{ + d_propEngine->getProofCnfStream()->notifyCurrPropagationInsertedAtLevel( + explLevel); +} + +void TheoryProxy::notifyClauseInsertedAtLevel(const SatClause& clause, + int clLevel) +{ + d_propEngine->getProofCnfStream()->notifyClauseInsertedAtLevel(clause, + clLevel); +} + void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Trace("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index b034f322f..ab780f4b1 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -87,7 +87,25 @@ class TheoryProxy : protected EnvObj, public Registrar void theoryCheck(theory::Theory::Effort effort); + /** Get an explanation for literal `l` and save it on clause `explanation`. */ void explainPropagation(SatLiteral l, SatClause& explanation); + /** Notify that current propagation inserted at lower level than current. + * + * This method should be called by the SAT solver when the explanation of the + * current propagation is added at lower level than the current user level. + * It'll trigger a call to the ProofCnfStream to notify it that the proof of + * this propagation should be saved in case it's needed after this user + * context is popped. + */ + void notifyCurrPropagationInsertedAtLevel(int explLevel); + /** Notify that added clause was inserted at lower level than current. + * + * As above, but for clauses asserted into the SAT solver. This cannot be done + * in terms of "current added clause" because the clause added at a lower + * level could be for example a lemma derived at a prior moment whose + * assertion the SAT solver delayed. + */ + void notifyClauseInsertedAtLevel(const SatClause& clause, int clLevel); void theoryPropagate(SatClause& output);