Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

use intermediate satisfier causes in priority statistics #291

Open
wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

use intermediate satisfier causes in priority statistics #291

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 39 additions & 8 deletions src/internal/core.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,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() {
Expand Down Expand Up @@ -169,12 +169,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.
Expand All @@ -190,16 +189,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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tried some editing:

Return the root cause or the terminal incompatibility. CF
<https://github.com/dart-lang/pub/blob/master/doc/solver.md#unit-propagation>

When we found a conflict, we want to learn as much as possible from it, to avoid making (or
keeping) decisions that will be rejected. Say we found that the decision for X and the
decision for Y are incompatible. We may find that the decisions on earlier packages B and C
require us to make incompatible decisions on X and Y, so we backtrack until either B or C
can be revisited. To make it 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 too specific, then the outer `solver` loop will
eventually end up calling us again until all possibilities are enumerated.

To end up with a more useful incompatibility, this function combines incompatibilities into
derivations. Fulfilling this derivation implies the later conflict. By banning it, we
prevent the intermediate steps from occurring again, at least in 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 we picked W and so on, until 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 check 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 them for prioritization.

Then if A turns out to also have a dependency on X the resulting root cause is still
useful.

How will we apply the root cause?

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 too
specific, then the outer solver loop will eventually end up calling us again until all
possibilities are enumerated.

In which direction are "too general" and "too specific" to be understood here?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall I like the edits. I have a nit about

Say we found that the decision for X and the decision for Y are incompatible.

I'm going to quibble about the term decision in this sentence. In my brain decision implies something that became constrained because of a call to choose_version/add_decision. Because we check for conflicts in add_version simple cases end up handled there. We generally do not end up here with a conflict that is already in terms of decisions. Instead We start with something abstract like X (in some range) depends on Y (in some range). It's the job of this function to peel back the layers, figure out why the partial solution has an assignment (which is not necessarily decision) that is disjoint with the mentioned range for Y and why the partial solution has an assignment that is a subset of the mentioned range for X.

How will we apply the root cause?

When we discover that A has a dependency on X unit_propagation will rescan the root cause
"the dependency on the package X is incompatible with the decision on C", and remove that version of C from the available range stored in partial solution.

In which direction are "too general" and "too specific" to be understood here?

I intended for to specific to mean referring to exact decided versions. "B == 123 is incompatible with C == 456" would be very specific. Extremely actionable, unit_propagation needs to do very little work to figure out if it's relevant. But also not likely to be reusable. We are likely to end up with O(# versions of B * # versions of C) of these incompatibilities laying around. "any version of X is incompatible with any version of Y" would be very general. There will only ever need to be one, and it will be relevant and useful any time X or Y come up again. But, it takes a lot of work to figure out how it relates to decisions or where we need to backtrack to.

Obviously the wording of the paragraphs needs work, thank you for helping me with it!

#[allow(clippy::type_complexity)]
#[cold]
fn conflict_resolution(
&mut self,
incompatibility: IncompDpId<DP>,
satisfier_causes: &mut SmallVec<(Id<DP::P>, IncompDpId<DP>)>,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If this turns out to show up in anyone's profile while they don't use the output, we can replace it by a callback, but for now :shipit:

) -> Result<(Id<DP::P>, IncompDpId<DP>), IncompDpId<DP>> {
let mut current_incompat_id = incompatibility;
let mut current_incompat_changed = false;
Expand All @@ -223,6 +252,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 } => {
Expand All @@ -234,6 +264,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;
}
}
Expand Down
3 changes: 2 additions & 1 deletion src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
24 changes: 13 additions & 11 deletions src/provider.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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]
Expand Down
4 changes: 2 additions & 2 deletions src/solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
Loading