Module Fcl_cstr

module Fcl_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:(Stdlib.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 : Stdlib.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.