module Fcl_goals:sig
..end
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.
val name : t -> string
name g
returns the name of the goal g
.
val fprint : Stdlib.out_channel -> t -> unit
fprint chan g
prints the name of goal g
on channel chan
.
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 the goal itself as argument and should return a goal
(success to stop). Useful to write recursive goals. name
default
value is "create_rec"
.
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:Fcl_domain.t -> (Fcl_var.Fd.t -> t) -> t
sigma ~domain:Domain.int 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).
val unify : Fcl_var.Fd.t -> int -> t
unify var x
instantiates variable var
to x
.
val indomain : Fcl_var.Fd.t -> t
Non-deterministic instantiation of a variable, by labeling its domain (in increasing order).
val instantiate : (Fcl_domain.t -> int) -> Fcl_var.Fd.t -> t
instantiate choose var
Non-deterministic instantiation of a variable,
by labeling its domain using the value returned by the choose
function.
val dichotomic : Fcl_var.Fd.t -> t
Non-deterministic instantiation of a variable, by dichotomic recursive exploration of its domain.
module Conjunto:sig
..end
module Array:sig
..end
module List:sig
..end
type
bb_mode =
| |
Restart |
|||
| |
Continue |
(* | Branch and bound mode. | *) |
val minimize : ?step:int ->
?mode:bb_mode ->
t -> Fcl_var.Fd.t -> (int -> unit) -> t
minimize ~step:1 ~mode:Continue 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.
val lds : ?step:int -> t -> t
lds ~step:1 g
returns a goal which will iteratively search g
with
increasing limited discrepancy (see ) by
increment step
. step
default value is 1.
val solve : ?control:(int -> unit) -> t -> bool
solve ~control:(fun _ -> ()) 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:
Stak.Fail
to force a failure of the search in the
current branch (i.e. backtrack);unit
to continue the search; this is the default
behavior.