Add node converter utility (#6878)

Adds a utility for converting nodes. This is the first step towards the LFSC proof conversion.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 094c7bcbd2eba8bd824f42aaa3f39bb8df43b11c..ed8a25f17c795a38bd4a747a35c8730651d43996 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -39,6 +39,8 @@ libcvc5_add_sources(
   node_algorithm.h
   node_builder.cpp
   node_builder.h
+  node_converter.cpp
+  node_converter.h
   node_manager.cpp
   node_manager.h
   node_manager_attributes.h

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
new file mode 100644 (file)
index 0000000..92b4591
--- /dev/null
+++ b/src/expr/node_converter.cpp
@@ -0,0 +1,251 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Node converter utility
+ */
+
+#include "expr/node_converter.h"
+
+#include "expr/attribute.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+
+NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {}
+
+Node NodeConverter::convert(Node n)
+{
+  Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<Node, Node>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = d_cache.find(cur);
+    Trace("nconv-debug2") << "convert " << cur << std::endl;
+    if (it == d_cache.end())
+    {
+      d_cache[cur] = Node::null();
+      Assert(d_preCache.find(cur) == d_preCache.end());
+      Node curp = preConvert(cur);
+      // If curp = cur, then we did not pre-rewrite. Hence, we should not
+      // revisit cur, and instead set curp to null.
+      curp = curp == cur ? Node::null() : curp;
+      d_preCache[cur] = curp;
+      if (!curp.isNull())
+      {
+        visit.push_back(cur);
+        visit.push_back(curp);
+      }
+      else
+      {
+        if (!shouldTraverse(cur))
+        {
+          addToCache(cur, cur);
+        }
+        else
+        {
+          visit.push_back(cur);
+          if (cur.getMetaKind() == metakind::PARAMETERIZED)
+          {
+            visit.push_back(cur.getOperator());
+          }
+          visit.insert(visit.end(), cur.begin(), cur.end());
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      it = d_preCache.find(cur);
+      Assert(it != d_preCache.end());
+      if (!it->second.isNull())
+      {
+        // it converts to what its prewrite converts to
+        Assert(d_cache.find(it->second) != d_cache.end());
+        Node ret = d_cache[it->second];
+        addToCache(cur, ret);
+      }
+      else
+      {
+        Node ret = cur;
+        bool childChanged = false;
+        std::vector<Node> children;
+        if (ret.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          it = d_cache.find(ret.getOperator());
+          Assert(it != d_cache.end());
+          Assert(!it->second.isNull());
+          childChanged = childChanged || ret.getOperator() != it->second;
+          children.push_back(it->second);
+        }
+        for (const Node& cn : ret)
+        {
+          it = d_cache.find(cn);
+          Assert(it != d_cache.end());
+          Assert(!it->second.isNull());
+          childChanged = childChanged || cn != it->second;
+          children.push_back(it->second);
+        }
+        if (childChanged)
+        {
+          ret = nm->mkNode(ret.getKind(), children);
+        }
+        // run the callback for the current application
+        Node cret = postConvert(ret);
+        if (!cret.isNull() && ret != cret)
+        {
+          AlwaysAssert(cret.getType().isComparableTo(ret.getType()))
+              << "Converting " << ret << " to " << cret << " changes type";
+          ret = cret;
+        }
+        addToCache(cur, ret);
+      }
+    }
+  } while (!visit.empty());
+  Assert(d_cache.find(n) != d_cache.end());
+  Assert(!d_cache.find(n)->second.isNull());
+  return d_cache[n];
+}
+
+TypeNode NodeConverter::convertType(TypeNode tn)
+{
+  if (tn.isNull())
+  {
+    return tn;
+  }
+  Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl;
+  std::unordered_map<TypeNode, TypeNode>::iterator it;
+  std::vector<TypeNode> visit;
+  TypeNode cur;
+  visit.push_back(tn);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = d_tcache.find(cur);
+    Trace("nconv-debug2") << "convert type " << cur << std::endl;
+    if (it == d_tcache.end())
+    {
+      d_tcache[cur] = TypeNode::null();
+      Assert(d_preTCache.find(cur) == d_preTCache.end());
+      TypeNode curp = preConvertType(cur);
+      // if curp = cur, set null to avoid infinite loop
+      curp = curp == cur ? TypeNode::null() : curp;
+      d_preTCache[cur] = curp;
+      if (!curp.isNull())
+      {
+        visit.push_back(cur);
+        visit.push_back(curp);
+      }
+      else
+      {
+        curp = curp.isNull() ? cur : curp;
+        if (cur.getNumChildren() == 0)
+        {
+          TypeNode ret = postConvertType(cur);
+          addToTypeCache(cur, ret);
+        }
+        else
+        {
+          visit.push_back(cur);
+          visit.insert(visit.end(), cur.begin(), cur.end());
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      it = d_preTCache.find(cur);
+      Assert(it != d_preTCache.end());
+      if (!it->second.isNull())
+      {
+        // it converts to what its prewrite converts to
+        Assert(d_tcache.find(it->second) != d_tcache.end());
+        TypeNode ret = d_tcache[it->second];
+        addToTypeCache(cur, ret);
+      }
+      else
+      {
+        TypeNode ret = cur;
+        // reconstruct using a node builder, which seems to be required for
+        // type nodes.
+        NodeBuilder nb(ret.getKind());
+        if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
+        {
+          // push the operator
+          nb << ret.getOperator();
+        }
+        for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
+             j != iend;
+             ++j)
+        {
+          it = d_tcache.find(*j);
+          Assert(it != d_tcache.end());
+          Assert(!it->second.isNull());
+          nb << it->second;
+        }
+        // construct the type node
+        ret = nb.constructTypeNode();
+        Trace("nconv-debug") << cur << " <- " << ret << std::endl;
+        // run the callback for the current application
+        TypeNode cret = postConvertType(ret);
+        if (!cret.isNull())
+        {
+          ret = cret;
+        }
+        Trace("nconv-debug")
+            << cur << " <- " << ret << " (post-convert)" << std::endl;
+        addToTypeCache(cur, ret);
+      }
+    }
+  } while (!visit.empty());
+  Assert(d_tcache.find(tn) != d_tcache.end());
+  Assert(!d_tcache.find(tn)->second.isNull());
+  Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn]
+                       << std::endl;
+  return d_tcache[tn];
+}
+
+void NodeConverter::addToCache(TNode cur, TNode ret)
+{
+  d_cache[cur] = ret;
+  // also force idempotency, if specified
+  if (d_forceIdem)
+  {
+    d_cache[ret] = ret;
+  }
+}
+void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret)
+{
+  d_tcache[cur] = ret;
+  // also force idempotency, if specified
+  if (d_forceIdem)
+  {
+    d_tcache[ret] = ret;
+  }
+}
+
+Node NodeConverter::preConvert(Node n) { return Node::null(); }
+Node NodeConverter::postConvert(Node n) { return Node::null(); }
+
+TypeNode NodeConverter::preConvertType(TypeNode tn) { return TypeNode::null(); }
+TypeNode NodeConverter::postConvertType(TypeNode tn)
+{
+  return TypeNode::null();
+}
+bool NodeConverter::shouldTraverse(Node n) { return true; }
+
+}  // namespace cvc5

diff --git a/src/expr/node_converter.h b/src/expr/node_converter.h
new file mode 100644 (file)
index 0000000..6edb252
--- /dev/null
+++ b/src/expr/node_converter.h
@@ -0,0 +1,107 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Node converter utility
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC4__EXPR__NODE_CONVERTER_H
+#define CVC4__EXPR__NODE_CONVERTER_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace cvc5 {
+
+/**
+ * A node converter for terms and types. Implements term/type traversals,
+ * calling the provided implementations of conversion methods (pre/postConvert
+ * and pre/postConvertType) at pre-traversal and post-traversal.
+ *
+ * This class can be used as a generic method for converting terms/types, which
+ * is orthogonal to methods for traversing nodes.
+ */
+class NodeConverter
+{
+ public:
+  /**
+   * @param forceIdem If true, this assumes that terms returned by postConvert
+   * and postConvertType should not be converted again.
+   */
+  NodeConverter(bool forceIdem = true);
+  virtual ~NodeConverter() {}
+  /**
+   * This converts node n based on the preConvert/postConvert methods that can
+   * be overriden by instances of this class.
+   */
+  Node convert(Node n);
+
+  /**
+   * This converts type node n based on the preConvertType/postConvertType
+   * methods that can be overriden by instances of this class.
+   */
+  TypeNode convertType(TypeNode tn);
+
+ protected:
+  //------------------------- virtual interface
+  /** Should we traverse n? */
+  virtual bool shouldTraverse(Node n);
+  /**
+   * Run the conversion for n during pre-order traversal.
+   * Returning null is equivalent to saying the node should not be changed.
+   */
+  virtual Node preConvert(Node n);
+  /**
+   * Run the conversion for post-order traversal, where notice n is a term
+   * of the form:
+   *   (f i_1 ... i_m)
+   * where i_1, ..., i_m are terms that have been returned by previous calls
+   * to postConvert.
+   *
+   * Returning null is equivalent to saying the node should not be changed.
+   */
+  virtual Node postConvert(Node n);
+  /**
+   * Run the conversion, same as `preConvert`, but for type nodes, which notice
+   * can be built from children similar to Node.
+   */
+  virtual TypeNode preConvertType(TypeNode n);
+  /**
+   * Run the conversion, same as `postConvert`, but for type nodes, which notice
+   * can be built from children similar to Node.
+   */
+  virtual TypeNode postConvertType(TypeNode n);
+  //------------------------- end virtual interface
+ private:
+  /** Add to cache */
+  void addToCache(TNode cur, TNode ret);
+  /** Add to type cache */
+  void addToTypeCache(TypeNode cur, TypeNode ret);
+  /** Node cache for preConvert */
+  std::unordered_map<Node, Node> d_preCache;
+  /** Node cache for postConvert */
+  std::unordered_map<Node, Node> d_cache;
+  /** TypeNode cache for preConvert */
+  std::unordered_map<TypeNode, TypeNode> d_preTCache;
+  /** TypeNode cache for postConvert */
+  std::unordered_map<TypeNode, TypeNode> d_tcache;
+  /** Whether this node converter is idempotent. */
+  bool d_forceIdem;
+};
+
+}  // namespace cvc5
+
+#endif