check that the SAT solver exempts the result from the resolver

crates/resolver-tests/src/lib.rs

@@ -1,7 +1,10 @@
+use std::cell::RefCell;
 use std::cmp::PartialEq;
 use std::cmp::{max, min};
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fmt;
+use std::fmt::Write;
+use std::rc::Rc;
 use std::time::Instant;
 
 use cargo::core::dependency::Kind;
@@ -24,17 +27,22 @@ pub fn resolve(deps: Vec<Dependency>, registry: &[Summary]) -> CargoResult<Vec<P
 pub fn resolve_and_validated(
     deps: Vec<Dependency>,
     registry: &[Summary],
-    sat_resolve: Option<&mut SatResolve>,
+    sat_resolve: Option<SatResolve>,
 ) -> CargoResult<Vec<PackageId>> {
-    let should_resolve = if let Some(sat) = sat_resolve {
+    let resolve = resolve_with_config_raw(deps.clone(), registry, None);
-        sat.sat_resolve(&deps)
-    } else {
-        SatResolve::new(registry).sat_resolve(&deps)
-    };
-    let resolve = resolve_with_config_raw(deps, registry, None);
-    assert_eq!(resolve.is_ok(), should_resolve);
 
-    let resolve = resolve?;
+    match resolve {
+        Err(e) => {
+            let sat_resolve = sat_resolve.unwrap_or_else(|| SatResolve::new(registry));
+            if sat_resolve.sat_resolve(&deps) {
+                panic!(
+                    "the resolve err but the sat_resolve thinks this will work:\n{}",
+                    sat_resolve.use_packages().unwrap()
+                );
+            }
+            Err(e)
+        }
+        Ok(resolve) => {
             let mut stack = vec![pkg_id("root")];
             let mut used = HashSet::new();
             let mut links = HashSet::new();
@@ -83,7 +91,16 @@ pub fn resolve_and_validated(
                     }
                 }
             }
+            let sat_resolve = sat_resolve.unwrap_or_else(|| SatResolve::new(registry));
+            if !sat_resolve.sat_is_valid_solution(&out) {
+                panic!(
+                    "the sat_resolve err but the resolve thinks this will work:\n{:?}",
+                    resolve
+                );
+            }
             Ok(out)
+        }
+    }
 }
 
 pub fn resolve_with_config(
@@ -234,7 +251,9 @@ fn sat_at_most_one_by_key<K: std::hash::Hash + Eq>(
 ///
 /// The SAT library dose not optimize for the newer version,
 /// so the selected packages may not match the real resolver.
-pub struct SatResolve {
+#[derive(Clone)]
+pub struct SatResolve(Rc<RefCell<SatResolveInner>>);
+struct SatResolveInner {
     solver: varisat::Solver<'static>,
     var_for_is_packages_used: HashMap<PackageId, varisat::Var>,
     by_name: HashMap<&'static str, Vec<PackageId>>,
@@ -397,27 +416,27 @@ impl SatResolve {
         solver
             .solve()
             .expect("docs say it can't error in default config");
-
+        SatResolve(Rc::new(RefCell::new(SatResolveInner {
-        SatResolve {
             solver,
             var_for_is_packages_used,
             by_name,
+        })))
     }
-    }
+    pub fn sat_resolve(&self, deps: &[Dependency]) -> bool {
-    pub fn sat_resolve(&mut self, deps: &[Dependency]) -> bool {
+        let mut s = self.0.borrow_mut();
         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<varisat::Lit> = self
+            let matches: Vec<varisat::Lit> = s
                 .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())
+                .map(|p| s.var_for_is_packages_used[p].positive())
                 .collect();
             if matches.is_empty() {
                 return false;
@@ -425,22 +444,58 @@ impl SatResolve {
                 assumption.extend_from_slice(&matches)
             } else {
                 if this_call.is_none() {
-                    let new_var = self.solver.new_var();
+                    let new_var = s.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);
+                s.solver.add_clause(&matches);
             }
         }
 
-        self.solver.assume(&assumption);
+        s.solver.assume(&assumption);
 
-        self.solver
+        s.solver
             .solve()
             .expect("docs say it can't error in default config")
     }
+    pub fn sat_is_valid_solution(&self, pids: &[PackageId]) -> bool {
+        let mut s = self.0.borrow_mut();
+        for p in pids {
+            if p.name().as_str() != "root" && !s.var_for_is_packages_used.contains_key(p) {
+                return false;
+            }
+        }
+        let assumption: Vec<_> = s
+            .var_for_is_packages_used
+            .iter()
+            .map(|(p, v)| v.lit(pids.contains(p)))
+            .collect();
+
+        s.solver.assume(&assumption);
+
+        s.solver
+            .solve()
+            .expect("docs say it can't error in default config")
+    }
+    fn use_packages(&self) -> Option<String> {
+        self.0.borrow().solver.model().map(|lits| {
+            let lits: HashSet<_> = lits
+                .iter()
+                .filter(|l| l.is_positive())
+                .map(|l| l.var())
+                .collect();
+            let mut out = String::new();
+            out.push_str("used:\n");
+            for (p, v) in self.0.borrow().var_for_is_packages_used.iter() {
+                if lits.contains(v) {
+                    writeln!(&mut out, "    {}", p).unwrap();
+                }
+            }
+            out
+        })
+    }
 }
 
 pub trait ToDep {

crates/resolver-tests/tests/resolve.rs

@@ -39,7 +39,7 @@ proptest! {
         PrettyPrintRegistry(input) in registry_strategy(50, 20, 60)
     )  {
         let reg = registry(input.clone());
-        let mut sat_resolve = SatResolve::new(&reg);
+        let sat_resolve = SatResolve::new(&reg);
         // there is only a small chance that any one
         // crate will be interesting.
         // So we try some of the most complicated.
@@ -47,7 +47,7 @@ proptest! {
             let _ = resolve_and_validated(
                 vec![dep_req(&this.name(), &format!("={}", this.version()))],
                 &reg,
-                Some(&mut sat_resolve),
+                Some(sat_resolve.clone()),
             );
         }
     }