#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"
// 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
// 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
// (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:
//
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
}
}
+// 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)
projects / cvc5.git / commitdiff