tests: add a SAT var for package being un-selected

pubgrub-rs · Oct 17, 2022 · 12355f3 · 12355f3
1 parent 78562c5
commit 12355f3
Showing 1 changed file with 19 additions and 9 deletions.
diff --git a/tests/sat_dependency_provider.rs b/tests/sat_dependency_provider.rs
@@ -48,26 +48,31 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va
 /// so the selected packages may not match the real resolver.
 pub struct SatResolve<P: Package, VS: VersionSet> {
     solver: varisat::Solver<'static>,
-    all_versions_by_p: Map<P, Vec<(VS::V, varisat::Var)>>,
+    all_versions_by_p: Map<P, Vec<(Option<VS::V>, varisat::Var)>>,
 }
 
 impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
     pub fn new(dp: &OfflineDependencyProvider<P, VS>) -> Self {
         let mut cnf = varisat::CnfFormula::new();
 
         let mut all_versions = vec![];
-        let mut all_versions_by_p: Map<P, Vec<(VS::V, varisat::Var)>> = Map::default();
+        let mut all_versions_by_p: Map<P, Vec<(Option<VS::V>, varisat::Var)>> = Map::default();
 
         for p in dp.packages() {
-            let mut versions_for_p = vec![];
+            let new_var = cnf.new_var();
+            let mut versions_for_p = vec![new_var];
+            all_versions_by_p
+                .entry(p.clone())
+                .or_default()
+                .push((None, new_var));
             for v in dp.versions(p).unwrap() {
                 let new_var = cnf.new_var();
                 all_versions.push((p.clone(), v.clone(), new_var));
                 versions_for_p.push(new_var);
                 all_versions_by_p
                     .entry(p.clone())
                     .or_default()
-                    .push((v.clone(), new_var));
+                    .push((Some(v.clone()), new_var));
             }
             // no two versions of the same package
             sat_at_most_one(&mut cnf, &versions_for_p);
@@ -80,12 +85,17 @@ impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
                 Dependencies::Known(d) => d,
             };
             for (p1, range) in &deps {
-                let empty_vec = vec![];
                 let mut matches: Vec<varisat::Lit> = all_versions_by_p
                     .get(p1)
-                    .unwrap_or(&empty_vec)
+                    .unwrap_or(&vec![])
                     .iter()
-                    .filter(|(v1, _)| range.contains(v1))
+                    .filter(|(v1, _)| {
+                        if let Some(v1) = v1 {
+                            range.contains(v1)
+                        } else {
+                            false // range.is_constrained()
+                        }
+                    })
                     .map(|(_, var1)| var1.positive())
                     .collect();
                 // ^ the `dep` is satisfied or
@@ -112,7 +122,7 @@ impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
 
     pub fn sat_resolve(&mut self, name: &P, ver: &VS::V) -> bool {
         if let Some(vers) = self.all_versions_by_p.get(name) {
-            if let Some((_, var)) = vers.iter().find(|(v, _)| v == ver) {
+            if let Some((_, var)) = vers.iter().find(|(v, _)| v.as_ref() == Some(ver)) {
                 self.solver.assume(&[var.positive()]);
 
                 self.solver
@@ -131,7 +141,7 @@ impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
 
         for (p, vs) in &self.all_versions_by_p {
             for (v, var) in vs {
-                assumption.push(if pids.get(p) == Some(v) {
+                assumption.push(if pids.get(p) == v.as_ref() {
                     var.positive()
                 } else {
                     var.negative()