Investigate Bitwuzla

[hargoniX]

https://github.com/bitwuzla/bitwuzla is currently the best QF_BV solver out there. While it is capable of a lot of things that we cannot imitate it might be interesting to:

• check out their rewrite and normalization rules
• check out their abstraction refinement loop
• check out their AIG implementation: They also use the Brummayer-Bier optimizations and a slightly funkier AIG implementation that is similar to ours but with more bit-hacks etc. included.
• check out their circuits.

There is a collection of simplification rules from Bitwuzla here https://docs.google.com/spreadsheets/d/1QFgtrqc9IXtYn0sa9gkmteUhIKTsOo-idYoeKx6nj-I/edit#gid=0 anyone can feel free to provide simp rules/simprocs that implement these as a PR