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