feat(BV): Only store domains on variable parts

This patch changes the way that bit-vector domains are stored in order
to share domains between multiple bit-vectors with the same variable
part, including across different bit-width. Currently, if we had terms
[x], [00 @ x], and [10 @ x], we would store domains for each of these.
With this patch, we only store a domain for [x] and rebuild the domains
for [00 @ x] and [10 @ x] dynamically; we do this by computing normal
forms composed of a variable part ([x] here) and a constant offset
(either [0] or [10]).

This reduces the number of variables handled by the system (which is
important for global domains such as global difference) and reduces the
number of trivial propagations.

Note that this patch is not reverting #1044. In particular, we are
considering [x @ y] as a unique (composite) variable built up from the
atomic variables [x] and [y] (in the same way that the polynomial
[x + y] is built up from the monomial [x] and [y] in the
IntervalCalculus module; in fact, the implementation is intentionally
abstracted in order to be useable with polynomials). This is necessary
because, as noted in #1044, the interval domain for [x @ y] cannot be
built reconstructed precisely from the interval domains for [x] and [y].

The patch includes a bit of refactoring of the way we handle
constraints; notably, instead of aggressively substituting constraints,
we now store the original constraint and call [Uf.find] at propagation
time. This avoids having to define a substitution operation on normal
forms and allows storing the constraint dependencies directly inside the
domain (in the previous design, we could not do it easily without
repeating the expensive substitution of constraint arguments).

src/lib/reasoners/adt_rel.ml

@@ -191,7 +191,7 @@ module Domains = struct
       with Not_found ->
         Domain.unknown (X.type_info r)
 
-  let add r t =
+  let init r t =
     match Th.embed r with
     | Alien _ when not (MX.mem r t.domains) ->
       (* We have to add a default domain if the key `r` is not in map in order
@@ -236,7 +236,7 @@ module Domains = struct
       let t = remove r t in
       tighten nr nd t
 
-    | exception Not_found -> add nr t
+    | exception Not_found -> init nr t
 
   (* [propagate f a t] iterates on all the changed domains of [t] since the
      last call of [propagate]. The list of changed domains is flushed after
@@ -431,7 +431,7 @@ let add r uf domains =
   | Ty.Tadt _ ->
     Debug.add r;
     let rr, _ = Uf.find_r uf r in
-    Domains.add rr domains
+    Domains.init rr domains
   | _ ->
     domains