From 4b3a87a6b460a882b37916b80344f4ec30e3b79b Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 8 Feb 2024 11:39:40 -0300
Subject: [PATCH] fixing processing of alpha-equiv

---
 src/proof/alethe/alethe_post_processor.cpp | 49 ++++++++++------------
 1 file changed, 22 insertions(+), 27 deletions(-)

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index b271aabfe94..08f28c2b5fb 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1557,20 +1557,25 @@ bool AletheProofPostprocessCallback::update(Node res,
     // ... (zn An)) G*sigma)
     //
     //
-    // -----    ----- REFL  ----- REFL
-    //  VP1 .... VPn         VP
-    // -------------------------- BIND, ((:= (y1 A1) z1) ... (:= (yn An) zn))
-    //         (= F F*sigma)
-    //
-    // VPi: (cl (= yi zi))^
-    // VP: (cl (= G G*sigma))
+    //  ------------------ REFL
+    //  (cl (= G G*sigma))
+    // -------------------- BIND, ((= y1 z1) ... (= yn zn))
+    //  (= F F*sigma)
     //
     // ^ the corresponding proof node is F*sigma
     case ProofRule::ALPHA_EQUIV:
     {
+      std::vector<Node> varEqs;
       // performance optimization
       // If y1 ... yn are mapped to y1 ... yn it suffices to use a refl step
-      if (res[0].toString() == res[1].toString())
+      bool allSame = true;
+      for (size_t i = 0, size = res[0][0].getNumChildren(); i < size; ++i)
+      {
+        Node v0 = res[0][0][i], v1 = res[1][0][i];
+        allSame = allSame && v0.getName() == v1.getName();
+        varEqs.push_back(v0.eqNode(v1));
+      }
+      if (allSame)
       {
         return addAletheStep(AletheRule::REFL,
                              res,
@@ -1579,27 +1584,17 @@ bool AletheProofPostprocessCallback::update(Node res,
                              {},
                              *cdp);
       }
-
-      std::vector<Node> new_children;
-      bool success = true;
-      for (size_t i = 1, size = args.size(); i < size; i++)
-      {
-        Node vpi = nm->mkNode(Kind::SEXPR, d_cl, args[i]);
-        new_children.push_back(vpi);
-        success&& addAletheStep(AletheRule::REFL, vpi, vpi, {}, {}, *cdp);
-      }
+      // Reflexivity over the quantified bodies
       Node vp = nm->mkNode(
           Kind::SEXPR, d_cl, nm->mkNode(Kind::EQUAL, res[0][1], res[1][1]));
-      success&& addAletheStep(AletheRule::REFL, vp, vp, {}, {}, *cdp);
-      new_children.push_back(vp);
-      new_args.insert(new_args.begin(), args.begin() + 1, args.end());
-      return success
-             && addAletheStep(AletheRule::ANCHOR_BIND,
-                              res,
-                              nm->mkNode(Kind::SEXPR, d_cl, res),
-                              new_children,
-                              new_args,
-                              *cdp);
+      addAletheStep(AletheRule::REFL, vp, vp, {}, {}, *cdp);
+      new_args.insert(new_args.end(), varEqs.begin(), varEqs.end());
+      return addAletheStep(AletheRule::ANCHOR_BIND,
+                           res,
+                           nm->mkNode(Kind::SEXPR, d_cl, res),
+                           {vp},
+                           new_args,
+                           *cdp);
     }
     //================================================= Arithmetic rules
     // ======== Adding Scaled Inequalities