diff --git a/src/internal/core.rs b/src/internal/core.rs index 7116c7b8..4b574689 100644 --- a/src/internal/core.rs +++ b/src/internal/core.rs @@ -27,9 +27,10 @@ pub struct State { pub incompatibilities: Map>>, - /// Store the ids of incompatibilities that are already contradicted - /// and will stay that way until the next conflict and backtrack is operated. - contradicted_incompatibilities: rustc_hash::FxHashSet>, + /// 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, DecisionLevel>, /// All incompatibilities expressing dependencies, /// with common dependents merged. @@ -62,7 +63,7 @@ impl State { root_package, root_version, incompatibilities, - contradicted_incompatibilities: rustc_hash::FxHashSet::default(), + contradicted_incompatibilities: Map::default(), partial_solution: PartialSolution::empty(), incompatibility_store, unit_propagation_buffer: SmallVec::Empty, @@ -111,7 +112,10 @@ impl State { let mut conflict_id = None; // We only care about incompatibilities if it contains the current package. for &incompat_id in self.incompatibilities[¤t_package].iter().rev() { - if self.contradicted_incompatibilities.contains(&incompat_id) { + if self + .contradicted_incompatibilities + .contains_key(&incompat_id) + { continue; } let current_incompat = &self.incompatibility_store[incompat_id]; @@ -135,10 +139,12 @@ impl State { &self.incompatibility_store, ); // With the partial solution updated, the incompatibility is now contradicted. - self.contradicted_incompatibilities.insert(incompat_id); + self.contradicted_incompatibilities + .insert(incompat_id, self.partial_solution.current_decision_level()); } Relation::Contradicted(_) => { - self.contradicted_incompatibilities.insert(incompat_id); + self.contradicted_incompatibilities + .insert(incompat_id, self.partial_solution.current_decision_level()); } _ => {} } @@ -155,7 +161,8 @@ impl State { ); // After conflict resolution and the partial solution update, // the root cause incompatibility is now contradicted. - self.contradicted_incompatibilities.insert(root_cause); + self.contradicted_incompatibilities + .insert(root_cause, self.partial_solution.current_decision_level()); } } // If there are no more changed packages, unit propagation is done. @@ -220,7 +227,9 @@ impl State { ) { self.partial_solution .backtrack(decision_level, &self.incompatibility_store); - self.contradicted_incompatibilities.clear(); + // 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); } diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs index 6a8a2bff..b1889a3f 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -511,6 +511,10 @@ impl PartialSolution DecisionLevel { + self.current_decision_level + } } impl PackageAssignments {