From f6563f7d1e25279c6446e74ce358ea63c4b53ab0 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 20 Sep 2021 16:49:22 -0300
Subject: [PATCH] [proofs] Alethe: adds a node converter

Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
---
 src/CMakeLists.txt                         |  2 +
 src/proof/alethe/alethe_node_converter.cpp | 38 +++++++++++++++++
 src/proof/alethe/alethe_node_converter.h   | 48 ++++++++++++++++++++++
 3 files changed, 88 insertions(+)
 create mode 100644 src/proof/alethe/alethe_node_converter.cpp
 create mode 100644 src/proof/alethe/alethe_node_converter.h

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d6fbfba37..8053340e8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -221,6 +221,8 @@ libcvc5_add_sources(
   proof/theory_proof_step_buffer.h
   proof/unsat_core.cpp
   proof/unsat_core.h
+  proof/alethe/alethe_node_converter.cpp
+  proof/alethe/alethe_node_converter.h
   prop/bv_sat_solver_notify.h
   prop/bvminisat/bvminisat.cpp
   prop/bvminisat/bvminisat.h
diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
new file mode 100644
index 000000000..d78c185a4
--- /dev/null
+++ b/src/proof/alethe/alethe_node_converter.cpp
@@ -0,0 +1,38 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of Alethe node conversion
+ */
+
+#include "proof/alethe/alethe_node_converter.h"
+
+#include "expr/node_algorithm.h"
+
+namespace cvc5 {
+namespace proof {
+
+AletheNodeConverter::AletheNodeConverter() {}
+
+Node AletheNodeConverter::postConvert(Node n)
+{
+  // whether node is a quantifier with attributes, in which case we remove it
+  if (n.getKind() == kind::FORALL && n.getNumChildren() == 3)
+  {
+    return NodeManager::currentNM()->mkNode(kind::FORALL, n[0], n[1]);
+  }
+  return n;
+}
+
+bool AletheNodeConverter::shouldTraverse(Node n) { return expr::hasClosure(n); }
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/alethe/alethe_node_converter.h b/src/proof/alethe/alethe_node_converter.h
new file mode 100644
index 000000000..310bc70ff
--- /dev/null
+++ b/src/proof/alethe/alethe_node_converter.h
@@ -0,0 +1,48 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Alethe node conversion
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__ALETHE__ALETHE_NODE_CONVERTER_H
+#define CVC4__PROOF__ALETHE__ALETHE_NODE_CONVERTER_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "expr/node_converter.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * This is a helper class for the Alethe post-processor that converts nodes into
+ * form that Alethe expects.
+ */
+class AletheNodeConverter : public NodeConverter
+{
+ public:
+  AletheNodeConverter();
+  ~AletheNodeConverter() {}
+  /** Convert by removing attributes of quantifiers. */
+  Node postConvert(Node n) override;
+  /** Should only traverse nodes containing closures. */
+  bool shouldTraverse(Node n) override;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif
-- 
2.30.2