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