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 = {
}
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 =
type
result =
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)