use intermediate satisfier causes in priority statistics

Author: Eh2406

src/internal/core.rs

@@ -133,7 +133,7 @@ impl<DP: DependencyProvider> State<DP> {
         &mut self,
         package: Id<DP::P>,
     ) -> Result<SmallVec<(Id<DP::P>, IncompDpId<DP>)>, NoSolutionError<DP>> {
-        let mut root_causes = SmallVec::default();
+        let mut satisfier_causes = SmallVec::default();
         self.unit_propagation_buffer.clear();
         self.unit_propagation_buffer.push(package);
         while let Some(current_package) = self.unit_propagation_buffer.pop() {
@@ -186,12 +186,11 @@ impl<DP: DependencyProvider> State<DP> {
                 }
             }
             if let Some(incompat_id) = conflict_id {
-                let (package_almost, root_cause) =
-                    self.conflict_resolution(incompat_id)
-                        .map_err(|terminal_incompat_id| {
-                            self.build_derivation_tree(terminal_incompat_id)
-                        })?;
-                root_causes.push((package, root_cause));
+                let (package_almost, root_cause) = self
+                    .conflict_resolution(incompat_id, &mut satisfier_causes)
+                    .map_err(|terminal_incompat_id| {
+                        self.build_derivation_tree(terminal_incompat_id)
+                    })?;
                 self.unit_propagation_buffer.clear();
                 self.unit_propagation_buffer.push(package_almost);
                 // Add to the partial solution with incompat as cause.
@@ -207,16 +206,46 @@ impl<DP: DependencyProvider> State<DP> {
             }
         }
         // If there are no more changed packages, unit propagation is done.
-        Ok(root_causes)
+        Ok(satisfier_causes)
     }
 
     /// Return the root cause or the terminal incompatibility.
     /// CF <https://github.com/dart-lang/pub/blob/master/doc/solver.md#unit-propagation>
+    ///
+    /// Usually by the time we have a conflict `unit_propagation` has done a lot of work.
+    /// So the actual conflict we find is important, but not particularly actionable.
+    /// It says something like "the dependency on package X and the dependency on package Y are incompatible".
+    /// To make it actionable we want to track it back to decisions that made the dependency required.
+    /// "The decision on B is incompatible with the decision on C,
+    ///  because unit propagation from just those decisions will lead to the conflict about X and Y"
+    /// is much more actionable, backtrack until one of those decisions can be revisited.
+    /// To make a practical, we really only need one of the terms to be a decision.
+    /// We may as well leave the other terms general. Something like
+    /// "the dependency on the package X is incompatible with the decision on C" tends to work out pretty well.
+    /// Then if A turns out to also have a dependency on X the resulting root cause is still useful.
+    /// Of course, this is more heuristics than science. If the output is too general, then `unit_propagation` will
+    /// handle the confusion by calling us again with the next most specific conflict it comes across.
+    /// If the output is to specific, then the outer `solver` loop will eventually end up calling us again
+    /// until all possibilities are enumerated.
+    ///
+    /// This function combines incompatibilities with things that make the problem inevitable to end up with a
+    /// more useful incompatibility. For the correctness of the PubGrub algorithm only the final output is required.
+    /// By banning the final output, unit propagation will prevent the intermediate steps from occurring again,
+    /// at least prevent the exact same way. However, the statistics collected for `prioritize`may want
+    /// to analyze those intermediate steps. For example we might start with "there is no version 1 of Z",
+    /// and `conflict_resolution` may be able to determine that "that was inevitable when we picked version 1 of X"
+    /// which was inevitable when picked W and ... and version 1 of B, which was depended on by version 1 of A.
+    /// Therefore the root cause may simplify all the way down to "we cannot pick version 1 of A".
+    /// This will prevent us going down this path again. However when we start looking at version 2 of A,
+    /// and discover that it depends on version 2 of B, we will want to prioritize the chain of intermediate steps
+    /// to confirm if it has a problem with the same shape.
+    /// The `satisfier_causes` argument keeps track of these intermediate steps so that the caller can use.
     #[allow(clippy::type_complexity)]
     #[cold]
     fn conflict_resolution(
         &mut self,
         incompatibility: IncompDpId<DP>,
+        satisfier_causes: &mut SmallVec<(Id<DP::P>, IncompDpId<DP>)>,
     ) -> Result<(Id<DP::P>, IncompDpId<DP>), IncompDpId<DP>> {
         let mut current_incompat_id = incompatibility;
         let mut current_incompat_changed = false;
@@ -240,6 +269,7 @@ impl<DP: DependencyProvider> State<DP> {
                             previous_satisfier_level,
                         );
                         log::info!("backtrack to {:?}", previous_satisfier_level);
+                        satisfier_causes.push((package, current_incompat_id));
                         return Ok((package, current_incompat_id));
                     }
                     SatisfierSearch::SameDecisionLevels { satisfier_cause } => {
@@ -251,6 +281,7 @@ impl<DP: DependencyProvider> State<DP> {
                         );
                         log::info!("prior cause: {}", prior_cause.display(&self.package_store));
                         current_incompat_id = self.incompatibility_store.alloc(prior_cause);
+                        satisfier_causes.push((package, current_incompat_id));
                         current_incompat_changed = true;
                     }
                 }

src/lib.rs

@@ -71,7 +71,8 @@
 //! and [SemanticVersion] for versions.
 //! This may be done quite easily by implementing the three following functions.
 //! ```
-//! # use pubgrub::{DependencyProvider, Dependencies, SemanticVersion, Ranges, DependencyConstraints, Map, PackageResolutionStatistics};
+//! # use pubgrub::{DependencyProvider, Dependencies, SemanticVersion, Ranges,
+//! #               DependencyConstraints, Map, PackageResolutionStatistics};
 //! # use std::error::Error;
 //! # use std::borrow::Borrow;
 //! # use std::convert::Infallible;

src/provider.rs

@@ -2,8 +2,10 @@ use std::cmp::Reverse;
 use std::collections::BTreeMap;
 use std::convert::Infallible;
 
-use crate::solver::PackageResolutionStatistics;
-use crate::{Dependencies, DependencyConstraints, DependencyProvider, Map, Package, VersionSet};
+use crate::{
+    Dependencies, DependencyConstraints, DependencyProvider, Map, Package,
+    PackageResolutionStatistics, VersionSet,
+};
 
 /// A basic implementation of [DependencyProvider].
 #[derive(Debug, Clone, Default)]
@@ -102,15 +104,15 @@ impl<P: Package, VS: VersionSet> DependencyProvider for OfflineDependencyProvide
         range: &Self::VS,
         package_statistics: &PackageResolutionStatistics,
     ) -> Self::Priority {
-        (
-            package_statistics.conflict_count(),
-            Reverse(
-                self.dependencies
-                    .get(package)
-                    .map(|versions| versions.keys().filter(|v| range.contains(v)).count())
-                    .unwrap_or(0),
-            ),
-        )
+        let version_count = self
+            .dependencies
+            .get(package)
+            .map(|versions| versions.keys().filter(|v| range.contains(v)).count())
+            .unwrap_or(0);
+        if version_count == 0 {
+            return (u32::MAX, Reverse(0));
+        }
+        (package_statistics.conflict_count(), Reverse(version_count))
     }
 
     #[inline]

src/solver.rs

@@ -126,8 +126,8 @@ pub fn resolve<DP: DependencyProvider>(
             "unit_propagation: {:?} = '{}'",
             &next, state.package_store[next]
         );
-        let root_causes = state.unit_propagation(next)?;
-        for (affected, incompat) in root_causes {
+        let satisfier_causes = state.unit_propagation(next)?;
+        for (affected, incompat) in satisfier_causes {
             conflict_tracker
                 .entry(affected)
                 .or_default()