Module Dose_algo.Depsolver_int

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 : Dose_common.EdosSolver.T with module X = R
type solver = {
  1. constraints : S.state;
    (*

    the sat problem

    *)
  2. map : Dose_common.Util.projection;
    (*

    a map from cudf package ids to solver ids

    *)
  3. 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 = [
  1. | `SolverPool of pool
  2. | `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 =
  1. | Success of unit -> int list
    (*

    return a function providing the list of the cudf packages belonging to the installation set

    *)
  2. | 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 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.

  • 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 in l 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