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`

.