module Array:sig..end
val foralli : ?select:('a array -> int) ->
(int -> 'a -> Fcl_goals.t) -> 'a array -> Fcl_goals.tforalli ?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.tforall ?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.texistsi ?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.texists ?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 -> intchoose_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 -> intnot_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.tStandard labeling, i.e. conjunctive non-deterministic instantiation of
an array of variables. Defined as forall indomain.