From b2cce731768066e5bdc62838cf14ae9e528da95e Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Wed, 1 Dec 2021 11:12:37 -0800 Subject: [PATCH] [proofs] Alethe: Add finalize function to insert missing OR steps (#7724) A post visit that adds an OR step is needed in case a premise is printed as a singleton (cl (or F1 ... Fn)) but used as a clause (cl F1 ... Fn). Co-authored-by: Haniel Barbosa --- src/options/proof_options.toml | 8 + src/proof/alethe/alethe_post_processor.cpp | 298 +++++++++++++-------- src/proof/alethe/alethe_post_processor.h | 11 + 3 files changed, 210 insertions(+), 107 deletions(-) diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 36891fd51..3eb32060e 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -90,3 +90,11 @@ name = "Proof" [[option.mode.DSL_REWRITE]] name = "dsl-rewrite" help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps." + +[[option]] + name = "proofAletheResPivots" + category = "regular" + long = "proof-alethe-res-pivots" + type = "bool" + default = "false" + help = "Add pivots to Alethe resolution steps" diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 7ef4bbbd6..2254c025f 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -16,6 +16,7 @@ #include "proof/alethe/alethe_post_processor.h" #include "expr/node_algorithm.h" +#include "options/proof_options.h" #include "proof/proof.h" #include "proof/proof_checker.h" #include "proof/proof_node_algorithm.h" @@ -86,6 +87,12 @@ bool AletheProofPostprocessCallback::update(Node res, // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof // node printed as (cl (or b c)). // + // Adding an OR node to a premises will take place in the finalize function + // where in the case that a step is printed as (cl (or F1 ... Fn)) but used + // as (cl F1 ... Fn) an OR step is added to transform it to this very thing. + // This is necessary for rules that work on clauses, i.e. RESOLUTION, + // CHAIN_RESOLUTION, REORDERING and FACTORING. + // // // Some proof rules have a close correspondence in Alethe. There are two // very frequent patterns that, to avoid repetition, are described here and @@ -488,8 +495,8 @@ bool AletheProofPostprocessCallback::update(Node res, // Because the RESOLUTION rule is merely a special case of CHAIN_RESOLUTION, // the same translation can be used for both. // - // The main complication for the translation is that in the case the - // conclusion C is (or G1 ... Gn), the result is ambigous. E.g., + // The main complication for the translation of the rule is that in the case + // that the conclusion C is (or G1 ... Gn), the result is ambigous. E.g., // // (cl F1 (or F2 F3)) (cl (not F1)) // -------------------------------------- RESOLUTION @@ -500,46 +507,7 @@ bool AletheProofPostprocessCallback::update(Node res, // (cl F2 F3) // // both (cl (or F2 F3)) and (cl F2 F3) correspond to the same proof node (or - // F2 F3). One way to deal with this issue is for the translation to keep - // track of the current clause generated after each resolution (the - // resolvent) and then compare it to the result. E.g. in the first case - // current_resolvent = {(or F2 F3)} indicates that the result is a singleton - // clause, while in the second current_resolvent = {F2,F3}, indicating the - // result is a non-singleton clause. - // - // It is always clear what clauses to add to current_resolvent, except for - // when a child is an assumption or the result of an equality resolution - // step. In these cases it might be necessary to add an additional or step. - // - // If for any Ci, rule(Ci) = ASSUME or rule(Ci) = EQ_RESOLVE and Ci = (or F1 - // ... Fn) and Ci != L_{i-1} (for C1, C1 != L_1) then: - // - // (Pi:Ci) - // ---------------------- OR - // (VPi:(cl F1 ... Fn)) - // - // Otherwise VPi = Ci. - // - // However to determine whether C is a singleton clause or not it is not - // necessary to calculate the complete current resolvent. Instead it - // suffices to find the last introduction of the conclusion as a subterm of - // a child and then check if it is eliminated by a later resolution step. If - // the conclusion was not introduced as a subterm it has to be a - // non-singleton clause. If it was introduced but not eliminated, it follows - // that it is indeed not a singleton clause and should be printed as (cl F1 - // ... Fn) instead of (cl (or F1 ... Fn)). - // - // This procedure is possible since the proof is already structured in a - // certain way. It can never contain a second occurrence of a literal when - // the first occurrence we found was eliminated from the proof. E.g., - // - // (cl (not (or a b))) (cl (or a b) (or a b)) - // --------------------------------------------- - // (cl (or a b)) - // - // is not possible because of the semantics of CHAIN_RESOLUTION, which only - // removes one occurence of the resolvent in the resolving clauses. - // + // F2 F3). Thus, it has to be checked if C is a singleton clause or not. // // If C = (or F1 ... Fn) is a non-singleton clause, then: // @@ -563,79 +531,18 @@ bool AletheProofPostprocessCallback::update(Node res, case PfRule::RESOLUTION: case PfRule::CHAIN_RESOLUTION: { - Node trueNode = nm->mkConst(true); - Node falseNode = nm->mkConst(false); - std::vector new_children = children; - - // If a child F = (or F1 ... Fn) is the result of ASSUME or - // EQ_RESOLVE it might be necessary to add an additional step with the - // Alethe or rule since otherwise it will be used as (cl (or F1 ... Fn)). - - // The first child is used as a non-singleton clause if it is not equal - // to its pivot L_1. Since it's the first clause in the resolution it can - // only be equal to the pivot in the case the polarity is true. - if (children[0].getKind() == kind::OR - && (args[0] != trueNode || children[0] != args[1])) - { - std::shared_ptr childPf = cdp->getProofFor(children[0]); - if (childPf->getRule() == PfRule::ASSUME - || childPf->getRule() == PfRule::EQ_RESOLVE) - { - // Add or step - std::vector subterms{d_cl}; - subterms.insert( - subterms.end(), children[0].begin(), children[0].end()); - Node conclusion = nm->mkNode(kind::SEXPR, subterms); - addAletheStep( - AletheRule::OR, conclusion, conclusion, {children[0]}, {}, *cdp); - new_children[0] = conclusion; - } - } - - // For all other children C_i the procedure is similar. There is however a - // key difference in the choice of the pivot element which is now the - // L_{i-1}, i.e. the pivot of the child with the result of the i-1 - // resolution steps between the children before it. Therefore, if the - // policy id_{i-1} is true, the pivot has to appear negated in the child - // in which case it should not be a (cl (or F1 ... Fn)) node. The same is - // true if it isn't the pivot element. - for (std::size_t i = 1, size = children.size(); i < size; ++i) - { - if (children[i].getKind() == kind::OR - && (args[2 * (i - 1)] != falseNode - || args[2 * (i - 1) + 1] != children[i])) - { - std::shared_ptr childPf = cdp->getProofFor(children[i]); - if (childPf->getRule() == PfRule::ASSUME - || childPf->getRule() == PfRule::EQ_RESOLVE) - { - // Add or step - std::vector lits{d_cl}; - lits.insert(lits.end(), children[i].begin(), children[i].end()); - Node conclusion = nm->mkNode(kind::SEXPR, lits); - addAletheStep(AletheRule::OR, - conclusion, - conclusion, - {children[i]}, - {}, - *cdp); - new_children[i] = conclusion; - } - } - } - if (!expr::isSingletonClause(res, children, args)) { return addAletheStepFromOr( - AletheRule::RESOLUTION, res, new_children, {}, *cdp); + AletheRule::RESOLUTION, res, children, args, *cdp); } return addAletheStep(AletheRule::RESOLUTION, res, - res == falseNode + res == nm->mkConst(false) ? nm->mkNode(kind::SEXPR, d_cl) : nm->mkNode(kind::SEXPR, d_cl, res), - new_children, - {}, + children, + args, *cdp); } // ======== Factoring @@ -1488,6 +1395,183 @@ 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 +// 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) +{ + NodeManager* nm = NodeManager::currentNM(); + AletheRule rule = getAletheRule(args[0]); + Trace("alethe-proof") << "... finalizer for rule " << rule << " / " << res + << std::endl; + switch (rule) + { + // In the case of a resolution rule that step might originally have been a + // cvc5 RESOLUTION or CHAIN_RESOLUTION step. So it is possible that one of + // the children was processed to be printed as (cl (or F1 ... Fn)) but it is + // being used by this rule as (cl F1 ... Fn). We can determine whether this + // is the case by looking at the pivot of the respective resolution step + // involving the child, adding an OR step to obtain the non-singleton clause + // needed. + case AletheRule::RESOLUTION: + { + // This means it's a resolution step generated during the processing of + // other rules, so the confusion we are looking for does not happen. + if (args.size() < 4) + { + return false; + } + std::vector new_children = children; + std::vector new_args = + options::proofAletheResPivots() + ? args + : std::vector(args.begin(), args.begin() + 3); + Node trueNode = nm->mkConst(true); + Node falseNode = nm->mkConst(false); + bool hasUpdated = false; + + // The first child is used as a non-singleton clause if it is not equal + // to its pivot L_1. Since it's the first clause in the resolution it can + // only be equal to the pivot in the case the polarity is true. + if (children[0].getKind() == kind::OR + && (args[3] != trueNode || children[0] != args[4])) + { + std::shared_ptr childPf = cdp->getProofFor(children[0]); + Node childConclusion = childPf->getArguments()[2]; + // if child conclusion is of the form (sexpr cl (or ...)), then we need + // to add an OR step, since this child must not be a singleton + if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl + && childConclusion[1].getKind() == kind::OR) + { + hasUpdated = true; + // Add or step + std::vector subterms{d_cl}; + subterms.insert(subterms.end(), + childConclusion[1].begin(), + childConclusion[1].end()); + Node newConclusion = nm->mkNode(kind::SEXPR, subterms); + addAletheStep(AletheRule::OR, + newConclusion, + newConclusion, + {children[0]}, + {}, + *cdp); + new_children[0] = newConclusion; + Trace("alethe-proof") + << "Added OR step in finalizer " << childConclusion << " / " + << newConclusion << std::endl; + } + } + // For all other children C_i the procedure is similar. There is however a + // key difference in the choice of the pivot element which is now the + // L_{i-1}, i.e. the pivot of the child with the result of the i-1 + // resolution steps between the children before it. Therefore, if the + // policy id_{i-1} is true, the pivot has to appear negated in the child + // in which case it should not be a (cl (or F1 ... Fn)) node. The same is + // true if it isn't the pivot element. + for (std::size_t i = 1, size = children.size(); i < size; ++i) + { + if (children[i].getKind() == kind::OR + && (args[2 * (i - 1) + 3] != falseNode + || args[2 * (i - 1) + 1 + 3] != children[i])) + { + std::shared_ptr childPf = cdp->getProofFor(children[i]); + Node childConclusion = childPf->getArguments()[2]; + // Add or step + if (childConclusion.getNumChildren() == 2 + && childConclusion[0] == d_cl + && childConclusion[1].getKind() == kind::OR) + { + hasUpdated = true; + std::vector lits{d_cl}; + lits.insert(lits.end(), + childConclusion[1].begin(), + childConclusion[1].end()); + Node conclusion = nm->mkNode(kind::SEXPR, lits); + addAletheStep(AletheRule::OR, + conclusion, + conclusion, + {children[i]}, + {}, + *cdp); + new_children[i] = conclusion; + Trace("alethe-proof") + << "Added OR step in finalizer" << childConclusion << " / " + << conclusion << std::endl; + } + } + } + if (hasUpdated || !options::proofAletheResPivots()) + { + Trace("alethe-proof") + << "... update alethe step in finalizer " << res << " " + << new_children << " / " << args << std::endl; + cdp->addStep(res, PfRule::ALETHE_RULE, new_children, new_args); + return true; + } + return false; + } + // A application of the FACTORING rule: + // + // (or a a b) + // ---------- FACTORING + // (or a b) + // + // might be translated during pre-visit (update) to: + // + // (or (cl a a b))* + // ---------------- CONTRACTION + // (cl a b)** + // + // In this post-visit an additional OR step is added in that case: + // + // (cl (or a a b))* + // ---------------- OR + // (cl a a b) + // ---------------- CONTRACTION + // (cl a b)** + // + // * the corresponding proof node is (or a a b) + // ** the corresponding proof node is (or a b) + // + // The process is anagolous for REORDERING. + case AletheRule::REORDERING: + case AletheRule::CONTRACTION: + { + std::shared_ptr childPf = cdp->getProofFor(children[0]); + Node childConclusion = childPf->getArguments()[2]; + if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl + && childConclusion[1].getKind() == kind::OR) + { + // Add or step for child + std::vector subterms{d_cl}; + subterms.insert(subterms.end(), + childConclusion[1].begin(), + childConclusion[1].end()); + Node newChild = nm->mkNode(kind::SEXPR, subterms); + addAletheStep( + AletheRule::OR, newChild, newChild, {children[0]}, {}, *cdp); + Trace("alethe-proof") + << "Added OR step in finalizer to child " << childConclusion + << " / " << newChild << std::endl; + // update res step + cdp->addStep(res, PfRule::ALETHE_RULE, {newChild}, args); + return true; + } + return false; + } + default: return false; + } + return false; +} + // The last step of the proof was: // // Children: (P1:C1) ... (Pn:Cn) diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index e01a95b56..7819c20bb 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -50,6 +50,17 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback const std::vector& args, CDProof* cdp, bool& continueUpdate) 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); /** * 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: -- 2.30.2