From: Lachnitt <lachnitt@stanford.edu>
Date: Tue, 21 Sep 2021 19:59:27 +0000 (-0700)
Subject: [Proofs] Alethe: Translate ASSUME rule (#7213)
X-Git-Tag: cvc5-1.0.0~1187
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=636012f559ff6df9f3ee774baba1b0805f4269c8;p=cvc5.git

[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>
---

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,