Previous  Up  Next

Module Goals


module Goals: sig .. end

Building and Solving Goals



This module provides functions and operators to build goals that will control the search, i.e. mainly choose and instantiate variables.

Access


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.

Creation


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".

Operators and Built-in Goals


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).

Instantiation of Finite Domain Variables


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.

Instantiation of Set Variables


module Conjunto: sig .. end

Operations on Array of Variables


module Array: sig .. end

Operations on List of Variables


module List: sig .. end

Optimization



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 always fails.

Search Strategy


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.

Solving


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: