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