projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 497a685) | patch
bv-to-int: avoid binarizing nodes twice (#5749)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 8 Jan 2021 15:08:05 +0000 (07:08 -0800)
committerGitHub <noreply@github.com>
Fri, 8 Jan 2021 15:08:05 +0000 (09:08 -0600)
commit819eedc38031d3befb9c3e855bbbfa0afa3bb3cc
treeb46343ac3cfb562dcc964d5c596d59b4199a559btree
parent497a685f14ff12eb05e4aa6ad7b05682609bf7a9commit | 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.
src/preprocessing/passes/bv_to_int.cpp diff | blob | history