/usr/lib/ocaml/dose3/depsolver.mli is in libdose3-ocaml-dev 3.3~beta1-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 | (**************************************************************************************)
(* Copyright (C) 2009 Pietro Abate <pietro.abate@pps.jussieu.fr> *)
(* Copyright (C) 2009 Mancoosi Project *)
(* *)
(* This library is free software: you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of the *)
(* License, or (at your option) any later version. A special linking *)
(* exception to the GNU Lesser General Public License applies to this *)
(* library, see the COPYING file for more information. *)
(**************************************************************************************)
(** Dependency solver. Implementation of the Edos algorithms *)
(** the solver is an abstract data type associated to a universe *)
type solver
(** initialize the solver. If [check] is true (default), then check
for universe consistency (cf. Cudf_checker.is_consistent) *)
val load : ?check : bool -> Cudf.universe -> solver
(** Turn a result from Diagnostic_int into one of Diagnostic *)
val result : Depsolver_int.identity -> Cudf.universe -> Diagnostic_int.result -> Diagnostic.result
(** Turn a request from Diagnostic_int into one of Diagnostic *)
val request : Cudf.universe -> Diagnostic_int.request -> Diagnostic.request
(** check if the given package can be installed in the universe
@param global_constraints : enforce global constraints on the given
universe. In particular packages marked as `Keep_package must be always
installed. Default false.
*)
val edos_install : ?global_constraints:bool -> Cudf.universe -> Cudf.package -> Diagnostic.diagnosis
(** check if the give package list can be installed in the universe
@param global_constraints : enforce global constraints on the given
universe. In particular packages marked as `Keep_package must be always
installed. Default false.
*)
val edos_coinstall : ?global_constraints:bool -> Cudf.universe -> Cudf.package list -> Diagnostic.diagnosis
(** accept a list of list of packages and return the coinstallability test of
the cartesian product. *)
val edos_coinstall_prod : ?global_constraints:bool -> Cudf.universe -> Cudf.package list list -> Diagnostic.diagnosis list
(** remove uninstallable packages from the universe . global_constraints is true
by default *)
val trim : ?global_constraints:bool -> Cudf.universe -> Cudf.universe
(** return the list of broken packages *)
val find_broken : ?global_constraints:bool -> Cudf.universe -> Cudf.package list
(** return the list of installable packages *)
val find_installable : ?global_constraints:bool -> Cudf.universe -> Cudf.package list
(** return the list of broken packages *)
val find_listbroken : ?global_constraints:bool -> Cudf.universe ->
Cudf.package list -> Cudf.package list
(** return the list of installable packages *)
val find_listinstallable : ?global_constraints:bool -> Cudf.universe ->
Cudf.package list -> Cudf.package list
(** [univcheck ] check if all packages in the universe can be installed.
Since not all packages are directly tested for installation, if a packages
is installable, the installation might be empty. To obtain an installation
set for each installable packages, the correct procedure is to iter on the
list of packages.
@param callback : execute a function for each package. This function can
have side effects and can be used to collect the installation set or the
failure reason.
@param global_constraints : enforce global constraints on the given
universe. In particular packages marked as `Keep_package must be always
installed. Default true.
@return the number of broken packages
*)
val univcheck : ?global_constraints:bool -> ?callback:(Diagnostic.diagnosis -> unit) -> Cudf.universe -> int
(** [listcheck ~callback:c solver l] check if all packages in [l] can be
installed.
Invariant : l is a subset of universe can be installed in the solver universe.
@param callback : execute a function for each package.
@param global_constraints : enforce global constraints on the given universe.
@return the number of broken packages
*)
val listcheck : ?global_constraints:bool -> ?callback:(Diagnostic.diagnosis -> unit) ->
Cudf.universe -> Cudf.package list -> int
(** [dependency_closure universe l] compute the dependencies closure
of the give package list.
Invariant : l must be a subset of universe *)
val dependency_closure : ?maxdepth:int -> ?conjunctive:bool ->
Cudf.universe -> Cudf.package list -> Cudf.package list
(** [reverse_dependencies univ ] compute the reverse dependency list of all
packages in the universe [univ] *)
val reverse_dependencies :
Cudf.universe -> (Cudf.package list) Common.CudfAdd.Cudf_hashtbl.t
(** [reverse_dependencies_closure univ ] compute the reverse dependency list of all
packages in [l] in the universe [univ] *)
val reverse_dependency_closure : ?maxdepth:int ->
Cudf.universe -> Cudf.package list -> Cudf.package list
type enc = Cnf | Dimacs
(** [output_clauses enc univ] return a string encoded accordingly to [enc]
(default cnf).
@param global_constraints : enforce global constraints on the given universe.
*)
val output_clauses : ?global_constraints:bool -> ?enc:enc -> Cudf.universe -> string
type solver_result =
|Sat of (Cudf.preamble option * Cudf.universe)
|Unsat of Diagnostic.diagnosis option
|Error of string
(** [check_request] check if there exists a solution for the give cudf document
if ?cmd is specified, it will be used to call an external cudf solver to
satisfy the request.
if ?criteria is specified it will be used as optimization criteria.
if ?explain is specified and there is no solution for the give request, the
result will contain the failure reason.
*)
val check_request : ?cmd : string -> ?callback:(int array * Diagnostic.diagnosis -> unit) ->
?criteria:string -> ?explain : bool -> Cudf.cudf -> solver_result
(** Same as [check_request], but allows to specify any function to call the
external solver. It should raise [Depsolver.Unsat] on failure *)
val check_request_using:
?call_solver:(Cudf.cudf -> Cudf.preamble option * Cudf.universe) ->
?callback:(int array * Diagnostic.diagnosis -> unit) ->
?criteria:string ->
?explain : bool ->
Cudf.cudf -> solver_result
|