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