[proofs] Alethe: adds a node converter

Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d6fbfba37a873b1a4d6c168cab1e4ec46c90218c..8053340e8c98a5ed21bf3fa652bf10354a6650ef 100644 (file)
--- 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 (file)
index 0000000..d78c185
--- /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 (file)
index 0000000..310bc70
--- /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