package dose3
Install
Dune Dependency
Authors
Maintainers
Sources
md5=bc99cbcea8fca29dca3ebbee54be45e1
sha512=98dc4bd28e9f4aa8384be71b31783ae1afac577ea587118b8457b554ffe302c98e83d0098971e6b81803ee5c4f2befe3a98ef196d6b0da8feb4121e982ad5c2f
doc/dose3.algo/Dose_algo/Depsolver_int/index.html
Module Dose_algo.Depsolver_int
Source
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.
type solver = {
constraints : S.state;
(*the sat problem
*)map : Dose_common.Util.projection;
(*a map from cudf package ids to solver ids
*)globalid : (bool * bool) * int;
(*(keep_constrains,global_constrains),gui) where gid is the last index of the cudfpool. Used to encode a 'dummy' package and to enforce global constraints. keep_constrains and global_constrains are true if either keep_constrains or global_constrains are enforceble.
*)
}
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
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
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. The boolean associate to the cudfpool is true if keep_constrains are present in the universe. The last index of the pool is the globalid
type result =
| Success of unit -> int list
(*return a function providing the list of the cudf packages belonging to the installation set
*)| Failure of unit -> Diagnostic.reason_int list
(*return a function with the failure explanations
*)
val init_pool_univ :
global_constraints:global_constraints ->
Cudf.universe ->
[> `CudfPool of bool * 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. The last index of the pool is the globalid.
val init_solver_pool :
Dose_common.Util.projection ->
[< `CudfPool of bool * 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
Initalise the sat solver. Operates only on solver ids SolverPool
val solve :
?tested:bool array ->
explain:bool ->
solver ->
Diagnostic.request_int ->
Diagnostic.result_int
Call the sat solver
val pkgcheck :
((Diagnostic.result_int * Diagnostic.request_int) -> unit) option ->
bool ->
solver ->
bool array ->
int ->
bool
pkgcheck callback solver tested id
. This function is used to "distcheck" a list of packages
val init_solver_univ :
global_constraints:global_constraints ->
?buffer:bool ->
?explain:bool ->
Cudf.universe ->
solver
Constraint solver initialization
val init_solver_closure :
global_constraints:global_constraints ->
?buffer:bool ->
[< `CudfPool of bool * pool ] ->
int list ->
solver
Constraint solver initialization
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 bool * pool ] ->
int list ->
int list
dependency_closure_cache pool l
return the union of the dependency closure of all packages in l
in the given pool of packages. The result always contains the globalid.
return the dependency closure of the reverse dependency graph. The visit is bfs.
This function use a memoization strategy.
Progress Bars