From: Haniel Barbosa Date: Tue, 26 Oct 2021 20:46:46 +0000 (-0300) Subject: [proofs] Modularize check for whether a clause is singleton (#7497) X-Git-Tag: cvc5-1.0.0~963 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d2c50986cb53207e0f99a950b939736db226634;p=cvc5.git [proofs] Modularize check for whether a clause is singleton (#7497) Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method. --- diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 119972863..2eb3d8d1d 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "proof/proof.h" #include "proof/proof_checker.h" +#include "proof/proof_node_algorithm.h" #include "theory/builtin/proof_checker.h" #include "util/rational.h" @@ -621,100 +622,7 @@ bool AletheProofPostprocessCallback::update(Node res, } } - // 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) + if (!expr::isSingletonClause(res, children, args)) { return addAletheStepFromOr( AletheRule::RESOLUTION, res, new_children, {}, *cdp); diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp index 5f56d785e..ce8ca55c3 100644 --- a/src/proof/proof_node_algorithm.cpp +++ b/src/proof/proof_node_algorithm.cpp @@ -237,5 +237,93 @@ bool containsSubproof(ProofNode* pn, return false; } +bool isSingletonClause(TNode res, + const std::vector& children, + const std::vector& args) +{ + if (res.getKind() != kind::OR) + { + return true; + } + size_t i; + Node trueNode = NodeManager::currentNM()->mkConst(true); + // 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 we return false in the end + --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 + return i == children.size(); +} + } // namespace expr } // namespace cvc5 diff --git a/src/proof/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h index f35a84c87..b2e20c478 100644 --- a/src/proof/proof_node_algorithm.h +++ b/src/proof/proof_node_algorithm.h @@ -91,6 +91,34 @@ bool containsSubproof(ProofNode* pn, ProofNode* pnc, std::unordered_set& visited); +/** Whether the result of a resolution corresponds to a singleton clause + * + * Viewing a node as a clause (i.e., as a list of literals), whether a node of + * the form (or t1 ... tn) corresponds to the clause [t1, ..., tn]) or to the + * clause [(or t1 ... tn)] can be ambiguous in different settings. + * + * This method determines whether a node `res`, corresponding to the result of a + * resolution inference with premises `children` and arguments `args` (see + * proof_rule.h for more details on the inference), is a singleton clause (i.e., + * a clause with a single literal). + * + * It does so relying on the fact that `res` is only a singleton if it occurs as + * a child in one of the premises and is not eliminated afterwards. So we search + * for `res` as a subterm of some child, 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. + * + * @param res the result of a resolution inference + * @param children the premises for the resolution inference + * @param args the arguments, i.e., the pivots and their polarities, for the + * resolution inference + * @return whether `res` is a singleton clause + */ +bool isSingletonClause(TNode res, + const std::vector& children, + const std::vector& args); + } // namespace expr } // namespace cvc5