Module type Fcl_var.BASICFD

module type BASICFD = sig .. end

Common variables module signature.


type t 

Type of finite domain variable.

type attr 

Type of attributes.

type domain 

Type of domains.

type elt 

Type of elements of domains.

type event 

Type of domain reduction events.

Creation

val create : ?name:string -> domain -> t

create ?name d returns a new variable with domain d. If provided, name will be used by the pretty printer.

val interval : ?name:string ->
elt -> elt -> t

interval ?name inf sup returns a new variable with domain [inf..sup]. If provided, name will be used by the pretty printer.

val array : ?name:string ->
int -> elt -> elt -> t array

array n inf sup returns an array of n new variables with domain [inf..sup]. If provided, name (suffixed with the index of the element) will be used by the pretty printer.

val elt : elt -> t

int n returns a new variable instantiated to integer value n.

Access

val is_var : t -> bool

is_var v returns true if v is not instantiated and false otherwise.

val is_bound : t -> bool

is_bound v returns true if v is instantiated and false otherwise.

val value : t ->
(attr, elt) Fcl_var.concrete

value v returns Val n if v is instantiated to n, Unk a otherwise where a is the attribute of v. Should always be used in a matching: match value v with Val n -> ... | Unk a -> ....

val min : t -> elt

min v returns the lower bound of v.

val max : t -> elt

max v returns the upper bound of v.

val min_max : t -> elt * elt

min_max v returns both the lower and upper bounds of v.

val elt_value : t -> elt

int_value v returns the value of v if it is instantiated and raises a Failure exception otherwise.

val int_value : t -> elt
val size : t -> int

size v returns the number of integer values in the domain of v (1 if v is instantiated).

val member : t -> elt -> bool

member v n returns true if n belongs to the domain of v and false otherwise.

val id : t -> int

id v returns a unique integer identifying the attribute associated with v. Must be called only on non ground variable, raise Failure otherwise.

val name : t -> string

name v returns the name of variable v (the empty string if it was not provided while created). Must be called only on non ground variable, raise Failure otherwise.

val compare : t -> t -> int

Compares two variables. Values (bound variables) are smaller than unknowns (unbound variables). Unknowns are sorted according to their attribute id.

val equal : t -> t -> bool

Tests if two variables are equal with respect to compare.

val fprint : Stdlib.out_channel -> t -> unit

fprint chan v prints variable v on channel chan.

val fprint_array : Stdlib.out_channel -> t array -> unit

fprint_array chan vs prints array of variables vs on channel chan.

Refinement

val unify : t -> elt -> unit

unify v n instantiates variable v with integer value n. Raises Fcl_stak.Fail in case of failure. unify may be called either on unbound variables or on instantiated variables.

val refine : t -> domain -> unit

refine v d reduces the domain of v with domain d. d must be included in the domain of v, otherwise the behaviour is unspecified (corrupted system or exception raised).

val refine_low : t -> elt -> unit

refine_low v inf reduces the domain of v by cutting all values strictly less than inf.

val refine_up : t -> elt -> unit

refine_up v sup reduces the domain of v by cutting all values strictly greater than sup.

val refine_low_up : t -> elt -> elt -> unit

refine_low_up v inf sup reduces the domain of v by cutting all values strictly less than inf and greater than sup. Robust even if v is already bound (checks that inf <= v <= sup, otherwise fails).

Events and suspending

val on_refine : event

Event occuring when a variable is changed, i.e. its domain modified.

val on_subst : event

Event occuring when a variable is instantiated.

val on_min : event
val on_max : event

Event occuring when the lower (resp. upper) bound of a variable decreases.

val delay : event list ->
t -> ?waking_id:int -> Fcl_cstr.t -> unit

delay event_list v ~waking_id:id c suspends constraint c on all the events in event_list occurring on v. An optional integer id may be associated to the wakening: it must be unique and range from 0 to nb_wakings-1, nb_wakings being the argument of Cstr.create specifying the number of calls to delay with distinct waking_id arguments. These integers are arguments to the "update" function of constraints and aim at discriminating waking events to fire the appropriate propagation rule. waking_id default value is 0. This function has no effect on instantiated variables (as no event could occur on a ground variable).