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 "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 mainly is an update function
(responsible for performing propagations) which is called when the
constraint is woken because a specific event occured. Events
are queued according to the priority of the constraint, and
the search control is resumed as soon as all queues are emptied.
An event (of type Var.Fd.event
) is a modification of 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, thanks
to the Var.Fd.delay
2 function. 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 Suspending to Events, Waking Identity
Constraints are suspended to events by invoking the delay
function wich takes an events list and an optional integer waking
identity as parameters (in addition to the constraint itself and to
the variable triggering the events of course). When posted, the
constraint will be registered to all the events appearing in the
events list, along with the waking identity. This integer will be
passed to the update
function whenever one of the events in the list
occurs. It allows to dicriminate the event and/or the variable
responsible for the wakening, so as to fire a specific rule without
having to inspect all the variables to find out the culprit.
A typical use of waking identities is in global constraints that takes
an array of variables as parameter. The index of the variable can be
associated to the event(s) on which the constraint is suspended and
the update
function may avoid traversing the entire array to
compute the propagation.
The use of a waking identity is optional and 0 is assumed (default
value) if the parameter is omitted. However, if this feature is used,
the identities must be consecutive integers ranging from 0 to n-1,
and n, the number of distinct wakings, must be passed as an optional
parameter (labelled nb_wakings
) to the Cstr.create
function. Actually, an array of size n is internally build to record
the result of the calls to update
with each identity. The
constraint is solved when all such calls have returned true
(see 3.3).
3.2.3 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.4 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. This function may take up to eight
arguments to precisely control the behaviour of the resulting
constraint :
Cstr.create;;
- : ?name:string ->
?nb_wakings:int ->
?fprint:(out_channel -> unit) ->
?priority:Facile.Cstr.priority ->
?init:(unit -> unit) ->
?check:(unit -> bool) ->
?not:(unit -> Facile.Cstr.t) ->
(int -> bool) -> (Facile.Cstr.t -> unit) -> Facile.Cstr.t
= <fun>
However, to define a new simple3 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 by
evaluating Cstr.create update delay
:
-
update
should perform propagation
(domains filtering and consistency checks). It must return true iff the
constraint is consistent, raise Stak.Fail
whenever an inconsistency
is detected and return false
otherwise. Its integer parameter should
be ignored (as in the first example below) if waking ids are not used
(as 0 will consistently be fed as argument).
delay
schedules the awakening of the constraint, i.e. the
execution of its [update] function. The delay
argument takes only
one argument ct
, which is the constraint itself. To specify on which events the
constraint is to be woken, this function must call Var.XxxFd.delay
(once or several times) as shown in the example below. This latter function
takes an events list, a variable and the constraint ct
as parameters
and returns ()
(unit).
However we recommend to name new constraints and precise their printing
facilities, 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 values...).
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
not therefore 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 (see 2.4.4).
To be able to use waking identities, their number must be specified:
-
?nb_wakings
default value is 1. This optional argument is
used in conjonction with waking identities specified in the delay
argument. If (contiguous) waking ids 0 to n-1 are used,
~nb_wakings:n
must be passed to Cstr.create
.
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 default and intended behaviours of init
are a
bit intricate when using waking identities. Its detailed use is
explained in the next paragraphs with the help of two examples.
The default behaviours of init
is:
-
to call
update 0
and ignores its result, when nb_wakings
is equal to 1 (which is its default value);
- to do nothing (
fun () -> ()
) when nb_wakings
is greater
than 1.
If this is not the desired behaviour, the init
argument must be
specified.
Example of reifiable constraints
The example below defines a new constraint stating that variable x
should be different from variable y
. This constraint specifies
an optional name and an optional printing function. It suspends itself to
instantiation events of its two variables (without using any waking identity).
Its update function ignores its integer argument (update _ = ...
)
and withdraws the instantiation value of one of its variable in the domain
of the other. This constraint is reifiable as the check
and not
functions are specified.
Note that no optional init
function is
provided, neither any nb_wakings
argument: in this case, the default
behaviour of init
will be to call update 0
. The init
function is the first function to be called as soon as the constraint is
posted, and its usual intended role is to perform an initial propagation
and possibly initialize internal data structures of the constraint. This
is what happens in this first example. However, if the constraint is
suspended on an instantiation event (XxxFd.on_subst
), and the
update
function relies on the fact that it will only be called
when the variable is instantiatied (e.g. without testing that the
variable is effectively bound), then the default init
behaviour
is not appropriate. Use a specific init
function instead by
providing this optional argument to Cstr.create
, as shown in
the second example (that uses waking ids).
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 =
(* The constraint is suspended on the instantiation of x or y. *)
Fd.delay [Fd.on_subst] x ct;
Fd.delay [Fd.on_subst] y ct
and update _ =
(* If one of the two variables is instantiated, its value is
removed in the domain of the other variable. *)
if Fd.is_bound x then
begin Fd.remove y (Fd.elt_value x); true end
else if Fd.is_bound y then
begin Fd.remove x (Fd.elt_value y); true end
else false
and check () = (* Consistency check for reified constraints. *)
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
(* If the intersection of domains is empty, the constraint is satisfied. *)
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 (* Negation for reification. *)
(* 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;;
2: different: 1 <> 2
2: different: 1 <> 3
2: different: 2 <> 3
- : unit = ()
Another example to test the reification function check
:
let x = Fd.create (Domain.create [1;3;5])
and y = Fd.create (Domain.create [2;4;6]);;
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 = ()
Variables x
and y
have disjoint domains, so the boolean
variable reified_diseq
is instantiated to 1 as expected.
Example of constraints using waking identities
The above example could benefit from the use of waking ids,
avoiding the cost of testing which variable has been instantiated
within the update
function. The next example features such
a disequality constraint. The delay
function must now
specify a waking id (argument waking_id
) along with its associated
events list and
variable. These ids must form an interval ranging from 0 to a
given n-1, and its size n must be provided to the Cstr.create
function through its optional nb_wakings
argument4. The update
function now makes use of this
information (argument id
) and performs the appropriate
propagation depending on which waking event has occurred. This
function must return true
if the constraint is satisfied
for this particular event and false
otherwise. The constraint
will be satisfied only when all the calls to update 0
, ...,
update (n-1)
have returned true
.
In this example, we must provide an init
function as well,
because the nb_wakings
argument is greater than 1 and the
default behaviour of init
is then to do nothing. But the
constraint should propagate at post time, so an appropriate
init
function (which incidentally calls the update
one) is provided.
diffid.ml
open Facile
open Easy
let cstr x y =
let delay ct = (* Ids are associated with waking events. *)
Fd.delay [Fd.on_subst] x ~waking_id:0 ct;
Fd.delay [Fd.on_subst] y ~waking_id:1 ct
and update id =
begin (* Update function using waking ids. *)
match id with
0 -> Fd.remove y (Fd.elt_value x)
| 1 -> Fd.remove x (Fd.elt_value y)
| _ -> failwith "Diff_if.cstr: unexpected waking id"
end;
true in
let init () =
(* Update should be called if x or y is already bound when posting
the constraint. This is the job of the init function. *)
if not (Fd.is_var x) then ignore (update 0)
else if not (Fd.is_var y) then ignore (update 1) in
(* Creation of the constraint with 2 waking ids. *)
Cstr.create ~nb_wakings:2 ~init update delay
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 " 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 -> Facile.Easy.Fd.elt -> 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.elt_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 -> Facile.Easy.Fd.elt 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.elt_value v
(see ??) 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.
3.5 Backtrackable Invariant References -- BIRs
FaCiLe provides through the module Invariant
some features to
handle data-structures which are functionnally dependant between each
other. These invariants are directly derived from the work of
[8], although they are meant to be used within CP
search goals. So they'll be called backtrackable invariant references
or BIRS in the sequel, as their values are restored upon backtracks.
An invariant is either:
-
a constant,
- or a mutable value,
- or the result of a function applied to other invariants,
- or an attribute of any dynamic data-structure, e.g. the maximal
value of a finite domain variable.
FaCiLe can provide efficient handling of the dependencies between
BIRs in order to keep them updated. For example, if an
integer (or floating point) BIR i is defined as the sum of n
others i1, ..., in, the change of the value of one of
i1, ... in will be taken into account in constant time to update i.
The main original use of invariants proposed in [8] is
within local search algorithms. In our context, it can be used also to
compute a heuristic criterion used during search. The implementation
of BIRs in FaCiLe is fully compatible with backtrack.
In the following, we call BIR a mutable value and invariant the
relation (a functional equation) between BIRs.
3.5.1 Type, creation, access and modification
BIRs of FaCiLe are polymorphic so you can handle any
data-structures with them. A BIR may be mutable or not and this
property is handled by the typing:
-
a mutable integer BIR has type
(int, setable) Inv.t
,
- whereas a non mutable float BIR has type
(float, notsetable) Inv.t
.
However, shortcuts with only one type parameter are defined in module
Invariant
to simplify the writting of BIRS: 'a setable_t
and 'a unsetable_t
.
We show in the following example how to create, access and modify a BIR:
let x = Invariant.create 1729 and y = Invariant.constant 3.14;;
val x : int Facile.Invariant.setable_t = <abstr>
val y : float Facile.Invariant.unsetable_t = <abstr>
(Invariant.get x, Invariant.get y);;
- : int * float = (1729, 3.14)
Invariant.set x 1730;;
- : unit = ()
Invariant.get x;;
- : int = 1730
Like finite domain variables, BIRs can be named thanks to an optional
string argument (?name
) and feature a unique integer identity
(accessible with function Invariant.id
).
3.5.2 Operations
FaCiLe provides basic arithmetic operators on integer BIRs.
These functions are completed by primitives working on
array of BIRs (submodule Invariant.Array
).
The following table gives the time and space complexity of the basic invariants :
|
|
Invariant |
Time |
Memory |
|
|
O(1) |
O(1) |
|
O(1)
|
O(1) |
|
O(logn) |
O(n) |
i = argmini Î [1,n] xi |
O(logn) |
O(n) |
|
let a = Array.map Invariant.create [|1;2;3;4|];;
val a : int Facile.Invariant.setable_t array =
[|<abstr>; <abstr>; <abstr>; <abstr>|]
let s = Invariant.sum a;;
val s : int Facile.Invariant.unsetable_t = <abstr>
Invariant.get s;;
- : int = 10
Invariant.set a.(3) 8;;
- : unit = ()
Invariant.get s;;
- : int = 14
The library also provides generic wrappers (unary
,
binary
and ternary
, for functions with arity up to tree)
for BIRs which allow the user to transform any function working on
the type a into a function working on an a BIR:
let x = Invariant.create name:"x" 2.71;;
val x : float Facile.Invariant.setable_t = <abstr>
let y = Invariant.unary name:"log" log x;;
val y : float Facile.Invariant.unsetable_t = <abstr>
Invariant.fprint stdout y; Invariant.get y;;
log(x)- : float = 0.996948634891609564
Invariant.set x 8.0; Invariant.get y;;
- : float = 2.07944154167983575
These wrapped functions can be named with an optional string argument.
3.5.3 Domain access
In order to implement computation of heuristic criterion, it is
required to be able to translate attributes of finite domain variables
(of type Fd.t
or SetFd.t
) into invariant references.
These functionalities are listed in submodules Invariant.Fd
and
Invariant.SetFd
.
For example, the heuristic criterion which selects the variable with
the smallest domain is easily computed as follows :
let best = fun vars ->
Invariant.Array.argmin (Array.map Invariant.Fd.size vars);;
val best :
Facile.Invariant.Fd.fd array ->
(int -> 'a) -> int Facile.Invariant.unsetable_t = <fun>
- 1
- It means that, e.g.
the event on_min occurs even if a variable is instantiated to its minimum
value.
- 2
- Or Var.SetFd.delay for set
variables.
- 3
- That is unreifiable and without the use of
waking identities.
- 4
- As
correctly guessed by the reader, these ids are used to access an
internal array.