diff options
Diffstat (limited to 'src/proof/alethe/alethe_post_processor.cpp')
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 298 |
1 files changed, 191 insertions, 107 deletions
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<Node> 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<ProofNode> childPf = cdp->getProofFor(children[0]); - if (childPf->getRule() == PfRule::ASSUME - || childPf->getRule() == PfRule::EQ_RESOLVE) - { - // Add or step - std::vector<Node> 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<ProofNode> childPf = cdp->getProofFor(children[i]); - if (childPf->getRule() == PfRule::ASSUME - || childPf->getRule() == PfRule::EQ_RESOLVE) - { - // Add or step - std::vector<Node> 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<Node>& children, + const std::vector<Node>& 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<Node> new_children = children; + std::vector<Node> new_args = + options::proofAletheResPivots() + ? args + : std::vector<Node>(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<ProofNode> 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<Node> 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<ProofNode> 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<Node> 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<ProofNode> 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<Node> 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) |