package dose3
Dose library (part of Mancoosi tools)
Install
Dune Dependency
Authors
Maintainers
Sources
dose3-7.0.0.tar.gz
md5=bc99cbcea8fca29dca3ebbee54be45e1
sha512=98dc4bd28e9f4aa8384be71b31783ae1afac577ea587118b8457b554ffe302c98e83d0098971e6b81803ee5c4f2befe3a98ef196d6b0da8feb4121e982ad5c2f
doc/src/dose3.algo/depsolver_int.ml.html
Source file depsolver_int.ml
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 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
(**************************************************************************************) (* 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. *) (**************************************************************************************) open ExtLib open Dose_common let progressbar_init = Util.Progress.create "Depsolver_int.init_solver" let progressbar_univcheck = Util.Progress.create "Depsolver_int.univcheck" include Util.Logging (struct let label = "Depsolver_int.init_solver" end) module R = struct type reason = Diagnostic.reason_int end module S = EdosSolver.M (R) type solver = { constraints : S.state; map : Util.projection; globalid : (bool * bool) * int } type global_constraints = (Cudf_types.vpkglist * int list) list type dep_t = (Cudf_types.vpkg list * S.var list) list * (Cudf_types.vpkg * S.var list) list and pool = dep_t array and t = [ `SolverPool of pool | `CudfPool of bool * pool ] type result = | Success of (unit -> int list) | Failure of (unit -> Diagnostic.reason_int list) (* cudf uid -> cudf uid array . Here we assume cudf uid are sequential and we can use them as an array index *) let init_pool_univ ~global_constraints univ = (* the last element of the array *) let size = Cudf.universe_size univ in let keep = Hashtbl.create 200 in let pool = (* here I initalize the pool to size + 1, that is I reserve one spot * to encode the global constraints associated with the universe. * However, since they are global, I've to add the at the end, after * I have analyzed all packages in the universe. *) Array.init (size + 1) (fun uid -> try if uid = size then ([], []) (* the last index *) else let pkg = Cudf.package_by_uid univ uid in let dll = List.map (fun vpkgs -> (vpkgs, CudfAdd.resolve_vpkgs_int univ vpkgs)) pkg.Cudf.depends in let cl = List.filter_map (fun vpkg -> match CudfAdd.resolve_vpkg_int univ vpkg with | [] -> None | l -> Some (vpkg, l)) pkg.Cudf.conflicts in (if pkg.Cudf.installed then match pkg.Cudf.keep with | `Keep_none -> () | `Keep_package -> List.iter (fun id -> CudfAdd.add_to_package_list keep (pkg.Cudf.package, None) id) (CudfAdd.resolve_vpkg_int univ (pkg.Cudf.package, None)) | `Keep_version -> CudfAdd.add_to_package_list keep (pkg.Cudf.package, Some (`Eq, pkg.Cudf.version)) uid | `Keep_feature -> List.iter (function | (name, None) -> List.iter (fun id -> CudfAdd.add_to_package_list keep (name, None) id) (CudfAdd.resolve_vpkg_int univ (name, None)) | (name, Some (`Eq, v)) -> List.iter (fun id -> CudfAdd.add_to_package_list keep (name, Some (`Eq, v)) id) (CudfAdd.resolve_vpkg_int univ (name, Some (`Eq, v)))) pkg.Cudf.provides) ; (dll, cl) with Not_found -> fatal "Package uid (%d) not found during solver pool initialization. \ Packages uid must have no gaps in the given universe" uid) in let keep_dll = Hashtbl.fold (fun cnstr { contents = l } acc -> ([cnstr], l) :: acc) keep global_constraints in pool.(size) <- (keep_dll, []) ; `CudfPool (keep_dll <> [], pool) (** this function creates an array indexed by solver ids that can be used to init the edos solver *) let init_solver_pool map (`CudfPool (_keep_constraints, cudfpool)) closure = let convert (dll, cl) = let sdll = List.map (fun (vpkgs, uidl) -> (vpkgs, List.map map#vartoint uidl)) dll in let scl = (* ignore conflicts that are not in the closure. * if nobody depends on a conflict package, then it is irrelevant. * This requires a leap of faith in the user ability to build an * appropriate closure. If the closure is wrong, you are on your own *) List.map (fun (vpkg, uidl) -> let l = List.filter_map (fun uid -> try Some (map#vartoint uid) with Not_found -> debug "Dropping Conflict %s" (Cudf_types_pp.string_of_vpkg vpkg) ; None) uidl in (vpkg, l)) cl in (sdll, scl) in let solverpool = Array.init (List.length closure) (fun sid -> convert cudfpool.(map#inttovar sid)) in `SolverPool solverpool (** initalise the sat solver. operate only on solver ids *) let init_solver_cache ?(buffer = false) ?(explain = true) (`SolverPool varpool) = let num_conflicts = ref 0 in let num_disjunctions = ref 0 in let num_dependencies = ref 0 in let if_explain l = if explain then l else [] in let varsize = Array.length varpool in let add_depend constraints vpkgs pkg_id l = let lit = S.lit_of_var pkg_id false in if List.length l = 0 then S.add_rule constraints [| lit |] (if_explain [Diagnostic.MissingInt (pkg_id, vpkgs)]) else let lits = List.map (fun id -> S.lit_of_var id true) l in num_disjunctions := !num_disjunctions + List.length lits ; S.add_rule constraints (Array.of_list (lit :: lits)) (if_explain [Diagnostic.DependencyInt (pkg_id, vpkgs, l)]) ; if List.length lits > 1 then S.associate_vars constraints (S.lit_of_var pkg_id true) l in let conflicts = Util.IntPairHashtbl.create (varsize / 10) in let add_conflict constraints vpkg (i, j) = if i <> j then let pair = (min i j, max i j) in (* we get rid of simmetric conflicts *) if not (Util.IntPairHashtbl.mem conflicts pair) then ( incr num_conflicts ; Util.IntPairHashtbl.add conflicts pair () ; let p = S.lit_of_var i false in let q = S.lit_of_var j false in S.add_rule constraints [| p; q |] (if_explain [Diagnostic.ConflictInt (i, j, vpkg)])) in let exec_depends constraints pkg_id dll = List.iter (fun (vpkgs, dl) -> incr num_dependencies ; add_depend constraints vpkgs pkg_id dl) dll in let exec_conflicts constraints pkg_id cl = List.iter (fun (vpkg, l) -> List.iter (fun id -> add_conflict constraints vpkg (pkg_id, id)) l) cl in Util.Progress.set_total progressbar_init varsize ; let constraints = S.initialize_problem ~buffer varsize in Array.iteri (fun id (dll, cl) -> Util.Progress.progress progressbar_init ; exec_depends constraints id dll ; exec_conflicts constraints id cl) varpool ; Util.IntPairHashtbl.clear conflicts ; debug "n. disjunctions %d" !num_disjunctions ; debug "n. dependencies %d" !num_dependencies ; debug "n. conflicts %d" !num_conflicts ; S.propagate constraints ; constraints (** low level call to the sat solver @param tested: optional int array used to cache older results *) let solve ?tested ~explain solver request = S.reset solver.constraints ; let result solve collect var = (* Real call to the SAT solver *) if solve solver.constraints var then if explain then ( let l = S.assignment_true solver.constraints in if not (Option.is_none tested) then List.iter (fun i -> (Option.get tested).(i) <- true) l ; Diagnostic.SuccessInt (fun [@ocaml.warning "-27"] ?(all = false) () -> l)) else ( (if not (Option.is_none tested) then let l = S.assignment_true solver.constraints in List.iter (fun i -> (Option.get tested).(i) <- true) l) ; Diagnostic.SuccessInt (fun [@ocaml.warning "-27"] ?(all = false) () -> [])) else if explain then Diagnostic.FailureInt (fun () -> collect solver.constraints var) else Diagnostic.FailureInt (fun () -> []) in match (request, solver.globalid) with | ([], ((false, false), _)) -> Diagnostic.SuccessInt (fun [@ocaml.warning "-27"] ?(all = false) () -> []) | ([], (((_, true) | (true, _)), gid)) -> result S.solve S.collect_reasons (solver.map#vartoint gid) | ([i], ((false, false), _)) -> result S.solve S.collect_reasons (solver.map#vartoint i) | (l, ((false, false), _)) -> let il = List.map solver.map#vartoint l in result S.solve_lst S.collect_reasons_lst il | (l, (_, gid)) -> let il = List.map solver.map#vartoint (gid :: l) in result S.solve_lst S.collect_reasons_lst il (* this function is used to "distcheck" a list of packages. The id is a cudfpool index *) let pkgcheck callback explain solver tested id = let res = Util.Progress.progress progressbar_univcheck ; if not tested.(id) then solve ~tested ~explain solver [id] else if (* this branch is true only if the package was previously added to the tested packages and therefore it is installable if all = true then the solver is called again to provide the list of installed packages despite the fact the the package was already tested. This is done to provide one installation set for each package in the universe *) explain then let f ?(all = false) () = if all then match solve solver ~explain [id] with | Diagnostic.SuccessInt f_int -> f_int () | Diagnostic.FailureInt _ -> assert false (* impossible *) else [] in Diagnostic.SuccessInt f (* avoid to allocate anything on the stack if not stricly needed *) else Diagnostic.SuccessInt (fun [@ocaml.warning "-27"] ?(all = false) () -> []) in match (callback, res) with | (None, Diagnostic.SuccessInt _) -> true | (None, Diagnostic.FailureInt _) -> false | (Some f, Diagnostic.SuccessInt _) -> f (res, [id]) ; true | (Some f, Diagnostic.FailureInt _) -> f (res, [id]) ; false (** low level constraint solver initialization @param buffer debug buffer to print out debug messages @param univ cudf package universe *) let init_solver_univ ~global_constraints ?(buffer = false) ?(explain = true) univ = let map = new Util.identity in (* here we convert a cudfpool in a varpool. The assumption * that cudf package identifiers are contiguous is essential ! *) let (`CudfPool (keep_constraints, pool)) = init_pool_univ ~global_constraints univ in let varpool = `SolverPool pool in let constraints = init_solver_cache ~buffer ~explain varpool in let gid = Cudf.universe_size univ in let global_constraints = global_constraints <> [] in { constraints; map; globalid = ((keep_constraints, global_constraints), gid) } (* pool = cudf pool - closure = dependency clousure . cudf uid list *) (** low level constraint solver initialization @param buffer debug buffer to print out debug messages @param pool dependencies and conflicts array idexed by package id @param closure subset of packages used to initialize the solver *) let init_solver_closure ~global_constraints ?(buffer = false) (`CudfPool (keep_constraints, cudfpool)) closure = let gid = Array.length cudfpool - 1 in let global_constraints = global_constraints <> [] in let map = new Util.intprojection (List.length closure) in List.iter map#add closure ; let varpool = init_solver_pool map (`CudfPool (keep_constraints, cudfpool)) closure in let constraints = init_solver_cache ~buffer varpool in { constraints; map; globalid = ((keep_constraints, global_constraints), gid) } (** return a copy of the state of the solver *) let copy_solver solver = { solver with constraints = S.copy solver.constraints } (***********************************************************) (** [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]. @param mdf the package universe *) let reverse_dependencies univ = let size = Cudf.universe_size univ in let reverse = Array.create size [] in Cudf.iteri_packages (fun i p -> List.iter (fun ll -> List.iter (fun q -> let j = CudfAdd.pkgtoint univ q in if i <> j then if not (List.mem i reverse.(j)) then reverse.(j) <- i :: reverse.(j)) ll) (CudfAdd.who_depends univ p)) univ ; reverse let dependency_closure_cache ?(maxdepth = max_int) ?(conjunctive = false) (`CudfPool (_, cudfpool)) idlist = let queue = Queue.create () in let globalid = Array.length cudfpool - 1 in let visited = Hashtbl.create (2 * List.length idlist) in List.iter (fun e -> Queue.add (e, 0) queue) (CudfAdd.normalize_set (globalid :: idlist)) ; while Queue.length queue > 0 do let (id, level) = Queue.take queue in if (not (Hashtbl.mem visited id)) && level < maxdepth then ( Hashtbl.add visited id () ; let (l, _) = cudfpool.(id) in List.iter (function | (_, [i]) when conjunctive = true -> if not (Hashtbl.mem visited i) then Queue.add (i, level + 1) queue | (_, dsj) when conjunctive = false -> List.iter (fun i -> if not (Hashtbl.mem visited i) then Queue.add (i, level + 1) queue) dsj | _ -> ()) l) done ; Hashtbl.fold (fun k _ l -> k :: l) visited [] (* XXX : elements in idlist should be included only if because * of circular dependencies *) (** return the dependency closure of the reverse dependency graph. The visit is bfs. @param maxdepth the maximum cone depth (infinite by default) @param index the package universe @param idlist a subset of [index] This function use a memoization strategy. *) let reverse_dependency_closure ?(maxdepth = max_int) reverse = let h = Hashtbl.create (Array.length reverse) in let cmp : int -> int -> bool = ( = ) in fun idlist -> try Hashtbl.find h (idlist, maxdepth) with Not_found -> let queue = Queue.create () in let visited = Hashtbl.create (List.length idlist) in List.iter (fun e -> Queue.add (e, 0) queue) (List.unique ~cmp idlist) ; while Queue.length queue > 0 do let (id, level) = Queue.take queue in if (not (Hashtbl.mem visited id)) && level < maxdepth then ( Hashtbl.add visited id () ; List.iter (fun i -> if not (Hashtbl.mem visited i) then Queue.add (i, level + 1) queue) reverse.(id)) done ; let result = Hashtbl.fold (fun k _ l -> k :: l) visited [] in Hashtbl.add h (idlist, maxdepth) result ; result
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>