From: Lachnitt Date: Wed, 1 Dec 2021 02:46:26 +0000 (-0800) Subject: Alethe: Add function that adds final steps to proof (#7710) X-Git-Tag: cvc5-1.0.0~745 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd7d8ce26f5d4a5864b1dce78473c97a51394e40;p=cvc5.git Alethe: Add function that adds final steps to proof (#7710) There are some cases when the result has to be transformed, e.g. when it was printed as (cl false) which is correct everywhere except in the last step. This function then transforms the result into (cl). Should be merged after PR #7675. Co-authored-by: Haniel Barbosa hanielbbarbosa@gmail.com --- diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index d5cb07f79..7ef4bbbd6 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1488,6 +1488,98 @@ bool AletheProofPostprocessCallback::update(Node res, } } +// The last step of the proof was: +// +// Children: (P1:C1) ... (Pn:Cn) +// Arguments: (AletheRule::VRULE,false,(cl false)) +// --------------------- +// Conclusion: (false) +// +// In Alethe: +// +// P1 ... Pn +// ------------------- VRULE ---------------------- FALSE +// (VP1:(cl false))* (VP2:(cl (not true))) +// -------------------------------------------------- RESOLUTION +// (cl)** +// +// * the corresponding proof node is ((false)) +// ** the corresponding proof node is (false) +bool AletheProofPostprocessCallback::finalStep( + Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp) +{ + NodeManager* nm = NodeManager::currentNM(); + Node falseNode = nm->mkConst(false); + + if ( + // If the last proof rule was not translated yet + (id == PfRule::ALETHE_RULE) && + // This case can only occur if the last step is an assumption + (args[2].getNumChildren() > 1) && + // If the proof node has result (false) additional steps have to be added. + (args[2][1] != falseNode)) + { + return false; + } + + // remove attribute for outermost scope + if (id != PfRule::ALETHE_RULE) + { + std::vector sanitized_args{ + res, + res, + nm->mkConst(CONST_RATIONAL, + static_cast(AletheRule::ASSUME))}; + for (const Node& arg : args) + { + sanitized_args.push_back(d_anc.convert(arg)); + } + return cdp->addStep(res, PfRule::ALETHE_RULE, children, sanitized_args); + } + + bool success = true; + Node vp1 = nm->mkNode(kind::SEXPR, res); // ((false)) + Node vp2 = nm->mkConst(false).notNode(); // (not true) + Node res2 = nm->mkNode(kind::SEXPR, d_cl); // (cl) + AletheRule vrule = getAletheRule(args[0]); + + // In the special case that false is an assumption, we print false instead of + // (cl false) + success &= addAletheStep( + vrule, + vp1, + (vrule == AletheRule::ASSUME ? res : nm->mkNode(kind::SEXPR, d_cl, res)), + children, + {}, + *cdp); + Trace("alethe-proof") << "... add Alethe step " << vp1 << " / " + << nm->mkNode(kind::SEXPR, d_cl, res) << " " << vrule + << " " << children << " / {}" << std::endl; + + success &= addAletheStep( + AletheRule::FALSE, vp2, nm->mkNode(kind::SEXPR, d_cl, vp2), {}, {}, *cdp); + Trace("alethe-proof") << "... add Alethe step " << vp2 << " / " + << nm->mkNode(kind::SEXPR, d_cl, vp2) << " " + << AletheRule::FALSE << " {} / {}" << std::endl; + + success &= + addAletheStep(AletheRule::RESOLUTION, res, res2, {vp2, vp1}, {}, *cdp); + Trace("alethe-proof") << "... add Alethe step " << res << " / " << res2 << " " + << AletheRule::RESOLUTION << " {" << vp2 << ", " << vp1 + << " / {}" << std::endl; + if (!success) + { + Trace("alethe-proof") << "... Error while printing final steps" + << std::endl; + } + + return true; +} + bool AletheProofPostprocessCallback::addAletheStep( AletheRule rule, Node res, @@ -1528,36 +1620,9 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr( return addAletheStep(rule, res, conclusion, children, args, cdp); } -AletheProofPostprocessFinalCallback::AletheProofPostprocessFinalCallback( - ProofNodeManager* pnm, AletheNodeConverter& anc) - : d_pnm(pnm), d_anc(anc) -{ - NodeManager* nm = NodeManager::currentNM(); - d_cl = nm->mkBoundVar("cl", nm->sExprType()); -} - -bool AletheProofPostprocessFinalCallback::shouldUpdate( - std::shared_ptr pn, - const std::vector& fa, - bool& continueUpdate) -{ - return false; -} - -bool AletheProofPostprocessFinalCallback::update( - Node res, - PfRule id, - const std::vector& children, - const std::vector& args, - CDProof* cdp, - bool& continueUpdate) -{ - return true; -} - AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc) - : d_pnm(pnm), d_cb(d_pnm, anc), d_fcb(d_pnm, anc) + : d_pnm(pnm), d_cb(d_pnm, anc) { } diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 810eb7433..e01a95b56 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -50,6 +50,23 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback const std::vector& args, CDProof* cdp, bool& continueUpdate) 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: + * + * 1. If the last step of a proof is reached (which is false) it is printed as + * (cl false). + * 2. If one of the assumptions is false it is printed as false. + * + * Thus, an additional resolution step with (cl (not true)) has to be added to + * transform (cl false) or false into (cl). + * + */ + bool finalStep(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp); private: /** The proof node manager */ @@ -103,55 +120,6 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback CDProof& cdp); }; -/** - * Final callback class used by the Alethe converter to add the last step to a - * proof in the following two cases. The last step should always be printed as - * (cl). - * - * 1. If the last step of a proof which is false is reached it is printed as (cl - * false). - * 2. If one of the assumptions is false it is printed as false. - * - * Thus, an additional resolution step with (cl (not true)) has to be added to - * transfer (cl false) into (cl). - */ -class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback -{ - public: - AletheProofPostprocessFinalCallback(ProofNodeManager* pnm, - AletheNodeConverter& anc); - ~AletheProofPostprocessFinalCallback() {} - /** Should proof pn be updated? It should, if the last step is printed as (cl - * false) or if it is an assumption (in that case it is printed as false). - * Since the proof node should not be traversed, this method will always set - * continueUpdate to false. - */ - bool shouldUpdate(std::shared_ptr pn, - const std::vector& fa, - bool& continueUpdate) override; - /** - * This method gets a proof node pn. If the last step of the proof is false - * which is printed as (cl false) it updates the proof for false such that - * (cl) is printed instead. - */ - bool update(Node res, - PfRule id, - const std::vector& children, - const std::vector& args, - CDProof* cdp, - bool& continueUpdate) override; - - private: - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** The Alethe node converter */ - AletheNodeConverter& d_anc; - /** The cl operator is defined as described in the - * AletheProofPostprocessCallback class above - **/ - Node d_cl; -}; - /** * The proof postprocessor module. This postprocesses a proof node into one * using the rules from the Alethe calculus. @@ -169,8 +137,6 @@ class AletheProofPostprocess ProofNodeManager* d_pnm; /** The post process callback */ AletheProofPostprocessCallback d_cb; - /** The final post process callback */ - AletheProofPostprocessFinalCallback d_fcb; }; } // namespace proof