Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
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
2 changes: 2 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,14 @@ include = ["Cargo.toml", "LICENSE", "README.md", "src/**", "tests/**", "examples
thiserror = "1.0"
rustc-hash = "1.1.0"
serde = { version = "1.0", features = ["derive"], optional = true }
log = { version = "0.4.14", default-features = false } # for debug logs in tests
Copy link
Member

Choose a reason for hiding this comment

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

No objection, just wondering:
What features are we trying to opted out of? Why default-features = false?


[dev-dependencies]
proptest = "0.10.1"
ron = "0.6"
varisat = "0.2.2"
criterion = "0.3"
env_logger = "0.9.0"

[[bench]]
name = "large_case"
Expand Down
6 changes: 6 additions & 0 deletions src/internal/core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,10 @@ impl<P: Package, V: Version> State<P, V> {
// If the partial solution satisfies the incompatibility
// we must perform conflict resolution.
Relation::Satisfied => {
log::info!(
"Start conflict resolution because incompat satisfied:\n {}",
current_incompat
);
conflict_id = Some(incompat_id);
break;
}
Expand Down Expand Up @@ -183,6 +187,7 @@ impl<P: Package, V: Version> State<P, V> {
current_incompat_changed,
previous_satisfier_level,
);
log::info!("backtrack to {:?}", previous_satisfier_level);
return Ok((package, current_incompat_id));
}
SameDecisionLevels { satisfier_cause } => {
Expand All @@ -192,6 +197,7 @@ impl<P: Package, V: Version> State<P, V> {
&package,
&self.incompatibility_store,
);
log::info!("prior cause: {}", prior_cause);
current_incompat_id = self.incompatibility_store.alloc(prior_cause);
current_incompat_changed = true;
}
Expand Down
63 changes: 63 additions & 0 deletions src/internal/partial_solution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@
//! A Memory acts like a structured partial solution
//! where terms are regrouped by package in a [Map](crate::type_aliases::Map).

use std::collections::BTreeSet;
use std::fmt::Display;

use crate::internal::arena::Arena;
use crate::internal::incompatibility::{IncompId, Incompatibility, Relation};
use crate::internal::small_map::SmallMap;
Expand Down Expand Up @@ -32,6 +35,24 @@ pub struct PartialSolution<P: Package, V: Version> {
package_assignments: Map<P, PackageAssignments<P, V>>,
}

impl<P: Package, V: Version> Display for PartialSolution<P, V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let assignments: BTreeSet<String> = self
.package_assignments
.iter()
.map(|(p, pa)| format!("{}: {}", p, pa))
.collect();
let assignments: Vec<_> = assignments.into_iter().collect();
Copy link
Member

Choose a reason for hiding this comment

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

I think it would be clearer to collect into a vec and then call sort.

write!(
f,
"next_global_index: {}\ncurrent_decision_level: {:?}\npackage_assignements:\n{}",
self.next_global_index,
self.current_decision_level,
assignments.join("\n")
)
}
}

/// Package assignments contain the potential decision and derivations
/// that have already been made for a given package,
/// as well as the intersection of terms by all of these.
Expand All @@ -43,19 +64,54 @@ struct PackageAssignments<P: Package, V: Version> {
assignments_intersection: AssignmentsIntersection<V>,
}

impl<P: Package, V: Version> Display for PackageAssignments<P, V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let derivations: Vec<_> = self
.dated_derivations
.iter()
.map(|dd| dd.to_string())
.collect();
write!(
f,
"decision range: {:?}..{:?}\nderivations:\n {}\n,assignments_intersection: {}",
self.smallest_decision_level,
self.highest_decision_level,
derivations.join("\n "),
self.assignments_intersection
)
}
}

#[derive(Clone, Debug)]
pub struct DatedDerivation<P: Package, V: Version> {
global_index: u32,
decision_level: DecisionLevel,
cause: IncompId<P, V>,
}

impl<P: Package, V: Version> Display for DatedDerivation<P, V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{:?}, cause: {:?}", self.decision_level, self.cause)
}
}

#[derive(Clone, Debug)]
enum AssignmentsIntersection<V: Version> {
Decision((u32, V, Term<V>)),
Derivations(Term<V>),
}

impl<V: Version> Display for AssignmentsIntersection<V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Self::Decision((lvl, version, _)) => {
write!(f, "Decision: level {}, v = {}", lvl, version)
}
Self::Derivations(term) => write!(f, "Derivations term: {}", term),
}
}
}

#[derive(Clone, Debug)]
pub enum SatisfierSearch<P: Package, V: Version> {
DifferentDecisionLevels {
Expand Down Expand Up @@ -258,7 +314,14 @@ impl<P: Package, V: Version> PartialSolution<P, V> {
// Check none of the dependencies (new_incompatibilities)
// would create a conflict (be satisfied).
if store[new_incompatibilities].iter().all(not_satisfied) {
log::info!("add_decision: {} @ {}", package, version);
self.add_decision(package, version);
} else {
log::info!(
"not adding {} @ {} because of its dependencies",
package,
version
);
}
}

Expand Down
7 changes: 7 additions & 0 deletions src/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,12 @@ pub fn resolve<P: Package, V: Version>(
.should_cancel()
.map_err(|err| PubGrubError::ErrorInShouldCancel(err))?;

log::info!("unit_propagation: {}", &next);
state.unit_propagation(next)?;
log::debug!(
"Partial solution after unit propagation: {}",
state.partial_solution
);

let potential_packages = state.partial_solution.potential_packages();
if potential_packages.is_none() {
Expand All @@ -109,6 +114,7 @@ pub fn resolve<P: Package, V: Version>(
let decision = dependency_provider
.choose_package_version(potential_packages.unwrap())
.map_err(PubGrubError::ErrorChoosingPackageVersion)?;
log::info!("DP chose: {} @ {:?}", decision.0, decision.1);
next = decision.0.clone();

// Pick the next compatible version.
Expand Down Expand Up @@ -195,6 +201,7 @@ pub fn resolve<P: Package, V: Version>(
} else {
// `dep_incompats` are already in `incompatibilities` so we know there are not satisfied
// terms and can add the decision directly.
log::info!("add_decision (not first time): {} @ {}", &next, v);
state.partial_solution.add_decision(next.clone(), v);
}
}
Expand Down
16 changes: 16 additions & 0 deletions tests/examples.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,21 @@ use pubgrub::solver::{resolve, OfflineDependencyProvider};
use pubgrub::type_aliases::Map;
use pubgrub::version::{NumberVersion, SemanticVersion};

use log::LevelFilter;
use std::io::Write;

fn init_log() {
let _ = env_logger::builder()
.filter_level(LevelFilter::Trace)
.format(|buf, record| writeln!(buf, "{}", record.args()))
.is_test(true)
.try_init();
}

#[test]
/// https://github.com/dart-lang/pub/blob/master/doc/solver.md#no-conflicts
fn no_conflict() {
init_log();
let mut dependency_provider = OfflineDependencyProvider::<&str, SemanticVersion>::new();
#[rustfmt::skip]
dependency_provider.add_dependencies(
Expand Down Expand Up @@ -38,6 +50,7 @@ fn no_conflict() {
#[test]
/// https://github.com/dart-lang/pub/blob/master/doc/solver.md#avoiding-conflict-during-decision-making
fn avoiding_conflict_during_decision_making() {
init_log();
let mut dependency_provider = OfflineDependencyProvider::<&str, SemanticVersion>::new();
#[rustfmt::skip]
dependency_provider.add_dependencies(
Expand Down Expand Up @@ -73,6 +86,7 @@ fn avoiding_conflict_during_decision_making() {
#[test]
/// https://github.com/dart-lang/pub/blob/master/doc/solver.md#performing-conflict-resolution
fn conflict_resolution() {
init_log();
let mut dependency_provider = OfflineDependencyProvider::<&str, SemanticVersion>::new();
#[rustfmt::skip]
dependency_provider.add_dependencies(
Expand Down Expand Up @@ -106,6 +120,7 @@ fn conflict_resolution() {
#[test]
/// https://github.com/dart-lang/pub/blob/master/doc/solver.md#conflict-resolution-with-a-partial-satisfier
fn conflict_with_partial_satisfier() {
init_log();
let mut dependency_provider = OfflineDependencyProvider::<&str, SemanticVersion>::new();
#[rustfmt::skip]
// root 1.0.0 depends on foo ^1.0.0 and target ^2.0.0
Expand Down Expand Up @@ -171,6 +186,7 @@ fn conflict_with_partial_satisfier() {
///
/// Solution: a0, b0, c0, d0
fn double_choices() {
init_log();
let mut dependency_provider = OfflineDependencyProvider::<&str, NumberVersion>::new();
dependency_provider.add_dependencies("a", 0, vec![("b", Range::any()), ("c", Range::any())]);
dependency_provider.add_dependencies("b", 0, vec![("d", Range::exact(0))]);
Expand Down