module Cstr: sig
.. end
Posting Constraints and Building New Ones
This module defines the type t
of constraints and functions to create
and post constraints: mainly a create
function which allows to build new
constraints from scratch (this function is not needed when using
standard FaCiLe predefined constraints) and the mostly useful post
function which must be called to actually add a constraint to the
constraint store.
exception DontKnow
Exception raised by the check
function of a reified constraint when it
is not known whether the constraint is satisfied or violated.
type
priority
Type of waking priority.
val immediate : priority
val normal : priority
val later : priority
Available priorities:
- immediate: as soon as possible, for quick updates;
- normal: standard priority;
- later: for time consuming constraints (e.g.
Gcc.cstr
, Alldiff.cstr
...).
type
t
The type of constraints.
val create : ?name:string ->
?nb_wakings:int ->
?fprint:(Pervasives.out_channel -> unit) ->
?priority:priority ->
?init:(unit -> unit) ->
?check:(unit -> bool) ->
?not:(unit -> t) -> (int -> bool) -> (t -> unit) -> t
create ?name ?nb_wakings ?fprint ?priority ?init ?check ?not update delay
builds a new constraint:
-
name
is a describing string for the constraint. Default value
is "anonymous"
.
-
nb_wakings
is the number of calls to Var.delay
with distinct
"waking_id
" arguments within the
constraint own delay
function (see below). Default value is 1
.
Beware that if nb_wakings
is greater than 1 and the optional init
argument is not provided, init
default behaviour is to do nothing
(i.e. the update
function will not be called).
-
fprint
should print the constraint on an output channel taken as
its only argument. Default value is to print the name
string.
-
priority
is either immediate
, normal
or later
. Time costly
constraints should be waken after quick ones. Default value is normal
.
-
init
is useful to perform initialization of auxiliary data
structures needed and maintained by the update
function.
init ()
is called as soon as the constraint is posted. Default
value is to call (update 0)
if nb_wakings
is equal to 1 to
perform an initial propagation; if nb_wakings
is greater than 1,
default value is fun () -> ()
, i.e. it does nothing. Hence, an
init
argument must be provided if this is not the desired
behaviour.
-
check
must be specified if the constraint is to be reifiable
(as well as the not
function). When the constraint is reified,
check ()
is called to verify whether the constraint is satisfied
or violated, i.e. the constraint itself or its negation is entailed
by the constraint store. It should return true
if the constraint
is satisfied, false
if it is violated and raise DontKnow
when
it is not known. check
must not change the domains of the
variables involved in the constraint.
Default: Failure
exception is raised.
-
not
must be specified if the constraint is reifiable (as well
as check
). not ()
should return a constraint which is the
negation of the constraint being defined. When the constraint is
reified, it is called to post the negation of the constraint whenever
check ()
return false
, i.e. the negation is entailed by the
constraint store. Default: Failure
exception is raised.
-
update
is a mandatory argument which propagates the constraint,
i.e. filters domains and checks consistency. This function takes an
integer as its unique parameter, according to the optional
waking_id
argument given to the Var.delay
calls featured in the
constraint own delay
function (see below). When a waking event
occurs, this function is called with the corresponding integer
"waking_id
", and must return true
when the constraint is
(partially) satisfied for this event, false
if further
propagations have to be performed, and raise Stak.Fail
whenever an inconsistency is detected. The whole
constraint is solved when update 0
, ..., update (nb_wakings-1)
have all returned true
. E.g. a global constraint on an array
of variables can be aware of which variable has triggered the
awakening by providing the integer index of the variable as its
"waking_id
" to the Var.delay
function. update
is called with
0
by default when the nb_wakings
argument has been omitted; in
this case, the constraint is solved as soon as update
returns true
.
-
delay
schedules the awakening of the constraint ct
(which is
taken as its unique argument), i.e. the execution of its update
function. If update id
should be called (because it may propagates)
when one of the events contained in the events
list es
occurred
on variable v
, then Var.delay es v ~waking_id:id ct
should be called
within the body of the delay
function. Beware that
all the "waking_id
s" must be contiguous integers ranging from
0
to nb_wakings-1
, otherwise the behaviour is unspecified.
delay
is a mandatory argument.
val post : t -> unit
post c
posts the constraint c
to the constraint store.
val one : t
val zero : t
The constraint which succeeds (resp. fails) immediately.
val id : t -> int
id c
returns a unique integer identifying the constraint c
.
val name : t -> string
name c
returns the name of the constraint c
.
val priority : t -> priority
priority c
returns the priority of the constraint c
.
val fprint : Pervasives.out_channel -> t -> unit
fprint chan c
prints the constraint c
on channel chan
. Calls
the fprint
function passed to create
.
val is_solved : t -> bool
is_solved c
returns true
if c
is satisfied and false
otherwise.
val active_store : unit -> t list
active_store ()
returns the list of all active constraints, i.e. whose
update
functions have returned false
.
val not : t -> t
not c
returns the negation of c
.