Get to the expressiveness of QF_BV

[hargoniX]

We want the bv_decide tactic to be able to solve things at the expressiveness of QF_BV (https://smt-lib.org/theories-FixedSizeBitVectors.shtml). This requires adding a lot of primitive operations to the bitblaster still. It also requires PRing lots of fundamental BitVec theorems about these operations to core.

The current status is tracked at: https://docs.google.com/spreadsheets/d/1AFUChxhNZhOC2XQEn_RXk3A1JwLeOP1OPbPjfYjdEUQ/edit?usp=sharing