[proofs] Adding NoSubtype node converter to Alethe (#7587)

Initial version. It'll be improved on demand according to new cases that may lead to issues.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c526bd13b3d045dd3d9eac7ddfb60fe3eafd7490..c145f7fda9b8e209ea5607774aa225de22d65352 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -217,6 +217,8 @@ libcvc5_add_sources(
   proof/theory_proof_step_buffer.h
   proof/unsat_core.cpp
   proof/unsat_core.h
+  proof/alethe/alethe_nosubtype_node_converter.cpp
+  proof/alethe/alethe_nosubtype_node_converter.h
   proof/alethe/alethe_node_converter.cpp
   proof/alethe/alethe_node_converter.h
   proof/alethe/alethe_post_processor.cpp

diff --git a/src/proof/alethe/alethe_nosubtype_node_converter.cpp b/src/proof/alethe/alethe_nosubtype_node_converter.cpp
new file mode 100644 (file)
index 0000000..54fb092
--- /dev/null
+++ b/src/proof/alethe/alethe_nosubtype_node_converter.cpp
@@ -0,0 +1,60 @@
+/******************************************************************************
+ * 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 to remove subtyping
+ */
+
+#include "proof/alethe/alethe_nosubtype_node_converter.h"
+
+namespace cvc5 {
+namespace proof {
+
+Node AletheNoSubtypeNodeConverter::postConvert(Node n)
+{
+  if (n.getKind() == kind::APPLY_UF)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    TypeNode tn = n.getOperator().getType();
+    std::vector<TypeNode> argTypes = tn.getArgTypes();
+    // if any of the argument types is real, in case the argument of that
+    // position is an integer constant we must turn it into a real constant
+    // look at all args, if any is an integer constant, transform it
+    bool childChanged = false;
+    std::vector<Node> children;
+    for (size_t i = 0, size = n.getNumChildren(); i < size; ++i)
+    {
+      if (!argTypes[i].isReal() || argTypes[i].isInteger() || !n[i].isConst()
+          || !n[i].getType().isInteger())
+      {
+        children.push_back(n[i]);
+        continue;
+      }
+      Trace("alethe-proof-subtyping")
+          << "\t\t..arg " << i << " is integer constant " << n[i]
+          << " in real position.\n";
+      childChanged = true;
+      children.push_back(nm->mkNode(kind::CAST_TO_REAL, n[i]));
+    }
+    if (childChanged)
+    {
+      if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        children.insert(children.begin(), n.getOperator());
+      }
+      return nm->mkNode(n.getKind(), children);
+    }
+  }
+  return n;
+}
+
+}  // namespace proof
+}  // namespace cvc5

diff --git a/src/proof/alethe/alethe_nosubtype_node_converter.h b/src/proof/alethe/alethe_nosubtype_node_converter.h
new file mode 100644 (file)
index 0000000..aef7efe
--- /dev/null
+++ b/src/proof/alethe/alethe_nosubtype_node_converter.h
@@ -0,0 +1,46 @@
+/******************************************************************************
+ * 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 to remove subtyping
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__ALETHE__ALETHE_NOSUBTYPE_NODE_CONVERTER_H
+#define CVC4__PROOF__ALETHE__ALETHE_NOSUBTYPE_NODE_CONVERTER_H
+
+#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. In particular it removes occurrences of mixed
+ * int/real typing.
+ */
+class AletheNoSubtypeNodeConverter : public NodeConverter
+{
+ public:
+  AletheNoSubtypeNodeConverter() {}
+  ~AletheNoSubtypeNodeConverter() {}
+  /** Convert by casting integer terms into real ones when it's identified that
+   * they occur in "real" positions. For example, (f 1 a), with f having as its
+   * type f : Real -> Real -> Real, will be turned into (f 1.0 a). */
+  Node postConvert(Node n) override;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif