diff --git a/src/solver/clause.rs b/src/solver/clause.rs index 7226068..087dead 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -9,6 +9,7 @@ use crate::{ }; use crate::internal::id::StringId; +use crate::solver::decision_tracker::DecisionTracker; use elsa::FrozenMap; use std::fmt::{Debug, Display, Formatter}; use std::hash::Hash; @@ -83,31 +84,74 @@ pub(crate) enum Clause { } impl Clause { - /// Returns the ids of the solvables that will be watched as well as the clause itself. + /// Returns the building blocks needed for a new [ClauseState] of the [Clause::Requires] kind. + /// + /// These building blocks are: + /// + /// - The [Clause] itself; + /// - The ids of the solvables that will be watched (unless there are no candidates, i.e. the + /// clause is actually an assertion); + /// - A boolean indicating whether the clause conflicts with existing decisions. This should + /// always be false when adding clauses before starting the solving process, but can be true + /// for clauses that are added dynamically. fn requires( - candidate: SolvableId, + parent: SolvableId, requirement: VersionSetId, candidates: &[SolvableId], - ) -> (Self, Option<[SolvableId; 2]>) { - ( - Clause::Requires(candidate, requirement), - if candidates.is_empty() { - None - } else { - Some([candidate, candidates[0]]) - }, - ) + decision_tracker: &DecisionTracker, + ) -> (Self, Option<[SolvableId; 2]>, bool) { + // It only makes sense to introduce a requires clause when the parent solvable is undecided + // or going to be installed + assert_ne!(decision_tracker.assigned_value(parent), Some(false)); + + let kind = Clause::Requires(parent, requirement); + if candidates.is_empty() { + (kind, None, false) + } else { + match candidates + .iter() + .find(|&&c| decision_tracker.assigned_value(c) != Some(false)) + { + // Watch any candidate that is not assigned to false + Some(watched_candidate) => (kind, Some([parent, *watched_candidate]), false), + + // All candidates are assigned to false! Therefore the clause conflicts with the + // current decisions. There are no valid watches for it at the moment, but we will + // assign default ones nevertheless, because they will become valid after the solver + // restarts. + None => (kind, Some([parent, candidates[0]]), true), + } + } } - /// Returns the ids of the solvables that will be watched as well as the clause itself. + /// Returns the building blocks needed for a new [ClauseState] of the [Clause::Constrains] kind. + /// + /// These building blocks are: + /// + /// - The [Clause] itself; + /// - The ids of the solvables that will be watched; + /// - A boolean indicating whether the clause conflicts with existing decisions. This should + /// always be false when adding clauses before starting the solving process, but can be true + /// for clauses that are added dynamically. fn constrains( - candidate: SolvableId, - constrained_candidate: SolvableId, + parent: SolvableId, + forbidden_solvable: SolvableId, via: VersionSetId, - ) -> (Self, Option<[SolvableId; 2]>) { + decision_tracker: &DecisionTracker, + ) -> (Self, Option<[SolvableId; 2]>, bool) { + // It only makes sense to introduce a constrains clause when the parent solvable is + // undecided or going to be installed + assert_ne!(decision_tracker.assigned_value(parent), Some(false)); + + // If the forbidden solvable is already assigned to true, that means that there is a + // conflict with current decisions, because it implies the parent solvable would be false + // (and we just asserted that it is not) + let conflict = decision_tracker.assigned_value(forbidden_solvable) == Some(true); + ( - Clause::Constrains(candidate, constrained_candidate, via), - Some([candidate, constrained_candidate]), + Clause::Constrains(parent, forbidden_solvable, via), + Some([parent, forbidden_solvable]), + conflict, ) } @@ -243,25 +287,48 @@ impl ClauseState { Self::from_kind_and_initial_watches(kind, watched_literals) } - /// Shorthand method to construct a Clause::Requires without requiring complicated arguments. + /// Shorthand method to construct a [Clause::Requires] without requiring complicated arguments. + /// + /// The returned boolean value is true when adding the clause resulted in a conflict. pub fn requires( candidate: SolvableId, requirement: VersionSetId, matching_candidates: &[SolvableId], - ) -> Self { - let (kind, watched_literals) = - Clause::requires(candidate, requirement, matching_candidates); - Self::from_kind_and_initial_watches(kind, watched_literals) + decision_tracker: &DecisionTracker, + ) -> (Self, bool) { + let (kind, watched_literals, conflict) = Clause::requires( + candidate, + requirement, + matching_candidates, + decision_tracker, + ); + + ( + Self::from_kind_and_initial_watches(kind, watched_literals), + conflict, + ) } + /// Shorthand method to construct a [Clause::Constrains] without requiring complicated arguments. + /// + /// The returned boolean value is true when adding the clause resulted in a conflict. pub fn constrains( candidate: SolvableId, constrained_package: SolvableId, requirement: VersionSetId, - ) -> Self { - let (kind, watched_literals) = - Clause::constrains(candidate, constrained_package, requirement); - Self::from_kind_and_initial_watches(kind, watched_literals) + decision_tracker: &DecisionTracker, + ) -> (Self, bool) { + let (kind, watched_literals, conflict) = Clause::constrains( + candidate, + constrained_package, + requirement, + decision_tracker, + ); + + ( + Self::from_kind_and_initial_watches(kind, watched_literals), + conflict, + ) } pub fn lock(locked_candidate: SolvableId, other_candidate: SolvableId) -> Self { @@ -556,6 +623,7 @@ impl Debug for ClauseDebug<'_, VS, N> mod test { use super::*; use crate::internal::arena::ArenaId; + use crate::solver::decision::Decision; fn clause(next_clauses: [ClauseId; 2], watched_solvables: [SolvableId; 2]) -> ClauseState { ClauseState { @@ -694,6 +762,104 @@ mod test { } } + #[test] + fn test_requires_with_and_without_conflict() { + let mut decisions = DecisionTracker::new(); + + let parent = SolvableId::from_usize(1); + let candidate1 = SolvableId::from_usize(2); + let candidate2 = SolvableId::from_usize(3); + + // No conflict, all candidates available + let (clause, conflict) = ClauseState::requires( + parent, + VersionSetId::from_usize(0), + &[candidate1, candidate2], + &decisions, + ); + assert!(!conflict); + assert_eq!(clause.watched_literals[0], parent); + assert_eq!(clause.watched_literals[1], candidate1); + + // No conflict, still one candidate available + decisions + .try_add_decision(Decision::new(candidate1, false, ClauseId::null()), 1) + .unwrap(); + let (clause, conflict) = ClauseState::requires( + parent, + VersionSetId::from_usize(0), + &[candidate1, candidate2], + &decisions, + ); + assert!(!conflict); + assert_eq!(clause.watched_literals[0], parent); + assert_eq!(clause.watched_literals[1], candidate2); + + // Conflict, no candidates available + decisions + .try_add_decision(Decision::new(candidate2, false, ClauseId::null()), 1) + .unwrap(); + let (clause, conflict) = ClauseState::requires( + parent, + VersionSetId::from_usize(0), + &[candidate1, candidate2], + &decisions, + ); + assert!(conflict); + assert_eq!(clause.watched_literals[0], parent); + assert_eq!(clause.watched_literals[1], candidate1); + + // Panic + decisions + .try_add_decision(Decision::new(parent, false, ClauseId::null()), 1) + .unwrap(); + let panicked = std::panic::catch_unwind(|| { + ClauseState::requires( + parent, + VersionSetId::from_usize(0), + &[candidate1, candidate2], + &decisions, + ) + }) + .is_err(); + assert!(panicked); + } + + #[test] + fn test_constrains_with_and_without_conflict() { + let mut decisions = DecisionTracker::new(); + + let parent = SolvableId::from_usize(1); + let forbidden = SolvableId::from_usize(2); + + // No conflict, forbidden package not installed + let (clause, conflict) = + ClauseState::constrains(parent, forbidden, VersionSetId::from_usize(0), &decisions); + assert!(!conflict); + assert_eq!(clause.watched_literals[0], parent); + assert_eq!(clause.watched_literals[1], forbidden); + + // Conflict, forbidden package installed + decisions + .try_add_decision(Decision::new(forbidden, true, ClauseId::null()), 1) + .unwrap(); + let (clause, conflict) = + ClauseState::constrains(parent, forbidden, VersionSetId::from_usize(0), &decisions); + assert!(conflict); + assert_eq!(clause.watched_literals[0], parent); + assert_eq!(clause.watched_literals[1], forbidden); + + // Panic + decisions + .try_add_decision(Decision::new(parent, false, ClauseId::null()), 1) + .unwrap(); + let panicked = std::panic::catch_unwind(|| { + ClauseState::constrains(parent, forbidden, VersionSetId::from_usize(0), &decisions) + }) + .is_err(); + assert!(panicked); + } + #[test] fn test_clause_size() { // This test is here to ensure we don't increase the size of `ClauseState` by accident, as diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 8cfc83f..66e9cbe 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -36,6 +36,8 @@ pub struct Solver> requires_clauses: Vec<(SolvableId, VersionSetId, ClauseId)>, watches: WatchMap, + negative_assertions: Vec<(SolvableId, ClauseId)>, + learnt_clauses: Arena>, learnt_why: Mapping>, learnt_clause_ids: Vec, @@ -57,6 +59,7 @@ impl> Solver> Sol ) -> Result, Problem> { // Clear state self.decision_tracker.clear(); + self.negative_assertions.clear(); self.learnt_clauses.clear(); self.learnt_why = Mapping::new(); self.clauses = Default::default(); @@ -135,12 +139,18 @@ impl> Sol /// Adds clauses for a solvable. These clauses include requirements and constrains on other /// solvables. - fn add_clauses_for_solvable(&mut self, solvable_id: SolvableId) -> Vec { + /// + /// Returns the added clauses, and an additional list with conflicting clauses (if any). + fn add_clauses_for_solvable( + &mut self, + solvable_id: SolvableId, + ) -> (Vec, Vec) { if self.clauses_added_for_solvable.contains(&solvable_id) { - return Vec::new(); + return (Vec::new(), Vec::new()); } let mut new_clauses = Vec::new(); + let mut conflicting_clauses = Vec::new(); let mut queue = vec![solvable_id]; let mut seen = HashSet::new(); seen.insert(solvable_id); @@ -166,7 +176,6 @@ impl> Sol // Add clauses for the requirements for version_set_id in requirements { - //self.add_clauses_for_requirement(solvable_id, requirement); let dependency_name = self.pool().resolve_version_set_package_name(version_set_id); self.add_clauses_for_package(dependency_name); @@ -185,11 +194,22 @@ impl> Sol } // Add the requires clause - let clause_id = self.add_and_watch_clause(ClauseState::requires( + let no_candidates = candidates.is_empty(); + let (clause, conflict) = ClauseState::requires( solvable_id, version_set_id, candidates, - )); + &self.decision_tracker, + ); + + let clause_id = self.add_and_watch_clause(clause); + + if conflict { + conflicting_clauses.push(clause_id); + } else if no_candidates { + // Add assertions for unit clauses (i.e. those with no matching candidates) + self.negative_assertions.push((solvable_id, clause_id)); + } new_clauses.push(clause_id); } @@ -206,9 +226,19 @@ impl> Sol // Add forbidden clauses for the candidates for forbidden_candidate in constrained_candidates.iter().copied().collect_vec() { - let clause = - ClauseState::constrains(solvable_id, forbidden_candidate, version_set_id); + let (clause, conflict) = ClauseState::constrains( + solvable_id, + forbidden_candidate, + version_set_id, + &self.decision_tracker, + ); + let clause_id = self.add_and_watch_clause(clause); + + if conflict { + conflicting_clauses.push(clause_id); + } + new_clauses.push(clause_id) } } @@ -217,7 +247,7 @@ impl> Sol self.clauses_added_for_solvable.insert(solvable_id); } - new_clauses + (new_clauses, conflicting_clauses) } /// Adds all clauses for a specific package name. @@ -330,9 +360,12 @@ impl> Sol let mut new_clauses = Vec::new(); loop { - // If the decision loop has been completely reset we want to + // A level of 0 means the decision loop has been completely reset because a partial + // solution was invalidated by newly added clauses. if level == 0 { + // Level 1 is the initial decision level level = 1; + // Assign `true` to the root solvable. This must be installed to satisfy the solution. // The root solvable contains the dependencies that were injected when calling // `Solver::solve`. If we can find a solution were the root is installable we found a @@ -349,17 +382,29 @@ impl> Sol .expect("already decided"); // Add the clauses for the root solvable. - new_clauses.append(&mut self.add_clauses_for_solvable(SolvableId::root())); + let (mut clauses, conflicting_clauses) = + self.add_clauses_for_solvable(SolvableId::root()); + if let Some(clause_id) = conflicting_clauses.into_iter().next() { + return Err(self.analyze_unsolvable(clause_id)); + } + new_clauses.append(&mut clauses); } - // Add decisions for Require clauses that form unit clauses. E.g. require clauses that - // have no matching candidates. - self.decide_requires_without_candidates(&std::mem::take(&mut new_clauses)) - .map_err(|clause_id| self.analyze_unsolvable(clause_id))?; - - // Propagate any decisions from assignments above. - self.propagate(level) - .map_err(|(_, _, clause_id)| self.analyze_unsolvable(clause_id))?; + // Propagate decisions from assignments above + let propagate_result = self.propagate(level); + if let Err((_, _, clause_id)) = propagate_result { + if level == 1 { + return Err(self.analyze_unsolvable(clause_id)); + } else { + // When the level is higher than 1, that means the conflict was caused because + // new clauses have been added dynamically. We need to start over. + tracing::debug!("├─ added clause {clause:?} introduces a conflict which invalidates the partial solution", + clause=self.clauses[clause_id].debug(self.pool())); + level = 0; + self.decision_tracker.clear(); + continue; + } + } // Enter the solver loop, return immediately if no new assignments have been made. level = self.resolve_dependencies(level)?; @@ -399,114 +444,21 @@ impl> Sol for (solvable, _) in new_solvables { // Add the clauses for this particular solvable. - let mut clauses_for_solvable = self.add_clauses_for_solvable(solvable); - - // Immediately assign unit clauses. If clause is found that is a unit clause we - // permanently fix that assignment to false and an error is returned. - for clause_id in clauses_for_solvable.iter().copied() { - let clause = &self.clauses[clause_id]; - - match clause.kind { - Clause::Requires(dependent, requirement) => { - let solvable_is_assigned = - self.decision_tracker.assigned_value(dependent) == Some(true); - if solvable_is_assigned { - let candidates = - self.cache.get_or_cache_matching_candidates(requirement); - let all_candidates_assigned_false = candidates.iter().all(|&s| { - self.decision_tracker.assigned_value(s) == Some(false) - }); - let is_empty = candidates.is_empty(); - - // If none of the candidates is selectable this clause will cause a - // conflict. We have to backtrack to the point where we made the - // decision to select - if all_candidates_assigned_false { - tracing::debug!( - "├─ there are no selectable candidates for {clause:?}", - clause = self.clauses[clause_id].debug(self.pool()) - ); - - self.decision_tracker.clear(); - level = 0; - - break; - } else if is_empty { - tracing::debug!("├─ added clause {clause:?} has no candidates which invalidates the partial solution", - clause=self.clauses[clause_id].debug(self.pool())); - - self.decision_tracker.clear(); - level = 0; - break; - } - } - } - Clause::Constrains(dependent, forbidden, _) => { - if self.decision_tracker.assigned_value(forbidden) == Some(true) - && self.decision_tracker.assigned_value(dependent) == Some(true) - { - tracing::debug!( - "├─ {clause:?} which was already set to true", - clause = self.clauses[clause_id].debug(self.pool()) - ); - self.decision_tracker.clear(); - level = 0; - break; - } - } - _ => unreachable!(), - } - } - + let (mut clauses_for_solvable, conflicting_causes) = + self.add_clauses_for_solvable(solvable); new_clauses.append(&mut clauses_for_solvable); - } - } - } - - /// Forbid packages that rely on dependencies without candidates - /// - /// Since a requires clause is represented as (¬A ∨ candidate_1 ∨ ... ∨ candidate_n), - /// a dependency without candidates becomes (¬A), which means that A should always be false. - fn decide_requires_without_candidates( - &mut self, - clauses: &[ClauseId], - ) -> Result { - tracing::trace!("=== Deciding assertions for requires without candidates"); - let mut conflicting_clause = None; - let mut made_a_decision = false; - for &clause_id in clauses.iter() { - let clause = &self.clauses[clause_id]; - let decision = match clause.kind { - // A requires clause without watches means it has a single literal (i.e. - // there are no candidates) - Clause::Requires(solvable_id, _) if !clause.has_watches() => self - .decision_tracker - .try_add_fixed_assignment(Decision::new(solvable_id, false, clause_id)) - .map(|b| b.then_some(solvable_id)), - _ => continue, - }; - - match decision { - Ok(Some(solvable_id)) => { - // We made a decision without conflict. - tracing::debug!("Set {} = false", solvable_id.display(self.pool())); - made_a_decision = true; - } - Err(_) => { - // Decision immediately caused a conflict! - conflicting_clause = Some(clause_id); - made_a_decision = true; - } - Ok(None) => { - // No new decision + for &clause_id in &conflicting_causes { + // Backtrack in the case of conflicts + tracing::debug!("├─ added clause {clause:?} introduces a conflict which invalidates the partial solution", + clause=self.clauses[clause_id].debug(self.pool())); } - }; - } - match conflicting_clause { - None => Ok(made_a_decision), - Some(clause_id) => Err(clause_id), + if !conflicting_causes.is_empty() { + self.decision_tracker.clear(); + level = 0; + } + } } } @@ -732,8 +684,25 @@ impl> Sol /// way, the clause can check whether the literal that is using the solvable has become false, in /// which case it picks a new solvable to watch (if available) or triggers an assignment. fn propagate(&mut self, level: u32) -> Result<(), (SolvableId, bool, ClauseId)> { - // Learnt assertions (assertions are clauses that consist of a single literal, and therefore - // do not have watches) + // Negative assertions derived from other rules (assertions are clauses that consist of a + // single literal, and therefore do not have watches) + for &(solvable_id, clause_id) in &self.negative_assertions { + let value = false; + let decided = self + .decision_tracker + .try_add_decision(Decision::new(solvable_id, value, clause_id), level) + .map_err(|_| (solvable_id, value, clause_id))?; + + if decided { + tracing::trace!( + "├─ Propagate assertion {} = {}", + solvable_id.display(self.pool()), + value + ); + } + } + + // Assertions derived from learnt rules for learn_clause_idx in 0..self.learnt_clause_ids.len() { let clause_id = self.learnt_clause_ids[learn_clause_idx]; let clause = &self.clauses[clause_id]; diff --git a/tests/solver.rs b/tests/solver.rs index b44a317..a6115bf 100644 --- a/tests/solver.rs +++ b/tests/solver.rs @@ -458,7 +458,6 @@ fn test_resolve_with_nonexisting() { #[test] #[traced_test] -#[should_panic] // TODO: Should be fixed, https://github.com/prefix-dev/rip/issues/75 fn test_resolve_with_nested_deps() { let provider = BundleBoxProvider::from_packages(&[ (