opt-bug-fe986b4-2
Pre-release
Pre-release
·
4153 commits
to master
since this release
feat: BitVec.add_shiftLeft_eq_or_shiftLeft (#7761)
This PR implements the core theorem for the Bitwuzla rewrites
[NORM_BV_NOT_OR_SHL](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv.cpp#L1495-L1510)
and
[BV_ADD_SHL](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv.cpp#L395-L401),
which convert the mixed-boolean-arithmetic expression into a purely
arithmetic expression:
```lean
theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
x + (y <<< x) = x ||| (y <<< x)
```