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`