diff options
| author | Lachnitt <lachnitt@stanford.edu> | 2021-09-21 12:59:27 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-21 16:59:27 -0300 |
| commit | 636012f559ff6df9f3ee774baba1b0805f4269c8 (patch) | |
| tree | fb345f85d9adeef5dce583e6ee75fe85c3711a8d | |
| parent | c07d80a0ce4dc7144bad7146b0dc96574dd250c9 (diff) | |
[Proofs] Alethe: Translate ASSUME rule (#7213)
Implementation of the translation of ASSUME rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 738497ece..0928ebe53 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -54,6 +54,12 @@ bool AletheProofPostprocessCallback::update(Node res, switch (id) { + //================================================= Core rules + //======================== Assume and Scope + case PfRule::ASSUME: + { + return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |