From d3d561b2b626b4df526de331d77cae6a804645b4 Mon Sep 17 00:00:00 2001 From: Jacob Finkelman Date: Wed, 20 Dec 2023 22:38:48 +0000 Subject: [PATCH 1/3] perf: do not recompute the accumulated_intersection when backtracking --- src/internal/core.rs | 3 +- src/internal/partial_solution.rs | 75 ++++++++++++++++---------------- 2 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/internal/core.rs b/src/internal/core.rs index 58831469..147a5a22 100644 --- a/src/internal/core.rs +++ b/src/internal/core.rs @@ -225,8 +225,7 @@ impl State { incompat_changed: bool, decision_level: DecisionLevel, ) { - self.partial_solution - .backtrack(decision_level, &self.incompatibility_store); + self.partial_solution.backtrack(decision_level); // Remove contradicted incompatibilities that depend on decisions we just backtracked away. self.contradicted_incompatibilities .retain(|_, dl| *dl <= decision_level); diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs index a40f4c97..64c5d6b2 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -107,6 +107,7 @@ pub struct DatedDerivation { global_index: u32, decision_level: DecisionLevel, cause: IncompId, + accumulated_intersection: Term, } impl Display for DatedDerivation { @@ -208,11 +209,7 @@ impl PartialSolution PartialSolution { @@ -227,6 +225,7 @@ impl PartialSolution { *t = t.intersection(&term); + accumulated_intersection = t.clone(); if t.is_positive() { // we can use `swap_indices` to make `changed_this_decision_level` only go down by 1 // but the copying is slower then the larger search @@ -235,7 +234,12 @@ impl PartialSolution { if term.is_positive() { @@ -245,7 +249,12 @@ impl PartialSolution PartialSolution>, - ) { + pub fn backtrack(&mut self, decision_level: DecisionLevel) { self.current_decision_level = decision_level; - self.package_assignments.retain(|p, pa| { + self.package_assignments.retain(|_p, pa| { if pa.smallest_decision_level > decision_level { // Remove all entries that have a smallest decision level higher than the backtrack target. false @@ -325,18 +330,14 @@ impl PartialSolution PartialSolution, store: &Arena>, ) -> (P, SatisfierSearch) { - let satisfied_map = Self::find_satisfier(incompat, &self.package_assignments, store); + let satisfied_map = Self::find_satisfier(incompat, &self.package_assignments); let (satisfier_package, &(satisfier_index, _, satisfier_decision_level)) = satisfied_map .iter() .max_by_key(|(_p, (_, global_index, _))| global_index) @@ -440,14 +441,13 @@ impl PartialSolution, package_assignments: &FnvIndexMap>, - store: &Arena>, ) -> SmallMap { 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, Term::any(), store), + pa.satisfier(package, incompat_term, &Term::any()), ); } satisfied @@ -483,7 +483,7 @@ impl PartialSolution PackageAssignments { &self, package: &P, incompat_term: &Term, - start_term: Term, - store: &Arena>, + start_term: &Term, ) -> (usize, u32, DecisionLevel) { - // Term where we accumulate intersections until incompat_term is satisfied. - let mut accum_term = start_term; // 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 this_term = store[dated_derivation.cause].get(package).unwrap().negate(); - accum_term = accum_term.intersection(&this_term); - if accum_term.subset_of(incompat_term) { + if dated_derivation + .accumulated_intersection + .intersection(start_term) + .subset_of(incompat_term) + { // We found the derivation causing satisfaction. return ( idx, @@ -524,13 +523,13 @@ impl PackageAssignments { } // 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 { + match &self.assignments_intersection { AssignmentsIntersection::Decision((global_index, _, _)) => ( self.dated_derivations.len(), - global_index, + *global_index, self.highest_decision_level, ), - AssignmentsIntersection::Derivations(_) => { + AssignmentsIntersection::Derivations(accumulated_intersection) => { unreachable!( concat!( "while processing package {}: ", @@ -539,7 +538,9 @@ impl PackageAssignments { "but instead it was a derivation. This shouldn't be possible! ", "(Maybe your Version ordering is broken?)" ), - package, accum_term, incompat_term + package, + accumulated_intersection.intersection(start_term), + incompat_term ) } } From 28a7c6e91b3a7a4309df226490e5adf98626ce3a Mon Sep 17 00:00:00 2001 From: Jacob Finkelman Date: Thu, 21 Dec 2023 16:03:11 +0000 Subject: [PATCH 2/3] more correct comment message --- 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 64c5d6b2..a0e59206 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -335,7 +335,7 @@ impl PartialSolution Date: Thu, 21 Dec 2023 16:26:20 +0000 Subject: [PATCH 3/3] make things dry again --- src/internal/partial_solution.rs | 28 +++++++++++----------------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs index a0e59206..68d4b41e 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -208,8 +208,12 @@ impl PartialSolution>, ) { use indexmap::map::Entry; - let term = store[cause].get(&package).unwrap().negate(); - let global_index = self.next_global_index; + let mut dated_derivation = DatedDerivation { + global_index: self.next_global_index, + decision_level: self.current_decision_level, + cause, + accumulated_intersection: store[cause].get(&package).unwrap().negate(), + }; self.next_global_index += 1; let pa_last_index = self.package_assignments.len().saturating_sub(1); match self.package_assignments.entry(package) { @@ -217,15 +221,14 @@ impl PartialSolution { panic!("add_derivation should not be called after a decision") } AssignmentsIntersection::Derivations(t) => { - *t = t.intersection(&term); - accumulated_intersection = t.clone(); + *t = t.intersection(&dated_derivation.accumulated_intersection); + dated_derivation.accumulated_intersection = t.clone(); if t.is_positive() { // we can use `swap_indices` to make `changed_this_decision_level` only go down by 1 // but the copying is slower then the larger search @@ -234,14 +237,10 @@ impl PartialSolution { + let term = dated_derivation.accumulated_intersection.clone(); if term.is_positive() { self.changed_this_decision_level = std::cmp::min(self.changed_this_decision_level, pa_last_index); @@ -249,12 +248,7 @@ impl PartialSolution