From: Lachnitt <lachnitt@stanford.edu>
Date: Fri, 22 Oct 2021 19:00:52 +0000 (-0700)
Subject: [proofs] Alethe: Translate FACTORING rule (#7398)
X-Git-Tag: cvc5-1.0.0~1002
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3774c9758b6a23c8ef5d98eaa0879a814114674;p=cvc5.git

[proofs] Alethe: Translate FACTORING rule (#7398)

Implementation of the translation of FACTORING 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 7bdc15c05..920ca7dcb 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -728,6 +728,38 @@ bool AletheProofPostprocessCallback::update(Node res,
                            {},
                            *cdp);
     }
+    // ======== Factoring
+    // See proof_rule.h for documentation on the FACTORING rule. This comment
+    // uses variable names as introduced there.
+    //
+    // If C2 = (or F1 ... Fn) but C1 != (or C2 ... C2), then VC2 = (cl F1 ...
+    // Fn) Otherwise, VC2 = (cl C2).
+    //
+    //    P
+    // ------- DUPLICATED_LITERALS
+    //   VC2*
+    //
+    // * the corresponding proof node is C2
+    case PfRule::FACTORING:
+    {
+      if (res.getKind() == kind::OR)
+      {
+        for (const Node& child : children[0])
+        {
+          if (child != res)
+          {
+            return addAletheStepFromOr(
+                AletheRule::DUPLICATED_LITERALS, res, children, {}, *cdp);
+          }
+        }
+      }
+      return addAletheStep(AletheRule::DUPLICATED_LITERALS,
+                           res,
+                           nm->mkNode(kind::SEXPR, d_cl, res),
+                           children,
+                           {},
+                           *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,