module SetDomain: sig
.. end
Integer Set Domain Operations
module S: sig
.. end
Implementation of sets of integers.
type
elt = S.t
Type of elements of set domains. They are sets themselves.
type
t
Type of finite domains of integer sets: a domain is a powerset lattice
of sets bounded by definite elements or glb (Greater Lower Bound) and
possible elements or lub (Lower Upper Bounds). The glb is a subset of
the lub. Note that the empty domain cannot be represented.
Creation
val elt_of_list : int list -> elt
Creates a set from a list of integers.
val interval : elt -> elt -> t
interval glb lub
builds the domain of sets greater than glb
and
smaller than lub
. An Invalid_argument
exception is raised if glb
is not a subset of lub
.
Access and Operations
val size : t -> int
size d
returns |glb(d)|-|lub(d)|+1, i.e. the height of the lattice,
not its number of elements.
val min : t -> elt
val max : t -> elt
val min_max : t -> elt * elt
Access to glb and lub.
val fprint_elt : Pervasives.out_channel -> elt -> unit
val fprint : Pervasives.out_channel -> t -> unit
Pretty printing of elements and domains.
val mem : elt -> t -> bool
mem x d
tests whether x
belongs to the domain d
.
val included : t -> t -> bool
included d1 d2
tests whether the domain d1
is included in d2
,
i.e. glb(d2
) included in glb(d1
) and lub(d1
) included in lub(d2
).
val iter : (elt -> 'a) -> t -> 'a
Iteration on values of the domain. Exponential with the size
of the domain.
val values : t -> elt list
Returns values of a domain. Exponential with the size
of the
domain.