From: Lachnitt Date: Fri, 22 Oct 2021 18:38:47 +0000 (-0700) Subject: [proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397) X-Git-Tag: cvc5-1.0.0~1003 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e283d0fb1c09cd482f8483a138d697720cf69ed2;p=cvc5.git [proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397) Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus. Co-authored-by: Haniel Barbosa --- diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index ef7735b44..7bdc15c05 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -18,8 +18,8 @@ #include "expr/node_algorithm.h" #include "proof/proof.h" #include "proof/proof_checker.h" -#include "util/rational.h" #include "theory/builtin/proof_checker.h" +#include "util/rational.h" namespace cvc5 { @@ -223,6 +223,7 @@ bool AletheProofPostprocessCallback::update(Node res, children, sanitized_args, *cdp); + Node andNode, vp3; if (args.size() == 1) { @@ -477,6 +478,256 @@ bool AletheProofPostprocessCallback::update(Node res, return addAletheStep( vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp); } + // ======== Resolution and N-ary Resolution + // See proof_rule.h for documentation on the RESOLUTION and CHAIN_RESOLUTION + // rule. This comment uses variable names as introduced there. + // + // 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., + // + // (cl F1 (or F2 F3)) (cl (not F1)) + // -------------------------------------- RESOLUTION + // (cl (or F2 F3)) + // + // (cl F1 F2 F3) (cl (not F1)) + // -------------------------------------- RESOLUTION + // (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. + // + // + // If C = (or F1 ... Fn) is a non-singleton clause, then: + // + // VP1 ... VPn + // ------------------ RESOLUTION + // (cl F1 ... Fn)* + // + // Else if, C = false: + // + // VP1 ... VPn + // ------------------ RESOLUTION + // (cl)* + // + // Otherwise: + // + // VP1 ... VPn + // ------------------ RESOLUTION + // (cl C)* + // + // * the corresponding proof node is C + 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 res is not an or node, then it's necessarily a singleton clause. + bool isSingletonClause = res.getKind() != kind::OR; + // Otherwise, we need to determine if res, which is of the form (or t1 ... + // tn), corresponds to the clause (cl t1 ... tn) or to (cl (OR t1 ... + // tn)). The only way in which the latter can happen is if res occurs as a + // child in one of the premises, and is not eliminated afterwards. So we + // search for res as a subterm of some children, which would mark its last + // insertion into the resolution result. If res does not occur as the + // pivot to be eliminated in a subsequent premise, then, and only then, it + // is a singleton clause. + if (!isSingletonClause) + { + size_t i; + // Find out the last child to introduced res, if any. We only need to + // look at the last one because any previous introduction would have + // been eliminated. + // + // After the loop finishes i is the index of the child C_i that + // introduced res. If i=0 none of the children introduced res as a + // subterm and therefore it cannot be a singleton clause. + for (i = children.size(); i > 0; --i) + { + // only non-singleton clauses may be introducing + // res, so we only care about non-singleton or nodes. We check then + // against the kind and whether the whole or node occurs as a pivot of + // the respective resolution + if (children[i - 1].getKind() != kind::OR) + { + continue; + } + size_t pivotIndex = (i != 1) ? 2 * (i - 1) - 1 : 1; + if (args[pivotIndex] == children[i - 1] + || args[pivotIndex].notNode() == children[i - 1]) + { + continue; + } + // if res occurs as a subterm of a non-singleton premise + if (std::find(children[i - 1].begin(), children[i - 1].end(), res) + != children[i - 1].end()) + { + break; + } + } + + // If res is a subterm of one of the children we still need to check if + // that subterm is eliminated + if (i > 0) + { + bool posFirst = (i == 1) ? (args[0] == trueNode) + : (args[(2 * (i - 1)) - 2] == trueNode); + Node pivot = (i == 1) ? args[1] : args[(2 * (i - 1)) - 1]; + + // Check if it is eliminated by the previous resolution step + if ((res == pivot && !posFirst) + || (res.notNode() == pivot && posFirst) + || (pivot.notNode() == res && posFirst)) + { + // We decrease i by one, since it could have been the case that i + // was equal to children.size(), so that isSingletonClause is set to + // false + --i; + } + else + { + // Otherwise check if any subsequent premise eliminates it + for (; i < children.size(); ++i) + { + posFirst = args[(2 * i) - 2] == trueNode; + pivot = args[(2 * i) - 1]; + // To eliminate res, the clause must contain it with opposite + // polarity. There are three successful cases, according to the + // pivot and its sign + // + // - res is the same as the pivot and posFirst is true, which + // means that the clause contains its negation and eliminates it + // + // - res is the negation of the pivot and posFirst is false, so + // the clause contains the node whose negation is res. Note that + // this case may either be res.notNode() == pivot or res == + // pivot.notNode(). + if ((res == pivot && posFirst) + || (res.notNode() == pivot && !posFirst) + || (pivot.notNode() == res && !posFirst)) + { + break; + } + } + } + } + // if not eliminated (loop went to the end), then it's a singleton + // clause + isSingletonClause = i == children.size(); + } + if (!isSingletonClause) + { + return addAletheStepFromOr( + AletheRule::RESOLUTION, res, new_children, {}, *cdp); + } + return addAletheStep(AletheRule::RESOLUTION, + res, + res == falseNode + ? nm->mkNode(kind::SEXPR, d_cl) + : nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 587190524..810eb7433 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -97,7 +97,7 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback * @return True if the step could be added, or false if not. */ bool addAletheStepFromOr(AletheRule rule, - Node res, + Node res, const std::vector& children, const std::vector& args, CDProof& cdp);