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

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 46ec3f25ea43d6fbfdd59be60d04c00fcab417a8..7ef9cc9dbb611738ac0a8b012f7fb07863cdd841 100644 (file)
--- 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);