Module UnionFind.Make

Parameters

Signature

type t
val compare : t -> t -> int
val equal : t -> t -> bool
val pp : pp_empty:(F.formatter -> unit) -> (F.formatter -> X.t -> unit) -> F.formatter -> t -> unit
type repr = private X.t
val empty : t
val union : t -> X.t -> X.t -> t * (X.t * repr) option

return the optional new equality added between the old representatives of the two items in the form of "old representative = new representative", None if they were already in the same congruence class

val find : t -> X.t -> repr

return the element given if it wasn't found in the relation

val fold_congruences : (trepr * XSet.t, 'acc) IStdlib.IStd.Container.fold

fold over the equivalence classes of the relation, singling out the representative for each class

val reorient : should_keep:(X.t -> bool) -> t -> X.t XMap.t

the relation x -> x' derived from the equality relation that relates all x, x' such that ¬(should_keep x), should_keep x', and x=x', as well as y -> y' when no element in the equivalence class of y satisfies should_keep and y' is the representative of the class

val apply_subst : _ XMap.t -> t -> t

apply_subst subst uf eliminate all variables in the domain of subst from uf, keeping the smallest representative not in the domain of subst for each class. Classes without any such elements are kept intact.

val filter_morphism : f:(X.t -> bool) -> t -> t

only keep items satisfying f, assuming that f is invariant under the relation, i.e. that if f x and x=y according to the relation then f y