Module Algo.Depsolver_int

module Depsolver_int: sig .. end


Dependency solver. Low Level API

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.

module R: sig .. end
Sat Solver instance
module S: Common.EdosSolver.T  with module X = R
type solver = {
   constraints : S.state;
   map : Common.Util.projection;
}
internal state of the sat solver. The map allows to transform sat solver variables (that must be contiguous) to integers representing the id of a package
type dep_t = (Cudf_types.vpkg list * int list) list * (Cudf_types.vpkg * int list) list 
Solver Package Pool. pool_t is an array where each index is an solver variable and the content of the array associates cudf dependencies to a list of solver varialbles representing a package
type pool = dep_t array 
A pool can either be a low level representation of the universe where all integers are interpreted as solver variables or a universe where all integers are interpreted as cudf package indentifiers
type t = [ `CudfPool of pool
| `SolverPool of 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 pool ]
Given a cudf universe , this function returns a CudfPool. We assume that cudf uid are sequential and we can use them as an array index
val init_solver_pool : Common.Util.projection ->
[< `CudfPool of pool ] ->
'a list -> [> `SolverPool of pool ]
this function creates an array indexed by solver ids that can be used to init the edos solver. Return a SolverPool
val init_solver_cache : ?buffer:bool ->
[< `SolverPool of pool ] -> S.state
Initalise the sat solver. Operates only on solver ids SolverPool
val solve : ?tested:bool array ->
solver ->
int option * int list -> Algo.Diagnostic.result_int
Call the sat solver
val pkgcheck : bool ->
(Algo.Diagnostic.result_int * (int option * int list) -> 'a) option ->
solver -> bool array -> int -> bool
val init_solver_univ : ?global_constraints:bool ->
?buffer:bool -> Cudf.universe -> solver
Constraint solver initialization
buffer : debug buffer to print out debug messages
val init_solver_closure : ?buffer:bool ->
[< `CudfPool of pool ] ->
int list -> solver
Constraint solver initialization
buffer : debug buffer to print out debug messages
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 ->
[< `CudfPool of pool ] ->
int list -> S.var list
val dependency_closure : ?maxdepth:int ->
?conjunctive:bool ->
?global_constraints: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)
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)
val progressbar_init : Common.Util.Progress.t

Progress Bars


val progressbar_univcheck : Common.Util.Progress.t