Module Fcl_setDomain

module Fcl_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 : Stdlib.out_channel -> elt -> unit

val fprint : Stdlib.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.