module 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 : ``Pervasives.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:Domain.t -> (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 : ``Var.Fd.t -> int -> t`

`unify var x`

instantiates variable `var`

to `x`

.`val indomain : ``Var.Fd.t -> t`

Non-deterministic instantiation of a variable, by labeling its domain
(in increasing order).

`val instantiate : ``(Domain.t -> int) -> 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 : ``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 -> 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`

`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:

- it can raise
`Stak.Fail`

to force a failure of the search in the current branch (i.e. backtrack);

- it can raise any other user exception to stop the search process;

- it must return
`unit`

to continue the search; this is the default behavior.