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:
-
All the infix operators from Arith, Goals and Reify
- Frequently used mapping functions of Arith: i2e and fd2e
- Type of finite domain variables from Var: concrete_fd
- Module Fd from Var
Note that the user of FaCiLe can extend this mechanism with its own
``Easier'' module aliasing any value or type of the library.