sig
  module type S = sig type reason end
  module type T =
    sig
      module X : S
      type state
      type var = int
      type value = True | False | Unknown
      type lit
      val lit_of_var : EdosSolver.T.var -> bool -> EdosSolver.T.lit
      val initialize_problem :
        ?print_var:(Format.formatter -> int -> unit) ->
        ?buffer:bool -> int -> EdosSolver.T.state
      val copy : EdosSolver.T.state -> EdosSolver.T.state
      val propagate : EdosSolver.T.state -> unit
      val protect : EdosSolver.T.state -> unit
      val reset : EdosSolver.T.state -> unit
      val assignment : EdosSolver.T.state -> EdosSolver.T.value array
      val assignment_true : EdosSolver.T.state -> EdosSolver.T.var list
      val add_rule :
        EdosSolver.T.state -> EdosSolver.T.lit array -> X.reason list -> unit
      val associate_vars :
        EdosSolver.T.state ->
        EdosSolver.T.lit -> EdosSolver.T.var list -> unit
      val solve_all :
        (EdosSolver.T.state -> unit) ->
        EdosSolver.T.state -> EdosSolver.T.var -> bool
      val solve : EdosSolver.T.state -> EdosSolver.T.var -> bool
      val solve_lst : EdosSolver.T.state -> EdosSolver.T.var list -> bool
      val collect_reasons :
        EdosSolver.T.state -> EdosSolver.T.var -> X.reason list
      val collect_reasons_lst :
        EdosSolver.T.state -> EdosSolver.T.var list -> X.reason list
      val dump : EdosSolver.T.state -> (int * bool) list list
      val debug : bool -> unit
      val stats : EdosSolver.T.state -> unit
    end
  module M :
    functor (X : S->
      sig
        module X : sig type reason = X.reason end
        type state
        type var = int
        type value = True | False | Unknown
        type lit
        val lit_of_var : var -> bool -> lit
        val initialize_problem :
          ?print_var:(Format.formatter -> int -> unit) ->
          ?buffer:bool -> int -> state
        val copy : state -> state
        val propagate : state -> unit
        val protect : state -> unit
        val reset : state -> unit
        val assignment : state -> value array
        val assignment_true : state -> var list
        val add_rule : state -> lit array -> X.reason list -> unit
        val associate_vars : state -> lit -> var list -> unit
        val solve_all : (state -> unit) -> state -> var -> bool
        val solve : state -> var -> bool
        val solve_lst : state -> var list -> bool
        val collect_reasons : state -> var -> X.reason list
        val collect_reasons_lst : state -> var list -> X.reason list
        val dump : state -> (int * bool) list list
        val debug : bool -> unit
        val stats : state -> unit
      end
end