From 9602b78cc708395dc4494577632e9543f2e629d4 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Mon, 20 May 2019 12:11:07 -0400 Subject: [PATCH 01/13] use varisat to verify the resolver --- Cargo.toml | 1 + tests/testsuite/support/resolver.rs | 107 +++++++++++++++++++++++++++- 2 files changed, 107 insertions(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index cf5aa2ff969..d2d1e29501e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -103,6 +103,7 @@ features = [ [dev-dependencies] bufstream = "0.1" proptest = "0.9.1" +varisat = "0.2.1" [[bin]] name = "cargo" diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index f2e8f68a429..bfadb1821bc 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -19,6 +19,7 @@ use proptest::sample::Index; use proptest::strategy::ValueTree; use proptest::string::string_regex; use proptest::test_runner::TestRunner; +use varisat::{self, ExtendFormula}; pub fn resolve( pkg: PackageId, @@ -33,7 +34,11 @@ pub fn resolve_and_validated( deps: Vec, registry: &[Summary], ) -> CargoResult> { - let resolve = resolve_with_config_raw(pkg, deps, registry, None)?; + let should_resolve = sat_resolve(&deps, registry); + let resolve = resolve_with_config_raw(pkg, deps, registry, None); + assert_eq!(resolve.is_ok(), should_resolve.is_some()); + + let resolve = resolve?; let mut stack = vec![pkg]; let mut used = HashSet::new(); let mut links = HashSet::new(); @@ -176,6 +181,106 @@ pub fn resolve_with_config_raw( resolve } +// Returns if `a` and `b` are compatible in the semver sense. This is a +// commutative operation. +// +// Versions `a` and `b` are compatible if their left-most nonzero digit is the +// same. +fn compatible(a: &semver::Version, b: &semver::Version) -> bool { + if a.major != b.major { + return false; + } + if a.major != 0 { + return true; + } + if a.minor != b.minor { + return false; + } + if a.minor != 0 { + return true; + } + a.patch == b.patch +} + +/// Resolution can be reduced to the SAT problem. So this is an alternative implementation +/// of the resolver that uses a SAT library for the hard work. This is intended to be easy to read, +/// as compared to the real resolver. +/// +/// For the subset of functionality that are currently made by `registry_strategy` this will, +/// find a valid resolution if one exists. +/// +/// The SAT library dose not optimize for the newer version, +/// so the selected packages may not match the real resolver. +fn sat_resolve(deps: &[Dependency], registry: &[Summary]) -> Option> { + let mut solver = varisat::Solver::new(); + let var_for_is_packages_used: HashMap = registry + .iter() + .map(|s| s.package_id()) + .zip(solver.new_var_iter(registry.len())) + .collect(); + + let packages_is_used_for_var: HashMap = var_for_is_packages_used + .iter() + .map(|(&p, &v)| (v, p)) + .collect(); + + // the starting `deps` need to be satisfied + for dep in deps.iter() { + let matches: Vec = registry + .iter() + .map(|s| s.package_id()) + .filter(|&p| dep.matches_id(p)) + .map(|p| var_for_is_packages_used[&p].positive()) + .collect(); + solver.add_clause(&matches); + } + + // no two packages with the same links set + // no two semver compatible versions of the same package. + for (i, p) in registry.iter().enumerate() { + for o in registry[i..].iter().skip(1) { + assert_ne!(p.package_id(), o.package_id()); + if (p.name() == o.name() && compatible(p.version(), o.version())) + || (p.links().is_some() && p.links() == o.links()) + { + // These two packages can not be activated at the same time. + // There is a more efficient way to encode a "at most one" constraint but this works. + solver.add_clause(&[ + var_for_is_packages_used[&p.package_id()].negative(), + var_for_is_packages_used[&o.package_id()].negative(), + ]); + } + } + } + + // active packages need each of there `deps` to be satisfied + for p in registry.iter() { + for dep in p.dependencies() { + let mut matches: Vec = registry + .iter() + .map(|s| s.package_id()) + .filter(|&p| dep.matches_id(p)) + .map(|p| var_for_is_packages_used[&p].positive()) + .collect(); + // ^ the `dep` is satisfied or `p` is not active + matches.push(var_for_is_packages_used[&p.package_id()].negative()); + solver.add_clause(&matches); + } + } + + // TODO: public & private deps + + solver + .solve() + .expect("docs say it can't error in default config"); + + solver.model().map(|l| { + l.iter() + .filter_map(|v| packages_is_used_for_var.get(&v.var()).cloned()) + .collect() + }) +} + pub trait ToDep { fn to_dep(self) -> Dependency; } From f8008a46cf2fc225fe56d2065e178b9da0f697fc Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Mon, 20 May 2019 16:34:46 -0400 Subject: [PATCH 02/13] make n smaller in the O(n^2) parts --- tests/testsuite/support/resolver.rs | 91 ++++++++++++++++------------- 1 file changed, 49 insertions(+), 42 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index bfadb1821bc..35af628488c 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -181,25 +181,14 @@ pub fn resolve_with_config_raw( resolve } -// Returns if `a` and `b` are compatible in the semver sense. This is a -// commutative operation. -// -// Versions `a` and `b` are compatible if their left-most nonzero digit is the -// same. -fn compatible(a: &semver::Version, b: &semver::Version) -> bool { - if a.major != b.major { - return false; - } - if a.major != 0 { - return true; - } - if a.minor != b.minor { - return false; - } - if a.minor != 0 { - return true; +fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) { + for (i, p) in vars.iter().enumerate() { + for o in vars[i..].iter().skip(1) { + assert_ne!(p, o); + // There is a more efficient way to encode a "at most one" constraint but this works. + solver.add_clause(&[p.negative(), o.negative()]); + } } - a.patch == b.patch } /// Resolution can be reduced to the SAT problem. So this is an alternative implementation @@ -224,42 +213,60 @@ fn sat_resolve(deps: &[Dependency], registry: &[Summary]) -> Option> = HashMap::new(); + for p in registry.iter() { + if let Some(l) = p.links() { + by_links + .entry(l) + .or_default() + .push(var_for_is_packages_used[&p.package_id()]) + } + } + for link in by_links.values() { + sat_at_most_one(&mut solver, link); + } + + // no two semver compatible versions of the same package + let mut by_activations_keys: HashMap<_, Vec> = HashMap::new(); + for p in registry.iter() { + by_activations_keys + .entry(p.package_id().as_activations_key()) + .or_default() + .push(var_for_is_packages_used[&p.package_id()]) + } + for key in by_activations_keys.values() { + sat_at_most_one(&mut solver, key); + } + + let mut by_name: HashMap<_, Vec> = HashMap::new(); + + for p in registry.iter() { + by_name.entry(p.name()).or_default().push(p.package_id()) + } + + let empty_vec = vec![]; + // the starting `deps` need to be satisfied for dep in deps.iter() { - let matches: Vec = registry + let matches: Vec = by_name + .get(&dep.package_name()) + .unwrap_or(&empty_vec) .iter() - .map(|s| s.package_id()) - .filter(|&p| dep.matches_id(p)) + .filter(|&p| dep.matches_id(*p)) .map(|p| var_for_is_packages_used[&p].positive()) .collect(); solver.add_clause(&matches); } - // no two packages with the same links set - // no two semver compatible versions of the same package. - for (i, p) in registry.iter().enumerate() { - for o in registry[i..].iter().skip(1) { - assert_ne!(p.package_id(), o.package_id()); - if (p.name() == o.name() && compatible(p.version(), o.version())) - || (p.links().is_some() && p.links() == o.links()) - { - // These two packages can not be activated at the same time. - // There is a more efficient way to encode a "at most one" constraint but this works. - solver.add_clause(&[ - var_for_is_packages_used[&p.package_id()].negative(), - var_for_is_packages_used[&o.package_id()].negative(), - ]); - } - } - } - // active packages need each of there `deps` to be satisfied for p in registry.iter() { for dep in p.dependencies() { - let mut matches: Vec = registry + let mut matches: Vec = by_name + .get(&dep.package_name()) + .unwrap_or(&empty_vec) .iter() - .map(|s| s.package_id()) - .filter(|&p| dep.matches_id(p)) + .filter(|&p| dep.matches_id(*p)) .map(|p| var_for_is_packages_used[&p].positive()) .collect(); // ^ the `dep` is satisfied or `p` is not active From 52cf0f733eda45ac9cb7ce5341e39710a81b50e3 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Mon, 20 May 2019 17:31:05 -0400 Subject: [PATCH 03/13] use a better encoding --- tests/testsuite/support/resolver.rs | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 35af628488c..2f67be4bd55 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -181,12 +181,25 @@ pub fn resolve_with_config_raw( resolve } +const fn num_bits() -> usize { + std::mem::size_of::() * 8 +} + +fn log_bits(x: usize) -> usize { + if x == 0 { + return 0; + } + assert!(x > 0); + (num_bits::() as u32 - x.leading_zeros()) as usize +} + fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) { + // use the "Binary Encoding" from + // https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf + let bits: Vec = solver.new_var_iter(log_bits(vars.len())).collect(); for (i, p) in vars.iter().enumerate() { - for o in vars[i..].iter().skip(1) { - assert_ne!(p, o); - // There is a more efficient way to encode a "at most one" constraint but this works. - solver.add_clause(&[p.negative(), o.negative()]); + for b in 0..bits.len() { + solver.add_clause(&[p.negative(), bits[b].lit(((1 << b) & i) > 0)]); } } } From 3c87b4026e8ae8f3d28b13f618c06c0604c38a9d Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Mon, 20 May 2019 22:39:18 -0400 Subject: [PATCH 04/13] amortize constructing the SAT solver --- tests/testsuite/resolve.rs | 7 +- tests/testsuite/support/resolver.rs | 146 +++++++++++++--------------- 2 files changed, 74 insertions(+), 79 deletions(-) diff --git a/tests/testsuite/resolve.rs b/tests/testsuite/resolve.rs index 3a79477659e..b36d0bd2f73 100644 --- a/tests/testsuite/resolve.rs +++ b/tests/testsuite/resolve.rs @@ -9,7 +9,7 @@ use crate::support::registry::Package; use crate::support::resolver::{ assert_contains, assert_same, dep, dep_kind, dep_loc, dep_req, dep_req_kind, loc_names, names, pkg, pkg_dep, pkg_id, pkg_loc, registry, registry_strategy, remove_dep, resolve, - resolve_and_validated, resolve_with_config, PrettyPrintRegistry, ToDep, ToPkgId, + resolve_and_validated, resolve_with_config, PrettyPrintRegistry, SatResolve, ToDep, ToPkgId, }; use proptest::prelude::*; @@ -41,15 +41,18 @@ proptest! { PrettyPrintRegistry(input) in registry_strategy(50, 20, 60) ) { let reg = registry(input.clone()); + let mut sat_resolve = SatResolve::new(®); // there is only a small chance that any one // crate will be interesting. // So we try some of the most complicated. for this in input.iter().rev().take(20) { - let _ = resolve_and_validated( + let should_resolve = sat_resolve.sat_resolve(this.package_id()); + let resolve = resolve_and_validated( pkg_id("root"), vec![dep_req(&this.name(), &format!("={}", this.version()))], ®, ); + assert_eq!(resolve.is_ok(), should_resolve); } } diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 2f67be4bd55..23acfe5b51f 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -34,11 +34,7 @@ pub fn resolve_and_validated( deps: Vec, registry: &[Summary], ) -> CargoResult> { - let should_resolve = sat_resolve(&deps, registry); - let resolve = resolve_with_config_raw(pkg, deps, registry, None); - assert_eq!(resolve.is_ok(), should_resolve.is_some()); - - let resolve = resolve?; + let resolve = resolve_with_config_raw(pkg, deps, registry, None)?; let mut stack = vec![pkg]; let mut used = HashSet::new(); let mut links = HashSet::new(); @@ -213,92 +209,88 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va /// /// The SAT library dose not optimize for the newer version, /// so the selected packages may not match the real resolver. -fn sat_resolve(deps: &[Dependency], registry: &[Summary]) -> Option> { - let mut solver = varisat::Solver::new(); - let var_for_is_packages_used: HashMap = registry - .iter() - .map(|s| s.package_id()) - .zip(solver.new_var_iter(registry.len())) - .collect(); +pub struct SatResolve { + solver: varisat::Solver<'static>, + var_for_is_packages_used: HashMap, +} - let packages_is_used_for_var: HashMap = var_for_is_packages_used - .iter() - .map(|(&p, &v)| (v, p)) - .collect(); - - // no two packages with the same links set - let mut by_links: HashMap<_, Vec> = HashMap::new(); - for p in registry.iter() { - if let Some(l) = p.links() { - by_links - .entry(l) +impl SatResolve { + pub fn new(registry: &[Summary]) -> Self { + let mut solver = varisat::Solver::new(); + let var_for_is_packages_used: HashMap = registry + .iter() + .map(|s| s.package_id()) + .zip(solver.new_var_iter(registry.len())) + .collect(); + + // no two packages with the same links set + let mut by_links: HashMap<_, Vec> = HashMap::new(); + for p in registry.iter() { + if let Some(l) = p.links() { + by_links + .entry(l) + .or_default() + .push(var_for_is_packages_used[&p.package_id()]) + } + } + for link in by_links.values() { + sat_at_most_one(&mut solver, link); + } + + // no two semver compatible versions of the same package + let mut by_activations_keys: HashMap<_, Vec> = HashMap::new(); + for p in registry.iter() { + by_activations_keys + .entry(p.package_id().as_activations_key()) .or_default() .push(var_for_is_packages_used[&p.package_id()]) } - } - for link in by_links.values() { - sat_at_most_one(&mut solver, link); - } + for key in by_activations_keys.values() { + sat_at_most_one(&mut solver, key); + } - // no two semver compatible versions of the same package - let mut by_activations_keys: HashMap<_, Vec> = HashMap::new(); - for p in registry.iter() { - by_activations_keys - .entry(p.package_id().as_activations_key()) - .or_default() - .push(var_for_is_packages_used[&p.package_id()]) - } - for key in by_activations_keys.values() { - sat_at_most_one(&mut solver, key); - } + let mut by_name: HashMap<_, Vec> = HashMap::new(); - let mut by_name: HashMap<_, Vec> = HashMap::new(); + for p in registry.iter() { + by_name.entry(p.name()).or_default().push(p.package_id()) + } - for p in registry.iter() { - by_name.entry(p.name()).or_default().push(p.package_id()) - } + let empty_vec = vec![]; - let empty_vec = vec![]; + // active packages need each of there `deps` to be satisfied + for p in registry.iter() { + for dep in p.dependencies() { + let mut matches: Vec = by_name + .get(&dep.package_name()) + .unwrap_or(&empty_vec) + .iter() + .filter(|&p| dep.matches_id(*p)) + .map(|p| var_for_is_packages_used[&p].positive()) + .collect(); + // ^ the `dep` is satisfied or `p` is not active + matches.push(var_for_is_packages_used[&p.package_id()].negative()); + solver.add_clause(&matches); + } + } - // the starting `deps` need to be satisfied - for dep in deps.iter() { - let matches: Vec = by_name - .get(&dep.package_name()) - .unwrap_or(&empty_vec) - .iter() - .filter(|&p| dep.matches_id(*p)) - .map(|p| var_for_is_packages_used[&p].positive()) - .collect(); - solver.add_clause(&matches); - } + // TODO: public & private deps - // active packages need each of there `deps` to be satisfied - for p in registry.iter() { - for dep in p.dependencies() { - let mut matches: Vec = by_name - .get(&dep.package_name()) - .unwrap_or(&empty_vec) - .iter() - .filter(|&p| dep.matches_id(*p)) - .map(|p| var_for_is_packages_used[&p].positive()) - .collect(); - // ^ the `dep` is satisfied or `p` is not active - matches.push(var_for_is_packages_used[&p.package_id()].negative()); - solver.add_clause(&matches); + SatResolve { + solver, + var_for_is_packages_used, } } + pub fn sat_resolve(&mut self, dep: PackageId) -> bool { + // the starting `dep` need to be satisfied + self.solver + .assume(&[self.var_for_is_packages_used[&dep].positive()]); - // TODO: public & private deps + self.solver + .solve() + .expect("docs say it can't error in default config"); - solver - .solve() - .expect("docs say it can't error in default config"); - - solver.model().map(|l| { - l.iter() - .filter_map(|v| packages_is_used_for_var.get(&v.var()).cloned()) - .collect() - }) + self.solver.model().is_some() + } } pub trait ToDep { From c7e23ae20f6db422efb3f2ec1e3740b6229b3e95 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Tue, 21 May 2019 12:58:05 -0400 Subject: [PATCH 05/13] maintain almost the same interface --- tests/testsuite/resolve.rs | 15 ++++---- tests/testsuite/support/resolver.rs | 58 +++++++++++++++++++++++++---- 2 files changed, 57 insertions(+), 16 deletions(-) diff --git a/tests/testsuite/resolve.rs b/tests/testsuite/resolve.rs index b36d0bd2f73..0ffc14ee6ba 100644 --- a/tests/testsuite/resolve.rs +++ b/tests/testsuite/resolve.rs @@ -46,13 +46,12 @@ proptest! { // crate will be interesting. // So we try some of the most complicated. for this in input.iter().rev().take(20) { - let should_resolve = sat_resolve.sat_resolve(this.package_id()); - let resolve = resolve_and_validated( + let _ = resolve_and_validated( pkg_id("root"), vec![dep_req(&this.name(), &format!("={}", this.version()))], ®, + Some(&mut sat_resolve), ); - assert_eq!(resolve.is_ok(), should_resolve); } } @@ -248,7 +247,7 @@ fn basic_public_dependency() { pkg!("C" => [dep("A"), dep("B")]), ]); - let res = resolve_and_validated(pkg_id("root"), vec![dep("C")], ®).unwrap(); + let res = resolve_and_validated(pkg_id("root"), vec![dep("C")], ®, None).unwrap(); assert_same( &res, &names(&[ @@ -284,7 +283,7 @@ fn public_dependency_filling_in() { pkg!("d" => [dep("c"), dep("a"), dep("b")]), ]); - let res = resolve_and_validated(pkg_id("root"), vec![dep("d")], ®).unwrap(); + let res = resolve_and_validated(pkg_id("root"), vec![dep("d")], ®, None).unwrap(); assert_same( &res, &names(&[ @@ -319,7 +318,7 @@ fn public_dependency_filling_in_and_update() { pkg!("C" => [dep("A"),dep("B")]), pkg!("D" => [dep("B"),dep("C")]), ]); - let res = resolve_and_validated(pkg_id("root"), vec![dep("D")], ®).unwrap(); + let res = resolve_and_validated(pkg_id("root"), vec![dep("D")], ®, None).unwrap(); assert_same( &res, &names(&[ @@ -1410,7 +1409,7 @@ fn conflict_store_bug() { ]; let reg = registry(input); - let _ = resolve_and_validated(pkg_id("root"), vec![dep("j")], ®); + let _ = resolve_and_validated(pkg_id("root"), vec![dep("j")], ®, None); } #[test] @@ -1438,5 +1437,5 @@ fn conflict_store_more_then_one_match() { ]), ]; let reg = registry(input); - let _ = resolve_and_validated(pkg_id("root"), vec![dep("nA")], ®); + let _ = resolve_and_validated(pkg_id("root"), vec![dep("nA")], ®, None); } diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 23acfe5b51f..7db80f98678 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -33,8 +33,17 @@ pub fn resolve_and_validated( pkg: PackageId, deps: Vec, registry: &[Summary], + sat_resolve: Option<&mut SatResolve>, ) -> CargoResult> { - let resolve = resolve_with_config_raw(pkg, deps, registry, None)?; + let should_resolve = if let Some(sat) = sat_resolve { + sat.sat_resolve(&deps) + } else { + SatResolve::new(registry).sat_resolve(&deps) + }; + let resolve = resolve_with_config_raw(pkg, deps, registry, None); + assert_eq!(resolve.is_ok(), should_resolve); + + let resolve = resolve?; let mut stack = vec![pkg]; let mut used = HashSet::new(); let mut links = HashSet::new(); @@ -212,6 +221,7 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va pub struct SatResolve { solver: varisat::Solver<'static>, var_for_is_packages_used: HashMap, + by_name: HashMap<&'static str, Vec>, } impl SatResolve { @@ -249,10 +259,13 @@ impl SatResolve { sat_at_most_one(&mut solver, key); } - let mut by_name: HashMap<_, Vec> = HashMap::new(); + let mut by_name: HashMap<&'static str, Vec> = HashMap::new(); for p in registry.iter() { - by_name.entry(p.name()).or_default().push(p.package_id()) + by_name + .entry(p.name().as_str()) + .or_default() + .push(p.package_id()) } let empty_vec = vec![]; @@ -261,7 +274,7 @@ impl SatResolve { for p in registry.iter() { for dep in p.dependencies() { let mut matches: Vec = by_name - .get(&dep.package_name()) + .get(dep.package_name().as_str()) .unwrap_or(&empty_vec) .iter() .filter(|&p| dep.matches_id(*p)) @@ -278,12 +291,41 @@ impl SatResolve { SatResolve { solver, var_for_is_packages_used, + by_name, } } - pub fn sat_resolve(&mut self, dep: PackageId) -> bool { - // the starting `dep` need to be satisfied - self.solver - .assume(&[self.var_for_is_packages_used[&dep].positive()]); + pub fn sat_resolve(&mut self, deps: &[Dependency]) -> bool { + let mut assumption = vec![]; + let mut this_call = None; + + // the starting `deps` need to be satisfied + for dep in deps.iter() { + let empty_vec = vec![]; + let matches: Vec = self + .by_name + .get(dep.package_name().as_str()) + .unwrap_or(&empty_vec) + .iter() + .filter(|&p| dep.matches_id(*p)) + .map(|p| self.var_for_is_packages_used[&p].positive()) + .collect(); + if matches.is_empty() { + return false; + } else if matches.len() == 1 { + assumption.extend_from_slice(&matches) + } else { + if this_call.is_none() { + let new_var = self.solver.new_var(); + this_call = Some(new_var); + assumption.push(new_var.positive()); + } + let mut matches = matches; + matches.push(this_call.unwrap().negative()); + self.solver.add_clause(&matches); + } + } + + self.solver.assume(&assumption); self.solver .solve() From 6454efdd67dfbc426b275a7a1cfc45dd6fc0f392 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Wed, 22 May 2019 09:28:58 -0400 Subject: [PATCH 06/13] support public & private deps --- tests/testsuite/resolve.rs | 12 +++ tests/testsuite/support/resolver.rs | 114 ++++++++++++++++++++++++++-- 2 files changed, 118 insertions(+), 8 deletions(-) diff --git a/tests/testsuite/resolve.rs b/tests/testsuite/resolve.rs index 0ffc14ee6ba..fc86cb3ce9f 100644 --- a/tests/testsuite/resolve.rs +++ b/tests/testsuite/resolve.rs @@ -238,6 +238,18 @@ proptest! { } } +#[test] +fn pub_fail() { + let input = vec![ + pkg!(("a", "0.0.4")), + pkg!(("a", "0.0.5")), + pkg!(("e", "0.0.6") => [dep_req_kind("a", "<= 0.0.4", Kind::Normal, true),]), + pkg!(("kB", "0.0.3") => [dep_req("a", ">= 0.0.5"),dep("e"),]), + ]; + let reg = registry(input.clone()); + assert!(resolve_and_validated(pkg_id("root"), vec![dep("kB")], ®, None).is_err()); +} + #[test] fn basic_public_dependency() { let reg = registry(vec![ diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 7db80f98678..b8870cf9c2d 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -199,6 +199,15 @@ fn log_bits(x: usize) -> usize { } fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) { + if vars.len() <= 1 { + return; + } else if vars.len() == 2 { + solver.add_clause(&[vars[0].negative(), vars[1].negative()]); + } else if vars.len() == 3 { + solver.add_clause(&[vars[0].negative(), vars[1].negative()]); + solver.add_clause(&[vars[0].negative(), vars[2].negative()]); + solver.add_clause(&[vars[1].negative(), vars[2].negative()]); + } // use the "Binary Encoding" from // https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf let bits: Vec = solver.new_var_iter(log_bits(vars.len())).collect(); @@ -229,8 +238,7 @@ impl SatResolve { let mut solver = varisat::Solver::new(); let var_for_is_packages_used: HashMap = registry .iter() - .map(|s| s.package_id()) - .zip(solver.new_var_iter(registry.len())) + .map(|s| (s.package_id(), solver.new_var())) .collect(); // no two packages with the same links set @@ -270,23 +278,113 @@ impl SatResolve { let empty_vec = vec![]; + let mut version_selected_for: HashMap< + (PackageId, Dependency), + HashMap, + > = HashMap::new(); // active packages need each of there `deps` to be satisfied for p in registry.iter() { for dep in p.dependencies() { - let mut matches: Vec = by_name + let version: HashMap = by_name .get(dep.package_name().as_str()) .unwrap_or(&empty_vec) .iter() .filter(|&p| dep.matches_id(*p)) - .map(|p| var_for_is_packages_used[&p].positive()) + .map(|&p| (p, solver.new_var())) + .collect(); + // if `p` is active then we need to select one of the versions + let matches: Vec<_> = version + .values() + .map(|v| v.positive()) + .chain(Some(var_for_is_packages_used[&p.package_id()].negative())) .collect(); - // ^ the `dep` is satisfied or `p` is not active - matches.push(var_for_is_packages_used[&p.package_id()].negative()); solver.add_clause(&matches); + for (pid, var) in version.iter() { + // if a version is selected then it needs to be activated + solver.add_clause(&[var.negative(), var_for_is_packages_used[pid].positive()]); + } + version_selected_for.insert((p.package_id(), dep.clone()), version); } } - // TODO: public & private deps + let publicly_exports: HashMap> = registry + .iter() + .map(|s| { + ( + s.package_id(), + registry + .iter() + .map(|s| (s.package_id(), solver.new_var())) + .collect(), + ) + }) + .collect(); + + for s in registry.iter() { + // everything publicly depends on itself + solver.add_clause(&[publicly_exports[&s.package_id()][&s.package_id()].positive()]); + } + + // if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports` + for p in registry.iter() { + for dep in p.dependencies().iter().filter(|d| d.is_public()) { + for (ver, sel) in version_selected_for[&(p.package_id(), dep.clone())].iter() { + for export in registry.iter() { + solver.add_clause(&[ + sel.negative(), + publicly_exports[ver][&export.package_id()].negative(), + publicly_exports[&p.package_id()][&export.package_id()].positive(), + ]); + } + } + } + } + + let can_see: HashMap> = registry + .iter() + .map(|s| { + ( + s.package_id(), + registry + .iter() + .map(|s| (s.package_id(), solver.new_var())) + .collect(), + ) + }) + .collect(); + + // if `p` `publicly_exports` `export` then it `can_see` `export` + for p in registry.iter() { + for export in registry.iter() { + solver.add_clause(&[ + publicly_exports[&p.package_id()][&export.package_id()].negative(), + can_see[&p.package_id()][&export.package_id()].positive(), + ]); + } + } + + // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports` + for p in registry.iter() { + for dep in p.dependencies().iter() { + for (ver, sel) in version_selected_for[&(p.package_id(), dep.clone())].iter() { + for export in registry.iter() { + solver.add_clause(&[ + sel.negative(), + publicly_exports[ver][&export.package_id()].negative(), + can_see[&p.package_id()][&export.package_id()].positive(), + ]); + } + } + } + } + + // a package `can_see` only one version by each name + for (_, see) in can_see.iter() { + for (_, vers) in by_name.iter() { + let same_name: Vec<_> = vers.iter().map(|p| see[p]).collect(); + sat_at_most_one(&mut solver, &same_name); + } + } SatResolve { solver, @@ -686,7 +784,7 @@ pub fn registry_strategy( // => Kind::Development, // Development has no impact so don't gen _ => panic!("bad index for Kind"), }, - p, + p && k == 0, )) } From a25d8e9e96df7942b57bdf914b3b5d88877c4b79 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Wed, 22 May 2019 12:02:01 -0400 Subject: [PATCH 07/13] use a topological_order to only make a var where needed --- tests/testsuite/support/resolver.rs | 109 +++++++++++++++------------- 1 file changed, 58 insertions(+), 51 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index b8870cf9c2d..6c38b5f95cc 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -11,7 +11,7 @@ use cargo::core::resolver::{self, Method}; use cargo::core::source::{GitReference, SourceId}; use cargo::core::Resolve; use cargo::core::{Dependency, PackageId, Registry, Summary}; -use cargo::util::{CargoResult, Config, ToUrl}; +use cargo::util::{CargoResult, Config, Graph, ToUrl}; use proptest::collection::{btree_map, vec}; use proptest::prelude::*; @@ -278,12 +278,15 @@ impl SatResolve { let empty_vec = vec![]; + let mut graph: Graph = Graph::new(); + let mut version_selected_for: HashMap< - (PackageId, Dependency), - HashMap, + PackageId, + HashMap>, > = HashMap::new(); // active packages need each of there `deps` to be satisfied for p in registry.iter() { + graph.add(p.package_id()); for dep in p.dependencies() { let version: HashMap = by_name .get(dep.package_name().as_str()) @@ -302,76 +305,80 @@ impl SatResolve { for (pid, var) in version.iter() { // if a version is selected then it needs to be activated solver.add_clause(&[var.negative(), var_for_is_packages_used[pid].positive()]); + graph.link(p.package_id(), *pid); } - version_selected_for.insert((p.package_id(), dep.clone()), version); + version_selected_for + .entry(p.package_id()) + .or_default() + .insert(dep.clone(), version); } } - let publicly_exports: HashMap> = registry - .iter() - .map(|s| { - ( - s.package_id(), - registry - .iter() - .map(|s| (s.package_id(), solver.new_var())) - .collect(), - ) - }) - .collect(); + let topological_order = graph.sort(); + + let mut publicly_exports: HashMap> = + HashMap::new(); for s in registry.iter() { // everything publicly depends on itself - solver.add_clause(&[publicly_exports[&s.package_id()][&s.package_id()].positive()]); + let var = publicly_exports + .entry(s.package_id()) + .or_default() + .entry(s.package_id()) + .or_insert_with(|| solver.new_var()); + solver.add_clause(&[var.positive()]); } // if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports` - for p in registry.iter() { - for dep in p.dependencies().iter().filter(|d| d.is_public()) { - for (ver, sel) in version_selected_for[&(p.package_id(), dep.clone())].iter() { - for export in registry.iter() { - solver.add_clause(&[ - sel.negative(), - publicly_exports[ver][&export.package_id()].negative(), - publicly_exports[&p.package_id()][&export.package_id()].positive(), - ]); + for &p in topological_order.iter() { + if let Some(deps) = version_selected_for.get(&p) { + for (_, versions) in deps.iter().filter(|(d, _)| d.is_public()) { + for (ver, sel) in versions { + for (&export_pid, &export_var) in publicly_exports[ver].clone().iter() { + let our_var = publicly_exports + .entry(p) + .or_default() + .entry(export_pid) + .or_insert_with(|| solver.new_var()); + solver.add_clause(&[ + sel.negative(), + export_var.negative(), + our_var.positive(), + ]); + } } } } } - let can_see: HashMap> = registry - .iter() - .map(|s| { - ( - s.package_id(), - registry - .iter() - .map(|s| (s.package_id(), solver.new_var())) - .collect(), - ) - }) - .collect(); + let mut can_see: HashMap> = HashMap::new(); // if `p` `publicly_exports` `export` then it `can_see` `export` - for p in registry.iter() { - for export in registry.iter() { - solver.add_clause(&[ - publicly_exports[&p.package_id()][&export.package_id()].negative(), - can_see[&p.package_id()][&export.package_id()].positive(), - ]); + for (&p, exports) in &publicly_exports { + for (&export_pid, export_var) in exports { + let our_var = can_see + .entry(p) + .or_default() + .entry(export_pid) + .or_insert_with(|| solver.new_var()); + solver.add_clause(&[export_var.negative(), our_var.positive()]); } } // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports` - for p in registry.iter() { - for dep in p.dependencies().iter() { - for (ver, sel) in version_selected_for[&(p.package_id(), dep.clone())].iter() { - for export in registry.iter() { + for (&p, deps) in version_selected_for.iter() { + for (_, versions) in deps { + for (ver, sel) in versions { + for (&export_pid, &export_var) in publicly_exports[ver].iter() { + let our_var = can_see + .entry(p) + .or_default() + .entry(export_pid) + .or_insert_with(|| solver.new_var()); solver.add_clause(&[ sel.negative(), - publicly_exports[ver][&export.package_id()].negative(), - can_see[&p.package_id()][&export.package_id()].positive(), + export_var.negative(), + our_var.positive(), ]); } } @@ -381,7 +388,7 @@ impl SatResolve { // a package `can_see` only one version by each name for (_, see) in can_see.iter() { for (_, vers) in by_name.iter() { - let same_name: Vec<_> = vers.iter().map(|p| see[p]).collect(); + let same_name: Vec<_> = vers.iter().filter_map(|p| see.get(p).cloned()).collect(); sat_at_most_one(&mut solver, &same_name); } } From c68334ff4a78382feb8b07730b46f75e0866e41a Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Wed, 22 May 2019 12:49:57 -0400 Subject: [PATCH 08/13] Think of `publicly_exports` as being in terms of a set of `activations_key`s --- tests/testsuite/support/resolver.rs | 64 ++++++++++++++++++----------- 1 file changed, 40 insertions(+), 24 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 6c38b5f95cc..44dcf7a23c1 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -282,49 +282,60 @@ impl SatResolve { let mut version_selected_for: HashMap< PackageId, - HashMap>, + HashMap>, > = HashMap::new(); // active packages need each of there `deps` to be satisfied for p in registry.iter() { graph.add(p.package_id()); for dep in p.dependencies() { - let version: HashMap = by_name + let mut by_key: HashMap<_, Vec> = HashMap::new(); + for &m in by_name .get(dep.package_name().as_str()) .unwrap_or(&empty_vec) .iter() .filter(|&p| dep.matches_id(*p)) - .map(|&p| (p, solver.new_var())) - .collect(); - // if `p` is active then we need to select one of the versions - let matches: Vec<_> = version + { + by_key + .entry(m.as_activations_key()) + .or_default() + .push(var_for_is_packages_used[&m].positive()); + } + let keys: HashMap<_, _> = by_key.keys().map(|&k| (k, solver.new_var())).collect(); + + // if `p` is active then we need to select one of the keys + let matches: Vec<_> = keys .values() .map(|v| v.positive()) .chain(Some(var_for_is_packages_used[&p.package_id()].negative())) .collect(); solver.add_clause(&matches); - for (pid, var) in version.iter() { - // if a version is selected then it needs to be activated - solver.add_clause(&[var.negative(), var_for_is_packages_used[pid].positive()]); - graph.link(p.package_id(), *pid); + + // if a key is active then we need to select one of the versions + for (key, vars) in by_key.iter() { + let mut matches = vars.clone(); + matches.push(keys[key].negative()); + solver.add_clause(&matches); } + version_selected_for .entry(p.package_id()) .or_default() - .insert(dep.clone(), version); + .insert(dep.clone(), keys); } } let topological_order = graph.sort(); - let mut publicly_exports: HashMap> = - HashMap::new(); + // we already ensure there is only one version for each `activations_key` so we can think of + // `publicly_exports` as being in terms of a set of `activations_key`s + let mut publicly_exports: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new(); - for s in registry.iter() { + for &key in by_activations_keys.keys() { // everything publicly depends on itself let var = publicly_exports - .entry(s.package_id()) + .entry(key) .or_default() - .entry(s.package_id()) + .entry(key) .or_insert_with(|| solver.new_var()); solver.add_clause(&[var.positive()]); } @@ -336,7 +347,7 @@ impl SatResolve { for (ver, sel) in versions { for (&export_pid, &export_var) in publicly_exports[ver].clone().iter() { let our_var = publicly_exports - .entry(p) + .entry(p.as_activations_key()) .or_default() .entry(export_pid) .or_insert_with(|| solver.new_var()); @@ -351,7 +362,9 @@ impl SatResolve { } } - let mut can_see: HashMap> = HashMap::new(); + // we already ensure there is only one version for each `activations_key` so we can think of + // `can_see` as being in terms of a set of `activations_key`s + let mut can_see: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new(); // if `p` `publicly_exports` `export` then it `can_see` `export` for (&p, exports) in &publicly_exports { @@ -368,10 +381,10 @@ impl SatResolve { // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports` for (&p, deps) in version_selected_for.iter() { for (_, versions) in deps { - for (ver, sel) in versions { - for (&export_pid, &export_var) in publicly_exports[ver].iter() { + for (&ver, sel) in versions { + for (&export_pid, &export_var) in publicly_exports[&ver].iter() { let our_var = can_see - .entry(p) + .entry(p.as_activations_key()) .or_default() .entry(export_pid) .or_insert_with(|| solver.new_var()); @@ -387,9 +400,12 @@ impl SatResolve { // a package `can_see` only one version by each name for (_, see) in can_see.iter() { - for (_, vers) in by_name.iter() { - let same_name: Vec<_> = vers.iter().filter_map(|p| see.get(p).cloned()).collect(); - sat_at_most_one(&mut solver, &same_name); + let mut by_name: HashMap<&'static str, Vec> = HashMap::new(); + for ((name, _, _), &var) in see { + by_name.entry(name.as_str()).or_default().push(var); + } + for same_name in by_name.values() { + sat_at_most_one(&mut solver, same_name); } } From 5143c0cab3ec0161903680e35496243f5a7d004d Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Thu, 23 May 2019 13:58:18 -0400 Subject: [PATCH 09/13] Work around accidentally quadratic debug_assert in varisat --- tests/testsuite/support/resolver.rs | 47 +++++++++++++++++------------ 1 file changed, 28 insertions(+), 19 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 44dcf7a23c1..54f9ba8d5b7 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -235,10 +235,10 @@ pub struct SatResolve { impl SatResolve { pub fn new(registry: &[Summary]) -> Self { - let mut solver = varisat::Solver::new(); + let mut cnf = varisat::CnfFormula::new(); let var_for_is_packages_used: HashMap = registry .iter() - .map(|s| (s.package_id(), solver.new_var())) + .map(|s| (s.package_id(), cnf.new_var())) .collect(); // no two packages with the same links set @@ -252,7 +252,7 @@ impl SatResolve { } } for link in by_links.values() { - sat_at_most_one(&mut solver, link); + sat_at_most_one(&mut cnf, link); } // no two semver compatible versions of the same package @@ -264,7 +264,7 @@ impl SatResolve { .push(var_for_is_packages_used[&p.package_id()]) } for key in by_activations_keys.values() { - sat_at_most_one(&mut solver, key); + sat_at_most_one(&mut cnf, key); } let mut by_name: HashMap<&'static str, Vec> = HashMap::new(); @@ -288,6 +288,9 @@ impl SatResolve { for p in registry.iter() { graph.add(p.package_id()); for dep in p.dependencies() { + // This can more easily be written as: + // !is_active(p) or one of the things that match dep is_active + // All the complexity, from here to the end, is to support public and private dependencies! let mut by_key: HashMap<_, Vec> = HashMap::new(); for &m in by_name .get(dep.package_name().as_str()) @@ -300,7 +303,7 @@ impl SatResolve { .or_default() .push(var_for_is_packages_used[&m].positive()); } - let keys: HashMap<_, _> = by_key.keys().map(|&k| (k, solver.new_var())).collect(); + let keys: HashMap<_, _> = by_key.keys().map(|&k| (k, cnf.new_var())).collect(); // if `p` is active then we need to select one of the keys let matches: Vec<_> = keys @@ -308,13 +311,13 @@ impl SatResolve { .map(|v| v.positive()) .chain(Some(var_for_is_packages_used[&p.package_id()].negative())) .collect(); - solver.add_clause(&matches); + cnf.add_clause(&matches); // if a key is active then we need to select one of the versions for (key, vars) in by_key.iter() { let mut matches = vars.clone(); matches.push(keys[key].negative()); - solver.add_clause(&matches); + cnf.add_clause(&matches); } version_selected_for @@ -336,8 +339,8 @@ impl SatResolve { .entry(key) .or_default() .entry(key) - .or_insert_with(|| solver.new_var()); - solver.add_clause(&[var.positive()]); + .or_insert_with(|| cnf.new_var()); + cnf.add_clause(&[var.positive()]); } // if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports` @@ -350,8 +353,8 @@ impl SatResolve { .entry(p.as_activations_key()) .or_default() .entry(export_pid) - .or_insert_with(|| solver.new_var()); - solver.add_clause(&[ + .or_insert_with(|| cnf.new_var()); + cnf.add_clause(&[ sel.negative(), export_var.negative(), our_var.positive(), @@ -373,8 +376,8 @@ impl SatResolve { .entry(p) .or_default() .entry(export_pid) - .or_insert_with(|| solver.new_var()); - solver.add_clause(&[export_var.negative(), our_var.positive()]); + .or_insert_with(|| cnf.new_var()); + cnf.add_clause(&[export_var.negative(), our_var.positive()]); } } @@ -387,8 +390,8 @@ impl SatResolve { .entry(p.as_activations_key()) .or_default() .entry(export_pid) - .or_insert_with(|| solver.new_var()); - solver.add_clause(&[ + .or_insert_with(|| cnf.new_var()); + cnf.add_clause(&[ sel.negative(), export_var.negative(), our_var.positive(), @@ -405,9 +408,17 @@ impl SatResolve { by_name.entry(name.as_str()).or_default().push(var); } for same_name in by_name.values() { - sat_at_most_one(&mut solver, same_name); + sat_at_most_one(&mut cnf, same_name); } } + let mut solver = varisat::Solver::new(); + solver.add_formula(&cnf); + + // We dont need to `solve` now. We know that "use nothing" will satisfy all the clauses so far. + // But things run faster if we let it spend some time figuring out how the constraints interact before we add assumptions. + solver + .solve() + .expect("docs say it can't error in default config"); SatResolve { solver, @@ -450,9 +461,7 @@ impl SatResolve { self.solver .solve() - .expect("docs say it can't error in default config"); - - self.solver.model().is_some() + .expect("docs say it can't error in default config") } } From 514039eda0c359b67b01663bcaaad4fadc7b06f8 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Thu, 23 May 2019 16:48:16 -0400 Subject: [PATCH 10/13] make sure the complicated cases are at the end --- tests/testsuite/support/resolver.rs | 43 ++++++++++++++++------------- 1 file changed, 24 insertions(+), 19 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 54f9ba8d5b7..dcc530d2206 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -820,25 +820,30 @@ pub fn registry_strategy( )) } - PrettyPrintRegistry( - list_of_pkgid - .into_iter() - .zip(dependency_by_pkgid.into_iter()) - .map(|(((name, ver), allow_deps), deps)| { - pkg_dep( - (name, ver).to_pkgid(), - if !allow_deps { - vec![dep_req("bad", "*")] - } else { - let mut deps = deps; - deps.sort_by_key(|d| d.name_in_toml()); - deps.dedup_by_key(|d| d.name_in_toml()); - deps - }, - ) - }) - .collect(), - ) + let mut out: Vec = list_of_pkgid + .into_iter() + .zip(dependency_by_pkgid.into_iter()) + .map(|(((name, ver), allow_deps), deps)| { + pkg_dep( + (name, ver).to_pkgid(), + if !allow_deps { + vec![dep_req("bad", "*")] + } else { + let mut deps = deps; + deps.sort_by_key(|d| d.name_in_toml()); + deps.dedup_by_key(|d| d.name_in_toml()); + deps + }, + ) + }) + .collect(); + + if reverse_alphabetical { + // make sure the complicated cases are at the end + out.reverse(); + } + + PrettyPrintRegistry(out) }, ) } From a7676ebc39708874e840af4029c3aab57eb3e075 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Thu, 23 May 2019 18:04:42 -0400 Subject: [PATCH 11/13] remove a redundant clause --- tests/testsuite/support/resolver.rs | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index dcc530d2206..ccb6b9621e3 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -369,18 +369,6 @@ impl SatResolve { // `can_see` as being in terms of a set of `activations_key`s let mut can_see: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new(); - // if `p` `publicly_exports` `export` then it `can_see` `export` - for (&p, exports) in &publicly_exports { - for (&export_pid, export_var) in exports { - let our_var = can_see - .entry(p) - .or_default() - .entry(export_pid) - .or_insert_with(|| cnf.new_var()); - cnf.add_clause(&[export_var.negative(), our_var.positive()]); - } - } - // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports` for (&p, deps) in version_selected_for.iter() { for (_, versions) in deps { From 84586611af27515f5f10692f52f0cc8eeb480692 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Fri, 24 May 2019 10:45:38 -0400 Subject: [PATCH 12/13] reuse vars where publicly_exports implies can_see --- tests/testsuite/support/resolver.rs | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index ccb6b9621e3..755dfc66b18 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -223,7 +223,8 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va /// as compared to the real resolver. /// /// For the subset of functionality that are currently made by `registry_strategy` this will, -/// find a valid resolution if one exists. +/// find a valid resolution if one exists. The big thing that the real resolver does, +/// that this one does not do is work with features and optional dependencies. /// /// The SAT library dose not optimize for the newer version, /// so the selected packages may not match the real resolver. @@ -346,14 +347,12 @@ impl SatResolve { // if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports` for &p in topological_order.iter() { if let Some(deps) = version_selected_for.get(&p) { + let mut p_exports = publicly_exports.remove(&p.as_activations_key()).unwrap(); for (_, versions) in deps.iter().filter(|(d, _)| d.is_public()) { for (ver, sel) in versions { - for (&export_pid, &export_var) in publicly_exports[ver].clone().iter() { - let our_var = publicly_exports - .entry(p.as_activations_key()) - .or_default() - .entry(export_pid) - .or_insert_with(|| cnf.new_var()); + for (&export_pid, &export_var) in publicly_exports[ver].iter() { + let our_var = + p_exports.entry(export_pid).or_insert_with(|| cnf.new_var()); cnf.add_clause(&[ sel.negative(), export_var.negative(), @@ -362,23 +361,22 @@ impl SatResolve { } } } + publicly_exports.insert(p.as_activations_key(), p_exports); } } // we already ensure there is only one version for each `activations_key` so we can think of // `can_see` as being in terms of a set of `activations_key`s - let mut can_see: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new(); + // and if `p` `publicly_exports` `export` then it `can_see` `export` + let mut can_see: HashMap<_, HashMap<_, varisat::Var>> = publicly_exports.clone(); // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports` for (&p, deps) in version_selected_for.iter() { - for (_, versions) in deps { + let p_can_see = can_see.entry(p.as_activations_key()).or_default(); + for (_, versions) in deps.iter().filter(|(d, _)| !d.is_public()) { for (&ver, sel) in versions { for (&export_pid, &export_var) in publicly_exports[&ver].iter() { - let our_var = can_see - .entry(p.as_activations_key()) - .or_default() - .entry(export_pid) - .or_insert_with(|| cnf.new_var()); + let our_var = p_can_see.entry(export_pid).or_insert_with(|| cnf.new_var()); cnf.add_clause(&[ sel.negative(), export_var.negative(), From e08d0324828c8c39419347c91c84ba649829f8f4 Mon Sep 17 00:00:00 2001 From: Eh2406 Date: Fri, 24 May 2019 12:09:15 -0400 Subject: [PATCH 13/13] add a helper function --- tests/testsuite/support/resolver.rs | 58 ++++++++++++++--------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/tests/testsuite/support/resolver.rs b/tests/testsuite/support/resolver.rs index 755dfc66b18..d43aacaa425 100644 --- a/tests/testsuite/support/resolver.rs +++ b/tests/testsuite/support/resolver.rs @@ -218,6 +218,21 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va } } +fn sat_at_most_one_by_key( + cnf: &mut impl varisat::ExtendFormula, + data: impl Iterator, +) -> HashMap> { + // no two packages with the same links set + let mut by_keys: HashMap> = HashMap::new(); + for (p, v) in data { + by_keys.entry(p).or_default().push(v) + } + for key in by_keys.values() { + sat_at_most_one(cnf, key); + } + by_keys +} + /// Resolution can be reduced to the SAT problem. So this is an alternative implementation /// of the resolver that uses a SAT library for the hard work. This is intended to be easy to read, /// as compared to the real resolver. @@ -243,30 +258,21 @@ impl SatResolve { .collect(); // no two packages with the same links set - let mut by_links: HashMap<_, Vec> = HashMap::new(); - for p in registry.iter() { - if let Some(l) = p.links() { - by_links - .entry(l) - .or_default() - .push(var_for_is_packages_used[&p.package_id()]) - } - } - for link in by_links.values() { - sat_at_most_one(&mut cnf, link); - } + sat_at_most_one_by_key( + &mut cnf, + registry + .iter() + .map(|s| (s.links(), var_for_is_packages_used[&s.package_id()])) + .filter(|(l, _)| l.is_some()), + ); // no two semver compatible versions of the same package - let mut by_activations_keys: HashMap<_, Vec> = HashMap::new(); - for p in registry.iter() { - by_activations_keys - .entry(p.package_id().as_activations_key()) - .or_default() - .push(var_for_is_packages_used[&p.package_id()]) - } - for key in by_activations_keys.values() { - sat_at_most_one(&mut cnf, key); - } + let by_activations_keys = sat_at_most_one_by_key( + &mut cnf, + var_for_is_packages_used + .iter() + .map(|(p, &v)| (p.as_activations_key(), v)), + ); let mut by_name: HashMap<&'static str, Vec> = HashMap::new(); @@ -389,13 +395,7 @@ impl SatResolve { // a package `can_see` only one version by each name for (_, see) in can_see.iter() { - let mut by_name: HashMap<&'static str, Vec> = HashMap::new(); - for ((name, _, _), &var) in see { - by_name.entry(name.as_str()).or_default().push(var); - } - for same_name in by_name.values() { - sat_at_most_one(&mut cnf, same_name); - } + sat_at_most_one_by_key(&mut cnf, see.iter().map(|((name, _, _), &v)| (name, v))); } let mut solver = varisat::Solver::new(); solver.add_formula(&cnf);