Fix assertion failure when a package constrains itself

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<Box<dyn Any>> {
         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

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<D: DependencyProvider>(
 pub(crate) struct Encoder<'a, 'cache, D: DependencyProvider> {
     state: &'a mut SolverState<D>,
     cache: &'cache SolverCache<D>,
+    config: &'a SolverConfig,
     level: u32,
 
     /// The dependencies of the root solvable.
@@ -192,13 +197,15 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> {
     pub fn new(
         state: &'a mut SolverState<D>,
         cache: &'cache SolverCache<D>,
+        config: &'a SolverConfig,
         root_dependencies: &'cache Dependencies,
         level: u32,
         future_queue_mode: FutureQueueMode,
     ) -> Self {
         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<D::SolvableId>,
+        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

src/solver/mod.rs

@@ -176,6 +176,23 @@ impl<N> Clauses<N> {
 
 type RequirementCandidateVariables = Vec<Vec<VariableId>>;
 
+/// 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<D: DependencyProvider, RT: AsyncRuntime = NowOrNeverRuntime> {
     /// The runtime to use for async operations.
@@ -191,6 +208,9 @@ pub struct Solver<D: DependencyProvider, RT: AsyncRuntime = NowOrNeverRuntime> {
     /// 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<D: DependencyProvider> Solver<D, NowOrNeverRuntime> {
     /// 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<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             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<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         }
     }
 
+    /// 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<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                     Encoder::new(
                         &mut self.state,
                         &self.cache,
+                        &self.config,
                         root_deps,
                         level,
                         self.future_queue_mode,
@@ -804,6 +834,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 Encoder::new(
                     &mut self.state,
                     &self.cache,
+                    &self.config,
                     root_deps,
                     level,
                     self.future_queue_mode,