Optimize incompatibility contradiction

Author: x-hgg-x

src/internal/arena.rs

@@ -1,7 +1,7 @@
 use std::fmt;
 use std::hash::{Hash, Hasher};
 use std::marker::PhantomData;
-use std::ops::{Index, Range};
+use std::ops::{Index, IndexMut, Range};
 
 /// The index of a value allocated in an arena that holds `T`s.
 ///
@@ -118,9 +118,21 @@ impl<T> Index<Id<T>> for Arena<T> {
     }
 }
 
+impl<T> IndexMut<Id<T>> for Arena<T> {
+    fn index_mut(&mut self, id: Id<T>) -> &mut Self::Output {
+        &mut self.data[id.raw as usize]
+    }
+}
+
 impl<T> Index<Range<Id<T>>> for Arena<T> {
     type Output = [T];
     fn index(&self, id: Range<Id<T>>) -> &[T] {
         &self.data[(id.start.raw as usize)..(id.end.raw as usize)]
     }
 }
+
+impl<T> IndexMut<Range<Id<T>>> for Arena<T> {
+    fn index_mut(&mut self, id: Range<Id<T>>) -> &mut Self::Output {
+        &mut self.data[(id.start.raw as usize)..(id.end.raw as usize)]
+    }
+}

src/internal/core.rs

@@ -23,11 +23,6 @@ pub(crate) struct State<DP: DependencyProvider> {
     #[allow(clippy::type_complexity)]
     incompatibilities: Map<PackageId, Vec<IncompDpId<DP>>>,
 
-    /// Store the ids of incompatibilities that are already contradicted.
-    /// For each one keep track of the decision level when it was found to be contradicted.
-    /// These will stay contradicted until we have backtracked beyond its associated decision level.
-    contradicted_incompatibilities: Map<IncompDpId<DP>, DecisionLevel>,
-
     /// All incompatibilities expressing dependencies,
     /// with common dependents merged.
     #[allow(clippy::type_complexity)]
@@ -60,7 +55,6 @@ impl<DP: DependencyProvider> State<DP> {
             root_package_id,
             root_version_index,
             incompatibilities,
-            contradicted_incompatibilities: Map::default(),
             partial_solution: PartialSolution::empty(),
             incompatibility_store,
             unit_propagation_buffer: SmallVec::Empty,
@@ -112,13 +106,10 @@ impl<DP: DependencyProvider> State<DP> {
             let mut conflict_id = None;
             // We only care about incompatibilities if it contains the current package.
             for &incompat_id in self.incompatibilities[&current_package].iter().rev() {
-                if self
-                    .contradicted_incompatibilities
-                    .contains_key(&incompat_id)
-                {
+                let current_incompat = &mut self.incompatibility_store[incompat_id];
+                if self.partial_solution.is_contradicted(current_incompat) {
                     continue;
                 }
-                let current_incompat = &self.incompatibility_store[incompat_id];
                 match self.partial_solution.relation(current_incompat) {
                     // If the partial solution satisfies the incompatibility
                     // we must perform conflict resolution.
@@ -142,15 +133,13 @@ impl<DP: DependencyProvider> State<DP> {
                         self.partial_solution.add_derivation(
                             package_almost,
                             incompat_id,
-                            &self.incompatibility_store,
+                            current_incompat.get(package_almost).unwrap(),
                         );
                         // With the partial solution updated, the incompatibility is now contradicted.
-                        self.contradicted_incompatibilities
-                            .insert(incompat_id, self.partial_solution.current_decision_level());
+                        self.partial_solution.contradict(current_incompat);
                     }
                     Relation::Contradicted(_) => {
-                        self.contradicted_incompatibilities
-                            .insert(incompat_id, self.partial_solution.current_decision_level());
+                        self.partial_solution.contradict(current_incompat);
                     }
                     _ => {}
                 }
@@ -163,16 +152,16 @@ impl<DP: DependencyProvider> State<DP> {
                     })?;
                 self.unit_propagation_buffer.clear();
                 self.unit_propagation_buffer.push(package_almost);
+                let root_incompat = &mut self.incompatibility_store[root_cause];
                 // Add to the partial solution with incompat as cause.
                 self.partial_solution.add_derivation(
                     package_almost,
                     root_cause,
-                    &self.incompatibility_store,
+                    root_incompat.get(package_almost).unwrap(),
                 );
                 // After conflict resolution and the partial solution update,
                 // the root cause incompatibility is now contradicted.
-                self.contradicted_incompatibilities
-                    .insert(root_cause, self.partial_solution.current_decision_level());
+                self.partial_solution.contradict(root_incompat);
             }
         }
         // If there are no more changed packages, unit propagation is done.
@@ -241,9 +230,6 @@ impl<DP: DependencyProvider> State<DP> {
         decision_level: DecisionLevel,
     ) {
         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);
         if incompat_changed {
             self.merge_incompatibility(incompat_id);
         }

src/internal/incompatibility.rs

@@ -7,11 +7,46 @@ use std::fmt::{self, Debug, Display};
 use std::sync::Arc;
 
 use crate::{
-    internal::{Arena, Id, SmallMap},
+    internal::{Arena, DecisionLevel, Id, SmallMap},
     term, DefaultStringReportFormatter, DependencyProvider, DerivationTree, Derived, External, Map,
     PackageArena, PackageId, ReportFormatter, Set, Term, VersionIndex, VersionSet,
 };
 
+#[derive(Debug, Clone)]
+struct ContradicationInfo {
+    /// Store the decision level when the incompatibility was found to be contradicted.
+    /// These will stay contradicted until we have backtracked beyond its associated decision level.
+    decision_level: DecisionLevel,
+    /// Store the backtrack generation for the decision level.
+    backtrack_generation: u32,
+}
+
+impl ContradicationInfo {
+    /// Construct a new value.
+    fn new(decision_level: DecisionLevel, backtrack_generation: u32) -> Self {
+        Self {
+            decision_level,
+            backtrack_generation,
+        }
+    }
+
+    /// Construct a value interpreted as not contradicted.
+    fn not_contradicted() -> Self {
+        Self {
+            decision_level: DecisionLevel::MAX,
+            backtrack_generation: 0,
+        }
+    }
+
+    /// Check for contradiction.
+    fn is_contradicted(&self, last_valid_decision_levels: &[DecisionLevel]) -> bool {
+        last_valid_decision_levels
+            .get(self.backtrack_generation as usize)
+            .map(|&l| self.decision_level <= l)
+            .unwrap_or(true)
+    }
+}
+
 /// An incompatibility is a set of terms for different packages
 /// that should never be satisfied all together.
 /// An incompatibility usually originates from a package dependency.
@@ -31,6 +66,7 @@ use crate::{
 pub(crate) struct Incompatibility<M: Eq + Clone + Debug + Display> {
     package_terms: SmallMap<PackageId, Term>,
     kind: Kind<M>,
+    contradiction_info: ContradicationInfo,
 }
 
 /// Type alias of unique identifiers for incompatibilities.
@@ -96,6 +132,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
                 Term::negative(VersionSet::singleton(version_index)),
             )]),
             kind: Kind::NotRoot(package_id, version_index),
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -109,6 +146,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
         Self {
             package_terms: SmallMap::One([(package_id, term)]),
             kind: Kind::NoVersions(package_id, set),
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -123,6 +161,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
         Self {
             package_terms: SmallMap::One([(package_id, term)]),
             kind: Kind::Custom(package_id, set, metadata),
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -137,6 +176,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
         Self {
             package_terms: SmallMap::One([(package_id, term)]),
             kind: Kind::Custom(package_id, set, metadata),
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -157,6 +197,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
                 ])
             },
             kind: Kind::FromDependencyOf(package_id, vs, pid2, set2),
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -232,6 +273,7 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
         Self {
             package_terms,
             kind,
+            contradiction_info: ContradicationInfo::not_contradicted(),
         }
     }
 
@@ -252,6 +294,21 @@ impl<M: Eq + Clone + Debug + Display> Incompatibility<M> {
         }
     }
 
+    /// Check if an incompatibility is contradicted.
+    pub(crate) fn is_contradicted(&self, last_valid_decision_levels: &[DecisionLevel]) -> bool {
+        self.contradiction_info
+            .is_contradicted(last_valid_decision_levels)
+    }
+
+    /// Set incompatibility contradication info.
+    pub(crate) fn set_contradication_info(
+        &mut self,
+        decision_level: DecisionLevel,
+        backtrack_generation: u32,
+    ) {
+        self.contradiction_info = ContradicationInfo::new(decision_level, backtrack_generation);
+    }
+
     /// Get the term related to a given package (if it exists).
     pub(crate) fn get(&self, package_id: PackageId) -> Option<Term> {
         self.package_terms.get(&package_id).copied()
@@ -401,12 +458,14 @@ pub(crate) mod tests {
             let mut store = Arena::new();
             let i1 = store.alloc(Incompatibility {
                 package_terms: SmallMap::Two([(PackageId(1), t1), (PackageId(2), t2.negate())]),
-                kind: Kind::<String>::FromDependencyOf(PackageId(1), VersionSet::full(), PackageId(2), VersionSet::full())
+                kind: Kind::<String>::FromDependencyOf(PackageId(1), VersionSet::full(), PackageId(2), VersionSet::full()),
+                contradiction_info: ContradicationInfo::not_contradicted(),
             });
 
             let i2 = store.alloc(Incompatibility {
                 package_terms: SmallMap::Two([(PackageId(2), t2), (PackageId(3), t3)]),
-                kind: Kind::<String>::FromDependencyOf(PackageId(2), VersionSet::full(), PackageId(3), VersionSet::full())
+                kind: Kind::<String>::FromDependencyOf(PackageId(2), VersionSet::full(), PackageId(3), VersionSet::full()),
+                contradiction_info: ContradicationInfo::not_contradicted(),
             });
 
             let mut i3 = Map::default();

src/internal/partial_solution.rs

@@ -15,9 +15,12 @@ use crate::{
 };
 
 #[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)]
+#[repr(transparent)]
 pub(crate) struct DecisionLevel(u32);
 
 impl DecisionLevel {
+    pub(crate) const MAX: Self = Self(u32::MAX);
+
     fn increment(self) -> Self {
         Self(self.0 + 1)
     }
@@ -41,12 +44,12 @@ pub(crate) struct PartialSolution<DP: DependencyProvider> {
     ///    did not have a change. Within this range there is no sorting.
     #[allow(clippy::type_complexity)]
     package_assignments: FxIndexMap<PackageId, PackageAssignments<DP::M>>,
-    /// `prioritized_potential_packages` is primarily a HashMap from a package with no desition and a positive assignment
+    /// `prioritized_potential_packages` is primarily a HashMap from a package with no decision and a positive assignment
     /// to its `Priority`. But, it also maintains a max heap of packages by `Priority` order.
     prioritized_potential_packages:
         PriorityQueue<PackageId, DP::Priority, BuildHasherDefault<FxHasher>>,
     changed_this_decision_level: usize,
-    has_ever_backtracked: bool,
+    last_valid_decision_levels: Vec<DecisionLevel>,
 }
 
 impl<DP: DependencyProvider> PartialSolution<DP> {
@@ -169,10 +172,23 @@ impl<DP: DependencyProvider> PartialSolution<DP> {
             package_assignments: FxIndexMap::default(),
             prioritized_potential_packages: PriorityQueue::default(),
             changed_this_decision_level: 0,
-            has_ever_backtracked: false,
+            last_valid_decision_levels: vec![DecisionLevel(0)],
         }
     }
 
+    /// Check if an incompatibility is contradicted.
+    pub(crate) fn is_contradicted(&self, incompat: &Incompatibility<DP::M>) -> bool {
+        incompat.is_contradicted(&self.last_valid_decision_levels)
+    }
+
+    /// Contradict an incompatibility.
+    pub(crate) fn contradict(&self, incompat: &mut Incompatibility<DP::M>) {
+        incompat.set_contradication_info(
+            self.current_decision_level,
+            self.last_valid_decision_levels.len() as u32,
+        );
+    }
+
     /// Add a decision.
     pub(crate) fn add_decision(&mut self, package_id: PackageId, version_index: VersionIndex) {
         // Check that add_decision is never used in the wrong context.
@@ -222,14 +238,14 @@ impl<DP: DependencyProvider> PartialSolution<DP> {
         &mut self,
         package_id: PackageId,
         cause: IncompDpId<DP>,
-        store: &Arena<Incompatibility<DP::M>>,
+        incompat_term: Term,
     ) {
         use indexmap::map::Entry;
         let mut dated_derivation = DatedDerivation {
             global_index: self.next_global_index,
             decision_level: self.current_decision_level,
             cause,
-            accumulated_intersection: store[cause].get(package_id).unwrap().negate(),
+            accumulated_intersection: incompat_term.negate(),
         };
         self.next_global_index += 1;
         let pa_last_index = self.package_assignments.len().saturating_sub(1);
@@ -366,7 +382,16 @@ impl<DP: DependencyProvider> PartialSolution<DP> {
         // Throw away all stored priority levels, And mark that they all need to be recomputed.
         self.prioritized_potential_packages.clear();
         self.changed_this_decision_level = self.current_decision_level.0.saturating_sub(1) as usize;
-        self.has_ever_backtracked = true;
+
+        // Update list of last valid contradicted decision levels
+        self.last_valid_decision_levels
+            .push(DecisionLevel(u32::MAX));
+
+        let index = self
+            .last_valid_decision_levels
+            .partition_point(|&l| l <= decision_level);
+
+        self.last_valid_decision_levels[index..].fill(decision_level);
     }
 
     /// We can add the version to the partial solution as a decision
@@ -383,7 +408,7 @@ impl<DP: DependencyProvider> PartialSolution<DP> {
         package_store: &PackageArena<DP::P>,
         dependency_provider: &DP,
     ) {
-        if !self.has_ever_backtracked {
+        if self.last_valid_decision_levels.len() == 1 {
             // Nothing has yet gone wrong during this resolution. This call is unlikely to be the first problem.
             // So let's live with a little bit of risk and add the decision without checking the dependencies.
             // The worst that can happen is we will have to do a full backtrack which only removes this one decision.
@@ -546,10 +571,6 @@ impl<DP: DependencyProvider> PartialSolution<DP> {
             .unwrap();
         decision_level.max(DecisionLevel(1))
     }
-
-    pub(crate) fn current_decision_level(&self) -> DecisionLevel {
-        self.current_decision_level
-    }
 }
 
 impl<M: Eq + Clone + Debug + Display> PackageAssignments<M> {