sig
  module R : sig type reason = Algo.Diagnostic.reason_int end
  module S :
    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
  type solver = {
    constraints : Algo.Depsolver_int.S.state;
    map : Common.Util.projection;
  }
  type dep_t =
      (Cudf_types.vpkg list * int list) list *
      (Cudf_types.vpkg * int list) list
  and pool = Algo.Depsolver_int.dep_t array
  and t =
      [ `CudfPool of Algo.Depsolver_int.pool
      | `SolverPool of Algo.Depsolver_int.pool ]
  type result =
      Success of (unit -> int list)
    | Failure of (unit -> Algo.Diagnostic.reason_int list)
  val init_pool_univ :
    global_constraints:bool ->
    Cudf.universe -> [> `CudfPool of Algo.Depsolver_int.pool ]
  val init_solver_pool :
    Common.Util.projection ->
    [< `CudfPool of Algo.Depsolver_int.pool ] ->
    'a list -> [> `SolverPool of Algo.Depsolver_int.pool ]
  val init_solver_cache :
    ?buffer:bool ->
    [< `SolverPool of Algo.Depsolver_int.pool ] -> Algo.Depsolver_int.S.state
  val solve :
    ?tested:bool array ->
    Algo.Depsolver_int.solver ->
    int option * int list -> Algo.Diagnostic.result_int
  val pkgcheck :
    bool ->
    (Algo.Diagnostic.result_int * (int option * int list) -> 'a) option ->
    Algo.Depsolver_int.solver -> bool array -> int -> bool
  val init_solver_univ :
    ?global_constraints:bool ->
    ?buffer:bool -> Cudf.universe -> Algo.Depsolver_int.solver
  val init_solver_closure :
    ?buffer:bool ->
    [< `CudfPool of Algo.Depsolver_int.pool ] ->
    int list -> Algo.Depsolver_int.solver
  val copy_solver : Algo.Depsolver_int.solver -> Algo.Depsolver_int.solver
  val reverse_dependencies : Cudf.universe -> int list array
  val dependency_closure_cache :
    ?maxdepth:int ->
    ?conjunctive:bool ->
    [< `CudfPool of Algo.Depsolver_int.pool ] ->
    int list -> Algo.Depsolver_int.S.var list
  val dependency_closure :
    ?maxdepth:int ->
    ?conjunctive:bool ->
    ?global_constraints:bool ->
    Cudf.universe -> Cudf.package list -> Cudf.package list
  val reverse_dependency_closure :
    ?maxdepth:int -> int list array -> int list -> int list
  val progressbar_init : Common.Util.Progress.t
  val progressbar_univcheck : Common.Util.Progress.t
end