From d5275e10906dd18ea2e83ab1b51b91e59ab59477 Mon Sep 17 00:00:00 2001
From: Lachnitt <lachnitt@stanford.edu>
Date: Tue, 7 Dec 2021 12:25:03 -0800
Subject: [PATCH] [proofs] Alethe: Fix Bug in Finalize (#7746)

Assumptions in Alethe are printed as (or F1 ... Fn) but should be treated as if they are printed as (cl (or F1 ... Fn)). Thus, if in the post visit it is checked whether an additional or step is needed this has to be treated as a special case.
---
 src/proof/alethe/alethe_post_processor.cpp | 65 ++++++++++++++++------
 1 file changed, 49 insertions(+), 16 deletions(-)

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 46ec3f25e..7ef9cc9db 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1446,17 +1446,28 @@ bool AletheProofPostprocessCallback::finalize(Node res,
       {
         std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
         Node childConclusion = childPf->getArguments()[2];
+        AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
         // if child conclusion is of the form (sexpr cl (or ...)), then we need
         // to add an OR step, since this child must not be a singleton
-        if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
-            && childConclusion[1].getKind() == kind::OR)
+        if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
+             && childConclusion[1].getKind() == kind::OR)
+            || (childRule == AletheRule::ASSUME
+                && childConclusion.getKind() == kind::OR))
         {
           hasUpdated = true;
           // Add or step
           std::vector<Node> subterms{d_cl};
-          subterms.insert(subterms.end(),
-                          childConclusion[1].begin(),
-                          childConclusion[1].end());
+          if (childRule == AletheRule::ASSUME)
+          {
+            subterms.insert(
+                subterms.end(), childConclusion.begin(), childConclusion.end());
+          }
+          else
+          {
+            subterms.insert(subterms.end(),
+                            childConclusion[1].begin(),
+                            childConclusion[1].end());
+          }
           Node newConclusion = nm->mkNode(kind::SEXPR, subterms);
           addAletheStep(AletheRule::OR,
                         newConclusion,
@@ -1485,16 +1496,27 @@ bool AletheProofPostprocessCallback::finalize(Node res,
         {
           std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[i]);
           Node childConclusion = childPf->getArguments()[2];
+          AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
           // Add or step
-          if (childConclusion.getNumChildren() == 2
-              && childConclusion[0] == d_cl
-              && childConclusion[1].getKind() == kind::OR)
+          if ((childConclusion.getNumChildren() == 2
+               && childConclusion[0] == d_cl
+               && childConclusion[1].getKind() == kind::OR)
+              || (childRule == AletheRule::ASSUME
+                  && childConclusion.getKind() == kind::OR))
           {
             hasUpdated = true;
             std::vector<Node> lits{d_cl};
-            lits.insert(lits.end(),
-                        childConclusion[1].begin(),
-                        childConclusion[1].end());
+            if (childRule == AletheRule::ASSUME)
+            {
+              lits.insert(
+                  lits.end(), childConclusion.begin(), childConclusion.end());
+            }
+            else
+            {
+              lits.insert(lits.end(),
+                          childConclusion[1].begin(),
+                          childConclusion[1].end());
+            }
             Node conclusion = nm->mkNode(kind::SEXPR, lits);
             addAletheStep(AletheRule::OR,
                           conclusion,
@@ -1548,14 +1570,25 @@ bool AletheProofPostprocessCallback::finalize(Node res,
     {
       std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
       Node childConclusion = childPf->getArguments()[2];
-      if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
-          && childConclusion[1].getKind() == kind::OR)
+      AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
+      if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
+           && childConclusion[1].getKind() == kind::OR)
+          || (childRule == AletheRule::ASSUME
+              && childConclusion.getKind() == kind::OR))
       {
         // Add or step for child
         std::vector<Node> subterms{d_cl};
-        subterms.insert(subterms.end(),
-                        childConclusion[1].begin(),
-                        childConclusion[1].end());
+        if (getAletheRule(childPf->getArguments()[0]) == AletheRule::ASSUME)
+        {
+          subterms.insert(
+              subterms.end(), childConclusion.begin(), childConclusion.end());
+        }
+        else
+        {
+          subterms.insert(subterms.end(),
+                          childConclusion[1].begin(),
+                          childConclusion[1].end());
+        }
         Node newChild = nm->mkNode(kind::SEXPR, subterms);
         addAletheStep(
             AletheRule::OR, newChild, newChild, {children[0]}, {}, *cdp);
-- 
2.30.2