sig
module Domain :
sig
type elt = int
type t
val empty : Facile.Domain.t
val create : Facile.Domain.elt list -> Facile.Domain.t
val unsafe_create : Facile.Domain.elt list -> Facile.Domain.t
val interval :
Facile.Domain.elt -> Facile.Domain.elt -> Facile.Domain.t
val int : Facile.Domain.t
val boolean : Facile.Domain.t
val is_empty : Facile.Domain.t -> bool
val size : Facile.Domain.t -> Facile.Domain.elt
val min : Facile.Domain.t -> Facile.Domain.elt
val max : Facile.Domain.t -> Facile.Domain.elt
val min_max : Facile.Domain.t -> Facile.Domain.elt * Facile.Domain.elt
val iter : (Facile.Domain.elt -> unit) -> Facile.Domain.t -> unit
val interval_iter :
(Facile.Domain.elt -> Facile.Domain.elt -> unit) ->
Facile.Domain.t -> unit
val member : Facile.Domain.elt -> Facile.Domain.t -> bool
val values : Facile.Domain.t -> Facile.Domain.elt list
val fprint_elt : Pervasives.out_channel -> Facile.Domain.elt -> unit
val fprint : Pervasives.out_channel -> Facile.Domain.t -> unit
val sprint : Facile.Domain.t -> string
val included : Facile.Domain.t -> Facile.Domain.t -> bool
val add : Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val remove : Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val remove_up : Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val remove_low :
Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val remove_low_up :
Facile.Domain.elt ->
Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val remove_closed_inter :
Facile.Domain.elt ->
Facile.Domain.elt -> Facile.Domain.t -> Facile.Domain.t
val intersection :
Facile.Domain.t -> Facile.Domain.t -> Facile.Domain.t
val union : Facile.Domain.t -> Facile.Domain.t -> Facile.Domain.t
val difference : Facile.Domain.t -> Facile.Domain.t -> Facile.Domain.t
val diff : Facile.Domain.t -> Facile.Domain.t -> Facile.Domain.t
val remove_min : Facile.Domain.t -> Facile.Domain.t
val minus : Facile.Domain.t -> Facile.Domain.t
val plus : Facile.Domain.t -> Facile.Domain.elt -> Facile.Domain.t
val times : Facile.Domain.t -> Facile.Domain.elt -> Facile.Domain.t
val smallest_geq :
Facile.Domain.t -> Facile.Domain.elt -> Facile.Domain.elt
val greatest_leq :
Facile.Domain.t -> Facile.Domain.elt -> Facile.Domain.elt
val largest_hole_around :
Facile.Domain.t ->
Facile.Domain.elt -> Facile.Domain.elt * Facile.Domain.elt
val choose :
(Facile.Domain.elt -> Facile.Domain.elt -> bool) ->
Facile.Domain.t -> Facile.Domain.elt
val compare : Facile.Domain.t -> Facile.Domain.t -> Facile.Domain.elt
val compare_elt :
Facile.Domain.elt -> Facile.Domain.elt -> Facile.Domain.elt
val disjoint : Facile.Domain.t -> Facile.Domain.t -> bool
end
module SetDomain :
sig
module S :
sig
type t
val empty : Facile.SetDomain.S.t
val is_empty : Facile.SetDomain.S.t -> bool
val mem : int -> Facile.SetDomain.S.t -> bool
val add : int -> Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val singleton : int -> Facile.SetDomain.S.t
val remove : int -> Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val union :
Facile.SetDomain.S.t ->
Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val inter :
Facile.SetDomain.S.t ->
Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val diff :
Facile.SetDomain.S.t ->
Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val compare : Facile.SetDomain.S.t -> Facile.SetDomain.S.t -> int
val equal : Facile.SetDomain.S.t -> Facile.SetDomain.S.t -> bool
val subset : Facile.SetDomain.S.t -> Facile.SetDomain.S.t -> bool
val iter : (int -> unit) -> Facile.SetDomain.S.t -> unit
val cardinal : Facile.SetDomain.S.t -> int
val elements : Facile.SetDomain.S.t -> int list
val min_elt : Facile.SetDomain.S.t -> int
val max_elt : Facile.SetDomain.S.t -> int
val choose : Facile.SetDomain.S.t -> int
val remove_up : int -> Facile.SetDomain.S.t -> Facile.SetDomain.S.t
val remove_low :
int -> Facile.SetDomain.S.t -> Facile.SetDomain.S.t
end
type elt = Facile.SetDomain.S.t
type t
val min : Facile.SetDomain.t -> Facile.SetDomain.elt
val max : Facile.SetDomain.t -> Facile.SetDomain.elt
val min_max :
Facile.SetDomain.t -> Facile.SetDomain.elt * Facile.SetDomain.elt
val mem : Facile.SetDomain.elt -> Facile.SetDomain.t -> bool
val interval :
Facile.SetDomain.elt -> Facile.SetDomain.elt -> Facile.SetDomain.t
val fprint_elt : Pervasives.out_channel -> Facile.SetDomain.elt -> unit
val fprint : Pervasives.out_channel -> Facile.SetDomain.t -> unit
val included : Facile.SetDomain.t -> Facile.SetDomain.t -> bool
val iter : (Facile.SetDomain.elt -> 'a) -> Facile.SetDomain.t -> 'a
val values : Facile.SetDomain.t -> Facile.SetDomain.elt list
val elt_of_list : int list -> Facile.SetDomain.elt
end
module Stak :
sig
type level
val older : Facile.Stak.level -> Facile.Stak.level -> bool
val size : unit -> int
val depth : unit -> int
val level : unit -> Facile.Stak.level
val levels : unit -> Facile.Stak.level list
val nb_choice_points : unit -> int
exception Level_not_found of Facile.Stak.level
val cut : Facile.Stak.level -> unit
exception Fail of string
val fail : string -> 'a
val trail : (unit -> unit) -> unit
type 'a ref
val ref : 'a -> 'a Facile.Stak.ref
val set : 'a Facile.Stak.ref -> 'a -> unit
val get : 'a Facile.Stak.ref -> 'a
end
module Data :
sig
module Array : sig val set : 'a array -> int -> 'a -> unit end
module Hashtbl :
sig
type ('a, 'b) t
val create : ?random:bool -> int -> ('a, 'b) Facile.Data.Hashtbl.t
val get : ('a, 'b) Facile.Data.Hashtbl.t -> ('a, 'b) Hashtbl.t
val add : ('a, 'b) Facile.Data.Hashtbl.t -> 'a -> 'b -> unit
val find : ('a, 'b) Facile.Data.Hashtbl.t -> 'a -> 'b
val mem : ('a, 'b) Facile.Data.Hashtbl.t -> 'a -> bool
val remove : ('a, 'b) Facile.Data.Hashtbl.t -> 'a -> unit
val replace : ('a, 'b) Facile.Data.Hashtbl.t -> 'a -> 'b -> unit
val iter :
('a -> 'b -> unit) -> ('a, 'b) Facile.Data.Hashtbl.t -> unit
val fold :
('a -> 'b -> 'c -> 'c) ->
('a, 'b) Facile.Data.Hashtbl.t -> 'c -> 'c
end
end
module Cstr :
sig
exception DontKnow
type priority
val immediate : Facile.Cstr.priority
val normal : Facile.Cstr.priority
val later : Facile.Cstr.priority
type t
val id : Facile.Cstr.t -> int
val name : Facile.Cstr.t -> string
val priority : Facile.Cstr.t -> Facile.Cstr.priority
val fprint : Pervasives.out_channel -> Facile.Cstr.t -> unit
val is_solved : Facile.Cstr.t -> bool
val create :
?name:string ->
?nb_wakings:int ->
?fprint:(Pervasives.out_channel -> unit) ->
?priority:Facile.Cstr.priority ->
?init:(unit -> unit) ->
?check:(unit -> bool) ->
?not:(unit -> Facile.Cstr.t) ->
(int -> bool) -> (Facile.Cstr.t -> unit) -> Facile.Cstr.t
val post : Facile.Cstr.t -> unit
val init : Facile.Cstr.t -> unit
val one : Facile.Cstr.t
val zero : Facile.Cstr.t
val active_store : unit -> Facile.Cstr.t list
end
module Var :
sig
module type ATTR =
sig
type t
type domain
type elt
type event
val dom : Facile.Var.ATTR.t -> Facile.Var.ATTR.domain
val on_refine : Facile.Var.ATTR.event
val on_subst : Facile.Var.ATTR.event
val on_min : Facile.Var.ATTR.event
val on_max : Facile.Var.ATTR.event
val fprint : Pervasives.out_channel -> Facile.Var.ATTR.t -> unit
val min : Facile.Var.ATTR.t -> Facile.Var.ATTR.elt
val max : Facile.Var.ATTR.t -> Facile.Var.ATTR.elt
val member : Facile.Var.ATTR.t -> Facile.Var.ATTR.elt -> bool
val id : Facile.Var.ATTR.t -> int
val constraints_number : Facile.Var.ATTR.t -> int
val size : Facile.Var.ATTR.t -> int
end
module Attr :
sig
type t
type domain = Domain.t
type elt = int
type event
val dom : t -> domain
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val fprint : out_channel -> t -> unit
val min : t -> elt
val max : t -> elt
val member : t -> elt -> bool
val id : t -> int
val constraints_number : t -> int
val size : t -> int
end
module SetAttr :
sig
type t
type domain = SetDomain.t
type elt = SetDomain.S.t
type event
val dom : t -> domain
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val fprint : out_channel -> t -> unit
val min : t -> elt
val max : t -> elt
val member : t -> elt -> bool
val id : t -> int
val constraints_number : t -> int
val size : t -> int
end
type ('a, 'b) concrete = Unk of 'a | Val of 'b
module type BASICFD =
sig
type t
type attr
type domain
type elt
type event
val create :
?name:string -> Facile.Var.BASICFD.domain -> Facile.Var.BASICFD.t
val interval :
?name:string ->
Facile.Var.BASICFD.elt ->
Facile.Var.BASICFD.elt -> Facile.Var.BASICFD.t
val array :
?name:string ->
int ->
Facile.Var.BASICFD.elt ->
Facile.Var.BASICFD.elt -> Facile.Var.BASICFD.t array
val elt : Facile.Var.BASICFD.elt -> Facile.Var.BASICFD.t
val is_var : Facile.Var.BASICFD.t -> bool
val is_bound : Facile.Var.BASICFD.t -> bool
val value :
Facile.Var.BASICFD.t ->
(Facile.Var.BASICFD.attr, Facile.Var.BASICFD.elt)
Facile.Var.concrete
val min : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt
val max : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt
val min_max :
Facile.Var.BASICFD.t ->
Facile.Var.BASICFD.elt * Facile.Var.BASICFD.elt
val elt_value : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt
val int_value : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt
val size : Facile.Var.BASICFD.t -> int
val member : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> bool
val id : Facile.Var.BASICFD.t -> int
val name : Facile.Var.BASICFD.t -> string
val compare : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.t -> int
val equal : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.t -> bool
val fprint : Pervasives.out_channel -> Facile.Var.BASICFD.t -> unit
val fprint_array :
Pervasives.out_channel -> Facile.Var.BASICFD.t array -> unit
val unify : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> unit
val refine :
Facile.Var.BASICFD.t -> Facile.Var.BASICFD.domain -> unit
val refine_low :
Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> unit
val refine_up :
Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> unit
val refine_low_up :
Facile.Var.BASICFD.t ->
Facile.Var.BASICFD.elt -> Facile.Var.BASICFD.elt -> unit
val on_refine : Facile.Var.BASICFD.event
val on_subst : Facile.Var.BASICFD.event
val on_min : Facile.Var.BASICFD.event
val on_max : Facile.Var.BASICFD.event
val delay :
Facile.Var.BASICFD.event list ->
Facile.Var.BASICFD.t -> ?waking_id:int -> Facile.Cstr.t -> unit
val int : Facile.Var.BASICFD.elt -> Facile.Var.BASICFD.t
val subst : Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> unit
val unify_cstr :
Facile.Var.BASICFD.t -> Facile.Var.BASICFD.elt -> Facile.Cstr.t
end
module type FD =
sig
type t
type attr
type domain
type elt
type event
val create : ?name:string -> domain -> t
val interval : ?name:string -> elt -> elt -> t
val array : ?name:string -> int -> elt -> elt -> t array
val elt : elt -> t
val is_var : t -> bool
val is_bound : t -> bool
val value : t -> (attr, elt) concrete
val min : t -> elt
val max : t -> elt
val min_max : t -> elt * elt
val elt_value : t -> elt
val int_value : t -> elt
val size : t -> int
val member : t -> elt -> bool
val id : t -> int
val name : t -> string
val compare : t -> t -> int
val equal : t -> t -> bool
val fprint : out_channel -> t -> unit
val fprint_array : out_channel -> t array -> unit
val unify : t -> elt -> unit
val refine : t -> domain -> unit
val refine_low : t -> elt -> unit
val refine_up : t -> elt -> unit
val refine_low_up : t -> elt -> elt -> unit
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val delay : event list -> t -> ?waking_id:int -> Cstr.t -> unit
val int : elt -> t
val subst : t -> elt -> unit
val unify_cstr : t -> elt -> Cstr.t
val remove : t -> elt -> unit
val values : t -> elt list
val iter : (elt -> unit) -> t -> unit
end
module Fd :
sig
type t
type attr = Attr.t
type domain = Domain.t
type elt = Domain.elt
type event = Attr.event
val create : ?name:string -> domain -> t
val interval : ?name:string -> elt -> elt -> t
val array : ?name:string -> int -> elt -> elt -> t array
val elt : elt -> t
val is_var : t -> bool
val is_bound : t -> bool
val value : t -> (attr, elt) concrete
val min : t -> elt
val max : t -> elt
val min_max : t -> elt * elt
val elt_value : t -> elt
val int_value : t -> elt
val size : t -> int
val member : t -> elt -> bool
val id : t -> int
val name : t -> string
val compare : t -> t -> int
val equal : t -> t -> bool
val fprint : out_channel -> t -> unit
val fprint_array : out_channel -> t array -> unit
val unify : t -> elt -> unit
val refine : t -> domain -> unit
val refine_low : t -> elt -> unit
val refine_up : t -> elt -> unit
val refine_low_up : t -> elt -> elt -> unit
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val delay : event list -> t -> ?waking_id:int -> Cstr.t -> unit
val int : elt -> t
val subst : t -> elt -> unit
val unify_cstr : t -> elt -> Cstr.t
val remove : t -> elt -> unit
val values : t -> elt list
val iter : (elt -> unit) -> t -> unit
end
module SetFd :
sig
type t
type attr = SetAttr.t
type domain = SetDomain.t
type elt = SetDomain.S.t
type event = SetAttr.event
val create : ?name:string -> domain -> t
val interval : ?name:string -> elt -> elt -> t
val array : ?name:string -> int -> elt -> elt -> t array
val elt : elt -> t
val is_var : t -> bool
val is_bound : t -> bool
val value : t -> (attr, elt) concrete
val min : t -> elt
val max : t -> elt
val min_max : t -> elt * elt
val elt_value : t -> elt
val int_value : t -> elt
val size : t -> int
val member : t -> elt -> bool
val id : t -> int
val name : t -> string
val compare : t -> t -> int
val equal : t -> t -> bool
val fprint : out_channel -> t -> unit
val fprint_array : out_channel -> t array -> unit
val unify : t -> elt -> unit
val refine : t -> domain -> unit
val refine_low : t -> elt -> unit
val refine_up : t -> elt -> unit
val refine_low_up : t -> elt -> elt -> unit
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val delay : event list -> t -> ?waking_id:int -> Cstr.t -> unit
val int : elt -> t
val subst : t -> elt -> unit
val unify_cstr : t -> elt -> Cstr.t
end
val delay :
Facile.Var.Attr.event list ->
Facile.Var.Fd.t -> ?waking_id:int -> Facile.Cstr.t -> unit
end
module Reify :
sig
val boolean :
?delay_on_negation:bool -> Facile.Cstr.t -> Facile.Var.Fd.t
val cstr :
?delay_on_negation:bool ->
Facile.Cstr.t -> Facile.Var.Fd.t -> Facile.Cstr.t
val ( ||~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( &&~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( <=>~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val xor : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val not : Facile.Cstr.t -> Facile.Cstr.t
val ( =>~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
end
module Alldiff :
sig
type algo = Lazy | Bin_matching of Facile.Var.Fd.event
val cstr :
?algo:Facile.Alldiff.algo -> Facile.Var.Fd.t array -> Facile.Cstr.t
end
module Goals :
sig
type t
val name : Facile.Goals.t -> string
val fprint : Pervasives.out_channel -> Facile.Goals.t -> unit
val atomic : ?name:string -> (unit -> unit) -> Facile.Goals.t
val create :
?name:string -> ('a -> Facile.Goals.t) -> 'a -> Facile.Goals.t
val create_rec :
?name:string -> (Facile.Goals.t -> Facile.Goals.t) -> Facile.Goals.t
val fail : Facile.Goals.t
val success : Facile.Goals.t
val ( &&~ ) : Facile.Goals.t -> Facile.Goals.t -> Facile.Goals.t
val ( ||~ ) : Facile.Goals.t -> Facile.Goals.t -> Facile.Goals.t
val once : Facile.Goals.t -> Facile.Goals.t
val solve : ?control:(int -> unit) -> Facile.Goals.t -> bool
val lds : ?step:int -> Facile.Goals.t -> Facile.Goals.t
val unify : Facile.Var.Fd.t -> int -> Facile.Goals.t
val indomain : Facile.Var.Fd.t -> Facile.Goals.t
val instantiate :
(Facile.Domain.t -> int) -> Facile.Var.Fd.t -> Facile.Goals.t
val dichotomic : Facile.Var.Fd.t -> Facile.Goals.t
val forto : int -> int -> (int -> Facile.Goals.t) -> Facile.Goals.t
val fordownto : int -> int -> (int -> Facile.Goals.t) -> Facile.Goals.t
module Array :
sig
val foralli :
?select:('a array -> int) ->
(int -> 'a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val forall :
?select:('a array -> int) ->
('a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val existsi :
?select:('a array -> int) ->
(int -> 'a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val exists :
?select:('a array -> int) ->
('a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val choose_index :
(Facile.Var.Attr.t -> Facile.Var.Attr.t -> bool) ->
Facile.Var.Fd.t array -> int
val not_instantiated_fd : Facile.Var.Fd.t array -> int
val labeling : Facile.Var.Fd.t array -> Facile.Goals.t
end
module GlArray :
sig
val iter_h :
('a array -> int) ->
('a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val iter_hi :
('a array -> int) ->
(int -> 'a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val iter : ('a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val iteri :
(int -> 'a -> Facile.Goals.t) -> 'a array -> Facile.Goals.t
val iter2 :
('a -> 'b -> Facile.Goals.t) ->
'a array -> 'b array -> Facile.Goals.t
val labeling : Facile.Var.Fd.t array -> Facile.Goals.t
val choose_index :
(Facile.Var.Attr.t -> Facile.Var.Attr.t -> bool) ->
Facile.Var.Fd.t array -> int
val not_instantiated_fd : Facile.Var.Fd.t array -> int
end
module List :
sig
val forall :
?select:('a list -> 'a * 'a list) ->
('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t
val exists :
?select:('a list -> 'a * 'a list) ->
('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t
val member : Facile.Var.Fd.t -> int list -> Facile.Goals.t
val labeling : Facile.Var.Fd.t list -> Facile.Goals.t
end
module GlList :
sig
val iter : ('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t
val labeling : Facile.Var.Fd.t list -> Facile.Goals.t
val member : Facile.Var.Fd.t -> int list -> Facile.Goals.t
val iter_h :
('a list -> 'a * 'a list) ->
('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t
end
type bb_mode = Restart | Continue
val minimize :
?step:int ->
?mode:Facile.Goals.bb_mode ->
Facile.Goals.t -> Facile.Var.Fd.t -> (int -> unit) -> Facile.Goals.t
val sigma :
?domain:Facile.Domain.t ->
(Facile.Var.Fd.t -> Facile.Goals.t) -> Facile.Goals.t
module Conjunto :
sig val indomain : Facile.Var.SetFd.t -> Facile.Goals.t end
end
module Sorting :
sig
val sort : Facile.Var.Fd.t array -> Facile.Var.Fd.t array
val sortp :
Facile.Var.Fd.t array ->
Facile.Var.Fd.t array * Facile.Var.Fd.t array
val cstr :
Facile.Var.Fd.t array ->
?p:Facile.Var.Fd.t array option ->
Facile.Var.Fd.t array -> Facile.Cstr.t
end
module Boolean :
sig
val cstr : Facile.Var.Fd.t array -> Facile.Var.Fd.t -> Facile.Cstr.t
val sum : Facile.Var.Fd.t array -> Facile.Var.Fd.t
end
module Expr :
sig
type t
val fprint : Pervasives.out_channel -> Facile.Expr.t -> unit
val eval : Facile.Expr.t -> int
val min_of_expr : Facile.Expr.t -> int
val max_of_expr : Facile.Expr.t -> int
val min_max_of_expr : Facile.Expr.t -> int * int
end
module Arith :
sig
type t
val i2e : int -> Facile.Arith.t
val fd2e : Facile.Var.Fd.t -> Facile.Arith.t
val ( +~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( *~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( -~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( /~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( **~ ) : Facile.Arith.t -> int -> Facile.Arith.t
val ( %~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val abs : Facile.Arith.t -> Facile.Arith.t
val sum : Facile.Arith.t array -> Facile.Arith.t
val sum_fd : Facile.Var.Fd.t array -> Facile.Arith.t
val scalprod : int array -> Facile.Arith.t array -> Facile.Arith.t
val scalprod_fd : int array -> Facile.Var.Fd.t array -> Facile.Arith.t
val prod : Facile.Arith.t array -> Facile.Arith.t
val prod_fd : Facile.Var.Fd.t array -> Facile.Arith.t
val fprint : Pervasives.out_channel -> Facile.Arith.t -> unit
val eval : Facile.Arith.t -> int
val min_of_expr : Facile.Arith.t -> int
val max_of_expr : Facile.Arith.t -> int
val min_max_of_expr : Facile.Arith.t -> int * int
val ( <=~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( <~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( >~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( =~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( <>~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( >=~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val e2fd : Facile.Arith.t -> Facile.Var.Fd.t
val ( <=~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( <~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( >~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( =~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( <>~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( >=~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val shift : Facile.Var.Fd.t -> int -> Facile.Var.Fd.t
val get_boolsum_threshold : unit -> int
val set_boolsum_threshold : int -> unit
end
module Invariant :
sig
type ('a, 'b) t
type setable
type unsetable
type 'a setable_t = ('a, Facile.Invariant.setable) Facile.Invariant.t
type 'a unsetable_t =
('a, Facile.Invariant.unsetable) Facile.Invariant.t
val create : ?name:string -> 'a -> 'a Facile.Invariant.setable_t
val constant : ?name:string -> 'a -> 'a Facile.Invariant.unsetable_t
val set : 'a Facile.Invariant.setable_t -> 'a -> unit
val get : ('a, 'b) Facile.Invariant.t -> 'a
val id : ('a, 'b) Facile.Invariant.t -> int
val name : ('a, 'b) Facile.Invariant.t -> string
val fprint :
Pervasives.out_channel ->
?printer:(Pervasives.out_channel -> 'a -> unit) ->
('a, 'b) Facile.Invariant.t -> unit
val unary :
?name:string ->
('a -> 'b) ->
('a, 'c) Facile.Invariant.t -> 'b Facile.Invariant.unsetable_t
val binary :
?name:string ->
('a -> 'b -> 'c) ->
('a, 'd) Facile.Invariant.t ->
('b, 'e) Facile.Invariant.t -> 'c Facile.Invariant.unsetable_t
val ternary :
?name:string ->
('a -> 'b -> 'c -> 'd) ->
('a, 'e) Facile.Invariant.t ->
('b, 'f) Facile.Invariant.t ->
('c, 'g) Facile.Invariant.t -> 'd Facile.Invariant.unsetable_t
val sum :
(int, 'a) Facile.Invariant.t array ->
int Facile.Invariant.unsetable_t
val prod :
(int, 'a) Facile.Invariant.t array ->
int Facile.Invariant.unsetable_t
module Array :
sig
val get :
('a, 'b) Facile.Invariant.t array ->
(int, 'c) Facile.Invariant.t -> 'a Facile.Invariant.unsetable_t
val argmin :
('a, 'b) Facile.Invariant.t array ->
('a -> 'c) -> int Facile.Invariant.unsetable_t
val min :
('a, 'b) Facile.Invariant.t array ->
('a -> 'c) -> 'a Facile.Invariant.unsetable_t
end
module type FD =
sig
type fd
type elt
val min :
Facile.Invariant.FD.fd ->
Facile.Invariant.FD.elt Facile.Invariant.unsetable_t
val max :
Facile.Invariant.FD.fd ->
Facile.Invariant.FD.elt Facile.Invariant.unsetable_t
val size :
Facile.Invariant.FD.fd -> int Facile.Invariant.unsetable_t
val is_var :
Facile.Invariant.FD.fd -> bool Facile.Invariant.unsetable_t
val unary :
?name:string ->
(Facile.Invariant.FD.fd -> 'a) ->
Facile.Invariant.FD.fd -> 'a Facile.Invariant.unsetable_t
end
module Fd :
sig
type fd = Var.Fd.t
type elt = Var.Fd.elt
val min : fd -> elt unsetable_t
val max : fd -> elt unsetable_t
val size : fd -> int unsetable_t
val is_var : fd -> bool unsetable_t
val unary : ?name:string -> (fd -> 'a) -> fd -> 'a unsetable_t
end
module SetFd :
sig
type fd = Var.SetFd.t
type elt = Var.SetFd.elt
val min : fd -> elt unsetable_t
val max : fd -> elt unsetable_t
val size : fd -> int unsetable_t
val is_var : fd -> bool unsetable_t
val unary : ?name:string -> (fd -> 'a) -> fd -> 'a unsetable_t
end
end
module Interval :
sig
val is_member : Facile.Var.Fd.t -> int -> int -> Facile.Var.Fd.t
val cstr :
Facile.Var.Fd.t -> int -> int -> Facile.Var.Fd.t -> Facile.Cstr.t
end
module FdArray :
sig
val min : Facile.Var.Fd.t array -> Facile.Var.Fd.t
val min_cstr :
Facile.Var.Fd.t array -> Facile.Var.Fd.t -> Facile.Cstr.t
val max : Facile.Var.Fd.t array -> Facile.Var.Fd.t
val max_cstr :
Facile.Var.Fd.t array -> Facile.Var.Fd.t -> Facile.Cstr.t
val get : Facile.Var.Fd.t array -> Facile.Var.Fd.t -> Facile.Var.Fd.t
val get_cstr :
Facile.Var.Fd.t array ->
Facile.Var.Fd.t -> Facile.Var.Fd.t -> Facile.Cstr.t
end
module Gcc :
sig
type level = Basic | Medium | High
val cstr :
?level:Facile.Gcc.level ->
Facile.Var.Fd.t array ->
(Facile.Var.Fd.t * int) array -> Facile.Cstr.t
end
module Opti :
sig
type mode = Restart | Continue
val minimize :
Facile.Goals.t ->
Facile.Var.Fd.t ->
?control:(int -> unit) ->
?step:int -> ?mode:Facile.Opti.mode -> (int -> 'a) -> 'a option
end
module Conjunto :
sig
val subset : Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Cstr.t
val cardinal : Facile.Var.SetFd.t -> Facile.Var.Fd.t
val smallest : Facile.Var.SetFd.t -> Facile.Var.Fd.t
val union :
Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Var.SetFd.t
val inter :
Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Var.SetFd.t
val all_disjoint : Facile.Var.SetFd.t array -> Facile.Cstr.t
val disjoint :
Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Cstr.t
val inside : int -> Facile.Var.SetFd.t -> unit
val outside : int -> Facile.Var.SetFd.t -> unit
val inf_min : Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Cstr.t
val order : Facile.Var.SetFd.t -> Facile.Var.SetFd.t -> Facile.Cstr.t
val order_with_card :
Facile.Var.SetFd.t ->
Facile.Var.Fd.t ->
Facile.Var.SetFd.t -> Facile.Var.Fd.t -> Facile.Cstr.t
val member :
Facile.Var.SetFd.t -> Facile.SetDomain.elt list -> Facile.Cstr.t
val mem : Facile.Var.Fd.t -> Facile.Var.SetFd.t -> Facile.Cstr.t
val sum_weight :
Facile.Var.SetFd.t -> (int * int) list -> Facile.Var.Fd.t
val atmost1 : Facile.Var.SetFd.t array -> int -> unit
end
module Easy :
sig
val i2e : int -> Facile.Arith.t
val fd2e : Facile.Var.Fd.t -> Facile.Arith.t
val ( +~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( *~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( -~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( /~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( **~ ) : Facile.Arith.t -> int -> Facile.Arith.t
val ( %~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( <=~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( <~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( >~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( =~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( <>~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( >=~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Cstr.t
val ( <=~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( <~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( >~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( =~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( <>~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( >=~~ ) : Facile.Arith.t -> Facile.Arith.t -> Facile.Arith.t
val ( &&~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( ||~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( =>~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( <=>~~ ) : Facile.Cstr.t -> Facile.Cstr.t -> Facile.Cstr.t
val ( &&~ ) : Facile.Goals.t -> Facile.Goals.t -> Facile.Goals.t
val ( ||~ ) : Facile.Goals.t -> Facile.Goals.t -> Facile.Goals.t
module Fd :
sig
type t = Var.Fd.t
type attr = Var.Attr.t
type domain = Domain.t
type elt = Domain.elt
type event = Var.Attr.event
val create : ?name:string -> domain -> t
val interval : ?name:string -> elt -> elt -> t
val array : ?name:string -> int -> elt -> elt -> t array
val elt : elt -> t
val is_var : t -> bool
val is_bound : t -> bool
val value : t -> (attr, elt) Var.concrete
val min : t -> elt
val max : t -> elt
val min_max : t -> elt * elt
val elt_value : t -> elt
val int_value : t -> elt
val size : t -> int
val member : t -> elt -> bool
val id : t -> int
val name : t -> string
val compare : t -> t -> int
val equal : t -> t -> bool
val fprint : out_channel -> t -> unit
val fprint_array : out_channel -> t array -> unit
val unify : t -> elt -> unit
val refine : t -> domain -> unit
val refine_low : t -> elt -> unit
val refine_up : t -> elt -> unit
val refine_low_up : t -> elt -> elt -> unit
val on_refine : event
val on_subst : event
val on_min : event
val on_max : event
val delay : event list -> t -> ?waking_id:int -> Cstr.t -> unit
val int : elt -> t
val subst : t -> elt -> unit
val unify_cstr : t -> elt -> Cstr.t
val remove : t -> elt -> unit
val values : t -> elt list
val iter : (elt -> unit) -> t -> unit
end
type ('a, 'b) concrete' =
('a, 'b) Facile.Var.concrete =
Unk of 'a
| Val of 'b
type concrete_fd =
(Facile.Easy.Fd.attr, Facile.Easy.Fd.elt) Facile.Easy.concrete'
end
end