From 819eedc38031d3befb9c3e855bbbfa0afa3bb3cc Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 8 Jan 2021 07:08:05 -0800 Subject: [PATCH] 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. --- src/preprocessing/passes/bv_to_int.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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(); /* -- 2.30.2