Module Dose_algo.Depsolver_int
module R : sig ... end
Sat Solver instance
module S : Dose_common.EdosSolver.T with module X = R
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
type global_constraints
= (Cudf_types.vpkglist * int list) list
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
and pool
= dep_t array
and t
=[
|
`SolverPool of pool
|
`CudfPool of bool * pool
]
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
val init_solver_cache : ?buffer:bool -> ?explain:bool -> [< `SolverPool of pool ] -> S.state
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
- parameter tested:
optional int array used to cache older results
- parameter explain:
if try we add all the information needed to create the explanation graph
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
- parameter buffer
debug buffer to print out debug messages
- parameter univ
cudf package universe
val init_solver_closure : global_constraints:global_constraints -> ?buffer:bool -> [< `CudfPool of bool * pool ] -> int list -> solver
Constraint solver initialization
- parameter buffer
debug buffer to print out debug messages
- parameter pool
dependencies and conflicts array idexed by package id
- parameter closure
subset of packages used to initialize the solver
val reverse_dependencies : Cudf.universe -> int list array
reverse_dependencies index
return an array that associates to a package idi
the list of all packages ids that have a dependency oni
.- parameter mdf
the package universe
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 inl
in the given pool of packages. The result always contains the globalid.- parameter maxdepth
the maximum cone depth (infinite by default)
- parameter 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.
- parameter maxdepth
the maximum cone depth (infinite by default)
- parameter index
the package universe
- parameter idlist
a subset of
index
This function use a memoization strategy.
val progressbar_init : Dose_common.Util.Progress.t
Progress Bars
val progressbar_univcheck : Dose_common.Util.Progress.t