diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-26 06:40:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-26 13:40:07 +0000 |
commit | f767e820881e57fd315616efa2a1817110758e93 (patch) | |
tree | dc755205e5170b396e4c93797b04b8a0a8c83a73 | |
parent | 2b2ccd57aed86414a6cee5251e3b55aeafd256e3 (diff) |
[proofs] Alethe: Translate AND_ELIM rule (#7404)
Implementation of the translation of AND_ELIM rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index c3925af22..ae6705025 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -949,6 +949,17 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + // ======== And elimination + // This rule is translated according to the singleton pattern. + case PfRule::AND_ELIM: + { + return addAletheStep(AletheRule::AND, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |