refactor(BV): Use Z.t in BV solver

[bclement-ocp]

The old implementation of the solver relied on the fact that each constant fragment of a bit-vector was either all ones or all zeroes because it defined a constant zero as the smallest bit-vector, a constant one as the biggest bit-vector, and then computed the min and max elements of a set of bit-vectors to check for consistency. With the new solver based on Tarjan's union-find, this limitation is no longer necessary, and it causes the solver to needlessly split bit-vector variables involved in equalities with non-uniform constants ¹.

This patch is a simple refactoring of the bit-vector solver to use integers rather than booleans to represent the constant parts of bit-vectors, hopefully improving performance for bit-vectors with non-uniform constant parts.

Footnotes

1. For instance, solving x = #b0000 can be done in a single swoop, but solving x = #b0101 currently first slices x into a @ b @ c @ d and then assigns values to each of a, b, c and d. ↩

[hra687261]

LGTM

[hra687261]

How is the size incorrect?

[bclement-ocp]

Because the underlying value is not resized, the size is just changed (for instance we could have 0b1111 with size = 1 which is "wrong" in other parts of the code). So the high bits must be ignored, which pop_bit does.

[hra687261]

Unrelated to the PR, but the comments in lines 1467-1668 should be fixed/reworded, with something like _ are the values we must (differentiate|distinguish) from (those) that start* with a _

[bclement-ocp]

Can you clarify what should be fixed? The values in [t] all start with a 1, and the model value must be distinct from all these values; the values in [f] all start with a 0 and the model value must also be distinct from all these values. I wouldn't understand that from your reformulation.

[hra687261]

It's just the wording, the current comments say:

    (* [t] are the values we must be distinct from that starts with a '1' *)
    (* [f] are the values we must be distinct from that starts with a '0' *)

It's true that what I suggested doesn't help. But I don't get your explanation from the current comments either.
Putting the explanation you gave as a comment instead of the two comments that are currently present would be better IMO.

[bclement-ocp]

Right. Would something like "[t] holds the values that (a) we must be distinct from and (b) start with a 1" be clearer? I will make a PR once this one is merged to avoid conflicts.

[hra687261]

Yes, it would be clearer.

[Halbaroth]

Please don't merge before I did my review ;)

[Halbaroth]

Sorry, I don't know why but my message doesn't appear ;/. I resend it:
You're PR is great but could you clarify this point please:

it defined a constant zero as the smallest bit-vector, a constant one as the biggest bit-vector, and then computed the min and max elements.

Not sure to understand what you mean by min and max elements here and I guess it's important to understand that as you assert this is not the way we check consistency anymore.

[bclement-ocp]

Not sure to understand what you mean by min and max elements here and I guess it's important to understand that as you assert this is not the way we check consistency anymore.

The old BV solver (removed as part of #856) created one set for each equivalence class, and stuffed all elements that were equal into the same class. It then needed to check:

• If there is one constant term in the class, then all the terms in the class must be equal to that constant
• If there are multiple distinct constant terms in the class, then the problem is unsolvable

It did so by imposing an order on simple terms such that Cte false < everything < Cte true, and then checking only for the minimum and maximum elements of the set rather than iterating over all possible elements of the set. This only works because there are exactly two possible constants (false and true).

The new solver that uses Tarjan's union-find introduced in #856 does not have such a limitation. Instead, the solver always selects constants as the roots of their equivalence classes, and fails if we ever try to merge two equivalence classes with distinct constant roots, which works with an arbitrary number of possible constants.

[bclement-ocp]

Note: I want to do a sanity performance check before merging, which is currently blocked by #954

[Halbaroth]

Is it ok?

[bclement-ocp]

Benches are running.

[bclement-ocp]

This is +5-0 on QF_BV with around 3% speedup, merging.

(I did not run benches on BV with quantifiers)