sig
  module type S = sig type reason end
  module M :
    functor (X : S->
      sig
        type state
        type var = int
        type lit
        val lit_of_var : Solver.M.var -> bool -> Solver.M.lit
        val initialize_problem :
          ?print_var:(Format.formatter -> int -> unit) ->
          int -> Solver.M.state
        val copy : Solver.M.state -> Solver.M.state
        val propagate : Solver.M.state -> unit
        val protect : Solver.M.state -> unit
        val reset : Solver.M.state -> unit
        type value = True | False | Unknown
        val assignment : Solver.M.state -> Solver.M.value array
        val add_un_rule :
          Solver.M.state -> Solver.M.lit -> X.reason list -> unit
        val add_bin_rule :
          Solver.M.state ->
          Solver.M.lit -> Solver.M.lit -> X.reason list -> unit
        val add_rule :
          Solver.M.state -> Solver.M.lit array -> X.reason list -> unit
        val associate_vars :
          Solver.M.state -> Solver.M.lit -> Solver.M.var list -> unit
        val solve : Solver.M.state -> Solver.M.var -> bool
        val solve_lst : Solver.M.state -> Solver.M.var list -> bool
        val collect_reasons : Solver.M.state -> Solver.M.var -> X.reason list
        val collect_reasons_lst :
          Solver.M.state -> Solver.M.var list -> X.reason list
      end
end