Previous Contents Next

Chapter 4   Modules

The following sections are extracted from .mli module interfaces of FaCiLe and sorted by alphabetic order. A comprehensive index of these sections can be found at the end of this document.

4.1   Module Alldiff: the "All Different" Constraint

type algo = Lazy | Bin_matching of Var.Attr.event
val cstr : ?algo:algo -> Var.Fd.t array -> Cstr.t
alldiff (?algo:Lazy) vars States that variables of vars are different from each other. The optional argument algo specifies the level of propagation. Lazy: waits for instantiation and removes from other domains. Bin_matching c: waits for event c (e.g. Var.Attr.on_refine) and uses a bin matching algorithm to ensure the constraint is consistent. algo default value is Lazy. Not reifiable.

4.2   Module Arith: Arithmetic Expressions over Variables of Type Var.Fd.t

Overview

This module provides functions and operators to build arithmetic expressions and state (in/dis)equation constraints over them.

Basic

type t
Type of arithmetic expressions over variables of type Var.Fd.t and integers.
val fprint : out_channel -> t -> unit
fprint chan e prints expression e on channel chan.
val eval : t -> int
eval e returns the integer numerical value of a fully instantiated expression e. Raises Invalid_argument if e is not instantiated.
val min_of_expr : t -> int
val max_of_expr : t -> int
min_of_expr e (resp. max_of_expr e) returns the minimal (resp. maximal) possible value of expression e.

Conversion

val i2e : int -> t
i2e n returns an expression which evaluates to n.
val fd2e : Var.Fd.t -> t
fd2e v returns an expression which evaluates to n when v is instantiated and Var.Fd.value v evaluates to Val n.
val e2fd : t -> Var.Fd.t
e2fd e creates and returns a new variable v and posts the constraint fd2e v =~ e.

Construction of Arithmetic Expressions

The arithmetic operators check whether any integer overflow (i.e. the result of an arithmetic operation over integers is less than min_int or greater than max_int) occurs during constraints internal computations and raise an assert failure only when using the byte code library facile.cma.
val (+~) : t -> t -> t
val (-~) : t -> t -> t
val ( *~) : t -> t -> t
Addition, substraction, multiplication over expressions.
val ( **~) : t -> int -> t
Exponentiation of an expression to an integer value.
val (/~) : t -> t -> t
val (%~) : t -> t -> t
Division and modulo over expressions. The exception Division_by_zero is raised whenever the second argument evaluates to 0.
val abs : t -> t
Absolute value over expressions.
val sum : t array -> t
val sum_fd : Var.Fd.t array -> t
sum exps (resp. sum_fd vars) returns the sum of all the elements of an array of expressions (resp. variables). Returns Fd.int 0 if the array is empty.
val scalprod : int array -> t array -> t
val scalprod_fd : int array -> Var.Fd.t array -> t
scalprod coeffs exps (resp. scalprod_fd coeffs vars) returns the scalar product of an array of integers and an array of expressions (resp. variables). Raises Invalid_argument if the arrays have not the same length.
val prod : t array -> t
val prod_fd : Var.Fd.t array -> t
prod exps (resp. prod_fd vars) returns the product of all the elements of an array of expressions (resp. variables).

Arithmetic Constraints over Expressions

val (<~)  : t -> t -> Cstr.t
val (<=~) : t -> t -> Cstr.t
val (=~)  : t -> t -> Cstr.t
val (>=~) : t -> t -> Cstr.t
val (>~)  : t -> t -> Cstr.t
val (<>~)  : t -> t -> Cstr.t
Constraints strictly less, less or equal, equal, greater or equal, strictly greater and different over expressions.

Reification

Reification of the arithmetic constraint which is replaced by an expression equal to a boolean variable instantiated to 1 if the constraint is satisfied and to 0 if it is violated. These operators are shortcuts to lighten the writing of reified expressions:
e1 op~~ e2 is equivalent to fd2e (Reify.boolean (e1 op~ e2)).
val (<~~)  : t -> t -> t
val (<=~~) : t -> t -> t
val (=~~)  : t -> t -> t
val (>=~~) : t -> t -> t
val (>~~)  : t -> t -> t
val (<>~~)  : t -> t -> t
Reified strictly less, less or equal, equal, greater or equal, strictly greater and different.

4.3   Module Cstr: Posting Constraints and Building New Ones

Overview

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 effectively add a constraint to the constraint store.

Basic

exception DontKnow
Exception raised by the check function of a constraint (of type t) when it is not known whether the constraint is satisfied or violated.
type priority
Waking priority.
val immediate : priority
As soon as possible, for quick updates.
val normal : priority
Standard priority.
val later : priority
For time consuming constraints (e.g. Gcc.cstr, Alldiff.cstr, ...).

type t
The type of constraints.
val create : ?name:string -> ?fprint:(out_channel -> unit) -> ?priority:prio
rity -> ?init:(unit -> unit) -> ?check:(unit -> bool) -> ?not:(unit -> t) ->
 (unit -> bool) -> (t -> unit) -> t
create ?name ?fprint ?priority ?init ?check ?not update delay builds a new constraint.

- name is a describing string name of the constraint. Default value is "anonymous".

- fprint (pretty-)printing of 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 fun () -> ().

- check must be specified if the constraint is reifiable (as well as not). 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, and 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 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. it is entailed by the constraint store. Default: Failure exception raised.

- update computes the domain reductions of the constraint. update () should return true when the constraint becomes solved, false if it is not yet entailed by the constraint store and raise Stak.Fail whenever a failure occurs. update is a mandatory argument.

- delay schedules the awakening of the constraint ct (which is taken as its only argument), i.e. the execution of its update function. If update () should be called (because it may reduce variables domains) when one of the events contained in the events list es occurred on variable v, then Var.delay es v ct should be called within the body of the delay function. 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.

Access

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 fprint : out_channel -> t -> unit
fprint chan c prints the constraint c on channel chan. Calls the fprint function passed to create.
val active_store : unit -> t list
active_store () returns the list of all active constraints, i.e. whose update functions have returned false.

4.4   Module Domain: Domain Operations

This module provides all necessary functions (and more) to create and handle domains, which are needed to create variables and perform propagation (i.e. domain reduction or filtering).
type t
Type of finite domains of integers (functional: no in place modifications, domains can be shared). Standard equality and comparison can be used on type domain.

Building New Domains

val empty : t
The empty domain.
val create : int list -> t
create l builds a new domain containing the values of l. Removes duplicates and sorts values. Returns empty if l is empty.
val unsafe_create : int list -> t
unsafe_create l builds a new domain containing the values of l. l must be sorted and must not contain duplicate values, otherwise behaviour is unspecified. Returns empty if l is empty. It is a more efficient variant of create.
val interval : int -> int -> t
interval inf sup returns the domain of all integers in the closed interval [inf..sup]. Raise Invalid_argument if inf > sup.
val int : t
The largest representable domain, handy to create variables for which bounds cannot be previously known. It is actually much smaller than interval min_int max_int (which really is the biggest one) to help to avoid overflows while computing bounds of expressions involving such variables.
val boolean : t
The domain containing 0 and 1.

Access

val is_empty : t -> bool
is_empty d tests if the domain d is empty.
val size : t -> int
size d returns the number of integers in d.
val min : t -> int
val max : t -> int
min d (resp. max d) returns the lower (resp. upper) bound of d. If d is empty, the behaviour is unspecified (incorrect return value or exception raised).
val min_max : t -> int * int
min_max d returns both the lower and upper bound of d. If d is empty, the behaviour is unspecified (incorrect return value or exception raised).
val iter : (int -> unit) -> t -> unit
iter f d successively applies function f to all element of d in increasing order.
val interval_iter : (int -> int -> unit) -> t -> unit
interval_iter f d successively applies function f to the bounds of all the disjoint intervals of d in increasing order. E.g. a suitable function to print a domain can be fun mini maxi -> Printf.printf "%d..%d " mini maxi.
val member : int -> t -> bool
member n d tests if n belongs to d.
val values : t -> int list
value d returns the list of values of the domain d
val fprint : out_channel -> t -> unit
fprint chan d prints d on channel chan.
val sprint : t -> string
sprint d returns a string representation of d.
val included : t -> t -> bool
included d1 d2 tests if domain d1 is included in domain d2.
val smallest_geq : t -> int -> int
val greatest_leq : t -> int -> int
smallest_geq dom val (resp. greatest_leq dom val) returns the smallest (resp. greatest) value in dom greater (resp. smaller) than or equal to val. Raises Not_found if max dom < val (resp. min dom > val).
val choose : (int -> int -> bool) -> t -> int
choose ord d returns the mininum value of d for order ord. Raises Not_found if d is empty.

Operations

val remove : int -> t -> t
remove n d returns d-n. Returns d if n is not in d.
val add : int -> t -> t
add n d returns d+n.
val remove_up : int -> t -> t
val remove_low : int -> t -> t
remove_up n d (resp. remove_low n d) returns d-[n+1..max_int] (resp. d-[min_int..n-1]), i.e. removes values stricly greater (resp. less) than n.
val remove_closed_inter : int -> int -> t -> t
remove_closed_inter inf sup d returns d-[inf..sup], i.e. removes values greater than or equal to inf and less or equal to sup in d. Returns d if inf > sup.
val intersection : t -> t -> t
val union : t -> t -> t
Intersection (resp. union) over domains.
val difference : t -> t -> t
difference big small returns big-small. small must be included in big, otherwise the behaviour is unspecified (incorrect return value or exception raised).
val remove_min : t -> t
val remove_max : t -> t
remove_min d (resp. remove_max d) returns d without its lower (resp. upper) bound. Raises Invalid_argument if d is empty.
val minus : t -> t
minus d returns the domain of opposite values of d.
val plus : t -> int -> t
plus d n translates a domain by n.

4.5   Module FdArray: Constraints over Arrays of Variables

val min : Var.Fd.t array -> Var.Fd.t
val max : Var.Fd.t array -> Var.Fd.t
min vars (resp. max vars) returns a variable constrained to be equal to the variable that will be instantiated to the minimal (resp. maximal) value among all the variables in the array vars. Raises Invalid_argument if vars is empty. Not reifiable.
val min_cstr : Var.Fd.t array -> Var.Fd.t -> Cstr.t
val max_cstr : Var.Fd.t array -> Var.Fd.t -> Cstr.t
min_cstr vars mini (resp. max_cstr vars maxi) returns the constraint fd2e (min vars) =~ fd2e mini (resp. fd2e (max vars) =~ fd2e maxi). Raises Invalid_argument if vars is empty. Not reifiable.
val get : Var.Fd.t array ->  Var.Fd.t -> Var.Fd.t
get vars index returns a variable constrained to be equal to vars.(index). Variable index is constrained within the range of the valid indices of the array (0..Array.length vars - 1). Raises Invalid_argument if vars is empty. Not reifiable.
val get_cstr : Var.Fd.t array -> Var.Fd.t -> Var.Fd.t -> Cstr.t
get_cstr vars index v returns the constraint fd2e vars.(index) =~ fd2e v. Variable index is constrained within the range of the valid indices of the array (0..Array.length vars - 1). Raises Invalid_argument if vars is empty. Not reifiable.

4.6   Module Gcc: Global Cardinality Constraint (a.k.a. Distribute)

type level = Basic | Medium | High
val cstr : ?level:level -> Var.Fd.t array -> (Var.Fd.t * int) array -> Cstr.
t
cstr (?level:High) vars distribution returns a constraint ensuring that for each pair (c,v) of cardinal variable c and integer value v in the list distribution, c variables in the array vars will be instantiated to v, i.e. card{vi = v | vi in vars} = c. All values v in distribution must be different otherwise the exception Invalid_argument is raised. Three levels of propagation are provided : Basic is the quickest, High performs the highest amount of propagation. level default value is High. The constraint posts the redundant constraint stating that the sum of the cardinals is equal to the number of variables. Not reifiable.

4.7   Module Goals: Building and Solving Goals

Overview

This module provides functions and operators to build goals that will control the search, i.e. mainly choose and instantiate variables.
type t
The type of goals.

Creation and Solving

val fail : t
val success : t
Failure (resp. success). Neutral element for the disjunction (resp. conjunction) over goals. Could be implemented as create (fun () -> Stak.fail "fail") (resp. create (fun () -> ())).
val atomic : ?name:string -> (unit -> unit) -> t
atomic (?name:"atomic") f returns a goal calling function f. f must take () as argument and return (). name default value is "atomic".
val create : ?name:string -> ('a -> t) -> 'a -> t
create (?name:"create") f a returns a goal calling f a. f should return a goal (success to stop). name default value is "create".
val create_rec : ?name:string -> (t -> t) -> t
create_rec (?name:"create_rec") f returns a goal calling f. f takes itself as argument and should return a goal (success to stop). Useful to write recursive goals. name default value is "create_rec".
val solve : ?control:(int -> unit) -> t -> bool
solve ?control g solves the goal g and returns a success (true) or a failure (false). The execution can be precisely controlled with the control argument whose single argument is the number of bactracks since the beginning of the search. This function is called after every local failure:

- it can raise Stak.Fail to force a failure of the search in the current branch (i.e. backtrack);

- it can raise any other user exception to stop the search process;

- it must return unit to continue the search; this is the default behavior.

Operators

val (&&~) : t -> t -> t
val (||~) : t -> t -> t
Conjunction and disjunction over goals. Note that these two operators do have the SAME PRIORITY. Goals expressions must therefore be carefully parenthesized to produce the expected result.
val forto : int -> int -> (int -> t) -> t
val fordownto : int -> int -> (int -> t) -> t
forto min max g (resp. fordownto min max g) returns the conjunctive iteration of goal g on increasing (resp. decreasing) integers from min (resp. max) to max (resp. min).
val once : t -> t
once g cuts choice points left on goal g.
val sigma : ?domain:Domain.t -> (Var.Fd.t -> t) -> t
sigma ?domain fgoal creates the goal (fgoal v) where v is a new variable of domain domain. Default domain is the largest one. It can be considered as an existential quantification, hence the concrete notation sigma of this function (because existential quantification can be seen as a generalized disjunction).

Instantiation

val unify : Var.Fd.t -> int -> t
unify var x instantiates variable var to x.
val indomain : Var.Fd.t -> t
Non-deterministic instanciation of a variable, by labeling its domain (in increasing order).
val instantiate : (Domain.t -> int) -> Var.Fd.t -> t
instantiate choose var Non-deterministic instanciation of a variable, by labeling its domain using the value returned by the choose function.
val dichotomic : Var.Fd.t -> t
Non-deterministic instanciation of a variable, by dichotomic recursive exploration of its domain.

Goal Operations on Array of Variables

module Array : sig
val foralli : ?select:('a array -> int) -> (int -> 'a -> t) -> 'a array -> t
foralli ?select g a returns the conjunctive iteration of goal g where order is computed by the heuristic ?select which must raise Not_found to terminate, i.e. g is successively applied to select a and a.(select a). Default heuristic is increasing order over indices.
val forall : ?select:('a array -> int) -> ('a -> t) -> 'a array -> t
forall ?select g a defined by foralli ?select (fun _i x -> g x) a.
val existsi : ?select:('a array -> int) -> (int -> 'a -> t) -> 'a array -> t
existsi ?select g a returns the disjunctive iteration of goal g where order is computed by the heuristic ?select which must raise Not_found to terminate, i.e. g is successively applied to select a and a.(select a). Default heuristic is increasing order over indices.
val exists : ?select:('a array -> int) -> ('a -> t) -> 'a array -> t
exists ?select g a defined by existsi ?select (fun _i x -> g x) a.
val choose_index : (Var.Attr.t -> Var.Attr.t -> bool) -> Var.Fd.t array -> i
nt
choose_index order fds returns the index of the best (minimun) free (not instantiated) variable in the array fds for the criterion order. Raises Not_found if all variables are bound (instantiated).
val not_instantiated_fd : Var.Fd.t array -> int
not_instantiated_fd fds returns the index of one element in fds which is not instantiated. Raises Not_found if all variables in array fds are bound.
val labeling: Var.Fd.t array -> t
Standard labeling defined by forall indomain.
end

Goal Operations on List of Variables

module List : sig
val forall : ?select:('a list -> 'a * 'a list) -> ('a -> t) -> 'a list -> t
forall ?select g [x1;x2;...;xn] is g x1 &&~ g x2 &&~ ... &&~ g xn, i.e. returns the conjunctive iteration of goal g on list a.
val exists : ?select:('a list -> 'a * 'a list) -> ('a -> t) -> 'a list -> t
exists ?select g [x1;x2;...;xn] is g x1 ||~ g x2 ||~ ... ||~ g xn, i.e. returns the disjunctive iteration of goal g on list a.
val member : Var.Fd.t -> int list -> t
member v l returns the disjunctive iteration of the instantiation of the variable v to the values in the integer list l. Defined by fun v l -> exists (fun x -> create (fun () -> Fd.unify v x)) l.
val labeling: Var.Fd.t list -> t
Standard labeling defined by forall indomain.
end

Optimization

type bb_mode = Restart | Continue
Branch and bound mode.
val minimize : ?step:int -> ?mode:bb_mode -> t -> Var.Fd.t -> (int -> unit) 
-> t
minimize ?step ?mode goal cost solution runs a Branch and Bound algorithm on goal for bound cost, with an improvement of at least step between each solution found. With mode equal to Restart, the search restarts from the beginning for every step whereas with mode Continue (default) the search simply carries on with an update of the cost constraint. solution is called with the instantiation value of cost (which must be instantiated by goal) as argument each time a solution is found; this function can therefore be used to store (e.g. in a reference) the current solution. Default step is 1. minimize always FAILS.

4.8   Module Interval: Variable Membership of an Interval

val is_member : Var.Fd.t -> int -> int -> Var.Fd.t
is_member v inf sup returns the boolean variable instantiated to 1 if v is in inf..sup and to 0 otherwise.
val cstr : Var.Fd.t -> int -> int -> Var.Fd.t -> Cstr.t
cstr v inf sup b returns the constraint ensuring that the boolean variable b is instantiated to 1 if v is in inf..sup and to 0 otherwise. Not reifiable.

4.9   Module Reify: Constraints Reification

All the reification functions and operators only work on REIFIABLE constraints, i.e. constraints which have a check function AND a not function (or built-in constraints for which the documentation does not mention "Not reifiable"). Otherwise a Failure ("fatal error") exception is raised.
val boolean : ?delay_on_negation:bool -> Cstr.t -> Var.Fd.t
boolean (?delay_on_negation:true) c returns a boolean (0..1) variable associated to the constraint c. The constraint is verified iff the boolean is equal to 1. The waking conditions of the contraint relating c and the boolean are the ones set by the delay function of c (set by the delay argument of Cstr.create). If the optional argument delay_on_negation is set to true, the new constraint is also attached to the events of the negation of c (i.e. the constraint returned by the not function of c), otherwise it is not. delay_on_negation default value is true.
val cstr : ?delay_on_negation:bool -> Cstr.t -> Var.Fd.t -> Cstr.t
cstr delay_on_negation c b is equivalent to the constraint boolean ?delay_on_negation c =~ b. delay_on_negation default value is true.

Operators

val (&&~~) : Cstr.t -> Cstr.t -> Cstr.t
val (||~~) : Cstr.t -> Cstr.t -> Cstr.t
val (=>~~) : Cstr.t -> Cstr.t -> Cstr.t
val (<=>~~) : Cstr.t -> Cstr.t -> Cstr.t
val xor : Cstr.t -> Cstr.t -> Cstr.t
val not : Cstr.t -> Cstr.t
Logical reification operators on constraints, namely and, or, implies, equivalent, exclusive or, not.

4.10   Module Sorting: Sorting Constraint

val sort : Var.Fd.t array -> Var.Fd.t array
sort a returns an array of variables constrained to be the variables in a sorted in increasing order.
val sortp : Var.Fd.t array -> Var.Fd.t array * Var.Fd.t array
sortp a same as sort but returns a couple (sorted, perm) where sorted is the array of sorted variables and perm is an array of variables constrained to be the permutation between a and sorted, i.e. a.(i) = sorted.(perm.(i)).
val cstr : Var.Fd.t array -> ?p:Var.Fd.t array option -> Var.Fd.t array -> C
str.t
cstr a (?perm:None) sorted returns the constraint ensuring that sorted is the result of sorting array a according to the permutation perm. perm default value is None, meaning the argument is irrelevant. Raises Invalid_argument if arrays have incompatible length. Not reifiable.

4.11   Module Stak: Global Stack of Goals, Backtrackable Operations

This module provides functions to control the execution of the goal stack, as well as backtrackable references. Nota: the module name Stak lacks a 'c' because of a possible clash with the Ocaml standard library module Stack.
type level
Type of a level in the stack.
val older : level -> level -> bool
older l1 l2 true if level l1 precedes l2.
exception Level_not_found of level
Raised by cut and cut_bottom.
val size : unit -> int
Size of the stack.
val level : unit -> level
Returns the current level.
val cut : level -> unit
cut l cuts the choice points left on the stack until level l. Raise Level_not_found if level is not reached and stack is empty.
type 'a ref
Backtrackable reference of type 'a.
val ref : 'a -> 'a ref
Returns a reference which modification will be trailed during the solving of a goal.
val set : 'a ref -> 'a -> unit
Sets a reference.
val get : 'a ref -> 'a
Dereference.
val incr : int ref -> unit
val decr : int ref -> unit
Increments (resp. decrements) a reference.

Control of Failure

exception Fail of string
Raised during solving whenever a failure occurs. The string argument is informative.
val fail : string -> 'a
fail x equivalent to raise (Fail x).

4.12   Module Var: Constrained, Attributed, Finite Domain Variables

The Attribute of a Domain Variable

module Attr : sig
type t
Type of attributes.
val dom : t -> Domain.t
dom a returns the integer domain of an attribute.
type event
Type of events (modifications on variables) on which to suspend a constraint.
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 fprint : out_channel -> t -> unit
fprint chan a prints attribute a on channel chan.
val size : t -> int
size a returns the number of integer values in the domain associated with a (i.e. dom a).
val min : t -> int
val max : t -> int
min a (resp. max a) returns the lower (resp. upper) bound of a.
val values : t -> int list
values a returns the list of all integers in dom a.
val iter : (int -> unit) -> t -> unit
iter f a iterates f on each integer in dom a.
val member : t -> int -> bool
member a n tests if n belongs to dom a.
val id : t -> int
id a returns a unique integer identifying the attribute a.
val constraints_number : t -> int
constraints_number a returns the number of different constraints attached to a.
end

A Domain Variable

type concrete_fd = Unk of Attr.t | Val of int
Type of the value of a Fd variable.
module Fd : sig
Finite domain variable
type t
Type of Fd variable.

Creation

val create : ?name:string -> Domain.t -> 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 -> int -> int -> 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 -> int -> int -> 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 int : int -> 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 value : t -> concrete_fd
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 size : t -> int
size v returns the number of integer values in the domain of v (1 if v is instantiated.
val min : t -> int
min v returns the lower bound of v.
val max : t -> int
max v returns the upper bound of v.
val min_max : t -> int * int
min_max v returns both the lower and upper bounds of v.
val int_value : t -> int
int_value v returns the value of v if it is instantiated and raises a Failure exception otherwise.
val values : t -> int list
values v returns the list of all integers in the domain of v. If v is instantiated to n, returns the singleton list containing n.
val iter : (int -> unit) -> t -> unit
iter f v iterates f on each integer in the domain of v.
val member : t -> int -> 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 then attributed to 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 : out_channel -> t -> unit
fprint chan v prints variable v on channel chan.
val fprint_array : out_channel -> t array -> unit
fprint_array chan vs prints array of variables vs on channel chan.

Reduction

val unify : t -> int -> unit
unify v n instantiates variable v with integer value n. Raises Stak.Fail in case of failure. unify may be called either on unbound variables or on instantiated variables.
val refine : t -> Domain.t -> 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).
end
val delay : Attr.event list -> Fd.t -> Cstr.t -> unit
delay event_list v c suspends constraint c on all the events in event_list occurring on v. No effect on instantiated variables. To be used within new constraints "delay" functions.

4.13   Module Easy

Easy is a module that the user is strongly recommended to open to facilitate access to FaCiLe (unless names clash with other open modules). It simply defines aliases to values and types of other modules: Note that the user of FaCiLe can extend this mechanism with its own ``Easier'' module aliasing any value or type of the library.


Previous Contents Next