feat(BV): Interval domains for bit-vectors

[bclement-ocp]

This patch adds interval domains to the Bitv_rel module, as well as interreductions between the bitlist and interval domains following:

Sharpening Constraint Programming approaches for Bit-Vector Theory. Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin. CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy.

More precisely:

• The Intervals module is extended to support the extract operation, which is used to propagate between bit-vector compositions and their components;

• The interreductions are implemented using the new Bitlist.increase_lower_bound, Bitlist.decrease_upper_bound, and the new shared_msb helper in Bitv_rel;

• Propagations are performed by alternating propagations until fixpoint in each domain, followed by interreductions and propagations until fixpoint in the other domain, until reaching a fixpoint for the whole procedure. It is not clear that this is the best strategy; the goal is to try and limit interreductions since they are relatively expensive but we should revisit this once more operations are supported.

For now, only the bvule, bvult, bvugt and bvuge primitives are supported as built-in bit-vector operations; other operations such as bvadd are still encoded using bv2nat. These operations will be migrated to bit-vector primitives in a follow-up PR.

Finally, there are some tests for the tricky bits (Intervals.extract and the interreduction primitives) using QCheck.

[bclement-ocp]

Note: this is +107-515 or a net regression of about 400 problems on our QF_BV subset. This is expected: this PR uses bit-vector domains for bvule / bvult / etc. but does not change the use of bv2nat / int2bv round-trip for other arithmetic operators. This means that we are prevented from doing many interesting propagations.

A follow-up PR (should be ready sometime next week) fixes that by implementing arithmetic propagators for the BV interval domains: it is currently +1156-209 (or an improvement of almost 1000 problems) on that same subset compared to next, at least in part due to interreduction between arithmetic and bitwise constraints.

[bclement-ocp]

After reading and thinking a lot (and starting a small Coq developement) about the explanations for intervals:

• I am quite confident that the map_monotone function introduced in this PR, and the map2_monotone function introduced in #1085, are correct
• I am reasonably confident that the other interval functions introduced in this PR and following PRs are correct when called on a single interval, with the exception maybe of extract
• I am not convinced that the other interval functions are correct when called on an union of intervals.

That is not to say that I don't think they are correct (in particular, I am confident that all of these functions return the right values for the bounds), but that they may forget necessary explanations in some cases, causing unsoundness. I think the cases where we forget explanations are quite rare (or may be made impossible currently) so I will rewrite these functions to try to be less clever and add more explanations. I will also write a documentation for the intervals module, now that i understand the invariants better.

This does not impact the rest of the PR or the rest of the PRs in the stack.

[bclement-ocp]

I am quite confident that the map_monotone function introduced in this PR, and the map2_monotone function introduced inhttps://github.com/OCamlPro/alt-ergo/pull/1085, are correct

Turns out they are not (: I thought I had replicated the behavior of the add function properly, but turns out I missed a crucial detail.

[Halbaroth]

I started a review of the code? Should I discard it?

[bclement-ocp]

Everything except for changes to the Intervals.ml module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there are pre-existing hard-to-trigger soundness bugs lurking, although the module is very unclear about its invariants so maybe it is actually impossible), so I would hold off reviewing changes to this file specifically. But the rest should not be affected — again, it is just implementation details of the way the Intervals module stores explanations.

[Halbaroth]

Everything except for changes to the Intervals.ml module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there are pre-existing hard-to-trigger soundness bugs lurking, although the module is very unclear about its invariants so maybe it is actually impossible), so I would hold off reviewing changes to this file specifically. But the rest should not be affected — again, it is just implementation details of the way the Intervals module stores explanations.

Honestly, when I read this module months ago, my conclusion was we should rewrite it completely. It's not a priority but I plan to work on it later.

[bclement-ocp]

Honestly, when I read this module months ago, my conclusion was we should rewrite it completely. It's not a priority but I plan to work on it later.

I am about 99% sure there currently are soundness bugs that can be triggered by properly crafted formulas so I am actually looking into it now. Hopefully I will not need a full rewrite to fix them :/

[bclement-ocp]

I have adapted the code on top of #1108 (unfortunately I messed up the rebase so the history is a bit weird, apologies for that!).

[bclement-ocp]

I am about 99% sure there currently are soundness bugs that can be triggered by properly crafted formulas so I am actually looking into it now. Hopefully I will not need a full rewrite to fix them :/

FWIW: We were in the 1% of chances, but the code in this PR for Intervals.extract was still wrong. Fairly confident the new one is right (and if wrong that we have a chance to catch it by reading the code).