From 12355f3ee04ad41ada66b92de9384a8ff609efb5 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <Eh2406@wayne.edu>
Date: Sun, 16 Oct 2022 23:10:38 -0400
Subject: [PATCH] tests: add a SAT var for package being un-selected

---
 tests/sat_dependency_provider.rs | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/tests/sat_dependency_provider.rs b/tests/sat_dependency_provider.rs
index 97ecab3e..bb3b6f5a 100644
--- a/tests/sat_dependency_provider.rs
+++ b/tests/sat_dependency_provider.rs
@@ -48,7 +48,7 @@ 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> {
@@ -56,10 +56,15 @@ impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
         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));
@@ -67,7 +72,7 @@ impl<P: Package, VS: VersionSet> SatResolve<P, VS> {
                 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()