From: Lachnitt <lachnitt@stanford.edu>
Date: Mon, 25 Oct 2021 13:26:40 +0000 (-0700)
Subject: [proofs] Alethe: Translate SPLIT rule  (#7399)
X-Git-Tag: cvc5-1.0.0~987
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=418d9264428c56983c92f02537eef321989495b6;p=cvc5.git

[proofs] Alethe: Translate SPLIT rule  (#7399)

Implementation of the translation of SPLIT 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 920ca7dcb..7acdbfffe 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -760,6 +760,32 @@ bool AletheProofPostprocessCallback::update(Node res,
                            {},
                            *cdp);
     }
+    // ======== Split
+    // See proof_rule.h for documentation on the SPLIT rule. This comment
+    // uses variable names as introduced there.
+    //
+    // --------- NOT_NOT      --------- NOT_NOT
+    //    VP1                    VP2
+    // -------------------------------- RESOLUTION
+    //          (cl F (not F))*
+    //
+    // VP1: (cl (not (not (not F))) F)
+    // VP2: (cl (not (not (not (not F)))) (not F))
+    //
+    // * the corresponding proof node is (or F (not F))
+    case PfRule::SPLIT:
+    {
+      Node vp1 = nm->mkNode(
+          kind::SEXPR, d_cl, args[0].notNode().notNode().notNode(), args[0]);
+      Node vp2 = nm->mkNode(kind::SEXPR,
+                              d_cl,
+                              args[0].notNode().notNode().notNode().notNode(),
+                              args[0].notNode());
+
+      return addAletheStep(AletheRule::NOT_NOT, vp2, vp2, {}, {}, *cdp)
+          && addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
+          && addAletheStepFromOr(AletheRule::RESOLUTION, res, {vp1, vp2}, {}, *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,