From 47475915f02ebf66169e0ef45aa331a5ef799a4e Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 01/17] check that nothing changed

---
 src/internal/partial_solution.rs | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 68d4b41e..3c0dbf98 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -502,11 +502,19 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
     ) -> (usize, u32, DecisionLevel) {
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
-            if dated_derivation
+            let new = dated_derivation
                 .accumulated_intersection
                 .intersection(start_term)
-                .subset_of(incompat_term)
+                .subset_of(incompat_term);
+            #[cfg(debug_assertions)]
             {
+                let old = dated_derivation
+                    .accumulated_intersection
+                    .intersection(start_term)
+                    .subset_of(incompat_term);
+                assert_eq!(old, new);
+            }
+            if new {
                 // We found the derivation causing satisfaction.
                 return (
                     idx,

From 295acd8c2c9aad2a21a74a2d6fc38cafd0c70ee4 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 02/17] inline subset_of

---
 src/internal/partial_solution.rs | 6 +++---
 src/term.rs                      | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 3c0dbf98..32ab992c 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -502,10 +502,10 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
     ) -> (usize, u32, DecisionLevel) {
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
-            let new = dated_derivation
+            let accumulated = dated_derivation
                 .accumulated_intersection
-                .intersection(start_term)
-                .subset_of(incompat_term);
+                .intersection(start_term);
+            let new = accumulated == accumulated.intersection(incompat_term);
             #[cfg(debug_assertions)]
             {
                 let old = dated_derivation
diff --git a/src/term.rs b/src/term.rs
index 3a9906bd..e51357a9 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -107,6 +107,7 @@ impl<VS: VersionSet> Term<VS> {
     /// Indicate if this term is a subset of another term.
     /// Just like for sets, we say that t1 is a subset of t2
     /// if and only if t1 ∩ t2 = t1.
+    #[cfg(debug_assertions)]
     pub(crate) fn subset_of(&self, other: &Self) -> bool {
         self == &self.intersection(other)
     }

From c004e21a4f1d1555e5686126c1d668aa76125cc6 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 03/17] Apply !incompat_term to both sides

---
 src/internal/partial_solution.rs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 32ab992c..df0e9a08 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -504,8 +504,12 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let accumulated = dated_derivation
                 .accumulated_intersection
-                .intersection(start_term);
-            let new = accumulated == accumulated.intersection(incompat_term);
+                .intersection(start_term)
+                .intersection(&incompat_term.negate());
+            let new = accumulated
+                == accumulated
+                    .intersection(incompat_term)
+                    .intersection(&incompat_term.negate());
             #[cfg(debug_assertions)]
             {
                 let old = dated_derivation

From a853ca84f38347bad0df5d0be59d49a4098ef2e1 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 04/17] T.intersection( !T ) == empty

---
 src/internal/partial_solution.rs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index df0e9a08..a4ae99d9 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -500,16 +500,14 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         incompat_term: &Term<VS>,
         start_term: &Term<VS>,
     ) -> (usize, u32, DecisionLevel) {
+        let empty = Term::empty();
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let accumulated = dated_derivation
                 .accumulated_intersection
                 .intersection(start_term)
                 .intersection(&incompat_term.negate());
-            let new = accumulated
-                == accumulated
-                    .intersection(incompat_term)
-                    .intersection(&incompat_term.negate());
+            let new = accumulated == empty;
             #[cfg(debug_assertions)]
             {
                 let old = dated_derivation

From 4992c5180a67e4657ec3a4e99ff6d8e0b303136b Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 05/17] precomputed
 start_term.intersection(&incompat_term.negate())

---
 src/internal/partial_solution.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index a4ae99d9..7d1d852a 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -501,12 +501,12 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         start_term: &Term<VS>,
     ) -> (usize, u32, DecisionLevel) {
         let empty = Term::empty();
+        let intersection_term = start_term.intersection(&incompat_term.negate());
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let accumulated = dated_derivation
                 .accumulated_intersection
-                .intersection(start_term)
-                .intersection(&incompat_term.negate());
+                .intersection(&intersection_term);
             let new = accumulated == empty;
             #[cfg(debug_assertions)]
             {

From 10d70c7ac2bdd77c8109f36e436f3b073902f3ba Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 06/17] move the checking code

---
 src/internal/partial_solution.rs | 36 +++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 7d1d852a..da756b88 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -503,26 +503,32 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         let empty = Term::empty();
         let intersection_term = start_term.intersection(&incompat_term.negate());
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
+        let mut new_idx = None;
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let accumulated = dated_derivation
                 .accumulated_intersection
                 .intersection(&intersection_term);
-            let new = accumulated == empty;
-            #[cfg(debug_assertions)]
-            {
-                let old = dated_derivation
-                    .accumulated_intersection
-                    .intersection(start_term)
-                    .subset_of(incompat_term);
-                assert_eq!(old, new);
+            if accumulated == empty {
+                new_idx = Some(idx);
+                break;
             }
-            if new {
-                // We found the derivation causing satisfaction.
-                return (
-                    idx,
-                    dated_derivation.global_index,
-                    dated_derivation.decision_level,
-                );
+        }
+        #[cfg(debug_assertions)]
+        for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
+            let old = dated_derivation
+                .accumulated_intersection
+                .intersection(start_term)
+                .subset_of(incompat_term);
+            if old {
+                assert_eq!(new_idx, Some(idx));
+                break;
+            } else {
+                assert!(Some(idx) < new_idx || new_idx.is_none());
+            }
+        }
+        if let Some(idx) = new_idx {
+            if let Some(dd) = self.dated_derivations.get(idx) {
+                return (new_idx.unwrap(), dd.global_index, dd.decision_level);
             }
         }
         // If it wasn't found in the derivations,

From 5468475ec2b285c6b3b9c57cb6faf35624e49f5c Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 07/17] switch to partition_point

---
 src/internal/partial_solution.rs | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index da756b88..c50ce3fd 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -503,16 +503,9 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         let empty = Term::empty();
         let intersection_term = start_term.intersection(&incompat_term.negate());
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
-        let mut new_idx = None;
-        for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
-            let accumulated = dated_derivation
-                .accumulated_intersection
-                .intersection(&intersection_term);
-            if accumulated == empty {
-                new_idx = Some(idx);
-                break;
-            }
-        }
+        let new_idx = Some(self.dated_derivations.as_slice().partition_point(|dd| {
+            dd.accumulated_intersection.intersection(&intersection_term) != empty
+        }));
         #[cfg(debug_assertions)]
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let old = dated_derivation
@@ -528,6 +521,10 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         }
         if let Some(idx) = new_idx {
             if let Some(dd) = self.dated_derivations.get(idx) {
+                debug_assert_eq!(
+                    dd.accumulated_intersection.intersection(&intersection_term),
+                    empty
+                );
                 return (new_idx.unwrap(), dd.global_index, dd.decision_level);
             }
         }

From a21a9477e8203d734139c65ff2f87ad6a896f950 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 08/17] remove the option

---
 src/internal/partial_solution.rs | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index c50ce3fd..6e5d6c7e 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -503,9 +503,9 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         let empty = Term::empty();
         let intersection_term = start_term.intersection(&incompat_term.negate());
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
-        let new_idx = Some(self.dated_derivations.as_slice().partition_point(|dd| {
+        let new_idx = self.dated_derivations.as_slice().partition_point(|dd| {
             dd.accumulated_intersection.intersection(&intersection_term) != empty
-        }));
+        });
         #[cfg(debug_assertions)]
         for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
             let old = dated_derivation
@@ -513,20 +513,18 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
                 .intersection(start_term)
                 .subset_of(incompat_term);
             if old {
-                assert_eq!(new_idx, Some(idx));
+                assert_eq!(new_idx, idx);
                 break;
             } else {
-                assert!(Some(idx) < new_idx || new_idx.is_none());
+                assert!(idx < new_idx);
             }
         }
-        if let Some(idx) = new_idx {
-            if let Some(dd) = self.dated_derivations.get(idx) {
-                debug_assert_eq!(
-                    dd.accumulated_intersection.intersection(&intersection_term),
-                    empty
-                );
-                return (new_idx.unwrap(), dd.global_index, dd.decision_level);
-            }
+        if let Some(dd) = self.dated_derivations.get(new_idx) {
+            debug_assert_eq!(
+                dd.accumulated_intersection.intersection(&intersection_term),
+                empty
+            );
+            return (new_idx, dd.global_index, dd.decision_level);
         }
         // If it wasn't found in the derivations,
         // it must be the decision which is last (if called in the right context).

From d9d2be4d8c13401fd0514839b4b9bd8ad2c351ab Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 09/17] compute intersection_term outside of satisfier

---
 src/internal/partial_solution.rs | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 6e5d6c7e..6677efe9 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -441,7 +441,12 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             let pa = package_assignments.get(package).expect("Must exist");
             satisfied.insert(
                 package.clone(),
-                pa.satisfier(package, incompat_term, &Term::any()),
+                pa.satisfier(
+                    package,
+                    incompat_term,
+                    &Term::any(),
+                    &Term::any().intersection(&incompat_term.negate()),
+                ),
             );
         }
         satisfied
@@ -477,7 +482,12 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
 
         satisfied_map.insert(
             satisfier_package.clone(),
-            satisfier_pa.satisfier(satisfier_package, incompat_term, &accum_term),
+            satisfier_pa.satisfier(
+                satisfier_package,
+                incompat_term,
+                &accum_term,
+                &accum_term.intersection(&incompat_term.negate()),
+            ),
         );
 
         // Finally, let's identify the decision level of that previous satisfier.
@@ -499,9 +509,9 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         package: &P,
         incompat_term: &Term<VS>,
         start_term: &Term<VS>,
+        intersection_term: &Term<VS>,
     ) -> (usize, u32, DecisionLevel) {
         let empty = Term::empty();
-        let intersection_term = start_term.intersection(&incompat_term.negate());
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         let new_idx = self.dated_derivations.as_slice().partition_point(|dd| {
             dd.accumulated_intersection.intersection(&intersection_term) != empty

From 7210001f03a39a7145ec2a5e2d1bad21eb9dfb68 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 10/17] intersection with any is self

---
 src/internal/partial_solution.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 6677efe9..b828e7c8 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -445,7 +445,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
                     package,
                     incompat_term,
                     &Term::any(),
-                    &Term::any().intersection(&incompat_term.negate()),
+                    &incompat_term.negate(),
                 ),
             );
         }

From d16e2342aecff97636356c36ae9b8d06e889204f Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 11/17] remove test code

---
 src/internal/partial_solution.rs | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index b828e7c8..899f6c88 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -516,19 +516,6 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         let new_idx = self.dated_derivations.as_slice().partition_point(|dd| {
             dd.accumulated_intersection.intersection(&intersection_term) != empty
         });
-        #[cfg(debug_assertions)]
-        for (idx, dated_derivation) in self.dated_derivations.iter().enumerate() {
-            let old = dated_derivation
-                .accumulated_intersection
-                .intersection(start_term)
-                .subset_of(incompat_term);
-            if old {
-                assert_eq!(new_idx, idx);
-                break;
-            } else {
-                assert!(idx < new_idx);
-            }
-        }
         if let Some(dd) = self.dated_derivations.get(new_idx) {
             debug_assert_eq!(
                 dd.accumulated_intersection.intersection(&intersection_term),

From d2b4669e1845cd545aeaec08abef3855ef493c4b Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 12/17] remove unused arguments

---
 src/internal/partial_solution.rs | 23 ++++-------------------
 1 file changed, 4 insertions(+), 19 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 899f6c88..baca10cc 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -441,12 +441,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             let pa = package_assignments.get(package).expect("Must exist");
             satisfied.insert(
                 package.clone(),
-                pa.satisfier(
-                    package,
-                    incompat_term,
-                    &Term::any(),
-                    &incompat_term.negate(),
-                ),
+                pa.satisfier(package, &incompat_term.negate()),
             );
         }
         satisfied
@@ -484,8 +479,6 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             satisfier_package.clone(),
             satisfier_pa.satisfier(
                 satisfier_package,
-                incompat_term,
-                &accum_term,
                 &accum_term.intersection(&incompat_term.negate()),
             ),
         );
@@ -504,13 +497,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
 }
 
 impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
-    fn satisfier(
-        &self,
-        package: &P,
-        incompat_term: &Term<VS>,
-        start_term: &Term<VS>,
-        intersection_term: &Term<VS>,
-    ) -> (usize, u32, DecisionLevel) {
+    fn satisfier(&self, package: &P, intersection_term: &Term<VS>) -> (usize, u32, DecisionLevel) {
         let empty = Term::empty();
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         let new_idx = self.dated_derivations.as_slice().partition_point(|dd| {
@@ -535,14 +522,12 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
                 unreachable!(
                     concat!(
                         "while processing package {}: ",
-                        "accum_term = {} isn't a subset of incompat_term = {}, ",
+                        "accum_term = {} has overlap with incompat_term = {}, ",
                         "which means the last assignment should have been a decision, ",
                         "but instead it was a derivation. This shouldn't be possible! ",
                         "(Maybe your Version ordering is broken?)"
                     ),
-                    package,
-                    accumulated_intersection.intersection(start_term),
-                    incompat_term
+                    package, accumulated_intersection, intersection_term
                 )
             }
         }

From 0f0ce588a64fa311e7b2ea0ad6eb23fa11f7b03a Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 13/17] rename vars

---
 src/internal/partial_solution.rs | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index baca10cc..ad7e0d29 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -497,18 +497,16 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
 }
 
 impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
-    fn satisfier(&self, package: &P, intersection_term: &Term<VS>) -> (usize, u32, DecisionLevel) {
+    fn satisfier(&self, package: &P, start_term: &Term<VS>) -> (usize, u32, DecisionLevel) {
         let empty = Term::empty();
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
-        let new_idx = self.dated_derivations.as_slice().partition_point(|dd| {
-            dd.accumulated_intersection.intersection(&intersection_term) != empty
-        });
-        if let Some(dd) = self.dated_derivations.get(new_idx) {
-            debug_assert_eq!(
-                dd.accumulated_intersection.intersection(&intersection_term),
-                empty
-            );
-            return (new_idx, dd.global_index, dd.decision_level);
+        let idx = self
+            .dated_derivations
+            .as_slice()
+            .partition_point(|dd| dd.accumulated_intersection.intersection(&start_term) != empty);
+        if let Some(dd) = self.dated_derivations.get(idx) {
+            debug_assert_eq!(dd.accumulated_intersection.intersection(&start_term), empty);
+            return (idx, dd.global_index, dd.decision_level);
         }
         // If it wasn't found in the derivations,
         // it must be the decision which is last (if called in the right context).
@@ -527,7 +525,7 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
                         "but instead it was a derivation. This shouldn't be possible! ",
                         "(Maybe your Version ordering is broken?)"
                     ),
-                    package, accumulated_intersection, intersection_term
+                    package, accumulated_intersection, start_term
                 )
             }
         }

From 5b1afcff7bfc0e00cafe6b27b10afd2b82e4dabe Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 14/17] dont clone P

---
 src/internal/core.rs             |  3 ++-
 src/internal/partial_solution.rs | 32 ++++++++++++++------------------
 2 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/src/internal/core.rs b/src/internal/core.rs
index 147a5a22..38bdca17 100644
--- a/src/internal/core.rs
+++ b/src/internal/core.rs
@@ -194,6 +194,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
                     DifferentDecisionLevels {
                         previous_satisfier_level,
                     } => {
+                        let package = package.clone();
                         self.backtrack(
                             current_incompat_id,
                             current_incompat_changed,
@@ -206,7 +207,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
                         let prior_cause = Incompatibility::prior_cause(
                             current_incompat_id,
                             satisfier_cause,
-                            &package,
+                            package,
                             &self.incompatibility_store,
                         );
                         log::info!("prior cause: {}", prior_cause);
diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index ad7e0d29..3d63195c 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -390,17 +390,16 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     }
 
     /// Figure out if the satisfier and previous satisfier are of different decision levels.
-    pub fn satisfier_search(
+    pub fn satisfier_search<'i>(
         &self,
-        incompat: &Incompatibility<P, VS>,
+        incompat: &'i Incompatibility<P, VS>,
         store: &Arena<Incompatibility<P, VS>>,
-    ) -> (P, SatisfierSearch<P, VS>) {
+    ) -> (&'i P, SatisfierSearch<P, VS>) {
         let satisfied_map = Self::find_satisfier(incompat, &self.package_assignments);
-        let (satisfier_package, &(satisfier_index, _, satisfier_decision_level)) = satisfied_map
+        let (&satisfier_package, &(satisfier_index, _, satisfier_decision_level)) = satisfied_map
             .iter()
             .max_by_key(|(_p, (_, global_index, _))| global_index)
             .unwrap();
-        let satisfier_package = satisfier_package.clone();
         let previous_satisfier_level = Self::find_previous_satisfier(
             incompat,
             &satisfier_package,
@@ -414,7 +413,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             };
             (satisfier_package, search_result)
         } else {
-            let satisfier_pa = self.package_assignments.get(&satisfier_package).unwrap();
+            let satisfier_pa = self.package_assignments.get(satisfier_package).unwrap();
             let dd = &satisfier_pa.dated_derivations[satisfier_index];
             let search_result = SatisfierSearch::SameDecisionLevels {
                 satisfier_cause: dd.cause,
@@ -432,17 +431,14 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     /// Question: This is possible since we added a "global_index" to every dated_derivation.
     /// It would be nice if we could get rid of it, but I don't know if then it will be possible
     /// to return a coherent previous_satisfier_level.
-    fn find_satisfier(
-        incompat: &Incompatibility<P, VS>,
+    fn find_satisfier<'i>(
+        incompat: &'i Incompatibility<P, VS>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
-    ) -> SmallMap<P, (usize, u32, DecisionLevel)> {
+    ) -> SmallMap<&'i P, (usize, u32, DecisionLevel)> {
         let mut satisfied = SmallMap::Empty;
         for (package, incompat_term) in incompat.iter() {
             let pa = package_assignments.get(package).expect("Must exist");
-            satisfied.insert(
-                package.clone(),
-                pa.satisfier(package, &incompat_term.negate()),
-            );
+            satisfied.insert(package, pa.satisfier(package, &incompat_term.negate()));
         }
         satisfied
     }
@@ -450,16 +446,16 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     /// Earliest assignment in the partial solution before satisfier
     /// such that incompatibility is satisfied by the partial solution up to
     /// and including that assignment plus satisfier.
-    fn find_previous_satisfier(
+    fn find_previous_satisfier<'i>(
         incompat: &Incompatibility<P, VS>,
-        satisfier_package: &P,
-        mut satisfied_map: SmallMap<P, (usize, u32, DecisionLevel)>,
+        satisfier_package: &'i P,
+        mut satisfied_map: SmallMap<&'i P, (usize, u32, DecisionLevel)>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
         store: &Arena<Incompatibility<P, VS>>,
     ) -> DecisionLevel {
         // First, let's retrieve the previous derivations and the initial accum_term.
         let satisfier_pa = package_assignments.get(satisfier_package).unwrap();
-        let (satisfier_index, _gidx, _dl) = satisfied_map.get_mut(satisfier_package).unwrap();
+        let (satisfier_index, _gidx, _dl) = satisfied_map.get_mut(&satisfier_package).unwrap();
 
         let accum_term = if *satisfier_index == satisfier_pa.dated_derivations.len() {
             match &satisfier_pa.assignments_intersection {
@@ -476,7 +472,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             .expect("satisfier package not in incompat");
 
         satisfied_map.insert(
-            satisfier_package.clone(),
+            satisfier_package,
             satisfier_pa.satisfier(
                 satisfier_package,
                 &accum_term.intersection(&incompat_term.negate()),

From 8594c12bdbca37d9c6f61b898da03bccba2db6bc Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 15/17] nothing meaningful

---
 src/internal/partial_solution.rs | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 3d63195c..3fbd38bc 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -407,19 +407,16 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             &self.package_assignments,
             store,
         );
-        if previous_satisfier_level < satisfier_decision_level {
-            let search_result = SatisfierSearch::DifferentDecisionLevels {
+        let search_result = if previous_satisfier_level < satisfier_decision_level {
+            SatisfierSearch::DifferentDecisionLevels {
                 previous_satisfier_level,
-            };
-            (satisfier_package, search_result)
+            }
         } else {
-            let satisfier_pa = self.package_assignments.get(satisfier_package).unwrap();
-            let dd = &satisfier_pa.dated_derivations[satisfier_index];
-            let search_result = SatisfierSearch::SameDecisionLevels {
-                satisfier_cause: dd.cause,
-            };
-            (satisfier_package, search_result)
-        }
+            let satisfier_pa = &self.package_assignments[satisfier_package];
+            let satisfier_cause = satisfier_pa.dated_derivations[satisfier_index].cause;
+            SatisfierSearch::SameDecisionLevels { satisfier_cause }
+        };
+        (satisfier_package, search_result)
     }
 
     /// A satisfier is the earliest assignment in partial solution such that the incompatibility

From f4b6dc21bb7028f11b71a9cd22a591ed7fcdc3e8 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 16/17] use cause not index

---
 src/internal/partial_solution.rs | 41 ++++++++++++++++----------------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 3fbd38bc..517cceb2 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -396,7 +396,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
         store: &Arena<Incompatibility<P, VS>>,
     ) -> (&'i P, SatisfierSearch<P, VS>) {
         let satisfied_map = Self::find_satisfier(incompat, &self.package_assignments);
-        let (&satisfier_package, &(satisfier_index, _, satisfier_decision_level)) = satisfied_map
+        let (&satisfier_package, &(satisfier_cause, _, satisfier_decision_level)) = satisfied_map
             .iter()
             .max_by_key(|(_p, (_, global_index, _))| global_index)
             .unwrap();
@@ -407,14 +407,14 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             &self.package_assignments,
             store,
         );
-        let search_result = if previous_satisfier_level < satisfier_decision_level {
+        let search_result = if previous_satisfier_level >= satisfier_decision_level {
+            SatisfierSearch::SameDecisionLevels {
+                satisfier_cause: satisfier_cause.unwrap(),
+            }
+        } else {
             SatisfierSearch::DifferentDecisionLevels {
                 previous_satisfier_level,
             }
-        } else {
-            let satisfier_pa = &self.package_assignments[satisfier_package];
-            let satisfier_cause = satisfier_pa.dated_derivations[satisfier_index].cause;
-            SatisfierSearch::SameDecisionLevels { satisfier_cause }
         };
         (satisfier_package, search_result)
     }
@@ -431,7 +431,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     fn find_satisfier<'i>(
         incompat: &'i Incompatibility<P, VS>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
-    ) -> SmallMap<&'i P, (usize, u32, DecisionLevel)> {
+    ) -> SmallMap<&'i P, (Option<IncompId<P, VS>>, u32, DecisionLevel)> {
         let mut satisfied = SmallMap::Empty;
         for (package, incompat_term) in incompat.iter() {
             let pa = package_assignments.get(package).expect("Must exist");
@@ -446,22 +446,21 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     fn find_previous_satisfier<'i>(
         incompat: &Incompatibility<P, VS>,
         satisfier_package: &'i P,
-        mut satisfied_map: SmallMap<&'i P, (usize, u32, DecisionLevel)>,
+        mut satisfied_map: SmallMap<&'i P, (Option<IncompId<P, VS>>, u32, DecisionLevel)>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
         store: &Arena<Incompatibility<P, VS>>,
     ) -> DecisionLevel {
         // First, let's retrieve the previous derivations and the initial accum_term.
         let satisfier_pa = package_assignments.get(satisfier_package).unwrap();
-        let (satisfier_index, _gidx, _dl) = satisfied_map.get_mut(&satisfier_package).unwrap();
+        let (satisfier_cause, _gidx, _dl) = satisfied_map.get(&satisfier_package).unwrap();
 
-        let accum_term = if *satisfier_index == satisfier_pa.dated_derivations.len() {
+        let accum_term = if let &Some(cause) = satisfier_cause {
+            store[cause].get(satisfier_package).unwrap().negate()
+        } else {
             match &satisfier_pa.assignments_intersection {
                 AssignmentsIntersection::Derivations(_) => panic!("must be a decision"),
                 AssignmentsIntersection::Decision((_, _, term)) => term.clone(),
             }
-        } else {
-            let dd = &satisfier_pa.dated_derivations[*satisfier_index];
-            store[dd.cause].get(satisfier_package).unwrap().negate()
         };
 
         let incompat_term = incompat
@@ -490,7 +489,11 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
 }
 
 impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
-    fn satisfier(&self, package: &P, start_term: &Term<VS>) -> (usize, u32, DecisionLevel) {
+    fn satisfier(
+        &self,
+        package: &P,
+        start_term: &Term<VS>,
+    ) -> (Option<IncompId<P, VS>>, u32, DecisionLevel) {
         let empty = Term::empty();
         // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
         let idx = self
@@ -499,16 +502,14 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
             .partition_point(|dd| dd.accumulated_intersection.intersection(&start_term) != empty);
         if let Some(dd) = self.dated_derivations.get(idx) {
             debug_assert_eq!(dd.accumulated_intersection.intersection(&start_term), empty);
-            return (idx, dd.global_index, dd.decision_level);
+            return (Some(dd.cause), dd.global_index, dd.decision_level);
         }
         // If it wasn't found in the derivations,
         // it must be the decision which is last (if called in the right context).
         match &self.assignments_intersection {
-            AssignmentsIntersection::Decision((global_index, _, _)) => (
-                self.dated_derivations.len(),
-                *global_index,
-                self.highest_decision_level,
-            ),
+            AssignmentsIntersection::Decision((global_index, _, _)) => {
+                (None, *global_index, self.highest_decision_level)
+            }
             AssignmentsIntersection::Derivations(accumulated_intersection) => {
                 unreachable!(
                     concat!(

From a890799ee29b87f8d75dbed264ca2e193b20ccd5 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 3 Jan 2024 18:12:00 +0000
Subject: [PATCH 17/17] clippy

---
 src/internal/partial_solution.rs | 12 +++++++-----
 src/term.rs                      |  2 +-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 517cceb2..cf1d24db 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -143,6 +143,8 @@ pub enum SatisfierSearch<P: Package, VS: VersionSet> {
     },
 }
 
+type SatisfiedMap<'i, P, VS> = SmallMap<&'i P, (Option<IncompId<P, VS>>, u32, DecisionLevel)>;
+
 impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, Priority> {
     /// Initialize an empty PartialSolution.
     pub fn empty() -> Self {
@@ -402,7 +404,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             .unwrap();
         let previous_satisfier_level = Self::find_previous_satisfier(
             incompat,
-            &satisfier_package,
+            satisfier_package,
             satisfied_map,
             &self.package_assignments,
             store,
@@ -431,7 +433,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     fn find_satisfier<'i>(
         incompat: &'i Incompatibility<P, VS>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
-    ) -> SmallMap<&'i P, (Option<IncompId<P, VS>>, u32, DecisionLevel)> {
+    ) -> SatisfiedMap<'i, P, VS> {
         let mut satisfied = SmallMap::Empty;
         for (package, incompat_term) in incompat.iter() {
             let pa = package_assignments.get(package).expect("Must exist");
@@ -446,7 +448,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
     fn find_previous_satisfier<'i>(
         incompat: &Incompatibility<P, VS>,
         satisfier_package: &'i P,
-        mut satisfied_map: SmallMap<&'i P, (Option<IncompId<P, VS>>, u32, DecisionLevel)>,
+        mut satisfied_map: SatisfiedMap<'i, P, VS>,
         package_assignments: &FnvIndexMap<P, PackageAssignments<P, VS>>,
         store: &Arena<Incompatibility<P, VS>>,
     ) -> DecisionLevel {
@@ -499,9 +501,9 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
         let idx = self
             .dated_derivations
             .as_slice()
-            .partition_point(|dd| dd.accumulated_intersection.intersection(&start_term) != empty);
+            .partition_point(|dd| dd.accumulated_intersection.intersection(start_term) != empty);
         if let Some(dd) = self.dated_derivations.get(idx) {
-            debug_assert_eq!(dd.accumulated_intersection.intersection(&start_term), empty);
+            debug_assert_eq!(dd.accumulated_intersection.intersection(start_term), empty);
             return (Some(dd.cause), dd.global_index, dd.decision_level);
         }
         // If it wasn't found in the derivations,
diff --git a/src/term.rs b/src/term.rs
index e51357a9..2974da62 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -107,7 +107,7 @@ impl<VS: VersionSet> Term<VS> {
     /// Indicate if this term is a subset of another term.
     /// Just like for sets, we say that t1 is a subset of t2
     /// if and only if t1 ∩ t2 = t1.
-    #[cfg(debug_assertions)]
+    #[cfg(test)]
     pub(crate) fn subset_of(&self, other: &Self) -> bool {
         self == &self.intersection(other)
     }