From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 8 Jan 2021 15:08:05 +0000 (-0800)
Subject: bv-to-int: avoid binarizing nodes twice (#5749)
X-Git-Tag: cvc5-1.0.0~2393
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=819eedc38031d3befb9c3e855bbbfa0afa3bb3cc;p=cvc5.git

bv-to-int: avoid binarizing nodes twice (#5749)

In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.
---

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 47170c607..04d6b7a0c 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -77,7 +77,13 @@ Node BVToInt::modpow2(Node n, uint64_t exponent)
  */
 Node BVToInt::makeBinary(Node n)
 {
-  for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER))
+  for (TNode current : NodeDfsIterable(n,
+                                       VisitOrder::POSTORDER,
+                                       // skip visited nodes
+                                       [this](TNode tn) {
+                                         return d_binarizeCache.find(tn)
+                                                != d_binarizeCache.end();
+                                       }))
   {
     uint64_t numChildren = current.getNumChildren();
     /*