diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-08 07:08:05 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-08 09:08:05 -0600 |
| commit | 819eedc38031d3befb9c3e855bbbfa0afa3bb3cc (patch) | |
| tree | b46343ac3cfb562dcc964d5c596d59b4199a559b /src/preprocessing | |
| parent | 497a685f14ff12eb05e4aa6ad7b05682609bf7a9 (diff) | |
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.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
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(); /* |