diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-26 07:00:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-26 14:00:55 +0000 |
commit | 8995119775293b5b3e618701d2e4e318f18e5fed (patch) | |
tree | cc80a2e1bd0f3c5b3fdd964b4f1cd0524d3ca6ee | |
parent | f767e820881e57fd315616efa2a1817110758e93 (diff) |
[proofs] Alethe: Translate AND_INTRO rule (#7405)
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index ae6705025..8060eb697 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -960,6 +960,39 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + // ======== And introduction + // See proof_rule.h for documentation on the AND_INTRO rule. This + // comment uses variable names as introduced there. + // + // + // ----- AND_NEG + // VP1 P1 ... Pn + // -------------------------- RESOLUTION + // (cl (and F1 ... Fn))* + // + // VP1:(cl (and F1 ... Fn) (not F1) ... (not Fn)) + // + // * the corresponding proof node is (and F1 ... Fn) + case PfRule::AND_INTRO: + { + std::vector<Node> neg_Nodes = {d_cl,res}; + for (size_t i = 0, size = children.size(); i < size; i++) + { + neg_Nodes.push_back(children[i].notNode()); + } + Node vp1 = nm->mkNode(kind::SEXPR, neg_Nodes); + + std::vector<Node> new_children = {vp1}; + new_children.insert(new_children.end(), children.begin(), children.end()); + + return addAletheStep(AletheRule::AND_NEG, vp1, vp1, {}, {}, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + new_children, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |