Module Cstr

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:
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:
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.