refactor(BV): Track domains for uninterpreted leaves only

[bclement-ocp]

This patch changes the internal representation of domains in the bitvector relations. Without the patch, we are keeping track of domains for all bit-vector terms, which is correct but wasteful. With the patch, we only track the domains of (currently) uninterpreted class representatives, and rebuild the domain associated with other terms on-the-fly before propagation.

This avoids carrying around huge domain maps with a potentially large amount of duplication, and allow to share propagations between terms that include identical sub-terms immediately without a round-trip through Uf (without the patch, if we learn that 0 @ x -> 01??, it does not immediately propagate that 1 @ x -> 11??; we first have to assert x<2,2> = 1 which gets solved into the substitution x |-> 1 @ x' and we only learn 11 @ x' -> 11?? when performing the substitution). On the other hand, it means that Domains.get and Domains.update are a bit more expensive now.

Since the Congruence is now only used for constraints, and not for domains, we only need to add the arguments of the constraints to the Congruence (which should also be a slight performance boost). Other changes to the use of the Congruence module are needed to fix the mismatch between what is stored in the Domains (whose keys are now uninterpreted terms) and the Constraints (the actual arguments of the constraints in the original problem). There is one exception: we now add the arguments of Distinct to the congruence, which is required for completeness because the terms that we generate during case splits are not guaranteed to already exist (in fact, in general they don't, since we create 1-bit extractions that have no reason to be in the original problem).

Note that there is also a small bugfix in Congruence: when performing a substitution we need to remove the old terms, otherwise we will forget dependencies if we ever add it back later.

Note: this is +13-4 on BV (benches are running on QF_BV); the regressions seem to be due to poor interaction with bv2nat which will be improved upon in the future.

[bclement-ocp]

This is +36-179 on QF_BV, which is less good. From a cursory look at the problems, this seems to be (counter-intuitively) due to an improvement: because we have better propagators (now actually complete on ground inputs) Alt-Ergo degrades into full backtracking while doing splitting! This is confirmed by checking that the regressions (at least the 3-4 random ones I selected) are solved by doing either --case-split-policy after-matching or --case-split-policy before-matching.

I have opened #1005; in the meantime, I think this PR can be reviewed independently.

[Halbaroth]

LGTM but we shouldn't merge before solving #1005.

[bclement-ocp]

Following the dev meeting: since this is still a net positive compared to last release we should merge in spite of #1005 (partially because we want to merge #1010).