diff --git a/src/lib.rs b/src/lib.rs index fbda8fa..b3b3643 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,7 +34,9 @@ pub use id::{ }; use itertools::Itertools; pub use requirement::Requirement; -pub use solver::{EmptySolvables, Problem, Solver, SolverCache, UnsolvableOrCancelled}; +pub use solver::{ + EmptySolvables, Problem, Solver, SolverCache, SolverConfig, UnsolvableOrCancelled, +}; pub use solver_id::{DenseId, IdMap, IdSet, SolverId, SparseId}; pub use utils::{IndexedSet, Mapping, MappingIter}; @@ -158,6 +160,15 @@ pub trait DependencyProvider: Sized + Interner { fn should_cancel_with_value(&self) -> Option> { None } + + /// Returns the solver configuration for this dependency provider. + /// + /// Override this to customize solver behavior. The returned config is used + /// by [`Solver::new`] unless explicitly overridden with + /// [`Solver::with_config`]. + fn solver_config(&self) -> SolverConfig { + SolverConfig::default() + } } /// A list of candidate solvables for a specific package. This is returned from diff --git a/src/solver/encoding.rs b/src/solver/encoding.rs index 49fc6b7..5e05af3 100644 --- a/src/solver/encoding.rs +++ b/src/solver/encoding.rs @@ -1,6 +1,10 @@ use std::{any::Any, collections::VecDeque}; -use super::{SolverState, clause::WatchedLiterals, conditions}; +use super::{ + SolverConfig, SolverState, + clause::{Clause, WatchedLiterals}, + conditions, +}; use crate::{ Candidates, ConditionId, ConditionalRequirement, DenseIndex, Dependencies, DependencyProvider, Requirement, SolverCache, StringId, VariableId, VersionSetId, @@ -70,6 +74,7 @@ async fn get_requirement_candidates( pub(crate) struct Encoder<'a, 'cache, D: DependencyProvider> { state: &'a mut SolverState, cache: &'cache SolverCache, + config: &'a SolverConfig, level: u32, /// The dependencies of the root solvable. @@ -192,6 +197,7 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { pub fn new( state: &'a mut SolverState, cache: &'cache SolverCache, + config: &'a SolverConfig, root_dependencies: &'cache Dependencies, level: u32, future_queue_mode: FutureQueueMode, @@ -199,6 +205,7 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { Self { state, cache, + config, root_dependencies, pending_futures: FuturesUnordered::new(), conflicting_clauses: Vec::new(), @@ -693,30 +700,33 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { let variable = self.state.variable_map.intern_solvable_or_root(solvable_id); + // Whether the constraining solvable is itself one of the forbidden + // (non-matching) candidates: i.e. it conflicts with a capability it + // also provides (a self-conflict). + let self_conflict = candidates + .iter() + .any(|&c| SolvableIdOrRoot::from(c) == solvable_id); + if candidates.len() < CONSTRAINS_AUX_ENCODING_THRESHOLD { // Pairwise encoding: one (¬parent ∨ ¬candidate) clause per - // excluded candidate. - for &forbidden_candidate in candidates { - let forbidden_candidate_var = - self.state.variable_map.intern_solvable(forbidden_candidate); - let (watched_literals, conflict, kind) = WatchedLiterals::constrains( - variable, - forbidden_candidate_var, - constraint, - &self.state.decision_tracker, - ); - - let clause_id = self.state.add_clause(watched_literals, kind); - - if conflict { - self.conflicting_clauses.push(clause_id); - } + // excluded candidate, skipping the parent itself. + self.add_constrains_pairwise_for_parent(variable, solvable_id, constraint, candidates); + if self_conflict && self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); } return; } // Shared encoding: the (¬candidate ∨ aux) clauses are emitted once per - // version set, each parent only adds a single (¬parent ∨ ¬aux) clause. + // version set, each non-self parent only adds a single (¬parent ∨ ¬aux) + // clause. + // + // The aux variable means "some forbidden candidate of this constraint + // is installed" and MUST be defined over *all* candidates, so its + // meaning does not depend on which parent happens to build it. Skipping + // a candidate here (e.g. a self-conflicting parent) would both leave + // that candidate un-forbidden for every *other* parent and make every + // other self-conflicting provider that reuses the aux uninstallable. let aux_variable = match self.state.constrains_aux_vars.get(&constraint) { Some(&aux_variable) => aux_variable, None => { @@ -761,6 +771,25 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { } }; + // A self-conflicting parent is itself part of the aux definition + // (parent -> aux), so the shared (parent -> ¬aux) clause would make it + // uninstallable. Encode such a parent pairwise instead (forbidding the + // other providers but not itself), or, if self-conflicts are forbidden, + // mark it uninstallable directly. + if self_conflict { + if self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); + } else { + self.add_constrains_pairwise_for_parent( + variable, + solvable_id, + constraint, + candidates, + ); + } + return; + } + let (watched_literals, conflict, kind) = WatchedLiterals::constrains_parent( variable, aux_variable, @@ -773,6 +802,36 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { } } + /// Emits the pairwise constrains clauses `(¬parent ∨ ¬candidate)` for a + /// single parent, skipping the parent itself (a self-conflict). + fn add_constrains_pairwise_for_parent( + &mut self, + variable: VariableId, + solvable_id: SolvableIdOrRoot, + constraint: VersionSetId, + candidates: &[D::SolvableId], + ) { + for &forbidden_candidate in candidates { + if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { + continue; + } + let forbidden_candidate_var = + self.state.variable_map.intern_solvable(forbidden_candidate); + let (watched_literals, conflict, kind) = WatchedLiterals::constrains( + variable, + forbidden_candidate_var, + constraint, + &self.state.decision_tracker, + ); + + let clause_id = self.state.add_clause(watched_literals, kind); + + if conflict { + self.conflicting_clauses.push(clause_id); + } + } + } + /// Adds clauses to forbid any other clauses than the locked solvable to be /// installed. fn add_locked_package_clauses( @@ -819,6 +878,19 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { variable } + /// Adds a unary constrains clause that forbids a solvable that conflicts + /// with something it also provides (a self-conflict). + fn add_self_conflict_clause(&mut self, variable: VariableId, constraint: VersionSetId) { + let kind = Clause::Constrains(variable, variable, constraint); + let clause_id = self.state.add_clause(None, kind); + + self.state.negative_assertions.push((variable, clause_id)); + + if self.state.decision_tracker.assigned_value(variable) == Some(true) { + self.conflicting_clauses.push(clause_id); + } + } + /// Enqueues retrieving the dependencies for a solvable. /// /// This method requests the dependencies for the given solvable in an diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 3aace71..17cee5b 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -176,6 +176,23 @@ impl Clauses { type RequirementCandidateVariables = Vec>; +/// Configuration options for the solver. +#[derive(Debug, Clone)] +pub struct SolverConfig { + /// When `true`, a package that conflicts with something it also provides + /// (i.e. it conflicts with itself) is marked uninstallable. When `false`, + /// self-conflicts are silently ignored. + pub forbid_self_conflicts: bool, +} + +impl Default for SolverConfig { + fn default() -> Self { + Self { + forbid_self_conflicts: true, + } + } +} + /// Drives the SAT solving process. pub struct Solver { /// The runtime to use for async operations. @@ -191,6 +208,9 @@ pub struct Solver { /// runtime remains pending-capable without extending the public runtime contract. future_queue_mode: FutureQueueMode, + /// Solver configuration options. + config: SolverConfig, + /// The activity add factor. This is a value that is added to the activity /// score of each package that is part of a conflict. activity_add: f32, @@ -372,11 +392,13 @@ impl Solver { /// Creates a single threaded block solver, using the provided /// [`DependencyProvider`]. pub fn new(provider: D) -> Self { + let config = provider.solver_config(); Self { cache: SolverCache::new(provider), async_runtime: NowOrNeverRuntime, state: SolverState::default(), future_queue_mode: FutureQueueMode::Immediate, + config, activity_add: 1.0, activity_decay: 0.95, } @@ -454,6 +476,7 @@ impl Solver { cache: self.cache, state: self.state, future_queue_mode: FutureQueueMode::PendingCapable, + config: self.config, activity_decay: self.activity_decay, activity_add: self.activity_add, } @@ -470,6 +493,12 @@ impl Solver { } } + /// Set the solver configuration. + #[must_use] + pub fn with_config(self, config: SolverConfig) -> Self { + Self { config, ..self } + } + /// Solves the given [`Problem`]. /// /// The solver first solves for the root requirements and constraints, and @@ -643,6 +672,7 @@ impl Solver { Encoder::new( &mut self.state, &self.cache, + &self.config, root_deps, level, self.future_queue_mode, @@ -804,6 +834,7 @@ impl Solver { Encoder::new( &mut self.state, &self.cache, + &self.config, root_deps, level, self.future_queue_mode, diff --git a/tests/solver/main.rs b/tests/solver/main.rs index 6d26355..21115cf 100644 --- a/tests/solver/main.rs +++ b/tests/solver/main.rs @@ -7,7 +7,7 @@ use insta::assert_snapshot; use itertools::Itertools; use resolvo::{ ConditionalRequirement, DependencyProvider, Interner, Problem, SolvableId, Solver, - UnsolvableOrCancelled, VersionSetId, + SolverConfig, UnsolvableOrCancelled, VersionSetId, }; use tracing_test::traced_test; @@ -2131,6 +2131,174 @@ fn test_constrains_multiple_parents() { x=1 "###); } +mod test_self_conflict { + use super::*; + + /// When `forbid_self_conflicts` is false, a package that constrains itself + /// is silently allowed. Some ecosystems (e.g. RPM) explicitly support this. + /// The real-world examples are structured a bit differently however. + #[test] + fn test_self_conflict_allowed() { + let mut provider = BundleBoxProvider::new(); + // a=1 constrains "a" to [2,100) — version 1 is NOT in that range, + // so a=1 appears as a non-matching candidate for its own constraint + // (i.e. a self-conflict). + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).unwrap(); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r" + a=1 + "); + } + + /// When `forbid_self_conflicts` is true (the default), a package that + /// constrains itself is marked uninstallable. + #[test] + fn test_self_conflict_forbidden() { + let mut provider = BundleBoxProvider::new(); + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + + let requirements = provider.requirements(&["a"]); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + match solver.solve(problem) { + Ok(_) => panic!("expected unsat due to self-conflict"), + Err(UnsolvableOrCancelled::Unsolvable(_)) => {} + Err(UnsolvableOrCancelled::Cancelled(_)) => { + panic!("expected unsolvable, not cancelled") + } + } + } + + /// `allow_self_conflicts` works correctly when the self-conflicting + /// package is a transitive dependency discovered in a later solver pass. + #[test] + fn test_self_conflict_allowed_transitive() { + let mut provider = BundleBoxProvider::new(); + // "a" has a self-conflict and is a transitive dep of "app" via "lib". + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + provider.add_package("lib", 1.into(), &["a"], &[]); + provider.add_package("app", 1.into(), &["lib"], &[]); + + let requirements = provider.requirements(&["app"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).unwrap(); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r" + a=1 + app=1 + lib=1 + "); + } + + /// Multiple self-conflicting providers of the SAME capability, enough of + /// them (>= CONSTRAINS_AUX_ENCODING_THRESHOLD == 4) to trigger the shared + /// aux-variable constrains encoding. This mirrors the real CentOS case: + /// several versions of centos-stream-release each provide AND conflict + /// with `system-release`. Installing any one of them should succeed (it + /// just excludes the OTHER providers). The `100..200` range matches none of + /// the existing versions, so every version is a non-matching (forbidden) + /// candidate of its own constraint, i.e. a self-conflict. + #[test] + fn test_self_conflict_multiple_providers() { + let mut provider = BundleBoxProvider::new(); + for v in 1..=5u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should be solvable"); + let result = transaction_to_string(solver.provider(), &solved); + // Exactly one version of "a" should be installed. + assert_snapshot!(result, @"a=5"); + } + + /// Same shape as above (shared aux encoding), but the highest version — + /// which builds the shared aux variable — is unsatisfiable, forcing the + /// solver to fall back to a lower self-conflicting provider that reuses the + /// aux var. Regression test: the shared aux definition must cover *all* + /// candidates so the fallback provider is not spuriously uninstallable. + #[test] + fn test_self_conflict_multiple_providers_fallback() { + let mut provider = BundleBoxProvider::new(); + // a=5 pulls in a missing dependency, so it cannot be installed, but the + // solver considers it first (highest version) and builds the aux var. + provider.add_package("a", 5.into(), &["missing"], &["a 100..200"]); + for v in 1..=4u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should fall back to a=4"); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @"a=4"); + } + + /// Control for the above: identical fallback shape but only 3 providers + /// (< threshold), so the pairwise encoding is used instead of the shared + /// aux variable. This path was already correct; guard against regressions. + #[test] + fn test_self_conflict_pairwise_fallback() { + let mut provider = BundleBoxProvider::new(); + provider.add_package("a", 3.into(), &["missing"], &["a 100..200"]); + for v in 1..=2u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should fall back to a=2"); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @"a=2"); + } + + /// With `forbid_self_conflicts` (the default), multiple self-conflicting + /// providers on the shared-aux path are ALL uninstallable, so the whole + /// solve is unsat. + #[test] + fn test_self_conflict_multiple_providers_forbidden() { + let mut provider = BundleBoxProvider::new(); + for v in 1..=5u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + match solver.solve(problem) { + Ok(_) => panic!("expected unsat: all providers self-conflict"), + Err(UnsolvableOrCancelled::Unsolvable(_)) => {} + Err(UnsolvableOrCancelled::Cancelled(_)) => { + panic!("expected unsolvable, not cancelled") + } + } + } +} // ============================================================================ // Decide-queue wake-up scenarios