(***********************************************************************)
(* *)
(* FaCiLe *)
(* A Functional Constraint Library *)
(* *)
(* Nicolas Barnier, Pascal Brisset, LOG, CENA *)
(* *)
(* Copyright 2004 CENA. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License. *)
(***********************************************************************)
(* $Id: fcl_goals.mli,v 1.55 2004/07/30 10:37:13 barnier Exp $ *)
(** {1 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.
*)
(** {2 Access} *)
type t
(** The type of goals. *)
val name : t -> string
(** [name g] returns the name of the goal [g]. *)
val fprint : out_channel -> t -> unit
(** [fprint chan g] prints the name of goal [g] on channel [chan]. *)
(** {2 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"]. *)
(** {2 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 {b 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). *)
(** {3 Instantiation of Finite Domain Variables} *)
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. *)
(** {3 Instantiation of Set Variables} *)
module Conjunto : sig
val indomain : Fcl_var.SetFd.t -> t
(** Non-deterministic instantiation of set variables ([refine] of Gervet's
Conjunto{% ~\cite{conjunto}%}). *)
end
(** {2 Operations on Array of Variables} *)
module Array : sig
val foralli : ?select:('a array -> int) -> (int -> 'a -> t) -> 'a array -> t
(** [foralli ?select g a] returns the conjunctive iteration
of the application of goal [g] on the elements of array [a]
and on their indices. The order is computed by the heuristic
[?select] which must raise [Not_found] to terminate.
Default heuristic is increasing order over indices. *)
val forall : ?select:('a array -> int) -> ('a -> t) -> 'a array -> t
(** [forall ?select g a] defined by [foralli ?select (fun _i x -> g x) a],
i.e. indices of selected elements are not passed to goal [g]. *)
val existsi : ?select:('a array -> int) -> (int -> 'a -> t) -> 'a array -> t
(** [existsi ?select g a] returns the disjunctive iteration
of the application of goal [g] on the elements of array [a]
and on their indices. The order is computed by the heuristic
[?select] which must raise [Not_found] to terminate.
Default heuristic is increasing order over indices. *)
val exists : ?select:('a array -> int) -> ('a -> t) -> 'a array -> t
(** [exists ?select g a] defined by [existsi ?select (fun _i x -> g x) a],
i.e. indices of selected elements are not passed to goal [g]. *)
val choose_index : (Fcl_var.Attr.t -> Fcl_var.Attr.t -> bool) -> Fcl_var.Fd.t array -> int
(** [choose_index order fds] returns the index of the best (minimun)
free (not instantiated) variable in the array [fds] for the criterion
[order]. Raises [Not_found] if all variables are bound (instantiated). *)
val not_instantiated_fd : Fcl_var.Fd.t array -> int
(** [not_instantiated_fd fds] returns the index of one element in [fds]
which is not instantiated. Raises [Not_found] if all variables in array
[fds] are bound. *)
val labeling: Fcl_var.Fd.t array -> t
(** Standard labeling, i.e. conjunctive non-deterministic instantiation of
an array of variables. Defined as [forall indomain]. *)
end
(** {2 Operations on List of Variables} *)
module List : sig
val forall : ?select:('a list -> 'a * 'a list) -> ('a -> t) -> 'a list -> t
(** [forall ?select g [x1;x2;...;xn]] is [g x1 &&~ g x2 &&~ ... &&~ g xn],
i.e. returns the conjunctive iteration of goal [g] on list [a]. *)
val exists : ?select:('a list -> 'a * 'a list) -> ('a -> t) -> 'a list -> t
(** [exists ?select g [x1;x2;...;xn]] is [g x1 ||~ g x2 ||~ ... ||~ g xn],
i.e. returns the disjunctive iteration of goal [g] on list [a]. *)
val member : Fcl_var.Fd.t -> int list -> t
(** [member v l] returns the disjunctive iteration of the instantiation of
the variable [v] to the values in the integer list [l]. Defined by
[fun v l -> exists (fun x -> create (fun () -> Fd.unify v x)) l]. *)
val labeling: Fcl_var.Fd.t list -> t
(** Standard labeling, i.e. conjunctive non-deterministic instantiation of
a list of variables. Defined as [forall indomain]. *)
end
(** {2 Optimization} *)
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] {b always fails}. *)
(** {2 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 {% ~\cite{harvey95.lds}%}) by
increment [step]. [step] default value is 1. *)
(** {2 Solving} *)
val solve : ?control:(int -> unit) -> t -> bool
(** [solve ~control:(fun _ -> ()) g] solves the goal [g] and returns
a success ([true]) or a
