Improving reasoning for the BV theory

[Halbaroth]

This umbrella issue tracks the progression of the BV theory reasoning. Please add related issue here and what we plan to improve in the future.

• [X] Support of bvnot reasoning, see #800 and #856.
• [X] Constraint propagation for bvand, bvor, bvxor, etc (see #944)
• [ ] Constraint simplification (from (bvand (concat a b) (concat c d)) to (concat (bvand a c) (bvand b d)))
• [x] Constraint propagation for bv2nat and int2bv

[bclement-ocp]

Some updates here:

• Doing constraint propagation on bv2nat and int2bv is not easy to do properly, because we don't have access to the arithmetic domains from Bitv_rel
• This is even more true if we want to do interreductions between arithmetic and bitwise domains
• The plan is now to instead add separate interval domains for bitvectors to Bitv_rel and to perform interreductions following Sharpening Constraint Programming approaches for Bit-Vector Theory

• 1040 #1044 #1054 #1055 #1056 do some groundwork to prepare the addition of the new domains, including reworking some of the constraint APIs to be easier to use with multiple domains

• Additional PRs are currently being tested that actually add the interval domains & arithmetic propagators following the paper above
• At some point we might want to figure out how to reconcile the BV and Arith interval domains
• No progress on the "constraint simplification" part yet

[Halbaroth]

I think we can remove the milestone on this issue because we do not plan extra works on it before the next release.

[bclement-ocp]

Yes, we won't have constraint simplification for 2.6. Let's keep it to track bv2nat(bvadd) support.

[bclement-ocp]

I wanted to implement support for bv2nat applied to bvadd etc. operators but did not find the time — or rather, I have several tentative implementations that need to be rebased and compared to figure out which one to use, which I won't have time to do for this release.

We already have many bv improvements, and these changes only add a small additional improvement for the bv2nat problems from our partners (~ 0.2% more problems solved) so it will have to wait for the next release. I'll try to cut a point release once it is integrated.

[bclement-ocp]

I said this but then realised we are not even able to prove that (int2bv (+ (bv2nat x) (bv2nat y)) and (bvadd x y) are equal currently, so that's annoying. I will make a small patch for that.

[bclement-ocp]

Turns out this is somewhat rendered useless by #1228 which at least partially explain why I was seeing so little impact here.

[bclement-ocp]

Postponing the remaining tasks here to 2.7