Previous Contents Next

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: Note that these events are not independant and constitute a lattice which top is on_subst and bottom is 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: 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:

To define a reifiable constraint, two additional optional arguments must also be specified:

Finally two other optional arguments may be specified: 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.

Previous Contents Next