module Domain: sig
.. end
Domain Operations
This module provides functions to create
and handle domains, which are useful to build variables and perform
propagation (i.e. domain filtering).
type
elt = int
Type of element of domains (for generic interface,
).
type
t
Type of finite domains of integers (functional: no in-place
modifications, domains can be shared). Standard equality and
comparison can be used on domains.
val empty : t
The empty domain.
val create : elt list -> t
create l
builds a new domain containing the values of l
. Removes
duplicates and sorts values. Returns empty
if l
is
empty.
val unsafe_create : elt list -> t
unsafe_create l
builds a new domain containing the values of l
. l
must
be sorted and must not contain duplicate values, otherwise the behaviour is
unspecified. Returns empty
if l
is empty. It is a more efficient variant
of create
.
val interval : elt -> elt -> t
interval inf sup
returns the domain of all integers in the closed
interval [inf..sup]
. Raise Invalid_argument
if inf > sup
.
val int : t
The largest representable domain. Handy to create variables for which
bounds cannot be previously known. It is actually much smaller
than interval min_int max_int
(which really is the biggest one) to
try to prevent overflows while computing bounds of expressions
involving such variables.
val boolean : t
The domain containing 0
and 1
.
val is_empty : t -> bool
is_empty d
tests whether the domain d
is empty or not.
val size : t -> elt
size d
returns the number of integers in d
.
val min : t -> elt
val max : t -> elt
min d
(resp. max d
) returns the lower (resp. upper) bound of d
.
If d
is empty, the behaviour is unspecified (incorrect return value
or exception raised).
val min_max : t -> elt * elt
min_max d
returns both the lower and upper bound of d
. If d
is empty,
the behaviour is unspecified (incorrect return value or exception
raised).
val iter : (elt -> unit) -> t -> unit
iter f d
successively applies function f
to all element of d
in
increasing order.
val interval_iter : (elt -> elt -> unit) -> t -> unit
interval_iter f d
successively applies function f
to the bounds
of all the disjoint intervals of d
in increasing order. E.g. a
suitable function f
to print a domain can be defined as
fun mini maxi -> Printf.printf "%d..%d " mini maxi
.
val mem : elt -> t -> bool
val member : elt -> t -> bool
member n d
tests if n
belongs to d
.
val values : t -> elt list
value d
returns the list of values of the domain d
val fprint_elt : Pervasives.out_channel -> elt -> unit
val fprint : Pervasives.out_channel -> t -> unit
Pretty printing of elements and domains.
val sprint : t -> string
sprint d
returns a string representation of d
.
val included : t -> t -> bool
included d1 d2
tests whether domain d1
is included in domain d2
.
val smallest_geq : t -> elt -> elt
val greatest_leq : t -> elt -> elt
smallest_geq dom val
(resp. greatest_leq dom val
) returns the
smallest (resp. greatest) value in dom
greater (resp. smaller) than
or equal to val
. Raises Not_found
if max dom < val
(resp.
min dom > val
).
val largest_hole_around : t -> elt -> elt * elt
largest_hole_around dom val
returns the largest hole (interval)
in dom
centred around val
. Returns (val, val)
if val
belongs to dom
and raises Not_found
if val
is outside
dom
bounds. Equivalent to
(greatest_leq dom val, smallest_geq dom val)
but faster.
val choose : (elt -> elt -> bool) -> t -> elt
choose ord d
returns the mininum value of d
for order ord
.
Raises Not_found
if d
is empty.
val add : elt -> t -> t
add n d
returns d
{n}
.
val remove : elt -> t -> t
remove n d
returns d
{n}
. Returns d
if n
is not in d
.
val remove_up : elt -> t -> t
val remove_low : elt -> t -> t
remove_up n d
(resp. remove_low n d
) returns
d
[n+1..max_int]
(resp.
d
[min_int..n-1]
), i.e. removes values
stricly greater (resp. less) than n
.
val remove_low_up : elt -> elt -> t -> t
remove_low_up low up d
is a shortcut for
remove_up up (remove_low low d)
.
val remove_closed_inter : elt -> elt -> t -> t
remove_closed_inter inf sup d
returns
d
[inf..sup]
, i.e. removes
values greater than or equal to inf
and less or equal to sup
in d
.
Returns d
if inf > sup
.
val remove_min : t -> t
val remove_max : t -> t
remove_min d
(resp. remove_max d
) returns d
without its lower
(resp. upper) bound. Raises Invalid_argument
if d
is empty.
val intersection : t -> t -> t
val union : t -> t -> t
Intersection (resp. union) on domains.
val difference : t -> t -> t
difference big small
returns big
small
.
small
must be included in big
, otherwise the behaviour is
unspecified (incorrect return value or exception raised).
val diff : t -> t -> t
diff d1 d2
returns d1
d2
, i.e. domain of
elements in d1
which are not in d2
.
val minus : t -> t
minus d
returns the domain of opposite values of d
.
val plus : t -> elt -> t
plus d n
translates a domain by n
.
val times : t -> elt -> t
times d k
expands a domain by factor k
.
val compare : t -> t -> elt
compare d1 d2
is a comparison function working first on the cardinal,
then (if d1
and d2
have the same size) on the lexicographic order
of the domains (expressed in extension).
val compare_elt : elt -> elt -> elt
compare_elt e1 e2
is a comparison function on elements of domains.
Convenient to use the Domain
module as a functor argument as in
module Var
.
val disjoint : t -> t -> bool
disjoint d1 d2
tests whether d1
and d2
are disjoint.