Module Depsolver_int


module Depsolver_int: sig .. end
Dependency solver. Low Level API


Implementation of the EDOS algorithms (and more). This module respects the cudf semantic.

This module contains two type of functions. Normal functions work on a cudf universe. These are just a wrapper to _cache functions.

_cache functions work on a pool of ids that is a more compact representation of a cudf universe based on arrays of integers. _cache function can be used to avoid recreating the pool for each operation and therefore speed up operations.

val progressbar_init : Common.Util.Progress.t
progress bar
val progressbar_univcheck : Common.Util.Progress.t
include struct ... end
module R: sig .. end
module S: Common.EdosSolver.M(R)
class intprojection : int -> object .. end
associate a sat solver variable to a package id
class identity : object .. end
val init_map : Common.Util.IntHashtbl.key list -> 'a -> intprojection

type solver = {
   constraints : S.state; (*the sat problem*)
   map : intprojection; (*a map from cudf package ids to solver ids*)
}
low level solver data type
type dep_t = (Cudf_types.vpkg list * S.var list) list *
(Cudf_types.vpkg * S.var list) list
type pool_t = dep_t array 

type pool =
| SolverPool of pool_t
| CudfPool of pool_t

type result =
| Success of (unit -> int list)
| Failure of (unit -> Diagnostic_int.reason list)
val strip_solver_pool : pool -> pool_t
val strip_cudf_pool : pool -> pool_t
val init_pool_univ : global_constraints:bool -> Cudf.universe -> pool
val init_solver_pool : < inttovar : int -> int;
vartoint : S.var -> S.var; .. > ->
pool -> 'a list -> pool
this function creates an array indexed by solver ids that can be used to init the edos solver
val init_solver_cache : ?buffer:bool -> pool -> S.state
initalise the sat solver. operate only on solver ids
val solve : ?tested:bool array ->
solver -> Diagnostic_int.request -> Diagnostic_int.result
low level call to the sat solver
val pkgcheck : bool ->
(Diagnostic_int.result * Diagnostic_int.request -> unit) option ->
solver -> int Pervasives.ref -> bool array -> int -> unit
val init_solver_univ : ?global_constraints:bool ->
?buffer:bool -> Cudf.universe -> solver
low level constraint solver initialization
buffer : debug buffer to print out debug messages
univ : cudf package universe
val init_solver_closure : ?buffer:bool ->
pool -> Common.Util.IntHashtbl.key list -> solver
low level constraint solver initialization
buffer : debug buffer to print out debug messages
closure : subset of packages used to initialize the solver
val copy_solver : solver -> solver
return a copy of the state of the solver
val reverse_dependencies : Cudf.universe -> int list array
reverse_dependencies index return an array that associates to a package id i the list of all packages ids that have a dependency on i.
val dependency_closure_cache : ?maxdepth:int ->
?conjunctive:bool ->
pool -> int list -> S.var list
val dependency_closure : ?maxdepth:int ->
?conjunctive:bool -> Cudf.universe -> Cudf.package list -> Cudf.package list
dependency_closure index l return the union of the dependency closure of all packages in l .
maxdepth : the maximum cone depth (infinite by default)
conjunctive : consider only conjunctive dependencies (false by default)
universe : the package universe
pkglist : a subset of universe
val reverse_dependency_closure : ?maxdepth:int -> int list array -> int list -> int list
return the dependency closure of the reverse dependency graph. The visit is bfs.
maxdepth : the maximum cone depth (infinite by default)