(***********************************************************************)
(*                                                                     *)
(*                           FaCiLe                                    *)
(*                 A Functional Constraint Library                     *)
(*                                                                     *)
(*            Nicolas Barnier, Pascal Brisset, LOG, CENA               *)
(*                                                                     *)
(* Copyright 2004 CENA. All rights reserved. This file is distributed  *)
(* under the terms of the GNU Lesser General Public License.           *)
(***********************************************************************)
(* $Id: facile.mli,v 1.96 2004/09/03 13:25:55 barnier Exp $ *)

(* Module [Facile]: end-user interface to the FaCiLe library *)

module Domain :
    sig
      type elt = int
      type t
      val empty : t
      val create : elt list -> t
      val unsafe_create : elt list -> t
      val interval : elt -> elt -> t
      val int : t
      val boolean : t
      val is_empty : t -> bool
      val size : t -> elt
      val min : t -> elt
      val max : t -> elt
      val min_max : t -> elt * elt
      val iter : (elt -> unit) -> t -> unit
      val interval_iter : (elt -> elt -> unit) -> t -> unit
      val member : elt -> t -> bool
      val values : t -> elt list
      val fprint_elt : out_channel -> elt -> unit
      val fprint : out_channel -> t -> unit
      val sprint : t -> string
      val included : t -> t -> bool
      val add : elt -> t -> t
      val remove : elt -> t -> t
      val remove_up : elt -> t -> t
      val remove_low : elt -> t -> t
      val remove_low_up : elt -> elt -> t -> t
      val remove_closed_inter : elt -> elt -> t -> t
      val intersection : t -> t -> t
      val union : t -> t -> t
      val difference : t -> t -> t
      val diff : t -> t -> t
      val remove_min : t -> t
      val minus : t -> t
      val plus : t -> elt -> t
      val times : t -> elt -> t
      val smallest_geq : t -> elt -> elt
      val greatest_leq : t -> elt -> elt
      val largest_hole_around : t -> elt -> elt * elt
      val choose : (elt -> elt -> bool) -> t -> elt
      val compare : t -> t -> elt
      val compare_elt : elt -> elt -> elt
      val disjoint : t -> t -> bool
    end

module SetDomain :
    sig
      module S : sig
        type t
        val empty : t
        val is_empty : t -> bool
        val mem : int -> t -> bool
        val add : int -> t -> t
        val singleton : int -> t
        val remove : int -> t -> t
        val union : t -> t -> t
        val inter : t -> t -> t
        val diff : t -> t -> t
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val subset : t -> t -> bool
        val iter : (int -> unit) -> t -> unit
        val cardinal : t -> int
        val elements : t -> int list
        val min_elt : t -> int
        val max_elt : t -> int
        val choose : t -> int
        val remove_up : int -> t -> t
        val remove_low : int -> t -> t
      end
      type elt = S.t
      type t
      val min : t -> elt
      val max : t -> elt
      val min_max : t -> elt * elt
      val mem : elt -> t -> bool
      val interval : elt -> elt -> t
      val fprint_elt : out_channel -> elt -> unit
      val fprint : out_channel -> t -> unit
      val included : t -> t -> bool
      val iter : (elt -> 'a) -> t -> 'a
      val values : t -> elt list
      val elt_of_list : int list -> elt
    end

module Stak :
    sig
      type level
      val older : level -> level -> bool
      val size : unit -> int
      val depth : unit -> int
      val level : unit -> level
      val levels : unit -> level list
      val nb_choice_points : unit -> int
      exception Level_not_found of level
      val cut : level -> unit
      exception Fail of string
      val fail : string -> 'a
      val trail : (unit -> unit) -> unit
      type 'a ref
      val ref : 'a -> 'a ref
      val set : 'a ref -> 'a -> unit
      val get : 'a 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 : int -> ('a, 'b) t
	    val get : ('a, 'b) t -> ('a, 'b) Hashtbl.t
	    val add : ('a, 'b) t -> 'a -> 'b -> unit
	    val find : ('a, 'b) t -> 'a -> 'b
	    val mem : ('a, 'b) t -> 'a -> bool
	    val remove : ('a, 'b) t -> 'a -> unit
	    val replace : ('a, 'b) t -> 'a -> 'b -> unit
	    val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
	    val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
	  end
end

module Cstr :
    sig
      exception DontKnow
      type priority
      val immediate : priority
      val normal : priority
      val later : priority
      type t
      val id : t -> int
      val name : t -> string
      val priority : t -> priority
      val fprint : out_channel -> t -> unit
      val is_solved : t -> bool
      val create :
	  ?name:string ->
	    ?nb_wakings:int ->
	      ?fprint:(out_channel -> unit) ->
  	      	?priority:priority ->
	    	  ?init:(unit -> unit) ->
		    ?check:(unit -> bool) ->
		      ?not:(unit -> t) ->
		      	(int -> bool) ->
		      	  (t -> unit) ->
			    t
      val post : t -> unit
      val init : t -> unit
      val one : t
      val zero : t
      val active_store : unit -> t list
    end

module Var :
    sig
      module type ATTR =
  	sig
	  type t
	  type domain
	  type elt
	  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 Attr :
	  ATTR with type domain = Domain.t and type elt = int
      module SetAttr :
	  ATTR with type domain = SetDomain.t and type elt = SetDomain.S.t

      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 -> 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

      module type FD = sig
   	include BASICFD
	val remove : t -> elt -> unit
  	val values : t -> elt list
  	val iter : (elt -> unit) -> t -> unit
      end

      module Fd : FD with
      type domain = Domain.t and
      type elt = Domain.elt and
      type attr = Attr.t and
      type event = Attr.event

      module SetFd : BASICFD with
        type domain = SetDomain.t and
        type elt = SetDomain.S.t and
        type attr = SetAttr.t and
        type event = SetAttr.event

      val delay : Attr.event list -> Fd.t -> ?waking_id:int -> Cstr.t -> unit
    end
module Reify :
    sig
      val boolean : ?delay_on_negation:bool -> Cstr.t -> Var.Fd.t
      val cstr : ?delay_on_negation:bool -> Cstr.t -> Var.Fd.t -> Cstr.t
      val (||~~) : Cstr.t -> Cstr.t -> Cstr.t
      val (&&~~) : Cstr.t -> Cstr.t -> Cstr.t
      val (<=>~~) : Cstr.t -> Cstr.t -> Cstr.t
      val xor : Cstr.t -> Cstr.t -> Cstr.t
      val not : Cstr.t -> Cstr.t
      val (=>~~) : Cstr.t -> Cstr.t -> Cstr.t
    end
module Alldiff :
    sig
      type algo =
          Lazy
      	| Bin_matching of Var.Fd.event
      val cstr : ?algo:algo -> Var.Fd.t array -> Cstr.t
    end
module Goals :
    sig
      type t
      val name : t -> string
      val fprint : out_channel ->