Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.
#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"
}
}
- // 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);
return false;
}
+bool isSingletonClause(TNode res,
+ const std::vector<Node>& children,
+ const std::vector<Node>& 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
ProofNode* pnc,
std::unordered_set<const ProofNode*>& 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<Node>& children,
+ const std::vector<Node>& args);
+
} // namespace expr
} // namespace cvc5
projects / cvc5.git / commitdiff