From 381a6ed8f0dc31ce83ccc18f0e622babd3e80525 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 8 Feb 2024 11:09:47 -0300
Subject: [PATCH] fixing skolemization

---
 src/proof/alethe/alethe_node_converter.cpp | 21 +++++++++++++++------
 src/proof/alethe/alethe_post_processor.cpp | 15 +++++++--------
 2 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
index 65ef0e98805..66ee699e8ce 100644
--- a/src/proof/alethe/alethe_node_converter.cpp
+++ b/src/proof/alethe/alethe_node_converter.cpp
@@ -63,16 +63,25 @@ Node AletheNodeConverter::postConvert(Node n)
         uint32_t index;
         if (ProofRuleChecker::getUInt32(cacheVal[1], index))
         {
+          // Since cvc5 *always* skolemize FORALLs, we generate the choice term
+          // assuming it is gonna be introduced via a sko_forall rule, in which
+          // the body of the choice is negated, which means to have universal
+          // quantification of the remaining variables in the choice body, and
+          // the whole thing negated. Likewise, since during Skolemization cvc5
+          // will have negated the body of the original quantifier, we need to
+          // revert that as well.
           Assert(index < quant[0].getNumChildren());
+          Assert(quant[1].getKind() == Kind::NOT);
           Node body =
               index == quant[0].getNumChildren() - 1
                   ? quant[1]
-                  : nm->mkNode(
-                      Kind::EXISTS,
-                      nm->mkNode(Kind::BOUND_VAR_LIST,
-                                 std::vector<Node>{quant[0].begin() + index + 1,
-                                                   quant[0].end()}),
-                      quant[1]);
+                  : nm->mkNode(Kind::FORALL,
+                               nm->mkNode(Kind::BOUND_VAR_LIST,
+                                          std::vector<Node>{
+                                              quant[0].begin() + index + 1,
+                                              quant[0].end()}),
+                               quant[1][0])
+                        .notNode();
           // we need to replace in the body all the free variables (i.e., from 0
           // to index) by their respective choice terms. To do this, we get
           // the skolems for each of these variables, retrieve their
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index d1b544df72b..b271aabfe94 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1445,21 +1445,20 @@ bool AletheProofPostprocessCallback::update(Node res,
         Node choiceBody =
             i == size - 1
                 ? quant[1]
-                : nm->mkNode(
-                    quantKind,
-                    nm->mkNode(Kind::BOUND_VAR_LIST,
-                               std::vector<Node>{bVars.begin() + (size - i),
-                                                 bVars.end()}),
-                    quant[1]);
+                : nm->mkNode(quantKind,
+                             nm->mkNode(Kind::BOUND_VAR_LIST,
+                                        std::vector<Node>{bVars.begin() + i + 1,
+                                                          bVars.end()}),
+                             quant[1]);
         // The choice term is for the i-th variable, with the body as defined
         // above. Remember that when doing SKO_FORALL the body of the choice is
         // negated.
         Node ithChoice =
             nm->mkNode(Kind::WITNESS,
-                       nm->mkNode(Kind::BOUND_VAR_LIST, quant[0][i - 1]),
+                       nm->mkNode(Kind::BOUND_VAR_LIST, quant[0][i]),
                        isExists ? choiceBody : choiceBody.notNode());
         // add to the substitution
-        skoSubstitutions.push_back(quant[0][i - 1].eqNode(ithChoice));
+        skoSubstitutions.push_back(quant[0][i].eqNode(ithChoice));
       }
       Node conclusion = nm->mkNode(
           Kind::SEXPR, d_cl, d_anc.convert(quant.eqNode(skolemized)));