Module Equality.Set

module Set: sig .. end
Sets of equalities.

include Datatype.S

The set operators are redefined so that equalities involving a same term are joined: ∀ e₁, e₂ ∈ Set, e₁ ≠ e₂ ⇔ e₁ ∩ e₂ = ∅
val empty : t
val is_empty : t -> bool
val union : t -> t -> t
val inter : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (Equality.equality -> unit) -> t -> unit
val fold : (Equality.equality -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (Equality.equality -> bool) -> t -> bool
val exists : (Equality.equality -> bool) -> t -> bool
val elements : t -> Equality.equality list
val choose : t -> Equality.equality
val remove : Hcexprs.kill_type -> Cil_types.lval -> t -> t
remove lval set remove any expression e such that lval belongs to syntactic_lval e from the set of equalities set.
val unite : Equality.elt * Hcexprs.lvalues -> Equality.elt * Hcexprs.lvalues -> t -> t
unite (a, a_set) (b, b_set) map unites a and b in map. a_set must be equal to syntactic_lval a, and b_set to syntactic_lval b.
val find : Equality.elt -> t -> Equality.equality
find elt set return the (single) equality involving elt that belongs to set, or raise Not_found if no such equality exists.
val find_option : Equality.elt -> t -> Equality.equality option
Same as find, but return None in the last case.
val mem : Equality.equality -> t -> bool
mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq
val contains : Equality.elt -> t -> bool
contains elt set = true iff elt belongs to an equality of set.
val deep_fold : (Equality.equality -> Equality.elt -> 'a -> 'a) -> t -> 'a -> 'a
val cardinal : t -> int
val lvalues_only_left : t -> t -> Equality.elt Equality.tree