From 4723638a334acae00d2584cf18f6206de0074ad1 Mon Sep 17 00:00:00 2001 From: Jacob Finkelman Date: Thu, 21 Dec 2023 12:50:04 -0500 Subject: [PATCH] perf: do not recompute the accumulated_intersection when backtracking (#171) * perf: do not recompute the accumulated_intersection when backtracking * more correct comment message * make things dry again --- src/internal/core.rs | 3 +- src/internal/partial_solution.rs | 65 +++++++++++++++----------------- 2 files changed, 31 insertions(+), 37 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..68d4b41e 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 { @@ -207,11 +208,11 @@ impl PartialSolution>, ) { use indexmap::map::Entry; - let term = store[cause].get(&package).unwrap().negate(); - let dated_derivation = DatedDerivation { + 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); @@ -226,7 +227,8 @@ impl PartialSolution { - *t = t.intersection(&term); + *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 @@ -238,6 +240,7 @@ 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); @@ -297,13 +300,9 @@ impl 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 +324,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 +435,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 +477,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 +517,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 +532,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 ) } }