From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 4 Dec 2020 07:42:34 +0000 (-0800)
Subject: Use NodeDfsIterable for makeBinary (#5595)
X-Git-Tag: cvc5-1.0.0~2504
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6741daaf587f7602c6dc23753361a405c28c7ef6;p=cvc5.git

Use NodeDfsIterable for makeBinary (#5595)

Replaces the manual dag traversal in BVToInt::makeBinarywith NodeDfsIterable.

This is a subset of the changes in #4176, updated to apply to master.
---

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 7ffe1bc76..f14eafcc4 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/node_traversal.h"
 #include "options/uf_options.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
@@ -76,72 +77,49 @@ Node BVToInt::modpow2(Node n, uint64_t exponent)
  */
 Node BVToInt::makeBinary(Node n)
 {
-  vector<Node> toVisit;
-  toVisit.push_back(n);
-  while (!toVisit.empty())
+  for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER))
   {
-    Node current = toVisit.back();
     uint64_t numChildren = current.getNumChildren();
-    if (d_binarizeCache.find(current) == d_binarizeCache.end())
-    {
-      /**
-       * We still haven't visited the sub-dag rooted at the current node.
-       * In this case, we:
-       * mark that we have visited this node by assigning a null node to it in
-       * the cache, and add its children to toVisit.
-       */
-      d_binarizeCache[current] = Node();
-      toVisit.insert(toVisit.end(), current.begin(), current.end());
-    }
-    else if (d_binarizeCache[current].get().isNull())
+    /*
+     * We already visited the sub-dag rooted at the current node,
+     * and binarized all its children.
+     * Now we binarize the current node itself.
+     */
+    kind::Kind_t k = current.getKind();
+    if ((numChildren > 2)
+        && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
+            || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
+            || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
     {
-      /*
-       * We already visited the sub-dag rooted at the current node,
-       * and binarized all its children.
-       * Now we binarize the current node itself.
-       */
-      toVisit.pop_back();
-      kind::Kind_t k = current.getKind();
-      if ((numChildren > 2)
-          && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
-              || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
-              || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
+      // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat
+      Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end());
+      Node result = d_binarizeCache[current[0]];
+      for (uint64_t i = 1; i < numChildren; i++)
       {
-        // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat
-        Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end());
-        Node result = d_binarizeCache[current[0]];
-        for (uint64_t i = 1; i < numChildren; i++)
-        {
-          Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end());
-          Node child = d_binarizeCache[current[i]];
-          result = d_nm->mkNode(current.getKind(), result, child);
-        }
-        d_binarizeCache[current] = result;
+        Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end());
+        Node child = d_binarizeCache[current[i]];
+        result = d_nm->mkNode(current.getKind(), result, child);
       }
-      else if (numChildren > 0)
+      d_binarizeCache[current] = result;
+    }
+    else if (numChildren > 0)
+    {
+      // current has children, but we do not binarize it
+      NodeBuilder<> builder(k);
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
-        // current has children, but we do not binarize it
-        NodeBuilder<> builder(k);
-        if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
-        {
-          builder << current.getOperator();
-        }
-        for (Node child : current)
-        {
-          builder << d_binarizeCache[child].get();
-        }
-        d_binarizeCache[current] = builder.constructNode();
+        builder << current.getOperator();
       }
-      else
+      for (Node child : current)
       {
-        // current has no children
-        d_binarizeCache[current] = current;
+        builder << d_binarizeCache[child].get();
       }
+      d_binarizeCache[current] = builder.constructNode();
     }
     else
     {
-      // We already binarized current and it is in the cache.
-      toVisit.pop_back();
+      // current has no children
+      d_binarizeCache[current] = current;
     }
   }
   return d_binarizeCache[n];