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.

[Halbaroth]

Looks very good for me. I've very few remarks.

[Halbaroth]

Let's use Util.MI;)

[Halbaroth]

Suggested change

	val empty : Uf.t -> t * Uf.Domains.t
	val empty : Uf.t -> t * Uf.Domains.t
	(** [empty uf] creates a new environment for this relation theory and registers domains' identifiers in [uf]. The second value returned is used as an accumulator in [Relation.empty]. *)

[Halbaroth]

Suggested change

	(** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contains
	in the current domain of [r]. The representative [r] is marked [changed]
	(** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contained
	in the current domain of [r]. The representative [r] is marked [changed]

[Halbaroth]

Suggested change

	Uf.t -> (Shostak.Combine.r input) list ->
	t * Uf.Domains.t * Shostak.Combine.r result
	Uf.t -> (Shostak.Combine.r input) list ->
	t * Uf.Domains.t * Shostak.Combine.r result
	(** [assume env uf la] assumes the annotated literals [la] in the environment [env] and propagated these constraints in the domains of [uf]. The second value returned
	is an accumulator used in [Rel.assume]. *)

[Halbaroth]

global domain is confusing. This is a set of domains actually, not a domain. We may say set of domains of common identifier or common kind if we rename Id to Kind.

[bclement-ocp]

It is a domain (i.e. set of possible values) for the tuple comprising all of the currently defined variables (hence "global"). It so happens that all the implementations we currently have are represented as a product of per-variable ("local") domains, but I would rather not enshrine that fact in the documentation since one of the motivations is to use this API for the "delta" domain of Sharpening Constraint Programming approaches for Bit-Vector Theory.

I can clarify the documentation to mention that a global domain encodes a set of (correlated) values for multiples variables.

[Halbaroth]

I can clarify the documentation to mention that a global domain encodes a set of (correlated) values for multiples variables.

Yes, please ;)