From 636012f559ff6df9f3ee774baba1b0805f4269c8 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Tue, 21 Sep 2021 12:59:27 -0700 Subject: [PATCH] [Proofs] Alethe: Translate ASSUME rule (#7213) Implementation of the translation of ASSUME rules into the Alethe calculus. Co-authored-by: Haniel Barbosa --- src/proof/alethe/alethe_post_processor.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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, -- 2.30.2