Mitigate DNF explosion for depends field with disjoint disjunctions

master_changes.md

@@ -119,6 +119,7 @@ users)
 ## Internal
   * Improve cache-loading performance when using OCaml >= 5.4 by using `Gc.ramp_up` [#6515 @dra27]
   * Make OpamStd.String.compare_case allocation free [#6515 @dra27]
+  * Mitigate potential exponential blow-up converting dependency formulae to DNF [#6831 @dra27]
 
 ## Internal: Unix
 

src/format/opamFormula.ml

@@ -412,22 +412,49 @@ let all_names f =
     OpamPackage.Name.Set.empty f
 
 let packages pkgset f =
-  let names = all_names f in
-  (* dnf allows us to transform the formula into a union of intervals, where
-     ignoring atoms for different package names works. *)
-  let dnf = dnf_of_formula f in
   OpamPackage.Name.Set.fold (fun name acc ->
-      (* Ignore conjunctions where [name] doesn't appear *)
-      let name_formula =
-        map (fun ((n, _) as a) -> if n = name then Atom a else Empty) dnf
+      let is_name (n, _cstr) = OpamPackage.Name.equal n name in
+      let formula_or_empty cond f = if cond then f else Empty in
+      (* Determine if nv could possibly part of the solution for [f]. This
+         means checking that either [v] satisfies the constraints on name.
+         This is done by converting [f] to DNF, which allows us to transform
+         the formula into a union of intervals, where ignoring atoms for
+         different package names works. We can then ignore conjunctions
+         where [name] doesn't appear. However, this function is typically
+         used on a dependency formula, which is most normally a large
+         conjunction. We capitalise on this with a peephole simplification,
+         observing that if we're testing for package name A in the formula
+         [X & Y], then we can ignore X if it doesn't contain A (and likewise
+         Y). This eliminates unrelated sub-formula from the top-level
+         conjunction, in particular it means that
+         [Dep1 & Dep2 & (Dep3 | Dep4) & (Dep5 | Dep6)] does not cause
+         trigger worst-case expansion for DNF. *)
+      let rec simplify_formula f =
+        match f with
+        | Empty -> Empty
+        | Atom atom ->
+            formula_or_empty (is_name atom) f
+        | Block b ->
+            formula_or_empty (exists is_name b) f
+        | Or(a, b) ->
+            formula_or_empty (exists is_name a || exists is_name b) f
+        | And(a, b) ->
+            let a = simplify_formula a in
+            let b = simplify_formula b in
+            make_and a b
+      in
+      let f =
+        f
+        |> simplify_formula
+        |> dnf_of_formula
+        |> map (fun a -> formula_or_empty (is_name a) (Atom a))
       in
       OpamPackage.Set.union acc @@
       OpamPackage.Set.filter (fun nv ->
           let v = OpamPackage.version nv in
-          eval (fun (_name, cstr) -> check_version_formula cstr v)
-            name_formula)
+          eval (fun (_name, cstr) -> check_version_formula cstr v) f)
         (OpamPackage.packages_of_name pkgset name))
-    names OpamPackage.Set.empty
+    (all_names f) OpamPackage.Set.empty
 
 (* Convert a t an atom formula *)
 let to_atom_formula (t:t): atom formula =

src/state/opamSwitchState.ml

@@ -1024,13 +1024,15 @@ let universe st
                             OpamPackage.Map.find nv u_depopts ])
       |> OpamFormula.packages st.packages
     in
-    let requested_deps =
-      OpamPackage.Set.fixpoint resolve_deps requested_allpkgs
-    in
-    requested_deps %% Lazy.force st.reinstall ++
-    match reinstall with
-    | Some set -> set
-    | None -> OpamPackage.Set.empty
+    let reinstall = Option.value ~default:OpamPackage.Set.empty reinstall in
+    let lazy switch_reinstall = st.reinstall in
+    if OpamPackage.Set.is_empty switch_reinstall then
+      reinstall
+    else
+      let requested_deps =
+        OpamPackage.Set.fixpoint resolve_deps requested_allpkgs
+      in
+      requested_deps %% Lazy.force st.reinstall ++ reinstall
   in
   let missing_depexts =
     lazy (