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
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
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_ids" 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.