sig
  module X : sig type reason = Diagnostic.reason_int 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