Skip to content

Commit 3b4f3b0

Browse files
committed
test(resolver-tests): Remove public dep support from SAT resolver
1 parent 2f10699 commit 3b4f3b0

File tree

1 file changed

+8
-123
lines changed
  • crates/resolver-tests/src

1 file changed

+8
-123
lines changed

crates/resolver-tests/src/lib.rs

Lines changed: 8 additions & 123 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ use cargo::core::{Dependency, PackageId, Registry, Summary};
1818
use cargo::core::{GitReference, SourceId};
1919
use cargo::sources::source::QueryKind;
2020
use cargo::sources::IndexSummary;
21-
use cargo::util::{CargoResult, Config, Graph, IntoUrl, RustVersion};
21+
use cargo::util::{CargoResult, Config, IntoUrl, RustVersion};
2222

2323
use proptest::collection::{btree_map, vec};
2424
use proptest::prelude::*;
@@ -195,17 +195,6 @@ fn log_bits(x: usize) -> usize {
195195
}
196196

197197
fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) {
198-
if vars.len() <= 1 {
199-
return;
200-
} else if vars.len() == 2 {
201-
solver.add_clause(&[vars[0].negative(), vars[1].negative()]);
202-
return;
203-
} else if vars.len() == 3 {
204-
solver.add_clause(&[vars[0].negative(), vars[1].negative()]);
205-
solver.add_clause(&[vars[0].negative(), vars[2].negative()]);
206-
solver.add_clause(&[vars[1].negative(), vars[2].negative()]);
207-
return;
208-
}
209198
// use the "Binary Encoding" from
210199
// 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
211200
let bits: Vec<varisat::Var> = solver.new_var_iter(log_bits(vars.len())).collect();
@@ -254,7 +243,8 @@ impl SatResolve {
254243
let mut cnf = varisat::CnfFormula::new();
255244
let var_for_is_packages_used: HashMap<PackageId, varisat::Var> = registry
256245
.iter()
257-
.map(|s| (s.package_id(), cnf.new_var()))
246+
.map(|s| s.package_id())
247+
.zip(cnf.new_var_iter(registry.len()))
258248
.collect();
259249

260250
// no two packages with the same links set
@@ -266,14 +256,6 @@ impl SatResolve {
266256
.filter(|(l, _)| l.is_some()),
267257
);
268258

269-
// no two semver compatible versions of the same package
270-
let by_activations_keys = sat_at_most_one_by_key(
271-
&mut cnf,
272-
var_for_is_packages_used
273-
.iter()
274-
.map(|(p, &v)| (p.as_activations_key(), v)),
275-
);
276-
277259
let mut by_name: HashMap<&'static str, Vec<PackageId>> = HashMap::new();
278260

279261
for p in registry.iter() {
@@ -285,119 +267,22 @@ impl SatResolve {
285267

286268
let empty_vec = vec![];
287269

288-
let mut graph: Graph<PackageId, ()> = Graph::new();
289-
290-
let mut version_selected_for: HashMap<
291-
PackageId,
292-
HashMap<Dependency, HashMap<_, varisat::Var>>,
293-
> = HashMap::new();
294270
// active packages need each of there `deps` to be satisfied
295271
for p in registry.iter() {
296-
graph.add(p.package_id());
297272
for dep in p.dependencies() {
298-
// This can more easily be written as:
299-
// !is_active(p) or one of the things that match dep is_active
300-
// All the complexity, from here to the end, is to support public and private dependencies!
301-
let mut by_key: HashMap<_, Vec<varisat::Lit>> = HashMap::new();
302-
for &m in by_name
273+
let mut matches: Vec<varisat::Lit> = by_name
303274
.get(dep.package_name().as_str())
304275
.unwrap_or(&empty_vec)
305276
.iter()
306277
.filter(|&p| dep.matches_id(*p))
307-
{
308-
graph.link(p.package_id(), m);
309-
by_key
310-
.entry(m.as_activations_key())
311-
.or_default()
312-
.push(var_for_is_packages_used[&m].positive());
313-
}
314-
let keys: HashMap<_, _> = by_key.keys().map(|&k| (k, cnf.new_var())).collect();
315-
316-
// if `p` is active then we need to select one of the keys
317-
let matches: Vec<_> = keys
318-
.values()
319-
.map(|v| v.positive())
320-
.chain(Some(var_for_is_packages_used[&p.package_id()].negative()))
278+
.map(|p| var_for_is_packages_used[&p].positive())
321279
.collect();
280+
// ^ the `dep` is satisfied or `p` is not active
281+
matches.push(var_for_is_packages_used[&p.package_id()].negative());
322282
cnf.add_clause(&matches);
323-
324-
// if a key is active then we need to select one of the versions
325-
for (key, vars) in by_key.iter() {
326-
let mut matches = vars.clone();
327-
matches.push(keys[key].negative());
328-
cnf.add_clause(&matches);
329-
}
330-
331-
version_selected_for
332-
.entry(p.package_id())
333-
.or_default()
334-
.insert(dep.clone(), keys);
335-
}
336-
}
337-
338-
let topological_order = graph.sort();
339-
340-
// we already ensure there is only one version for each `activations_key` so we can think of
341-
// `publicly_exports` as being in terms of a set of `activations_key`s
342-
let mut publicly_exports: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new();
343-
344-
for &key in by_activations_keys.keys() {
345-
// everything publicly depends on itself
346-
let var = publicly_exports
347-
.entry(key)
348-
.or_default()
349-
.entry(key)
350-
.or_insert_with(|| cnf.new_var());
351-
cnf.add_clause(&[var.positive()]);
352-
}
353-
354-
// if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports`
355-
for &p in topological_order.iter() {
356-
if let Some(deps) = version_selected_for.get(&p) {
357-
let mut p_exports = publicly_exports.remove(&p.as_activations_key()).unwrap();
358-
for (_, versions) in deps.iter().filter(|(d, _)| d.is_public()) {
359-
for (ver, sel) in versions {
360-
for (&export_pid, &export_var) in publicly_exports[ver].iter() {
361-
let our_var =
362-
p_exports.entry(export_pid).or_insert_with(|| cnf.new_var());
363-
cnf.add_clause(&[
364-
sel.negative(),
365-
export_var.negative(),
366-
our_var.positive(),
367-
]);
368-
}
369-
}
370-
}
371-
publicly_exports.insert(p.as_activations_key(), p_exports);
372283
}
373284
}
374285

375-
// we already ensure there is only one version for each `activations_key` so we can think of
376-
// `can_see` as being in terms of a set of `activations_key`s
377-
// and if `p` `publicly_exports` `export` then it `can_see` `export`
378-
let mut can_see: HashMap<_, HashMap<_, varisat::Var>> = HashMap::new();
379-
380-
// if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports`
381-
for (&p, deps) in version_selected_for.iter() {
382-
let p_can_see = can_see.entry(p).or_default();
383-
for (_, versions) in deps.iter() {
384-
for (&ver, sel) in versions {
385-
for (&export_pid, &export_var) in publicly_exports[&ver].iter() {
386-
let our_var = p_can_see.entry(export_pid).or_insert_with(|| cnf.new_var());
387-
cnf.add_clause(&[
388-
sel.negative(),
389-
export_var.negative(),
390-
our_var.positive(),
391-
]);
392-
}
393-
}
394-
}
395-
}
396-
397-
// a package `can_see` only one version by each name
398-
for (_, see) in can_see.iter() {
399-
sat_at_most_one_by_key(&mut cnf, see.iter().map(|((name, _, _), &v)| (name, v)));
400-
}
401286
let mut solver = varisat::Solver::new();
402287
solver.add_formula(&cnf);
403288

@@ -840,7 +725,7 @@ pub fn registry_strategy(
840725
// => DepKind::Development, // Development has no impact so don't gen
841726
_ => panic!("bad index for DepKind"),
842727
},
843-
p && k == 0,
728+
p,
844729
))
845730
}
846731

0 commit comments

Comments
 (0)