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.
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;
}
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 : Cudf.universe -> pool
val init_solver_pool : < inttovar : int -> int;
vartoint : S.var -> S.var; .. > ->
pool -> 'a list -> pool
val init_solver_cache : ?buffer:bool -> pool -> S.state
val init_solver_univ : ?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
pool : dependencies and conflicts array idexed by package id
closure : subset of packages used to initialize the solver
val copy_solver : solver -> solver
return a copy of the state of the solver
val solve : solver -> Diagnostic_int.request -> result
low level call to the sat solver
val set_hard_constraints : solver -> ('a list list * 'b list) array -> bool
set_hard_constraints adds additional constraints to the solver. The rationale is that if the global constraints are satisfied and there is only **one** solution, then we can just fix this solution once for all and save precious time that would be otherwise spent to recompute this solution over and over again. Of cource if, either there is no solution, or if there are multiple solutions, then this is not possible anymore and we are forced to check if a request can be satisfied given a set of globla constraints.
val pkgcheck : bool ->
(Diagnostic_int.result * Diagnostic_int.request -> unit) option ->
solver -> int Pervasives.ref -> bool array -> int -> unit
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)