module E: sig end
Combination of individual equality sets.
type t
Combined equality set.
val u_of : t -> U.S.t
Projections to individual equality sets.
val la_of : t -> La.S.t
val nl_of : t -> Solution.Set.t
val p_of : t -> Solution.Set.t
val cop_of : t -> Solution.Set.t
val cl_of : t -> Solution.Set.t
val arr_of : t -> Solution.Set.t
val set_of : t -> Solution.Set.t
val empty : t
The empty equality configuration.
val copy : t -> t
val is_empty : t -> bool
Succeeds if all individual equality sets are empty.
val eq : t -> t -> bool
Identity test for two equality sets. Failure does
imply that the argument equality sets are not logically equivalent.
val pp : t Pretty.printer
Pretty-printing of combined equality set.
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
s |
: |
t
|
|
val pp_i : Th.t -> t Pretty.printer
Pretty-printing of an individual equality set.
| Parameters: |
|
i |
: |
Th.t
|
|
fmt |
: |
Format.formatter
|
|
s |
: |
t
|
|
val find : t * Partition.t -> Th.t -> Jst.Eqtrans.t
find s th x is a if x = a is in the solution set for theory th
in s; otherwise, the result is just x.
val inv : t * Partition.t -> Jst.Eqtrans.t
inv s a is x if there is x = a in the solution set for
theory th; otherwise Not_found is raised.
val dep : Th.t -> t -> Term.t -> Term.Var.Set.t
dep i s x returns a set ys of variables such that
y in ys iff there is an x = a in s with y a subterm of a.
val diff : t -> t -> t
diff s1 s2 returns the equality set s such that an equality e
is in s iff if it is in s1 but not in s2.