From b6f9e0016a3bbf3172196ce2ef13964b89f5fddf Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 31 Mar 2022 13:56:20 -0300 Subject: [PATCH] [proofs] Adding post-visit processing to proof node updater (#8431) Previously in the proof node updater only structural reasoning was done at post-visit time (merging subproofs, checking free assumptions). This commit adds a virtual method to allow updating the proof node at post-visit time. In particular this commit is important to functionality in the alethe post processing that is deactivated in master. CC @Lachnitt --- src/proof/alethe/alethe_post_processor.cpp | 32 +++++++++---- src/proof/alethe/alethe_post_processor.h | 17 +++++-- src/proof/proof_node_updater.cpp | 53 ++++++++++++++++++---- src/proof/proof_node_updater.h | 48 ++++++++++++++++---- 4 files changed, 117 insertions(+), 33 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index a78e5657b..3e182f882 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -45,6 +45,15 @@ bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, return pn->getRule() != PfRule::ALETHE_RULE; } +bool AletheProofPostprocessCallback::shouldUpdatePost( + std::shared_ptr pn, const std::vector& fa) +{ + Assert(!pn->getArguments().empty()); + AletheRule rule = getAletheRule(pn->getArguments()[0]); + return rule == AletheRule::RESOLUTION || rule == AletheRule::REORDERING + || rule == AletheRule::CONTRACTION; +} + bool AletheProofPostprocessCallback::update(Node res, PfRule id, const std::vector& children, @@ -324,8 +333,8 @@ bool AletheProofPostprocessCallback::update(Node res, return success; } case PfRule::THEORY_REWRITE: - { - return addAletheStep(AletheRule::ALL_SIMPLIFY, + { + return addAletheStep(AletheRule::ALL_SIMPLIFY, res, nm->mkNode(kind::SEXPR, d_cl, res), children, @@ -1468,16 +1477,17 @@ bool AletheProofPostprocessCallback::update(Node res, } // Adds an OR rule to the premises of a step if the premise is not a clause and -// should not be a singleton. Since FACTORING and REORDERING always take +// should not be a singleton. Since CONTRACTION and REORDERING always take // non-singletons, this function adds an OR step to their premise if it was // formerly printed as (cl (or F1 ... Fn)). For resolution, it is necessary to // check all children to find out whether they're singleton before determining // if they are already printed correctly. -bool AletheProofPostprocessCallback::finalize(Node res, - PfRule id, - const std::vector& children, - const std::vector& args, - CDProof* cdp) +bool AletheProofPostprocessCallback::updatePost( + Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp) { NodeManager* nm = NodeManager::currentNM(); AletheRule rule = getAletheRule(args[0]); @@ -1672,7 +1682,11 @@ bool AletheProofPostprocessCallback::finalize(Node res, } return false; } - default: return false; + default: + { + Unreachable(); + return false; + } } return false; } diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 1bdf98666..afff16471 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -50,17 +50,24 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback const std::vector& args, CDProof* cdp, bool& continueUpdate) override; + /** Should proof pn be updated at post-visit? + * + * Only if its top-level Alethe proof rule is RESOLUTION, REORDERING, or + * CONTRACTION. + */ + bool shouldUpdatePost(std::shared_ptr pn, + const std::vector& fa) override; /** * This method is used to add an additional application of the or-rule between * a conclusion (cl (or F1 ... Fn)) and a rule that uses this conclusion as a * premise and treats it as a clause, i.e. assumes that it has been printed * as (cl F1 ... Fn). */ - bool finalize(Node res, - PfRule id, - const std::vector& children, - const std::vector& args, - CDProof* cdp); + bool updatePost(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp) override; /** * This method is used to add some last steps to a proof when this is * necessary. The final step should always be printed as (cl). However: diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp index e550a3cd1..53647e238 100644 --- a/src/proof/proof_node_updater.cpp +++ b/src/proof/proof_node_updater.cpp @@ -35,6 +35,21 @@ bool ProofNodeUpdaterCallback::update(Node res, return false; } +bool ProofNodeUpdaterCallback::shouldUpdatePost(std::shared_ptr pn, + const std::vector& fa) +{ + return false; +} + +bool ProofNodeUpdaterCallback::updatePost(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp) +{ + return false; +} + ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb, bool mergeSubproofs, @@ -178,15 +193,11 @@ void ProofNodeUpdater::processInternal(std::shared_ptr pf, Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; } -bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, - const std::vector& fa, - bool& continueUpdate) +bool ProofNodeUpdater::updateProofNode(std::shared_ptr cur, + const std::vector& fa, + bool& continueUpdate, + bool preVisit) { - // should it be updated? - if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) - { - return false; - } PfRule id = cur->getRule(); // use CDProof to open a scope for which the callback updates CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); @@ -203,7 +214,9 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, 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)) + if (preVisit + ? d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate) + : d_cb.updatePost(res, id, ccn, cur->getArguments(), &cpf)) { std::shared_ptr npn = cpf.getProofFor(res); std::vector fullFa; @@ -222,7 +235,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, // We have that npn is a node we occurring the final updated version of // the proof. We can now debug based on the expected set of free // assumptions. - Trace("pfnu-debug") << "Ensure update closed..." << std::endl; + Trace("pfnu-debug") << "Ensure updated closed..." << std::endl; pfnEnsureClosedWrt( npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); } @@ -233,6 +246,20 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, return false; } +bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, + const std::vector& fa, + bool& continueUpdate, + bool preVisit) +{ + // should it be updated? + if (preVisit ? !d_cb.shouldUpdate(cur, fa, continueUpdate) + : !d_cb.shouldUpdatePost(cur, fa)) + { + return false; + } + return updateProofNode(cur, fa, continueUpdate, preVisit); +} + void ProofNodeUpdater::runFinalize( std::shared_ptr cur, const std::vector& fa, @@ -240,6 +267,12 @@ void ProofNodeUpdater::runFinalize( std::map>>& resCacheNcWaiting, std::unordered_map& cfaMap) { + // run update (marked as post-visit) to a fixed point + bool dummyContinueUpdate; + while (runUpdate(cur, fa, dummyContinueUpdate, false)) + { + Trace("pf-process-debug") << "...updated proof." << std::endl; + } if (d_mergeSubproofs) { Node res = cur->getResult(); diff --git a/src/proof/proof_node_updater.h b/src/proof/proof_node_updater.h index 85e3703f8..4b82148f6 100644 --- a/src/proof/proof_node_updater.h +++ b/src/proof/proof_node_updater.h @@ -67,6 +67,21 @@ class ProofNodeUpdaterCallback const std::vector& args, CDProof* cdp, bool& continueUpdate); + + /** As above, but at post-visit. + * + * We do not pass a continueUpdate flag to this method, or the one below, + * since the children of this proof node have already been updated. + */ + virtual bool shouldUpdatePost(std::shared_ptr pn, + const std::vector& fa); + + /** As above, but at post-visit. */ + virtual bool updatePost(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp); }; /** @@ -125,20 +140,35 @@ class ProofNodeUpdater */ void processInternal(std::shared_ptr pf, std::vector& fa); /** - * Update proof node cur based on the callback. This modifies curr using - * ProofNodeManager::updateNode based on the proof node constructed to - * replace it by the callback. Return true if cur was updated. If - * continueUpdate is updated to false, then cur is not updated further - * and its children are not traversed. + * Update proof node cur based on the callback and on whether we are updating + * at pre visit or post visit time. This modifies curr using + * ProofNodeManager::updateNode based on the proof node constructed to replace + * it by the callback. If we are debugging free assumptions, the set fa is + * used to check whether the updated proof node is closed with relation to + * them. Return true if cur was updated, and continueUpdate may be set to + * false by the callback. + */ + bool updateProofNode(std::shared_ptr cur, + const std::vector& fa, + bool& continueUpdate, + bool preVisit); + /** + * Update the node cur if it should be updated according to the callback. How + * the callback performs the update, if at all, depends if we are at pre- or + * post-visit time. If continueUpdate is updated to false, then cur is not + * updated further and its children are not traversed (when pre-visiting). */ bool runUpdate(std::shared_ptr cur, const std::vector& fa, - bool& continueUpdate); + bool& continueUpdate, + bool preVisit = true); /** * Finalize the node cur. This is called at the moment that it is established - * that cur will appear in the final proof. We do any final debug checking - * and add it to resCache/resCacheNcWaiting if we are merging subproofs, where - * these map result formulas to proof nodes with/without assumptions. + * that cur will appear in the final proof. We do any final debug checking and + * add it to resCache/resCacheNcWaiting if we are merging subproofs, where + * these map result formulas to proof nodes with/without assumptions. If we + * are updating nodes at post visit time, then we run updateProofNode on it. + * */ void runFinalize(std::shared_ptr cur, const std::vector& fa, -- 2.30.2