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