From cd91684f733e0e1d3e4fe558e6614844159a6919 Mon Sep 17 00:00:00 2001 From: Matthieu Pizenberg Date: Sun, 6 Jun 2021 02:13:50 +0200 Subject: [PATCH] refactor: unify history and memory in partial_solution (#92) * refactor: unify history and memory in partial_solution * refactor: use retain * refactor: use partition_point * perf: use more SmallVec Co-authored-by: Jacob Finkelman --- src/internal/assignment.rs | 52 ---- src/internal/core.rs | 7 +- src/internal/incompatibility.rs | 7 +- src/internal/memory.rs | 164 ---------- src/internal/mod.rs | 2 - src/internal/partial_solution.rs | 513 +++++++++++++++++++++---------- 6 files changed, 363 insertions(+), 382 deletions(-) delete mode 100644 src/internal/assignment.rs delete mode 100644 src/internal/memory.rs diff --git a/src/internal/assignment.rs b/src/internal/assignment.rs deleted file mode 100644 index c811782f..00000000 --- a/src/internal/assignment.rs +++ /dev/null @@ -1,52 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 - -//! Assignments are the building blocks of a PubGrub partial solution. -//! (partial solution = the current state of the solution we are building in the algorithm). - -use crate::internal::arena::Arena; -use crate::internal::incompatibility::IncompId; -use crate::internal::incompatibility::Incompatibility; -use crate::package::Package; -use crate::term::Term; -use crate::version::Version; - -/// An assignment is either a decision: a chosen version for a package, -/// or a derivation : a term specifying compatible versions for a package. -/// We also record the incompatibility at the origin of a derivation, called its cause. -#[derive(Clone)] -pub enum Assignment { - /// The decision. - Decision { - /// The package corresponding to the decision. - package: P, - /// The decided version. - version: V, - }, - /// The derivation. - Derivation { - /// The package corresponding to the derivation. - package: P, - /// Incompatibility cause of the derivation. - cause: IncompId, - }, -} - -impl Assignment { - /// Return the package for this assignment - pub fn package(&self) -> &P { - match self { - Self::Decision { package, .. } => package, - Self::Derivation { package, .. } => package, - } - } - - /// Retrieve the current assignment as a [Term]. - /// If this is decision, it returns a positive term with that exact version. - /// Otherwise, if this is a derivation, just returns its term. - pub fn as_term(&self, store: &Arena>) -> Term { - match &self { - Self::Decision { version, .. } => Term::exact(version.clone()), - Self::Derivation { package, cause } => store[*cause].get(&package).unwrap().negate(), - } - } -} diff --git a/src/internal/core.rs b/src/internal/core.rs index ee6d3fe6..8d9f15b2 100644 --- a/src/internal/core.rs +++ b/src/internal/core.rs @@ -7,9 +7,8 @@ use std::collections::HashSet as Set; use crate::error::PubGrubError; use crate::internal::arena::Arena; -use crate::internal::assignment::Assignment::{Decision, Derivation}; -use crate::internal::incompatibility::IncompId; -use crate::internal::incompatibility::{Incompatibility, Relation}; +use crate::internal::incompatibility::{IncompId, Incompatibility, Relation}; +use crate::internal::partial_solution::Assignment::{Decision, Derivation}; use crate::internal::partial_solution::{DecisionLevel, PartialSolution}; use crate::internal::small_vec::SmallVec; use crate::package::Package; @@ -175,7 +174,7 @@ impl State { &self.incompatibility_store[current_incompat_id], &self.incompatibility_store, ); - match satisfier.clone() { + match satisfier { Decision { package, .. } => { self.backtrack( current_incompat_id, diff --git a/src/internal/incompatibility.rs b/src/internal/incompatibility.rs index a7b403a7..acf900b8 100644 --- a/src/internal/incompatibility.rs +++ b/src/internal/incompatibility.rs @@ -54,7 +54,7 @@ enum Kind { /// A Relation describes how a set of terms can be compared to an incompatibility. /// Typically, the set of terms comes from the partial solution. -#[derive(Eq, PartialEq)] +#[derive(Eq, PartialEq, Debug)] pub enum Relation { /// We say that a set of terms S satisfies an incompatibility I /// if S satisfies every term in I. @@ -166,11 +166,6 @@ impl Incompatibility { self.package_terms.iter() } - // The number of packages. - pub fn len(&self) -> usize { - self.package_terms.len() - } - // Reporting ############################################################### /// Retrieve parent causes if of type DerivedFrom. diff --git a/src/internal/memory.rs b/src/internal/memory.rs deleted file mode 100644 index 0d43f534..00000000 --- a/src/internal/memory.rs +++ /dev/null @@ -1,164 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 - -//! A Memory acts like a structured partial solution -//! where terms are regrouped by package in a [Map](crate::type_aliases::Map). - -use crate::internal::arena::Arena; -use crate::internal::assignment::Assignment::{self, Decision, Derivation}; -use crate::internal::incompatibility::Incompatibility; -use crate::package::Package; -use crate::range::Range; -use crate::term::Term; -use crate::type_aliases::{Map, SelectedDependencies}; -use crate::version::Version; - -/// A memory is the set of all assignments in the partial solution, -/// organized by package instead of historically ordered. -/// -/// Contrary to PartialSolution, Memory does not store derivations causes, only the terms. -#[derive(Clone)] -pub struct Memory { - assignments: Map>, -} - -/// A package memory contains the potential decision and derivations -/// that have already been made for a given package. -#[derive(Clone)] -enum PackageAssignments { - Decision((V, Term)), - Derivations(Term), -} - -impl Memory { - /// Initialize an empty memory. - pub fn empty() -> Self { - Self { - assignments: Map::default(), - } - } - - /// Clears the memory. - pub fn clear(&mut self) { - self.assignments.clear(); - } - - /// Retrieve intersection of terms in memory related to package. - pub fn term_intersection_for_package(&self, package: &P) -> Option<&Term> { - self.assignments - .get(package) - .map(|pa| pa.assignment_intersection()) - } - - /// Building step of a Memory from a given assignment. - pub fn add_assignment( - &mut self, - assignment: &Assignment, - store: &Arena>, - ) { - match assignment { - Decision { package, version } => self.add_decision(package.clone(), version.clone()), - Derivation { package, cause } => self.add_derivation( - package.clone(), - store[*cause].get(&package).unwrap().negate(), - ), - } - } - - /// Add a decision to a Memory. - pub fn add_decision(&mut self, package: P, version: V) { - // Check that add_decision is never used in the wrong context. - if cfg!(debug_assertions) { - match self.assignments.get_mut(&package) { - None => panic!("Assignments must already exist"), - // Cannot be called when a decision has already been taken. - Some(PackageAssignments::Decision(_)) => panic!("Already existing decision"), - // Cannot be called if the versions is not contained in the terms intersection. - Some(pa) => debug_assert!(pa.assignment_intersection().contains(&version)), - } - } - - self.assignments.insert( - package, - PackageAssignments::Decision((version.clone(), Term::exact(version))), - ); - } - - /// Add a derivation to a Memory. - pub fn add_derivation(&mut self, package: P, term: Term) { - use std::collections::hash_map::Entry; - match self.assignments.entry(package) { - Entry::Occupied(mut o) => match o.get_mut() { - // Check that add_derivation is never called in the wrong context. - PackageAssignments::Decision(_) => debug_assert!(false), - PackageAssignments::Derivations(t) => { - *t = t.intersection(&term); - } - }, - Entry::Vacant(v) => { - v.insert(PackageAssignments::Derivations(term)); - } - } - } - - /// Extract all packages that may potentially be picked next - /// to continue solving package dependencies. - /// A package is a potential pick if there isn't an already - /// selected version (no "decision") - /// and if it contains at least one positive derivation term - /// in the partial solution. - pub fn potential_packages(&self) -> impl Iterator)> { - self.assignments - .iter() - .filter_map(|(p, pa)| pa.potential_package_filter(p)) - } - - /// If a partial solution has, for every positive derivation, - /// a corresponding decision that satisfies that assignment, - /// it's a total solution and version solving has succeeded. - pub fn extract_solution(&self) -> Option> { - let mut solution = Map::default(); - for (p, pa) in &self.assignments { - match pa { - PackageAssignments::Decision((v, _)) => { - solution.insert(p.clone(), v.clone()); - } - PackageAssignments::Derivations(intersected) => { - if intersected.is_positive() { - return None; - } - } - } - } - Some(solution) - } -} - -impl PackageAssignments { - /// Returns intersection of all assignments (decision included). - fn assignment_intersection(&self) -> &Term { - match self { - PackageAssignments::Decision((_, term)) => term, - PackageAssignments::Derivations(term) => term, - } - } - - /// A package is a potential pick if there isn't an already - /// selected version (no "decision") - /// and if it contains at least one positive derivation term - /// in the partial solution. - fn potential_package_filter<'a, P: Package>( - &'a self, - package: &'a P, - ) -> Option<(&'a P, &'a Range)> { - match self { - PackageAssignments::Decision(_) => None, - PackageAssignments::Derivations(intersected) => { - if intersected.is_positive() { - Some((package, self.assignment_intersection().unwrap_positive())) - } else { - None - } - } - } - } -} diff --git a/src/internal/mod.rs b/src/internal/mod.rs index e8db3d46..86d7e22e 100644 --- a/src/internal/mod.rs +++ b/src/internal/mod.rs @@ -3,10 +3,8 @@ //! Non exposed modules. pub mod arena; -pub mod assignment; pub mod core; pub mod incompatibility; -pub mod memory; pub mod partial_solution; pub mod small_map; pub mod small_vec; diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs index 5fc9bf3a..700dc199 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -1,103 +1,201 @@ // SPDX-License-Identifier: MPL-2.0 -//! The partial solution is the current state -//! of the solution being built by the algorithm. +//! A Memory acts like a structured partial solution +//! where terms are regrouped by package in a [Map](crate::type_aliases::Map). use crate::internal::arena::Arena; -use crate::internal::assignment::Assignment::{self, Decision, Derivation}; -use crate::internal::incompatibility::IncompId; -use crate::internal::incompatibility::{Incompatibility, Relation}; -use crate::internal::memory::Memory; +use crate::internal::incompatibility::{IncompId, Incompatibility, Relation}; +use crate::internal::small_map::SmallMap; use crate::package::Package; use crate::range::Range; use crate::term::Term; use crate::type_aliases::{Map, SelectedDependencies}; use crate::version::Version; -#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] -pub struct DecisionLevel(u32); +use super::small_vec::SmallVec; -impl std::ops::Add for DecisionLevel { - type Output = DecisionLevel; +#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] +pub struct DecisionLevel(pub u32); - fn add(self, other: DecisionLevel) -> DecisionLevel { - DecisionLevel(self.0 + other.0) +impl DecisionLevel { + pub fn increment(self) -> Self { + Self(self.0 + 1) } } -impl std::ops::SubAssign for DecisionLevel { - fn sub_assign(&mut self, other: DecisionLevel) { - self.0 -= other.0 - } +/// The partial solution contains all package assignments, +/// organized by package and historically ordered. +#[derive(Clone, Debug)] +pub struct PartialSolution { + next_global_index: u32, + current_decision_level: DecisionLevel, + package_assignments: Map>, } -#[derive(Clone)] -pub struct DatedAssignment { - decision_level: DecisionLevel, - assignment: Assignment, +/// Package assignments contain the potential decision and derivations +/// that have already been made for a given package, +/// as well as the intersection of terms by all of these. +#[derive(Clone, Debug)] +struct PackageAssignments { + smallest_decision_level: DecisionLevel, + highest_decision_level: DecisionLevel, + dated_derivations: SmallVec>, + assignments_intersection: AssignmentsIntersection, } -/// The partial solution is the current state -/// of the solution being built by the algorithm. -/// It is composed of a succession of assignments, -/// defined as either decisions or derivations. -#[derive(Clone)] -pub struct PartialSolution { +#[derive(Clone, Debug)] +pub struct DatedDerivation { + global_index: u32, decision_level: DecisionLevel, - /// Each assignment is stored with its decision level in the history. - /// The order in which assignments where added in the vec is kept, - /// so the oldest assignments are at the beginning of the vec. - history: Vec>, - memory: Memory, + cause: IncompId, +} + +#[derive(Clone, Debug)] +enum AssignmentsIntersection { + Decision((u32, V, Term)), + Derivations(Term), +} + +/// An assignment is either a decision: a chosen version for a package, +/// or a derivation : a term specifying compatible versions for a package. +/// We also record the incompatibility at the origin of a derivation, called its cause. +/// TODO: Remove. I only added that to not change the code in core.rs (except reference &). +#[derive(Clone, PartialEq, Debug)] +pub enum Assignment { + /// The decision. + Decision { + /// The package corresponding to the decision. + package: P, + /// The decided version. + version: V, + }, + /// The derivation. + Derivation { + /// The package corresponding to the derivation. + package: P, + /// Incompatibility cause of the derivation. + cause: IncompId, + }, } impl PartialSolution { - /// Initialize an empty partial solution. + /// Initialize an empty PartialSolution. pub fn empty() -> Self { Self { - decision_level: DecisionLevel(0), - history: Vec::new(), - memory: Memory::empty(), + next_global_index: 0, + current_decision_level: DecisionLevel(0), + package_assignments: Map::default(), } } - /// Add a decision to the partial solution. + /// Add a decision. pub fn add_decision(&mut self, package: P, version: V) { - self.decision_level = self.decision_level + DecisionLevel(1); - self.memory.add_decision(package.clone(), version.clone()); - self.history.push(DatedAssignment { - decision_level: self.decision_level, - assignment: Decision { package, version }, - }); + // Check that add_decision is never used in the wrong context. + if cfg!(debug_assertions) { + match self.package_assignments.get_mut(&package) { + None => panic!("Derivations must already exist"), + Some(pa) => match &pa.assignments_intersection { + // Cannot be called when a decision has already been taken. + AssignmentsIntersection::Decision(_) => panic!("Already existing decision"), + // Cannot be called if the versions is not contained in the terms intersection. + AssignmentsIntersection::Derivations(term) => { + debug_assert!(term.contains(&version)) + } + }, + } + } + self.current_decision_level = self.current_decision_level.increment(); + let mut pa = self + .package_assignments + .get_mut(&package) + .expect("Derivations must already exist"); + pa.highest_decision_level = self.current_decision_level; + pa.assignments_intersection = AssignmentsIntersection::Decision(( + self.next_global_index, + version.clone(), + Term::exact(version), + )); + self.next_global_index += 1; } - /// Add a derivation to the partial solution. + /// Add a derivation. pub fn add_derivation( &mut self, package: P, cause: IncompId, store: &Arena>, ) { - self.memory.add_derivation( - package.clone(), - store[cause].get(&package).unwrap().negate(), - ); - self.history.push(DatedAssignment { - decision_level: self.decision_level, - assignment: Derivation { package, cause }, - }); + use std::collections::hash_map::Entry; + let term = store[cause].get(&package).unwrap().negate(); + let dated_derivation = DatedDerivation { + global_index: self.next_global_index, + decision_level: self.current_decision_level, + cause, + }; + self.next_global_index += 1; + match self.package_assignments.entry(package) { + Entry::Occupied(mut occupied) => { + let mut pa = occupied.get_mut(); + pa.highest_decision_level = self.current_decision_level; + match &mut pa.assignments_intersection { + // Check that add_derivation is never called in the wrong context. + AssignmentsIntersection::Decision(_) => { + panic!("add_derivation should not be called after a decision") + } + AssignmentsIntersection::Derivations(t) => { + *t = t.intersection(&term); + } + } + pa.dated_derivations.push(dated_derivation); + } + Entry::Vacant(v) => { + v.insert(PackageAssignments { + smallest_decision_level: self.current_decision_level, + highest_decision_level: self.current_decision_level, + dated_derivations: SmallVec::One([dated_derivation]), + assignments_intersection: AssignmentsIntersection::Derivations(term), + }); + } + } + } + + /// Extract potential packages for the next iteration of unit propagation. + /// Return `None` if there is no suitable package anymore, which stops the algorithm. + /// A package is a potential pick if there isn't an already + /// selected version (no "decision") + /// and if it contains at least one positive derivation term + /// in the partial solution. + pub fn potential_packages(&self) -> Option)>> { + let mut iter = self + .package_assignments + .iter() + .filter_map(|(p, pa)| pa.assignments_intersection.potential_package_filter(p)) + .peekable(); + if iter.peek().is_some() { + Some(iter) + } else { + None + } } /// If a partial solution has, for every positive derivation, /// a corresponding decision that satisfies that assignment, /// it's a total solution and version solving has succeeded. pub fn extract_solution(&self) -> Option> { - self.memory.extract_solution() - } - - /// Compute, cache and retrieve the intersection of all terms for this package. - pub fn term_intersection_for_package(&self, package: &P) -> Option<&Term> { - self.memory.term_intersection_for_package(package) + let mut solution = Map::default(); + for (p, pa) in &self.package_assignments { + match &pa.assignments_intersection { + AssignmentsIntersection::Decision((_, v, _)) => { + solution.insert(p.clone(), v.clone()); + } + AssignmentsIntersection::Derivations(term) => { + if term.is_positive() { + return None; + } + } + } + } + Some(solution) } /// Backtrack the partial solution to a given decision level. @@ -106,37 +204,44 @@ impl PartialSolution { decision_level: DecisionLevel, store: &Arena>, ) { - let pos = self - .history - .binary_search_by(|probe| { - probe - .decision_level - .cmp(&decision_level) - // `binary_search_by` does not guarantee which element to return when more - // then one match. By all ways claiming that it does not match we ensure we - // get the last one. - .then(std::cmp::Ordering::Less) - }) - .unwrap_or_else(|x| x); - - self.history.truncate(pos); - self.decision_level = self.history.last().expect("no history left").decision_level; - self.memory.clear(); - let mem = &mut self.memory; - self.history - .iter() - .for_each(|da| mem.add_assignment(&da.assignment, store)); - } + self.current_decision_level = decision_level; + 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 + } else if pa.highest_decision_level <= decision_level { + // Do not change entries older than the backtrack decision level target. + true + } else { + // smallest_decision_level <= decision_level < highest_decision_level + // + // Since decision_level < highest_decision_level, + // We can be certain that there will be no decision in this package assignments + // after backtracking, because such decision would have been the last + // assignment and it would have the "highest_decision_level". - /// Extract potential packages for the next iteration of unit propagation. - /// Return `None` if there is no suitable package anymore, which stops the algorithm. - pub fn potential_packages(&self) -> Option)>> { - let mut iter = self.memory.potential_packages().peekable(); - if iter.peek().is_some() { - Some(iter) - } else { - None - } + // Truncate the history. + while pa.dated_derivations.last().map(|dd| dd.decision_level) > Some(decision_level) + { + pa.dated_derivations.pop(); + } + debug_assert!(!pa.dated_derivations.is_empty()); + + // Update highest_decision_level. + pa.highest_decision_level = pa.dated_derivations.last().unwrap().decision_level; + + // Recompute the assignments intersection. + pa.assignments_intersection = AssignmentsIntersection::Derivations( + pa.dated_derivations + .iter() + .fold(Term::any(), |acc, dated_derivation| { + let term = store[dated_derivation.cause].get(&p).unwrap().negate(); + acc.intersection(&term) + }), + ); + true + } + }); } /// We can add the version to the partial solution as a decision @@ -151,13 +256,13 @@ impl PartialSolution { new_incompatibilities: std::ops::Range>, store: &Arena>, ) { - let exact = &Term::exact(version.clone()); + let exact = Term::exact(version.clone()); let not_satisfied = |incompat: &Incompatibility| { incompat.relation(|p| { if p == &package { - Some(exact) + Some(&exact) } else { - self.memory.term_intersection_for_package(p) + self.term_intersection_for_package(p) } }) != Relation::Satisfied }; @@ -171,7 +276,14 @@ impl PartialSolution { /// Check if the terms in the partial solution satisfy the incompatibility. pub fn relation(&self, incompat: &Incompatibility) -> Relation

{ - incompat.relation(|package| self.memory.term_intersection_for_package(package)) + incompat.relation(|package| self.term_intersection_for_package(package)) + } + + /// Retrieve intersection of terms related to package. + pub fn term_intersection_for_package(&self, package: &P) -> Option<&Term> { + self.package_assignments + .get(package) + .map(|pa| pa.assignments_intersection.term()) } /// Find satisfier and previous satisfier decision level. @@ -179,25 +291,39 @@ impl PartialSolution { &self, incompat: &Incompatibility, store: &Arena>, - ) -> (&Assignment, DecisionLevel, DecisionLevel) { - let satisfier_map = Self::find_satisfier(incompat, &self.history, store); - assert_eq!( - satisfier_map.len(), - incompat.len(), - "We should always find a satisfier if called in the right context." - ); - let &satisfier_idx = satisfier_map.values().max().unwrap(); - let satisfier = &self.history[satisfier_idx]; + ) -> (Assignment, DecisionLevel, DecisionLevel) { + let satisfied_map = Self::find_satisfier(incompat, &self.package_assignments, store); + 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.assignment, - satisfier_map, - &self.history[0..=satisfier_idx], + &satisfier_package, + satisfied_map, + &self.package_assignments, store, ); + let satisfier_pa = self.package_assignments.get(&satisfier_package).unwrap(); + let satisfier_assignment = if satisfier_index == satisfier_pa.dated_derivations.len() { + match &satisfier_pa.assignments_intersection { + AssignmentsIntersection::Decision((_, version, _)) => Assignment::Decision { + package: satisfier_package, + version: version.clone(), + }, + AssignmentsIntersection::Derivations(_) => panic!("Must be a decision"), + } + } else { + let dd = &satisfier_pa.dated_derivations[satisfier_index]; + Assignment::Derivation { + package: satisfier_package, + cause: dd.cause, + } + }; ( - &satisfier.assignment, - satisfier.decision_level, + satisfier_assignment, + satisfier_decision_level, previous_satisfier_level, ) } @@ -207,42 +333,57 @@ impl PartialSolution { /// /// Returns a map indicating for each package term, when that was first satisfied in history. /// If we effectively found a satisfier, the returned map must be the same size that incompat. - fn find_satisfier<'a>( + /// + /// 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, - history: &'a [DatedAssignment], + package_assignments: &Map>, store: &Arena>, - ) -> Map { - let mut accum_satisfied: Map> = incompat - .iter() - .map(|(p, _)| (p.clone(), Term::any())) - .collect(); - let mut satisfied = Map::with_capacity_and_hasher(incompat.len(), Default::default()); - for (idx, dated_assignment) in history.iter().enumerate() { - let package = dated_assignment.assignment.package(); - if satisfied.contains_key(package) { - continue; // If that package term is already satisfied, no need to check. - } - let incompat_term = match incompat.get(package) { - // We only care about packages related to the incompatibility. - None => continue, - Some(i) => i, - }; - let accum_term = match accum_satisfied.get_mut(package) { - // We only care about packages related to the accum_satisfied. - None => continue, - Some(i) => i, - }; - - // Check if that incompat term is satisfied by our accumulated terms intersection. - *accum_term = accum_term.intersection(&dated_assignment.assignment.as_term(store)); - // Check if we have found the satisfier - // (that all terms are satisfied). - if accum_term.subset_of(incompat_term) { - satisfied.insert(package.clone(), idx); - if satisfied.len() == incompat.len() { + ) -> SmallMap { + let mut satisfied = SmallMap::Empty; + for (package, incompat_term) in incompat.iter() { + let pa = package_assignments.get(package).expect("Must exist"); + // Term where we accumulate intersections until incompat_term is satisfied. + let mut accum_term = Term::any(); + // Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision. + let mut derivation_satisfier_index = None; + for (idx, dated_derivation) in pa.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) { + // We found the derivation causing satisfaction. + derivation_satisfier_index = Some(( + idx, + dated_derivation.global_index, + dated_derivation.decision_level, + )); break; } } + match derivation_satisfier_index { + Some(indices) => { + satisfied.insert(package.clone(), indices); + } + // If it wasn't found in the derivations, + // it must be the decision which is last (if called in the right context). + None => match pa.assignments_intersection { + AssignmentsIntersection::Decision((global_index, _, _)) => { + satisfied.insert( + package.clone(), + ( + pa.dated_derivations.len(), + global_index, + pa.highest_decision_level, + ), + ); + } + AssignmentsIntersection::Derivations(_) => { + panic!("This must be a decision") + } + }, + }; } satisfied } @@ -250,32 +391,96 @@ impl PartialSolution { /// 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<'a>( + fn find_previous_satisfier( incompat: &Incompatibility, - satisfier: &Assignment, - mut satisfier_map: Map, - previous_assignments: &'a [DatedAssignment], + satisfier_package: &P, + mut satisfied_map: SmallMap, + package_assignments: &Map>, store: &Arena>, ) -> DecisionLevel { - let package = satisfier.package().clone(); - let mut accum_term = satisfier.as_term(store); - let incompat_term = incompat.get(&package).expect("package not in satisfier"); - // Search previous satisfier. - for (idx, dated_assignment) in previous_assignments.iter().enumerate() { - if dated_assignment.assignment.package() != &package { - // We only care about packages related to the incompatibility. - continue; - } + // First, let's retrieve the previous derivations and the initial accum_term. + let satisfier_pa = package_assignments.get(satisfier_package).unwrap(); + let (satisfier_index, ref mut _satisfier_global_idx, ref mut _satisfier_decision_level) = + satisfied_map.get_mut(satisfier_package).unwrap(); + // *satisfier_global_idx = 0; // Changes behavior + // *satisfier_decision_level = DecisionLevel(0); // Changes behavior + + let (previous_derivations, mut accum_term) = + if *satisfier_index == satisfier_pa.dated_derivations.len() { + match &satisfier_pa.assignments_intersection { + AssignmentsIntersection::Derivations(_) => panic!("must be a decision"), + AssignmentsIntersection::Decision((_, _, term)) => { + (satisfier_pa.dated_derivations.as_slice(), term.clone()) + } + } + } else { + let dd = &satisfier_pa.dated_derivations[*satisfier_index]; + ( + &satisfier_pa.dated_derivations[..=*satisfier_index], // [..satisfier_idx] to change behavior + store[dd.cause].get(satisfier_package).unwrap().negate(), + ) + }; + + let incompat_term = incompat + .get(satisfier_package) + .expect("satisfier package not in incompat"); + + for (idx, dated_derivation) in previous_derivations.iter().enumerate() { // Check if that incompat term is satisfied by our accumulated terms intersection. - accum_term = accum_term.intersection(&dated_assignment.assignment.as_term(store)); + let this_term = store[dated_derivation.cause] + .get(satisfier_package) + .unwrap() + .negate(); + accum_term = accum_term.intersection(&this_term); // Check if we have found the satisfier if accum_term.subset_of(incompat_term) { - satisfier_map.insert(package.clone(), idx); + satisfied_map.insert( + satisfier_package.clone(), + ( + idx, + dated_derivation.global_index, + dated_derivation.decision_level, + ), + ); break; } } - previous_assignments[*satisfier_map.values().max().unwrap()] - .decision_level - .max(DecisionLevel(1)) + + // Finally, let's identify the decision level of that previous satisfier. + let (_, &(_, _, decision_level)) = satisfied_map + .iter() + .max_by_key(|(_p, (_, global_index, _))| global_index) + .unwrap(); + decision_level.max(DecisionLevel(1)) + } +} + +impl AssignmentsIntersection { + /// Returns the term intersection of all assignments (decision included). + fn term(&self) -> &Term { + match self { + Self::Decision((_, _, term)) => term, + Self::Derivations(term) => term, + } + } + + /// A package is a potential pick if there isn't an already + /// selected version (no "decision") + /// and if it contains at least one positive derivation term + /// in the partial solution. + fn potential_package_filter<'a, P: Package>( + &'a self, + package: &'a P, + ) -> Option<(&'a P, &'a Range)> { + match self { + Self::Decision(_) => None, + Self::Derivations(term_intersection) => { + if term_intersection.is_positive() { + Some((package, term_intersection.unwrap_positive())) + } else { + None + } + } + } } }