module Array: sig .. end
val foralli : ?select:('a array -> int) -> (int -> 'a -> Goals.t) -> 'a array -> Goals.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 -> Goals.t) -> 'a array -> Goals.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 -> Goals.t) -> 'a array -> Goals.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 -> Goals.t) -> 'a array -> Goals.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 : (Var.Attr.t -> Var.Attr.t -> bool) -> 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 : 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 : Var.Fd.t array -> Goals.t
Standard labeling, i.e. conjunctive non-deterministic instantiation of
an array of variables. Defined as forall indomain.