feat(UF): Store domains inside the union-find

[bclement-ocp]

This patch adds the ability to store domains (as used in the bit-vector, enum and ADT theories) directly in the union-find structure, which is responsible for updating them automatically as class representatives are updated.

The advantages of doing this are twofold: we no longer need to manually keep track of substitutions (avoiding the issue that some of them are not propagated from the union-find to the relations), and having the domains stored in a central place rather than inside each relations module opens the path to more communication between the domains (e.g. accessing integer domains from the bit-vector module).

Note that constraints (notably for the bit-vector theory) are not integrated into the union-find and still need to be kept track of manually.

[bclement-ocp]

After the usual 5.0 cross-check, this PR is +0-2 on ae-format (but the -2 seems spurious/weak-table-related; at least they don't reproduce on my machine) and +0-17 on the QF_BV subset. The regressions on the QF_BV subset seem to be related to changes in the way the splits are performed; they disappear when increasing the --max-split limit or when using --enable-sat-cs (with #1118 applied). I think we can treat these as a particular case of #1120, as also discussed in #1027.