projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a7705df) | patch
[BV] Fix order of rewrites for `concat` (#8010)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 1 Feb 2022 20:27:56 +0000 (12:27 -0800)
committerGitHub <noreply@github.com>
Tue, 1 Feb 2022 20:27:56 +0000 (20:27 +0000)
commit1f47ed4a01d5cca1730bb27fb3c2a4e7a8ade232
tree73e39d818b01252bf6c56fc1753054a2c8c98580tree
parenta7705df3f4df10c0e26bdda3f119c74801ec275dcommit | diff
[BV] Fix order of rewrites for `concat` (#8010)

This commit fixes the order of the rewrites for bit-vector
concatentation such that the rewrite that merges adjacents constants
comes last (the commit also updates the comments to be less confusing).
Before, it could happen that the rewrite step that removes unnecessary
extract operations introduces constants then then would not get merged
before returning REWRITE_DONE.
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history