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