From 8d62f892ddc6ca1b38b3efb2134f12d5678d21ad Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 7 Apr 2021 18:17:33 -0300 Subject: [PATCH] [proof-new] Fixing SMT post-processor's handling of assumptions (#6277) Previously the SMT post-processor would update any assumption as long as it had a proof for it. This can be a problem when one as assumption introduced in a scope that should not be expanded. This commit fixes the issue by adding the option of configuring a proof node updater to track scopes and the assumptions they introduce, which can be used to determine the prood nodes which should be updated. It also changes the SMT post-processor to only update assumptions that have not been introduced in some scope. This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle. --- src/expr/proof_node_updater.cpp | 41 ++++++++----------- src/expr/proof_node_updater.h | 2 + src/options/proof_options.toml | 5 ++- src/prop/proof_post_processor.cpp | 1 + src/prop/proof_post_processor.h | 1 + src/smt/proof_manager.cpp | 24 ++++++++++- src/smt/proof_post_processor.cpp | 36 +++++++++++++---- src/smt/proof_post_processor.h | 18 ++++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/proofs/scope.smt2 | 54 +++++++++++++++++++++++++ 10 files changed, 147 insertions(+), 36 deletions(-) create mode 100644 test/regress/regress0/proofs/scope.smt2 diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 933e5b999..cbd457cd7 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -125,28 +125,21 @@ void ProofNodeUpdater::processInternal( } traversing.push_back(cur); visit.push_back(cur); - if (d_mergeSubproofs) + // If we are not the top-level proof, we were a scope, or became a scope + // after updating, we do a separate recursive call to this method. This + // allows us to properly track the assumptions in scope, which is + // important for example to merge or to determine updates based on free + // assumptions. + if (cur->getRule() == PfRule::SCOPE && cur != pf) { - // If we are not the top-level proof, we were a scope, or became a - // scope after updating, we need to make a separate recursive call to - // this method. This is not necessary if we are not merging subproofs. - if (cur->getRule() == PfRule::SCOPE && cur != pf) - { - std::vector nfa; - // if we are debugging free assumptions, update the set - if (d_debugFreeAssumps) - { - nfa.insert(nfa.end(), fa.begin(), fa.end()); - const std::vector& args = cur->getArguments(); - nfa.insert(nfa.end(), args.begin(), args.end()); - Trace("pfnu-debug2") - << "Process new scope with " << args << std::endl; - } - // Process in new call separately, since we should not cache - // the results of proofs that have a different scope. - processInternal(cur, nfa, traversing); - continue; - } + std::vector nfa; + nfa.insert(nfa.end(), fa.begin(), fa.end()); + const std::vector& args = cur->getArguments(); + nfa.insert(nfa.end(), args.begin(), args.end()); + Trace("pfnu-debug2") << "Process new scope with " << args << std::endl; + // Process in new call separately + processInternal(cur, nfa, traversing); + continue; } const std::vector>& ccp = cur->getChildren(); // now, process children @@ -180,7 +173,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, bool& continueUpdate) { // should it be updated? - if (!d_cb.shouldUpdate(cur, continueUpdate)) + if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) { return false; } @@ -196,9 +189,9 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, // store in the proof cpf.addProof(cp); } - Trace("pf-process-debug") - << "Updating (" << cur->getRule() << ")..." << std::endl; Node res = cur->getResult(); + Trace("pf-process-debug") + << "Updating (" << cur->getRule() << "): " << res << std::endl; // only if the callback updated the node if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) { diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 8e30f14d2..268fcda5e 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -41,10 +41,12 @@ class ProofNodeUpdaterCallback /** Should proof pn be updated? * * @param pn the proof node that maybe should be updated + * @param fa the assumptions in scope * @param continueUpdate whether we should continue recursively updating pn * @return whether we should run the update method on pn */ virtual bool shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) = 0; /** * Update the proof rule application, store steps in cdp. Return true if diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index ff03e70f5..f6a39e0fe 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -16,7 +16,10 @@ header = "options/proof_options.h" [[option.mode.DOT]] name = "dot" help = "Output DOT proof" - +[[option.mode.VERIT]] + name = "verit" + help = "Output veriT proof" + [[option]] name = "proofPrintConclusion" category = "regular" diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 6b31e6053..10bf53aa1 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -29,6 +29,7 @@ ProofPostprocessCallback::ProofPostprocessCallback( void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); } bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) { bool result = pn->getRule() == PfRule::ASSUME diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index 363970117..906faaafd 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -54,6 +54,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback * cancelled, i.e., continueUpdate is set to false. */ bool shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) override; /** Update the proof rule application. * diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index b651e390c..846df7e41 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -34,7 +34,27 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pnm(new ProofNodeManager(d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), u, "smt::PreprocessProofGenerator")), - d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())), + d_pfpp(new ProofPostproccess( + d_pnm.get(), + smte, + d_pppg.get(), + // by default the post-processor will update all assumptions, which + // can lead to SCOPE subproofs of the form + // A + // ... + // B1 B2 + // ... ... + // ------------ + // C + // ------------- SCOPE [B1, B2] + // B1 ^ B2 => C + // + // where A is an available assumption from outside the scope (note + // that B1 was an assumption of this SCOPE subproof but since it could + // be inferred from A, it was updated). This shape is problematic for + // the veriT reconstruction, so we disable the update of scoped + // assumptions (which would disable the update of B1 in this case). + options::proofFormatMode() != options::ProofFormatMode::VERIT)), d_finalProof(nullptr) { // add rules to eliminate here @@ -131,7 +151,7 @@ void PfManager::printProof(std::ostream& out, } // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node - + if (options::proofFormatMode() == options::ProofFormatMode::DOT) { proof::DotPrinter::print(out, fp.get()); diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index dedb686c3..a27a5697e 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -33,12 +33,15 @@ namespace smt { ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg) - : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm) + ProofGenerator* pppg, + bool updateScopedAssumptions) + : d_pnm(pnm), + d_smte(smte), + d_pppg(pppg), + d_wfpm(pnm), + d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); - // always check whether to update ASSUME - d_elimRules.insert(PfRule::ASSUME); } void ProofPostprocessCallback::initializeUpdate() @@ -53,9 +56,26 @@ void ProofPostprocessCallback::setEliminateRule(PfRule rule) } bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) { - return d_elimRules.find(pn->getRule()) != d_elimRules.end(); + PfRule id = pn->getRule(); + if (d_elimRules.find(id) != d_elimRules.end()) + { + return true; + } + // other than elimination rules, we always update assumptions as long as + // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in + // fa + if (id != PfRule::ASSUME + || (!d_updateScopedAssumptions + && std::find(fa.begin(), fa.end(), pn->getResult()) != fa.end())) + { + Trace("smt-proof-pp-debug") + << "... not updating in-scope assumption " << pn->getResult() << "\n"; + return false; + } + return true; } bool ProofPostprocessCallback::update(Node res, @@ -1108,6 +1128,7 @@ void ProofPostprocessFinalCallback::initializeUpdate() } bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) { PfRule r = pn->getRule(); @@ -1146,9 +1167,10 @@ bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg) + ProofGenerator* pppg, + bool updateScopedAssumptions) : d_pnm(pnm), - d_cb(pnm, smte, pppg), + d_cb(pnm, smte, pppg, updateScopedAssumptions), // the update merges subproofs d_updater(d_pnm, d_cb, true), d_finalCb(pnm), diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 9f3e7e55b..4111e83de 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -40,7 +40,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback public: ProofPostprocessCallback(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg); + ProofGenerator* pppg, + bool updateScopedAssumptions); ~ProofPostprocessCallback() {} /** * Initialize, called once for each new ProofNode to process. This initializes @@ -56,6 +57,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback void setEliminateRule(PfRule rule); /** Should proof pn be updated? */ bool shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) override; /** Update the proof rule application. */ bool update(Node res, @@ -80,6 +82,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback std::vector d_wfAssumptions; /** Kinds of proof rules we are eliminating */ std::unordered_set d_elimRules; + /** Whether we post-process assumptions in scope. */ + bool d_updateScopedAssumptions; //---------------------------------reset at the begining of each update /** Mapping assumptions to their proof from preprocessing */ std::map > d_assumpToProof; @@ -244,6 +248,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback void initializeUpdate(); /** Should proof pn be updated? Returns false, adds to stats. */ bool shouldUpdate(std::shared_ptr pn, + const std::vector& fa, bool& continueUpdate) override; /** was pedantic failure */ bool wasPedanticFailure(std::ostream& out) const; @@ -274,9 +279,18 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback class ProofPostproccess { public: + /** + * @param pnm The proof node manager we are using + * @param smte The SMT engine whose proofs are being post-processed + * @param pppg The proof generator for pre-processing proofs + * @param updateScopedAssumptions Whether we post-process assumptions in + * scope. Since doing so is sound and only problematic depending on who is + * consuming the proof, it's true by default. + */ ProofPostproccess(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg); + ProofGenerator* pppg, + bool updateScopedAssumptions = true); ~ProofPostproccess(); /** post-process */ void process(std::shared_ptr pf); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 967b027de..f3f31edbf 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -774,6 +774,7 @@ set(regress_0_tests regress0/printer/let_shadowing.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc + regress0/proofs/scope.smt2 regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/proofs/scope.smt2 b/test/regress/regress0/proofs/scope.smt2 new file mode 100644 index 000000000..7a324952e --- /dev/null +++ b/test/regress/regress0/proofs/scope.smt2 @@ -0,0 +1,54 @@ +; COMMAND-LINE: --produce-proofs +; EXIT: 0 +; SCRUBBER: grep -v -E '.*' +(set-logic AUFLIA) +(declare-sort A$ 0) +(declare-sort B$ 0) +(declare-sort C$ 0) +(declare-sort D$ 0) +(declare-sort E$ 0) +(declare-sort F$ 0) +(declare-sort G$ 0) +(declare-sort H$ 0) +(declare-sort I$ 0) +(declare-sort J$ 0) +(declare-sort K$ 0) +(declare-sort L$ 0) +(declare-sort M$ 0) +(declare-sort N$ 0) +(declare-sort O$ 0) +(declare-sort P$ 0) +(declare-fun f1$ (M$ J$) L$) +(declare-fun f2$ (N$ C$) L$) +(declare-fun f3$ (C$ A$) B$) +(declare-fun f4$ (D$ E$) B$) +(declare-fun f5$ (F$ G$) D$) +(declare-fun f6$ (A$) F$) +(declare-fun f7$ (A$) G$) +(declare-fun f8$ (A$) E$) +(declare-fun f9$ (A$) E$) +(declare-fun x1$ () M$) +(declare-fun x2$ () N$) +(declare-fun x3$ () C$) +(declare-fun x4$ () C$) +(declare-fun x5$ () D$) +(declare-fun x6$ () J$) +(declare-fun x7$ () J$) +(declare-fun x8$ () M$) +(declare-fun x9$ () O$) +(declare-fun f10$ (H$ A$) K$) +(declare-fun f3a$ (E$ H$) I$) +(declare-fun f3b$ (J$ K$) I$) +(declare-fun f5a$ (O$ P$) N$) +(declare-fun x10$ () P$) +(assert (! (forall ((?v0 A$)) (not (= (f3$ x3$ ?v0) (f4$ (f5$ (f6$ ?v0) (f7$ ?v0)) (f8$ ?v0))))) :named a0)) +(assert (! (forall ((?v0 A$)) (not (= (f3$ x4$ ?v0) (f4$ x5$ (f9$ ?v0))))) :named a1)) +(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f8$ ?v0) ?v1) (f3b$ x6$ (f10$ ?v1 ?v0))))) :named a2)) +(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f9$ ?v0) ?v1) (f3b$ x7$ (f10$ ?v1 ?v0))))) :named a3)) +(assert (! (not (= (f1$ x8$ x6$) (f2$ (f5a$ x9$ x10$) x3$))) :named a4)) +(assert (! (= (f1$ x1$ x7$) (f1$ x8$ x6$)) :named a5)) +(assert (! (= (f1$ x1$ x7$) (f2$ x2$ x4$)) :named a6)) +(assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7)) +(assert (! (not false) :named a8)) +(check-sat) +(get-proof) \ No newline at end of file -- 2.30.2