From 0e903619a662f47aa536c4db0c1118ccd22ad519 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sat, 18 Jan 2025 18:44:21 +0000 Subject: [PATCH] refactor(pkg): inline [Solver_core] (#11321) Signed-off-by: Rudi Grinberg --- src/dune_pkg/opam_solver.ml | 375 ++++++++++++++++++++++++++++++++++- src/dune_pkg/solver_core.ml | 367 ---------------------------------- src/dune_pkg/solver_core.mli | 15 -- 3 files changed, 374 insertions(+), 383 deletions(-) delete mode 100644 src/dune_pkg/solver_core.ml delete mode 100644 src/dune_pkg/solver_core.mli diff --git a/src/dune_pkg/opam_solver.ml b/src/dune_pkg/opam_solver.ml index 747e72a5588..31e44c03629 100644 --- a/src/dune_pkg/opam_solver.ml +++ b/src/dune_pkg/opam_solver.ml @@ -559,7 +559,380 @@ module Solver = struct Input.virtual_role [ impl ] ;; - module Solver = Solver_core.Make (Input) + module Solver = struct + (* Copyright (C) 2013, Thomas Leonard + *See the README file for details, or visit http://0install.net. + *) + module Model = Input + + (* We attach this data to each SAT variable. *) + module SolverData = struct + [@@@ocaml.warning "-37"] + + type t = + (* If the SAT variable is True then we selected this... *) + | ImplElem of Model.impl + | Role of Model.Role.t + + let pp = function + | ImplElem impl -> Model.pp_impl impl + | Role role -> Model.Role.pp role + ;; + end + + module S = Sat.Make (SolverData) + + type decision_state = + (* The next candidate to try *) + | Undecided of S.lit + (* The dependencies to check next *) + | Selected of Model.dependency list + | Unselected + + module Candidates = struct + type t = + { role : Model.Role.t + ; clause : S.at_most_one_clause option + ; vars : (S.lit * Model.impl) list + ; dummy_impl : Model.impl option + } + + let[@ocaml.warning "-32"] is_dummy t impl = + match t.dummy_impl with + | None -> false + | Some dummy_impl -> dummy_impl == impl + ;; + + let create role clause vars dummy_impl = { role; clause; vars; dummy_impl } + let vars t = List.map ~f:fst t.vars + + let selected t = + let open Option.O in + let* lit = t.clause >>= S.get_selected in + match S.get_user_data_for_lit lit with + | SolverData.ImplElem impl -> Some (lit, impl) + | _ -> assert false + ;; + + let state t = + match t.clause with + | None -> Unselected (* There were never any candidates *) + | Some clause -> + (match S.get_selected clause with + | Some lit -> + (* We've already chosen which to use. Follow dependencies. *) + let impl = + match S.get_user_data_for_lit lit with + | SolverData.ImplElem impl -> impl + | _ -> assert false + in + Selected (Model.requires t.role impl) + | None -> + (match S.get_best_undecided clause with + | Some lit -> Undecided lit + | None -> Unselected (* No remaining candidates, and none was chosen. *))) + ;; + + (* Apply [test impl] to each implementation, partitioning the vars into two + lists. Only defined for [impl_candidates]. *) + let partition t ~f:test = + List.partition_map t.vars ~f:(fun (var, impl) -> + if test impl then Stdune.Either.Left var else Right var) + ;; + end + + module RoleMap = Map.Make (struct + include Model.Role + + let to_dyn = Dyn.opaque + end) + + type diagnostics = S.lit + + let explain = S.explain_reason + + type selection = + { impl : Model.impl (** The implementation chosen to fill the role *) + ; diagnostics : diagnostics (** Extra information useful for diagnostics *) + } + + module Conflict_classes = struct + module Map = Map.Make (struct + type t = Model.conflict_class + + let compare (x : t) (y : t) = String.compare (x :> string) (y :> string) + let to_dyn (x : t) = Dyn.string (x :> string) + end) + + type t = + { sat : S.t + ; mutable groups : S.lit list ref Map.t + } + + let create sat = { sat; groups = Map.empty } + + let var t name = + match Map.find t.groups name with + | Some v -> v + | None -> + let v = ref [] in + t.groups <- Map.set t.groups name v; + v + ;; + + (* Add [impl] to its conflict groups, if any. *) + let process t impl_var impl = + Model.conflict_class impl + |> List.iter ~f:(fun name -> + let impls = var t name in + impls := impl_var :: !impls) + ;; + + (* Call this at the end to add the final clause with all discovered groups. + [t] must not be used after this. *) + let seal t = + Map.iter t.groups ~f:(fun impls -> + let impls = !impls in + if List.length impls > 1 + then ( + let (_ : S.at_most_one_clause) = S.at_most_one t.sat impls in + ())) + ;; + end + + (* Add the implementations of an interface to the implementation cache + (called the first time we visit it). *) + let make_impl_clause sat ~dummy_impl role = + let+ { impls } = Model.implementations role in + (* Insert dummy_impl (last) if we're trying to diagnose a problem. *) + let impls = + (match dummy_impl with + | None -> impls + | Some dummy_impl -> impls @ [ dummy_impl ]) + |> List.map ~f:(fun impl -> + let var = S.add_variable sat (SolverData.ImplElem impl) in + var, impl) + in + let clause = + let impl_clause = + match impls with + | [] -> None + | _ :: _ -> Some (S.at_most_one sat (List.map ~f:fst impls)) + in + Candidates.create role impl_clause impls dummy_impl + in + clause, impls + ;; + + (* Starting from [root_req], explore all the feeds and implementations we + might need, adding all of them to [sat_problem]. *) + let build_problem root_req sat ~dummy_impl = + (* For each (iface, source) we have a list of implementations. *) + let impl_cache = ref RoleMap.empty in + let conflict_classes = Conflict_classes.create sat in + let+ () = + let rec lookup_impl expand_deps role = + match RoleMap.find !impl_cache role with + | Some s -> Fiber.return s + | None -> + let* clause, impls = make_impl_clause sat ~dummy_impl role in + impl_cache := RoleMap.set !impl_cache role clause; + let+ () = + Fiber.sequential_iter impls ~f:(fun (impl_var, impl) -> + Conflict_classes.process conflict_classes impl_var impl; + match expand_deps with + | `No_expand -> Fiber.return () + | `Expand_and_collect_conflicts deferred -> + Model.requires role impl + |> Fiber.sequential_iter ~f:(fun dep -> + let { Model.dep_importance; _ } = Model.dep_info dep in + match dep_importance with + | `Essential -> process_dep expand_deps impl_var dep + | `Restricts -> + (* Defer processing restricting deps until all essential + deps have been processed for the entire problem. + Restricting deps will be processed later without + recurring into their dependencies. *) + deferred := (impl_var, dep) :: !deferred; + Fiber.return ())) + in + clause + and process_dep expand_deps user_var dep : unit Fiber.t = + (* Process a dependency of [user_var]: + - find the candidate implementations to satisfy it + - take just those that satisfy any restrictions in the dependency + - ensure that we don't pick an incompatbile version if we select + [user_var] + - ensure that we do pick a compatible version if we select + [user_var] (for "essential" dependencies only) *) + let { Model.dep_role; dep_importance } = Model.dep_info dep in + let+ pass, fail = + let meets_restrictions = + (* Restrictions on the candidates *) + let dep_restrictions = Model.restrictions dep in + fun impl -> List.for_all ~f:(Model.meets_restriction impl) dep_restrictions + in + lookup_impl expand_deps dep_role + >>| Candidates.partition ~f:meets_restrictions + in + match dep_importance with + | `Essential -> + S.implies + sat + ~reason:"essential dep" + user_var + pass (* Must choose a suitable candidate *) + | `Restricts -> + (* If [user_var] is selected, don't select an incompatible version of + the optional dependency. We don't need to do this explicitly in + the [essential] case, because we must select a good version and we can't + select two. *) + (try S.at_most_one sat (user_var :: fail) |> ignore with + | Invalid_argument reason -> + (* Explicitly conflicts with itself! *) + S.at_least_one sat [ S.neg user_var ] ~reason) + in + let conflicts = ref [] in + let* () = + (* This recursively builds the whole problem up. *) + lookup_impl (`Expand_and_collect_conflicts conflicts) root_req + >>| Candidates.vars + >>| S.at_least_one sat ~reason:"need root" (* Must get what we came for! *) + in + (* Now process any restricting deps. Due to the cache, only restricting + deps that aren't also an essential dep will be expanded. The solver will + not process any transitive dependencies here since the dependencies of + restricting dependencies are irrelevant to solving the dependency + problem. *) + List.rev !conflicts + |> Fiber.sequential_iter ~f:(fun (impl_var, dep) -> + process_dep `No_expand impl_var dep) + (* All impl_candidates have now been added, so snapshot the cache. *) + in + let impl_clauses = !impl_cache in + Conflict_classes.seal conflict_classes; + impl_clauses + ;; + + module Output = struct + module Input = Model + module Role = Input.Role + module RoleMap = RoleMap + + type impl = selection + type dependency = Model.dependency + + type dep_info = Model.dep_info = + { dep_role : Role.t + ; dep_importance : [ `Essential | `Restricts ] + } + + type requirements = Role.t + + let dep_info = Model.dep_info + let requires role impl = Model.requires role impl.impl + + type t = + { root_req : requirements + ; selections : selection RoleMap.t + } + + let to_map t = t.selections + let requirements t = t.root_req + + let explain t role = + match RoleMap.find t.selections role with + | Some sel -> explain sel.diagnostics + | None -> Pp.text "Role not used!" + ;; + + let get_selected role t = + match RoleMap.find t.selections role with + | Some selection when selection.impl == Model.dummy_impl -> None + | x -> x + ;; + + let unwrap sel = sel.impl + end + + (** [do_solve model req] finds an implementation matching the given + requirements, plus any other implementations needed + to satisfy its dependencies. + + @param closest_match + adds a lowest-ranked (but valid) implementation ([Input.dummy_impl]) to + every interface, so we can always select something. Useful for diagnostics. + Note: always try without [closest_match] first, or it may miss a valid solution. + @return None if the solve fails (only happens if [closest_match] is false). *) + let do_solve ~closest_match root_req = + (* The basic plan is this: + 1. Scan the root interface and all dependencies recursively, building up a SAT problem. + 2. Solve the SAT problem. Whenever there are multiple options, try the most preferred one first. + 3. Create the selections XML from the results. + + All three involve recursively walking the tree in a similar way: + 1) we follow every dependency of every implementation (order not important) + 2) we follow every dependency of every selected implementation (better versions first) + 3) we follow every dependency of every selected implementation + *) + let sat = S.create () in + let dummy_impl = if closest_match then Some Model.dummy_impl else None in + let+ impl_clauses = build_problem root_req sat ~dummy_impl in + let lookup role = RoleMap.find_exn impl_clauses role in + (* Run the solve *) + let decider () = + (* Walk the current solution, depth-first, looking for the first undecided interface. + Then try the most preferred implementation of it that hasn't been ruled out. *) + let seen = + let module Requirements = struct + type t = Output.requirements + + let equal x y = Ordering.is_eq (Output.Role.compare x y) + let hash = Poly.hash + let to_dyn = Dyn.opaque + end + in + Table.create (module Requirements) 100 + in + let rec find_undecided req = + if Table.mem seen req + then None (* Break cycles *) + else ( + Table.set seen req true; + let candidates = lookup req in + match Candidates.state candidates with + | Unselected -> None + | Undecided lit -> Some lit + | Selected deps -> + (* We've already selected a candidate for this component. Now check its dependencies. *) + let check_dep dep = + let { Model.dep_role; dep_importance } = Model.dep_info dep in + match dep_importance with + | `Restricts -> + (* Restrictions don't express that we do or don't want the + dependency, so skip them here. If someone else needs this, + we'll handle it when we get to them. + If noone wants it, it will be set to unselected at the end. *) + None + | `Essential -> find_undecided dep_role + in + List.find_map ~f:check_dep deps) + in + find_undecided root_req + in + match S.run_solver sat decider with + | None -> None + | Some _solution -> + (* Build the results object *) + let selections = + RoleMap.filter_mapi impl_clauses ~f:(fun _role candidates -> + Candidates.selected candidates + |> Option.map ~f:(fun (lit, impl) -> { impl; diagnostics = lit })) + in + Some { Output.root_req; selections } + ;; + end + module Diagnostics = Diagnostics.Make (Solver.Output) let solve context pkgs = diff --git a/src/dune_pkg/solver_core.ml b/src/dune_pkg/solver_core.ml deleted file mode 100644 index 83694f783ca..00000000000 --- a/src/dune_pkg/solver_core.ml +++ /dev/null @@ -1,367 +0,0 @@ -(* Copyright (C) 2013, Thomas Leonard - * See the README file for details, or visit http://0install.net. - *) - -(** Select a compatible set of components to run a program. *) - -open Stdune -open Fiber.O - -module Make (Model : S.SOLVER_INPUT) = struct - (** We attach this data to each SAT variable. *) - module SolverData = struct - [@@@ocaml.warning "-37"] - - type t = - (* If the SAT variable is True then we selected this... *) - | ImplElem of Model.impl - | Role of Model.Role.t - - let pp = function - | ImplElem impl -> Model.pp_impl impl - | Role role -> Model.Role.pp role - ;; - end - - module S = Sat.Make (SolverData) - - type decision_state = - (* The next candidate to try *) - | Undecided of S.lit - (* The dependencies to check next *) - | Selected of Model.dependency list - | Unselected - - module Candidates = struct - type t = - { role : Model.Role.t - ; clause : S.at_most_one_clause option - ; vars : (S.lit * Model.impl) list - ; dummy_impl : Model.impl option - } - - let[@ocaml.warning "-32"] is_dummy t impl = - match t.dummy_impl with - | None -> false - | Some dummy_impl -> dummy_impl == impl - ;; - - let create role clause vars dummy_impl = { role; clause; vars; dummy_impl } - let vars t = List.map ~f:fst t.vars - - let selected t = - let open Option.O in - let* lit = t.clause >>= S.get_selected in - match S.get_user_data_for_lit lit with - | SolverData.ImplElem impl -> Some (lit, impl) - | _ -> assert false - ;; - - let state t = - match t.clause with - | None -> Unselected (* There were never any candidates *) - | Some clause -> - (match S.get_selected clause with - | Some lit -> - (* We've already chosen which to use. Follow dependencies. *) - let impl = - match S.get_user_data_for_lit lit with - | SolverData.ImplElem impl -> impl - | _ -> assert false - in - Selected (Model.requires t.role impl) - | None -> - (match S.get_best_undecided clause with - | Some lit -> Undecided lit - | None -> Unselected (* No remaining candidates, and none was chosen. *))) - ;; - - (* Apply [test impl] to each implementation, partitioning the vars into two - lists. Only defined for [impl_candidates]. *) - let partition t ~f:test = - List.partition_map t.vars ~f:(fun (var, impl) -> - if test impl then Stdune.Either.Left var else Right var) - ;; - end - - module RoleMap = Map.Make (struct - include Model.Role - - let to_dyn = Dyn.opaque - end) - - type diagnostics = S.lit - - let explain = S.explain_reason - - type selection = - { impl : Model.impl (** The implementation chosen to fill the role *) - ; diagnostics : diagnostics (** Extra information useful for diagnostics *) - } - - module Conflict_classes = struct - module Map = Map.Make (struct - type t = Model.conflict_class - - let compare (x : t) (y : t) = String.compare (x :> string) (y :> string) - let to_dyn (x : t) = Dyn.string (x :> string) - end) - - type t = - { sat : S.t - ; mutable groups : S.lit list ref Map.t - } - - let create sat = { sat; groups = Map.empty } - - let var t name = - match Map.find t.groups name with - | Some v -> v - | None -> - let v = ref [] in - t.groups <- Map.set t.groups name v; - v - ;; - - (* Add [impl] to its conflict groups, if any. *) - let process t impl_var impl = - Model.conflict_class impl - |> List.iter ~f:(fun name -> - let impls = var t name in - impls := impl_var :: !impls) - ;; - - (* Call this at the end to add the final clause with all discovered groups. - [t] must not be used after this. *) - let seal t = - Map.iter t.groups ~f:(fun impls -> - let impls = !impls in - if List.length impls > 1 - then ( - let (_ : S.at_most_one_clause) = S.at_most_one t.sat impls in - ())) - ;; - end - - (* Add the implementations of an interface to the implementation cache - (called the first time we visit it). *) - let make_impl_clause sat ~dummy_impl role = - let+ { impls } = Model.implementations role in - (* Insert dummy_impl (last) if we're trying to diagnose a problem. *) - let impls = - (match dummy_impl with - | None -> impls - | Some dummy_impl -> impls @ [ dummy_impl ]) - |> List.map ~f:(fun impl -> - let var = S.add_variable sat (SolverData.ImplElem impl) in - var, impl) - in - let clause = - let impl_clause = - match impls with - | [] -> None - | _ :: _ -> Some (S.at_most_one sat (List.map ~f:fst impls)) - in - Candidates.create role impl_clause impls dummy_impl - in - clause, impls - ;; - - (* Starting from [root_req], explore all the feeds and implementations we - might need, adding all of them to [sat_problem]. *) - let build_problem root_req sat ~dummy_impl = - (* For each (iface, source) we have a list of implementations. *) - let impl_cache = ref RoleMap.empty in - let conflict_classes = Conflict_classes.create sat in - let+ () = - let rec lookup_impl expand_deps role = - match RoleMap.find !impl_cache role with - | Some s -> Fiber.return s - | None -> - let* clause, impls = make_impl_clause sat ~dummy_impl role in - impl_cache := RoleMap.set !impl_cache role clause; - let+ () = - Fiber.sequential_iter impls ~f:(fun (impl_var, impl) -> - Conflict_classes.process conflict_classes impl_var impl; - match expand_deps with - | `No_expand -> Fiber.return () - | `Expand_and_collect_conflicts deferred -> - Model.requires role impl - |> Fiber.sequential_iter ~f:(fun dep -> - let { Model.dep_importance; _ } = Model.dep_info dep in - match dep_importance with - | `Essential -> process_dep expand_deps impl_var dep - | `Restricts -> - (* Defer processing restricting deps until all essential - deps have been processed for the entire problem. - Restricting deps will be processed later without - recurring into their dependencies. *) - deferred := (impl_var, dep) :: !deferred; - Fiber.return ())) - in - clause - and process_dep expand_deps user_var dep : unit Fiber.t = - (* Process a dependency of [user_var]: - - find the candidate implementations to satisfy it - - take just those that satisfy any restrictions in the dependency - - ensure that we don't pick an incompatbile version if we select - [user_var] - - ensure that we do pick a compatible version if we select - [user_var] (for "essential" dependencies only) *) - let { Model.dep_role; dep_importance } = Model.dep_info dep in - let+ pass, fail = - let meets_restrictions = - (* Restrictions on the candidates *) - let dep_restrictions = Model.restrictions dep in - fun impl -> List.for_all ~f:(Model.meets_restriction impl) dep_restrictions - in - lookup_impl expand_deps dep_role >>| Candidates.partition ~f:meets_restrictions - in - match dep_importance with - | `Essential -> - S.implies - sat - ~reason:"essential dep" - user_var - pass (* Must choose a suitable candidate *) - | `Restricts -> - (* If [user_var] is selected, don't select an incompatible version of - the optional dependency. We don't need to do this explicitly in - the [essential] case, because we must select a good version and we can't - select two. *) - (try S.at_most_one sat (user_var :: fail) |> ignore with - | Invalid_argument reason -> - (* Explicitly conflicts with itself! *) - S.at_least_one sat [ S.neg user_var ] ~reason) - in - let conflicts = ref [] in - let* () = - (* This recursively builds the whole problem up. *) - lookup_impl (`Expand_and_collect_conflicts conflicts) root_req - >>| Candidates.vars - >>| S.at_least_one sat ~reason:"need root" (* Must get what we came for! *) - in - (* Now process any restricting deps. Due to the cache, only restricting - deps that aren't also an essential dep will be expanded. The solver will - not process any transitive dependencies here since the dependencies of - restricting dependencies are irrelevant to solving the dependency - problem. *) - List.rev !conflicts - |> Fiber.sequential_iter ~f:(fun (impl_var, dep) -> - process_dep `No_expand impl_var dep) - (* All impl_candidates have now been added, so snapshot the cache. *) - in - let impl_clauses = !impl_cache in - Conflict_classes.seal conflict_classes; - impl_clauses - ;; - - module Output = struct - module Input = Model - module Role = Input.Role - module RoleMap = RoleMap - - type impl = selection - type dependency = Model.dependency - - type dep_info = Model.dep_info = - { dep_role : Role.t - ; dep_importance : [ `Essential | `Restricts ] - } - - type requirements = Role.t - - let dep_info = Model.dep_info - let requires role impl = Model.requires role impl.impl - - type t = - { root_req : requirements - ; selections : selection RoleMap.t - } - - let to_map t = t.selections - let requirements t = t.root_req - - let explain t role = - match RoleMap.find t.selections role with - | Some sel -> explain sel.diagnostics - | None -> Pp.text "Role not used!" - ;; - - let get_selected role t = - match RoleMap.find t.selections role with - | Some selection when selection.impl == Model.dummy_impl -> None - | x -> x - ;; - - let unwrap sel = sel.impl - end - - let do_solve ~closest_match root_req = - (* The basic plan is this: - 1. Scan the root interface and all dependencies recursively, building up a SAT problem. - 2. Solve the SAT problem. Whenever there are multiple options, try the most preferred one first. - 3. Create the selections XML from the results. - - All three involve recursively walking the tree in a similar way: - 1) we follow every dependency of every implementation (order not important) - 2) we follow every dependency of every selected implementation (better versions first) - 3) we follow every dependency of every selected implementation - *) - let sat = S.create () in - let dummy_impl = if closest_match then Some Model.dummy_impl else None in - let+ impl_clauses = build_problem root_req sat ~dummy_impl in - let lookup role = RoleMap.find_exn impl_clauses role in - (* Run the solve *) - let decider () = - (* Walk the current solution, depth-first, looking for the first undecided interface. - Then try the most preferred implementation of it that hasn't been ruled out. *) - let seen = - let module Requirements = struct - type t = Output.requirements - - let equal x y = Ordering.is_eq (Output.Role.compare x y) - let hash = Poly.hash - let to_dyn = Dyn.opaque - end - in - Table.create (module Requirements) 100 - in - let rec find_undecided req = - if Table.mem seen req - then None (* Break cycles *) - else ( - Table.set seen req true; - let candidates = lookup req in - match Candidates.state candidates with - | Unselected -> None - | Undecided lit -> Some lit - | Selected deps -> - (* We've already selected a candidate for this component. Now check its dependencies. *) - let check_dep dep = - let { Model.dep_role; dep_importance } = Model.dep_info dep in - match dep_importance with - | `Restricts -> - (* Restrictions don't express that we do or don't want the - dependency, so skip them here. If someone else needs this, - we'll handle it when we get to them. - If noone wants it, it will be set to unselected at the end. *) - None - | `Essential -> find_undecided dep_role - in - List.find_map ~f:check_dep deps) - in - find_undecided root_req - in - match S.run_solver sat decider with - | None -> None - | Some _solution -> - (* Build the results object *) - let selections = - RoleMap.filter_mapi impl_clauses ~f:(fun _role candidates -> - Candidates.selected candidates - |> Option.map ~f:(fun (lit, impl) -> { impl; diagnostics = lit })) - in - Some { Output.root_req; selections } - ;; -end diff --git a/src/dune_pkg/solver_core.mli b/src/dune_pkg/solver_core.mli deleted file mode 100644 index abd2327f65f..00000000000 --- a/src/dune_pkg/solver_core.mli +++ /dev/null @@ -1,15 +0,0 @@ -(** Select a compatible set of components to run a program. - See [Zeroinstall.Solver] for the instantiation of this functor on the - actual 0install types. *) -module Make (Input : S.SOLVER_INPUT) : sig - module Output : S.SOLVER_RESULT with module Input = Input - - (** [do_solve model req] finds an implementation matching the given requirements, plus any other implementations needed - to satisfy its dependencies. - @param closest_match - adds a lowest-ranked (but valid) implementation ([Input.dummy_impl]) to - every interface, so we can always select something. Useful for diagnostics. - Note: always try without [closest_match] first, or it may miss a valid solution. - @return None if the solve fails (only happens if [closest_match] is false). *) - val do_solve : closest_match:bool -> Input.Role.t -> Output.t option Fiber.t -end