[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 738497ece18d5bdc8fa25aaee2f1ebfe787d8767..0928ebe53ea0be87e89d5cea4ac9a9d29121febf 100644 (file)
--- 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,