Chapter 3 Advanced Usage
3.1 Search Control
3.1.1 Basic Mechanisms
FaCiLe implements a standard depth-first search with backtracking.
OR control is handled with a stack (module Stak
), while AND
control is handled with continuations.
OR control can be modified with a cut à la Prolog: a level is
associated to each choice-point (node in the search tree) and
choice-points created since a specified level can be removed,
i.e. cut (functions Stak.level
and Stak.cut
).
OR and AND controls are implemented by the Goals.solve
function. AND is operationally mapped on the imperative sequence.
OR is based on the exception mechanism: backtrack is caused by the
exception Stak.fail
which is raised by failing constraints.
Note that this exception is caught and handled by the
Goals.solve
function only.
3.1.2 Combining Goals with Iterators
Functional programming allows the programmer to compose higher-order
functions using iterators. An iterator is associated to a
datatype and is the default control structure to process a value in
the datatype. There is a strong isomorphism between the datatypes and
the corresponding iterators and this isomorphism is a simple
guideline to use them.
Imitating the iterators of the standard OCaml library, FaCiLe
provides iterators for arrays and lists. While standard Array
and List modules allows to construct sequences (with a ';
')
of imperative functions (type 'a -> unit
), Goals.Array and
Goals.List modules of FaCiLe allows to construct conjunction
(with a &&~
) and disjunction (with a ||~
) of goals (type
Goals.t
).
The simplest iterator operates on integers and provides a standard
for-to loop by applying a goal to consecutive integers:
Goals.forto 3 7 g = (g 3) &&~ (g 4) &&~ ... &&~ (g 7)
Of course, iterators may be composed, as is illustrated below, where the
cartesian product [1..3] × [4..5] is deterministically enumerated:
let enum_couples =
Goals.forto 1 3
(fun i ->
Goals.forto 4 5
(fun j ->
Goals.atomic (fun () -> Printf.printf "%d-%d\\n" i j))) in
Goals.solve enum_couples;;
1-4
1-5
2-4
2-5
3-4
3-5
- : bool = true
Function Goals.atomic
(used in the previous example), which
builds an ``atomic'' goal (i.e. a goal which returns nothing), is
detailed in section 3.4.1.
Arrays: module Goals.Array
Standard Loop
The polymorphic Goals.Array.forall
function applies uniformally
a goal to every element of an array, connecting them with a
conjunction (&&~
).
Goals.Array.forall g [|e1; e2; ...; en|] = (g e1) &&~ (g e2) &&~ ... &&~ (g en)
Labeling of an array of variables is the iteration of the instantiation
of one variable (Goals.indomain):
let labeling_array = Goals.Array.forall Goals.indomain;;
val labeling_array : Facile.Var.Fd.t array -> Facile.Goals.t = <fun>
A matrix is an array of arrays; following the isomorphism, labeling of
a matrix must be simply a composition of the array iterator:
let labeling_matrix = Goals.Array.forall labeling_array;;
val labeling_matrix : Facile.Var.Fd.t array array -> Facile.Goals.t = <fun>
Changing the Order
An optional argument of Goals.Array.forall
, labelled
?select
, gives the user the possibility to choose the order in
which the elements are considered. ?select
is a function which is applied to the array by the iterator and which
must return the index of one element on which the goal is
applied. This function must raise the exception Not_found
to
stop the loop.
For example, if we want to apply the goal only on the unbound variables of
an array, we may write:
let first_unbound array =
let n = Array.length array in
let rec loop i = (* loop until free variable found *)
if i < n then
match Fd.value array.(i) with
Unk _ -> i
| Val _ -> loop (i+1)
else
raise Not_found in
loop 0;;
val first_unbound : Facile.Easy.Fd.t array -> int = <fun>
let forall_unbounds = Goals.Array.forall ~select:first_unbound;;
val forall_unbounds :
(Facile.Easy.Fd.t -> Facile.Goals.t) ->
Facile.Easy.Fd.t array -> Facile.Goals.t = <fun>
Note that the function forall
is polymorphic and can be used
for an array of any type.
The function Goals.Array.choose_index
facilitates the
construction of heuristic functions that may be provided to the forall
?select
argument. It constructs such a function from
an ordering function on variable attributes (free variables are
ignored). For example, the standard ``min size'' strategy will be
implemented as follows:
let min_size_order =
Goals.Array.choose_index (fun a1 a2 -> Var.Attr.size a1 < Var.Attr.size a2);;
val min_size_order : Facile.Var.Fd.t array -> int = <fun>
let min_size_strategy = Goals.Array.forall ~select:min_size_order;;
val min_size_strategy :
(Facile.Var.Fd.t -> Facile.Goals.t) ->
Facile.Var.Fd.t array -> Facile.Goals.t = <fun>
let min_size_labeling = min_size_strategy Goals.indomain;;
val min_size_labeling : Facile.Var.Fd.t array -> Facile.Goals.t = <fun>
Note that module Goals.Array
also provides a disjunctive
iterator, exists
, which has the same profile than
forall
. Variants Goals.Array.foralli
and
Goals.Array.existsi
allow to specify goals which take the
index of the relevant variable as an extra
argument (like the OCaml standard library iterator
Array.iteri
).
Lists: module Goals.List
FaCiLe Goals.List
module provides similar iterators for
lists except of course iterators which involve index of elements.
3.2 Constraints Control
Constraints may be seen operationally as ``reactive objects''. They
are attached to variables, more precisely to events related to
variable modifications. A constraint is mainly a function (the update function) which is called when the constraint is woken.
The update function usually performs a propagation using the event,
i.e. the modification of the domain of one variable, to process new
domains for the other variables involved in the same constraint.
3.2.1 Events
An event (of type Var.Attr.event
) is a modification of the
the domain of a variable. FaCiLe currently provides four specific
events:
-
Modification of the domain (
on_refine
);
- Substitution of the variable, i.e. reduction of the domain to a singleton (
on_subst
);
- Modification of the minimum value of the domain (
on_min
);
- Modification of the maximum value of the domain (
on_max
).
Note that these events are not independant and constitute a lattice which top is on_subst
and bottom is on_refine
:
-
on_subst
implies all other events1;
-
on_min
and on_max
imply on_refine
.
Constraints are attached to the variables through these events. In
concrete terms, lists of constraints (one per event) are put in the
attribute of the variable. Note that this attachement occurs only when
the constraint is posted.
3.2.2 Wakening, Queuing, Priorities
When an event occurs, related constraints are woken and put in a
queue. The queue is processed after each sequence of waking. This
processing is protected against reentrance. Constraints are considered
one after the other and each update function is called to perform
propagation. Propagation may fail by raising an exception or
succeed. The propagation of one constraint is also protected against
being woken again by itself. When a constraint is triggered, the update
function does not know by which event, nor gets information about the
variable responsible of it. A constraint is woken only once by
two distinct events. Note also that the waking queue contains constraints and
not variables.
FaCiLe implements three ordered queues and ensures that
a constraint in a lower queue is not propagated before a constraint
present in a higher queue. The queue is chosen according to the priority of a constraint (abstract type Cstr.priority
). The
priority is specified when the constraint is defined (see
3.3). It can be changed neither when the
constraint is posted nor later. Priorities are defined in module
Cstr
: immediate
, normal
or
later
.
3.2.3 Constraint Store
FaCiLe handles the constraint store of all the posted and
active constraints (a constraint becomes inactive if it is
solved, i.e. if its update function returns true, see
3.3). For debugging purpose, this store can be consulted
using the function Cstr.active_store
and the returned
constraints list may be processed using constraints (of type
Cstr.t
) access functions (Cstr.id
, Cstr.name
and
Cstr.fprint
).
3.3 User's Constraints
The Cstr.create
function allows the user to build new
constraints from scratch.
To define a new simple (unreifiable) constraint, very few arguments
must be passed to the create function as numbers of them are
optional (thus labelled) and have default values. Merely the two
following arguments are actually needed to build a new constraint:
-
update
should perform propagation
(domains reduction) and return true iff the constraint is consistent;
-
delay
specifies on which events the update
function will be called. As shown in the following example, delay
takes the constraint itself as its only argument and passes it to one or
several calls to Var.delay
.
However we recommend to name a new constraint and precise its printing
facility, which may obviously help debugging, by specifying the following
two optional arguments:
-
?name
should be a relevant string describing the purpose of the
constraint;
-
?fprint
to print more accurate information on the constraint state (variables domains, maintained data structures value, ...).
To define a reifiable constraint, two additional optional arguments
must also be specified:
-
?check
should return true if the constraint is entailed, false if
its negation is entailed and raise the exception DontKnow
otherwise.
check
is called when the constraint is reified and should therefore
not perform any domain modification.
-
?not
should return the negation of the constraint (which is a
constraint itself). It is called when the negation of a reified constraint
is entailed, and to access the waking conditions of the negation of a
constraint when its reification is posted (and the optional argument
?delay_on_negation
of Reify.boolean
is set to true
-
which is its default value). Logical operators of module Reify
also call the ?not
function for the same purpose, but they
systematically do it (see 2.4.4).
Finally two other optional arguments may be specified:
-
?priority
should be passed to the create
function to precise the
priority of the new constraint in the constraints queue. Constraints
with lower priority are waken only when there is no more constraint
of higher priority in the waking queue. Time costly constraints should
get a later
while quick elementary constraints should be
immediate
, and standard constraints normal
(default value).
-
?init
is executed as soon as the post
function is called on the
constraint to perform initialization of inner data structures
needed by update
(thus not called when dealing with a reified
constraint).
The example below defines a new constraint stating that variable x
should be different from variable y
:
diff.ml
open Facile
open Easy
let cstr x y =
let name = "different" in
let fprint c =
Printf.fprintf c "%s: %a <> %a\n" name Fd.fprint x Fd.fprint y
and delay ct =
Var.delay [Var.Attr.on_subst] x ct;
Var.delay [Var.Attr.on_subst] y ct
and update () =
(* Domain reduction is performed only when x or y is instantiated *)
match (Fd.value x, Fd.value y) with
(Val a, Val b) -> a <> b || Stak.fail name
(* If one of the two variables is instantiated, its value is
removed in the domain of the other variable *)
| (Val a, Unk attr_y) ->
let new_domy = Domain.remove a (Var.Attr.dom attr_y) in
Fd.refine y new_domy;
true (* Constraint is solved *)
| (Unk attr_x, Val b) ->
let new_domx = Domain.remove b (Var.Attr.dom attr_x) in
Fd.refine x new_domx;
true (* Constraint is solved *)
| _ -> false (* Constraint is not solved *)
and check () =
match (Fd.value x, Fd.value y) with
(Val a, Val b) -> a <> b
| (Val a, Unk attr_y) when not (Var.Attr.member attr_y a) -> true
| (Unk attr_x, Val b) when not (Var.Attr.member attr_x b) -> true
| (Unk attr_x, Unk attr_y) when
let dom_x = Var.Attr.dom attr_x and dom_y = Var.Attr.dom attr_y in
Domain.is_empty (Domain.intersection dom_x dom_y) -> true
| _ -> raise Cstr.DontKnow
and not () =
fd2e x =~ fd2e y in
(* Creation of the constraint. *)
Cstr.create ~name ~fprint ~check ~not update delay;;
Let's compile the file
ocamlc -c -I +facile diff.ml
and use the produced object:
#load "diff.cmo";;
let x = Fd.interval 1 2 and y = Fd.interval 2 3;;
val x : Facile.Easy.Fd.t = <abstr>
val y : Facile.Easy.Fd.t = <abstr>
let diseq = Diff.cstr x y;;
val diseq : Facile.Cstr.t = <abstr>
Cstr.post diseq;;
- : unit = ()
let goal =
Goals.indomain x &&~ Goals.indomain y
&&~ Goals.atomic (fun () -> Cstr.fprint stdout diseq)
&&~ Goals.fail in
while (Goals.solve goal) do () done;;
different: 1 <> 2
different: 1 <> 3
different: 2 <> 3
- : unit = ()
Another example to test the reification function check
:
let x = Fd.interval 1 2 and y = Fd.interval 3 4;;
val x : Facile.Easy.Fd.t = <abstr>
val y : Facile.Easy.Fd.t = <abstr>
let reified_diseq = Reify.boolean (Diff.cstr x y);;
val reified_diseq : Facile.Var.Fd.t = <abstr>
Fd.fprint stdout reified_diseq;;
1- : unit = ()
3.4 User's Goals
3.4.1 Atomic Goal: Goals.atomic
The simplest way to create a deterministic atomic goal is to use the
Goals.atomic
function which ``goalifies'' any unit function (i.e. of type
unit -> unit
).
Let's write the goal which writes a variable on the standard output:
let gprint_fd x = Goals.atomic (fun () -> Printf.printf "%a\\n" Fd.fprint x);;
val gprint_fd : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
To instantiate a variable inside a goal, we may write the following
definition:
let unify_goal x v = Goals.atomic (fun () -> Fd.unify x v);;
val unify_goal : Facile.Easy.Fd.t -> int -> Facile.Goals.t = <fun>
let v = Fd.interval 0 3 in
if Goals.solve (unify_goal v 2) then Fd.fprint stdout v;;
2- : unit = ()
Note that this goal is the built-in goal Goals.unify
.
This goal creation can be used to pack any side effect function:
let gprint_int x = Goals.atomic (fun () -> print_int x);;
val gprint_int : int -> Facile.Goals.t = <fun>
Goals.solve (Goals.forto 0 5 gprint_int);;
012345- : bool = true
The FaCiLe implementation of the classic ``findall'' of Prolog also
illustrates the use of Goals.atomic to perform side effects: in
this case to store all the solutions found in a list. The function
findall
in this example takes a ``functional goal'' g
as argument
which itself takes the very variable x
from which we want to find all the
possible values for which g
succeeds; it could correspond to the Prolog term:
findall(X, g(X), Sol)
let findall g x =
let sol = ref [] in
let store = Goals.atomic (fun () -> sol := Fd.int_value x :: !sol) in
let goal = g x &&~ store &&~ Goals.fail in
ignore (Goals.solve goal);
!sol;;
val findall :
(Facile.Easy.Fd.t -> Facile.Goals.t) -> Facile.Easy.Fd.t -> int list =
<fun>
We first declare a reference sol
on an empty list to store all the
solutions. Then the simple goal store
is defined to push any
new solution on the head of sol
-- note that we here use
Fd.int_value v
(see 4.12) for conciseness but it is
quite unsafe unless we are sure that v
is bound. The main goal is
the conjunction of g
, store
and a failure. This goal obviously
always fails, so we ``ignore'' the boolean returned by Goals.solve
,
and the solutions list is eventually returned.
The main point when creating goals is to precisely distinguish the
time of creation of the goal from the time of its execution. For example, the following goal does not produce what
might be expected:
let wrong_min_or_max var =
let min = Fd.min var and max = Fd.max var in
(Goals.unify var min ||~ Goals.unify var max);;
val wrong_min_or_max : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The min and max of the variable var are processed
when the goal is created and may be different from the min and max of
the variable when the goal will be called. To fix the problem, min and max must be computed within the goal. Then the latter must
return the disjunction, which cannot be done with a simple call to
Goals.atomic; function Goals.create
(described in the next
section) must be used instead.
3.4.2 Arbitrary Goal: Goals.create
The function Goals.atomic
does not allow to construct goals
which themselves construct new goals (similar to Prolog clauses). The
Goals.create
function ``goalifies'' a function which must return
another goal, possibly Goals.success
to terminate.
Let's write the goal which tries to instantiate a variable to its
minimum value or to its maximum:
let min_or_max v =
Goals.create
(fun () ->
let min = Fd.min v and max = Fd.max v in
Goals.unify v min ||~ Goals.unify v max)
();;
val min_or_max : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The other difference between Goals.create
and Goals.atomic
is
the argument of the goalified function which may be of any type
('a
) and which must be passed as the second argument to
Goals.create
. In the previous example, we use ()
.
Goals.create
allows the user to define recursive goals by a
mapping on a recursive function. In the next example, we iterate a
goal non-deterministically on a list. Note that this goal is equivalent
to the built-in goal Goals.List.exists
.
let rec iter_disj fgoal list =
Goals.create
(function
[] -> Goals.success
| x::xs -> fgoal x ||~ iter_disj fgoal xs)
list;;
val iter_disj : ('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t = <fun>
let gprint_int x = Goals.atomic (fun () -> print_int x);;
val gprint_int : int -> Facile.Goals.t = <fun>
let gprint_list = iter_disj gprint_int;;
val gprint_list : int list -> Facile.Goals.t = <fun>
if Goals.solve (gprint_list [1;7;2;9] &&~ Goals.fail ||~ Goals.success) then
print_newline ();;
1729
- : unit = ()
3.4.3 Recursive Goals: Goals.create_rec
FaCiLe provides also a constructor for intrinsically recursive
goals. Expression Goals.create_rec f
is similar to
Goals.create f
except that the argument of the function
f
is the created goal itself.
The simplest example using this feature is the classic repeat
predicate of Prolog implementing a non-deterministic loop:
let repeat = Goals.create_rec (fun self -> Goals.success ||~ self);;
val repeat : Facile.Goals.t = <abstr>
The goalified function simply returned the disjunction of a success
and itself.
The Goals.indomain
function which non-deterministically
instantiates a variable is written using Goals.create_rec
:
let indomain var =
Goals.create_rec ~name:"indomain"
(fun self ->
match Fd.value var with
Val _ -> Goals.success
| Unk attr ->
let dom = Var.Attr.dom attr in
let remove_min =
Goals.atomic (fun () -> Fd.refine var (Domain.remove_min dom))
and min = Domain.min dom in
Goals.unify var min ||~ (remove_min &&~ self));;
val indomain : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The goal first checks if the variable is already bound and does nothing
in this case. If it is an unknown, it returns a goal trying to
instantiate the variable to its minimum or to remove it before
continuing with the remaining domain.
- 1
- It means that, e.g.,
the event on_min occurs even if a variable is instantiated to its minimum
value.