Download FaCiLe - La Recherche

2.2 Variables
11
Attribute
A FaCiLe variable can be regarded as either in one of the following two states:
• uninstantiated or unbound, such that an “attribute” containing the current domain (of size
strictly greater than one) is attached to the variable;
• instantiated or bound, such that merely an integer is attached to the variable.
So an unbound variable is associated with an attribute of type Var.Attr.t holding its current
domain, its string name, a unique integer identifier and various internal data irrelevant to the
end-user. Functions to access attributes data are gathered in module Var.Attr:
• dom returns the current domain of an attribute;
• the mapping of fprint, min, max, size, member of module Domain applied on the embedded
domain of an attribute (e.g. min a is equivalent to Domain.min (dom a));
• id to get the identifier of an attribute;
• constraints_number returns the number of “active” constraints still attached to a variable.
Although variables are of abstract type Fd.t, function Fd.value v returns a concrete view of type
Var.concrete_fd = Unk of Attr.t | Val of int 1 of a variable v, so that a control structure
that depends on the instantiation of a variable will typically look like:
match Fd.value v with
Val n -> f_bound n
| Unk attr -> f_unbound attr
An alternative boolean function Fd.is_var returns the current state of a variable, sparing the
“match” construct.
#let v1 = Fd.create (Domain.create [1]) (* equivalent to Fd.int 1 *);;
val v1 : Facile.Var.Fd.t = <abstr>
#Fd.is_var v1;;
- : bool = false
#Fd.fprint stdout v1;;
1- : unit = ()
Domain Reduction
Module Fd provides two functions to perform backtrackable domain reductions on variables, typically used within instantiation goals and filtering of user-defined constraints:
• unify v n instantiates variable v to integer n or fails whenever n does not belong to the
domain of v. unify may be called on instantiated variables.
#let vr = Fd.interval 2 6;;
val vr : Facile.Var.Fd.t = <abstr>
#Fd.unify vr 7;;
Uncaught exception: Fcl_stak.Fail("Var.Fd.subst").
#Fd.unify vr 5;;
- : unit = ()
1 Type Var.concrete fd constructors Unk and Val stand respectively for “Unknown” (unbound) and “Value”
(bound).