Module Fcl_goals.Array

module Array: sig .. end

val foralli : ?select:('a array -> int) ->
(int -> 'a -> Fcl_goals.t) -> 'a array -> Fcl_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 -> Fcl_goals.t) -> 'a array -> Fcl_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 -> Fcl_goals.t) -> 'a array -> Fcl_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 -> Fcl_goals.t) -> 'a array -> Fcl_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 : (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 -> Fcl_goals.t

Standard labeling, i.e. conjunctive non-deterministic instantiation of an array of variables. Defined as forall indomain.