diff --git a/src/conflict.rs b/src/conflict.rs index e363313..0cf51ce 100644 --- a/src/conflict.rs +++ b/src/conflict.rs @@ -13,7 +13,7 @@ use petgraph::{ use crate::{ DenseIndex, DependencyProvider, Interner, Requirement, SolvableId, SolverId, StringId, - VersionSetId, + VariableId, VersionSetId, internal::{id::ClauseId, solver_id::SolvableIdOrRoot}, runtime::AsyncRuntime, solver::{Solver, clause::Clause, variable_map::VariableOrigin}, @@ -56,6 +56,72 @@ impl Conflict { let unresolved_node = graph.add_node(ConflictNode::UnresolvedDependency); let mut last_node_by_name: HashMap = HashMap::default(); + // The shared constrains encoding splits each (parent, excluded + // candidate) pair over two clauses linked by an auxiliary variable. + // Collect both sides per auxiliary variable so the original + // `parent -> candidate` edges can be reconstructed in the loop below. + let mut constrains_aux_parents: HashMap>> = + HashMap::default(); + let mut constrains_aux_candidates: HashMap< + VariableId, + Vec>, + > = HashMap::default(); + for clause_id in &self.clauses { + match state.clauses.kinds[clause_id.to_index()] { + Clause::ConstrainsParent(parent, aux, _) => { + let parent = parent + .as_solvable_or_root(&state.variable_map) + .expect("constrains parents are solvables or root"); + constrains_aux_parents.entry(aux).or_default().push(parent); + } + Clause::ConstrainsExcluded(candidate, aux, _) => { + let candidate = candidate + .as_solvable_or_root(&state.variable_map) + .expect("excluded candidates are solvables"); + constrains_aux_candidates + .entry(aux) + .or_default() + .push(candidate); + } + _ => {} + } + } + + // If only one side of a chain is part of the conflict, recover the + // other side from the assignment reason of the auxiliary variable. + let reason_clause = |aux: VariableId| { + state + .decision_tracker + .find_clause_for_assignment(aux) + .map(|clause_id| state.clauses.kinds[clause_id.to_index()]) + }; + for &aux in constrains_aux_parents.keys() { + if constrains_aux_candidates.contains_key(&aux) { + continue; + } + if let Some(Clause::ConstrainsExcluded(candidate, _, _)) = reason_clause(aux) { + let candidate = candidate + .as_solvable_or_root(&state.variable_map) + .expect("excluded candidates are solvables"); + constrains_aux_candidates.insert(aux, vec![candidate]); + } + } + for &aux in constrains_aux_candidates.keys() { + if constrains_aux_parents.contains_key(&aux) { + continue; + } + if let Some(Clause::ConstrainsParent(parent, _, _)) = reason_clause(aux) { + let parent = parent + .as_solvable_or_root(&state.variable_map) + .expect("constrains parents are solvables or root"); + constrains_aux_parents.insert(aux, vec![parent]); + } + } + + // Avoids adding the same edge once for each side of a chain. + type ConstrainsEdge = (SolvableIdOrRoot, SolvableIdOrRoot, VersionSetId); + let mut constrains_edges: HashSet> = HashSet::new(); + for clause_id in &self.clauses { let clause = &state.clauses.kinds[clause_id.to_index()]; match clause { @@ -160,6 +226,62 @@ impl Conflict { ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)), ); } + &Clause::ConstrainsParent(package_id, aux, version_set_id) => { + let package_solvable = package_id + .as_solvable_or_root(&state.variable_map) + .expect("constrains parents are solvables or root"); + + let Some(candidates) = constrains_aux_candidates.get(&aux) else { + continue; + }; + + for &dependency_solvable in candidates { + if !constrains_edges.insert(( + package_solvable, + dependency_solvable, + version_set_id, + )) { + continue; + } + + let package_node = Self::add_node(&mut graph, &mut nodes, package_solvable); + let dep_node = Self::add_node(&mut graph, &mut nodes, dependency_solvable); + + graph.add_edge( + package_node, + dep_node, + ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)), + ); + } + } + &Clause::ConstrainsExcluded(dep_id, aux, version_set_id) => { + let dependency_solvable = dep_id + .as_solvable_or_root(&state.variable_map) + .expect("excluded candidates are solvables"); + + let Some(parents) = constrains_aux_parents.get(&aux) else { + continue; + }; + + for &package_solvable in parents { + if !constrains_edges.insert(( + package_solvable, + dependency_solvable, + version_set_id, + )) { + continue; + } + + let package_node = Self::add_node(&mut graph, &mut nodes, package_solvable); + let dep_node = Self::add_node(&mut graph, &mut nodes, dependency_solvable); + + graph.add_edge( + package_node, + dep_node, + ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)), + ); + } + } Clause::AnyOf(selected, _variable) => { // Assumption: since `AnyOf` of clause can never be false, we dont add an edge // for it. diff --git a/src/solver/clause.rs b/src/solver/clause.rs index 06cefc9..5081ff2 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -81,6 +81,30 @@ pub(crate) enum Clause { /// /// In SAT terms: (¬A ∨ ¬B) Constrains(VariableId, VariableId, VersionSetId), + /// Makes the constraint's auxiliary variable turn true when a candidate + /// that is excluded by the constraint's version set is installed. + /// + /// Usage: constraints whose version set excludes many candidates share a + /// single auxiliary variable per version set. The clauses that link the + /// excluded candidates to the auxiliary variable are emitted once per + /// version set, and each (parent, version set) pair only adds a single + /// [`Clause::ConstrainsParent`] clause. Together these encode the same + /// restriction as [`Clause::Constrains`] with O(candidates + parents) + /// instead of O(candidates * parents) clauses. + /// + /// Only this implication direction is needed (the Plaisted-Greenbaum + /// one-sided form): the auxiliary variable is never decided directly, it + /// only receives a value through propagation. + /// + /// In SAT terms: (¬candidate ∨ aux) + ConstrainsExcluded(VariableId, VariableId, VersionSetId), + /// Forbids a parent solvable from being installed together with the + /// constraint's auxiliary variable, i.e. together with any candidate that + /// is excluded by the constraint's version set. See + /// [`Clause::ConstrainsExcluded`] for an overview of the encoding. + /// + /// In SAT terms: (¬parent ∨ ¬aux) + ConstrainsParent(VariableId, VariableId, VersionSetId), /// Forbids the package on the right-hand side /// /// Note that the package on the left-hand side is not part of the clause, @@ -117,6 +141,8 @@ impl Clause { matches!( self, Clause::Constrains(..) + | Clause::ConstrainsExcluded(..) + | Clause::ConstrainsParent(..) | Clause::ForbidMultipleInstances(..) | Clause::Lock(..) | Clause::AnyOf(..) @@ -218,6 +244,44 @@ impl Clause { ) } + /// Returns the building blocks needed for a new [WatchedLiterals] of the + /// [Clause::ConstrainsExcluded] kind. + fn constrains_excluded( + candidate: VariableId, + aux: VariableId, + via: VersionSetId, + ) -> (Self, Option<[Literal; 2]>) { + ( + Clause::ConstrainsExcluded(candidate, aux, via), + Some([candidate.negative(), aux.positive()]), + ) + } + + /// Returns the building blocks needed for a new [WatchedLiterals] of the + /// [Clause::ConstrainsParent] kind. See [`Clause::constrains`] for the + /// meaning of the returned values. + fn constrains_parent( + parent: VariableId, + aux: VariableId, + via: VersionSetId, + decision_tracker: &DecisionTracker, + ) -> (Self, Option<[Literal; 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 auxiliary variable is already true, an excluded candidate is + // installed, which implies the parent solvable would be false (and we + // just asserted that it is not). + let conflict = decision_tracker.assigned_value(aux) == Some(true); + + ( + Clause::ConstrainsParent(parent, aux, via), + Some([parent.negative(), aux.negative()]), + conflict, + ) + } + /// Returns the ids of the solvables that will be watched as well as the /// clause itself. fn forbid_multiple( @@ -311,6 +375,12 @@ impl Clause { Clause::Constrains(s1, s2, _) => [s1.negative(), s2.negative()] .into_iter() .try_fold(init, visit), + Clause::ConstrainsExcluded(candidate, aux, _) => [candidate.negative(), aux.positive()] + .into_iter() + .try_fold(init, visit), + Clause::ConstrainsParent(parent, aux, _) => [parent.negative(), aux.negative()] + .into_iter() + .try_fold(init, visit), Clause::ForbidMultipleInstances(s1, s2, _) => { [s1.negative(), s2].into_iter().try_fold(init, visit) } @@ -437,6 +507,38 @@ impl WatchedLiterals { ) } + /// Shorthand method to construct a [Clause::ConstrainsExcluded] without + /// requiring complicated arguments. + pub fn constrains_excluded( + candidate: VariableId, + aux: VariableId, + requirement: VersionSetId, + ) -> (Option, Clause) { + let (kind, watched_literals) = Clause::constrains_excluded(candidate, aux, requirement); + (Self::from_kind_and_initial_watches(watched_literals), kind) + } + + /// Shorthand method to construct a [Clause::ConstrainsParent] without + /// requiring complicated arguments. + /// + /// The returned boolean value is true when adding the clause resulted in a + /// conflict. + pub fn constrains_parent( + parent: VariableId, + aux: VariableId, + requirement: VersionSetId, + decision_tracker: &DecisionTracker, + ) -> (Option, bool, Clause) { + let (kind, watched_literals, conflict) = + Clause::constrains_parent(parent, aux, requirement, decision_tracker); + + ( + Self::from_kind_and_initial_watches(watched_literals), + conflict, + kind, + ) + } + pub fn lock( locked_candidate: VariableId, other_candidate: VariableId, @@ -652,6 +754,28 @@ impl Display for ClauseDisplay<'_, I> { self.interner.display_version_set(version_set_id) ) } + Clause::ConstrainsExcluded(candidate, aux, version_set_id) => { + write!( + f, + "ConstrainsExcluded({}({:?}), {}({:?}), {})", + candidate.display(self.variable_map, self.interner), + candidate, + aux.display(self.variable_map, self.interner), + aux, + self.interner.display_version_set(version_set_id) + ) + } + Clause::ConstrainsParent(parent, aux, version_set_id) => { + write!( + f, + "ConstrainsParent({}({:?}), {}({:?}), {})", + parent.display(self.variable_map, self.interner), + parent, + aux.display(self.variable_map, self.interner), + aux, + self.interner.display_version_set(version_set_id) + ) + } Clause::ForbidMultipleInstances(v1, v2, name) => { write!( f, diff --git a/src/solver/diagnostics.rs b/src/solver/diagnostics.rs index b78b60b..2d367c7 100644 --- a/src/solver/diagnostics.rs +++ b/src/solver/diagnostics.rs @@ -43,7 +43,9 @@ impl Solver { Clause::Learnt(..) => { learned_clauses += 1; } - Clause::Constrains(..) => { + Clause::Constrains(..) + | Clause::ConstrainsExcluded(..) + | Clause::ConstrainsParent(..) => { constrains_clauses += 1; } Clause::AnyOf(..) => { @@ -60,6 +62,8 @@ impl Solver { None => assertion_clauses += 1, Some(_) => match clause { Clause::Constrains(..) + | Clause::ConstrainsExcluded(..) + | Clause::ConstrainsParent(..) | Clause::ForbidMultipleInstances(..) | Clause::Lock(..) | Clause::AnyOf(..) => binary_watched += 1, diff --git a/src/solver/encoding.rs b/src/solver/encoding.rs index 4444490..cbe70e9 100644 --- a/src/solver/encoding.rs +++ b/src/solver/encoding.rs @@ -102,6 +102,12 @@ struct ConstraintCandidatesAvailable<'a, S> { candidates: &'a [S], } +/// The minimum number of non-matching candidates a constraint must have before +/// the shared auxiliary variable encoding is used (see +/// [`Encoder::on_constraint_candidates_available`]). Below this, pairwise +/// clauses need at most as many clauses and propagate in a single hop. +const CONSTRAINS_AUX_ENCODING_THRESHOLD: usize = 4; + impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { pub fn new( state: &'a mut SolverState, @@ -436,21 +442,84 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { ); let variable = self.state.variable_map.intern_solvable_or_root(solvable_id); - 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 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, + ); - if conflict { - self.conflicting_clauses.push(clause_id); + let clause_id = self.state.add_clause(watched_literals, kind); + + if conflict { + self.conflicting_clauses.push(clause_id); + } } + return; + } + + // Shared encoding: the (¬candidate ∨ aux) clauses are emitted once per + // version set, each parent only adds a single (¬parent ∨ ¬aux) clause. + let aux_variable = match self.state.constrains_aux_vars.get(&constraint) { + Some(&aux_variable) => aux_variable, + None => { + let aux_variable = self + .state + .variable_map + .alloc_constrains_violation_variable(constraint); + self.state + .constrains_aux_vars + .insert(constraint, aux_variable); + + for &forbidden_candidate in candidates { + let forbidden_candidate_var = + self.state.variable_map.intern_solvable(forbidden_candidate); + let (watched_literals, kind) = WatchedLiterals::constrains_excluded( + forbidden_candidate_var, + aux_variable, + constraint, + ); + let clause_id = self.state.add_clause(watched_literals, kind); + + // An already installed candidate must propagate + // immediately so the parent clause below observes the + // violation, just like the pairwise encoding does. + if self + .state + .decision_tracker + .assigned_value(forbidden_candidate_var) + == Some(true) + { + self.state + .decision_tracker + .try_add_decision( + Decision::new(aux_variable, true, clause_id), + self.level, + ) + .expect("a freshly allocated variable cannot be assigned false"); + } + } + + aux_variable + } + }; + + let (watched_literals, conflict, kind) = WatchedLiterals::constrains_parent( + variable, + aux_variable, + constraint, + &self.state.decision_tracker, + ); + let clause_id = self.state.add_clause(watched_literals, kind); + if conflict { + self.conflicting_clauses.push(clause_id); } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 35b213a..5de5536 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -225,6 +225,11 @@ pub(crate) struct SolverState { /// solvable for a package. at_least_one_tracker: ::Map>, + /// The auxiliary variable of the shared constrains encoding per version + /// set. The [`Clause::ConstrainsExcluded`] clauses are emitted exactly + /// once, when the variable is allocated. + constrains_aux_vars: HashMap, + pub(crate) decision_tracker: DecisionTracker, /// Activity score per package. @@ -251,6 +256,7 @@ impl Default for SolverState { clauses_added_for_solvable: Default::default(), at_most_one_trackers: Default::default(), at_least_one_tracker: Default::default(), + constrains_aux_vars: Default::default(), decision_tracker: Default::default(), name_activity: Default::default(), #[cfg(feature = "diagnostics")] @@ -303,7 +309,9 @@ impl PropagationVisitsByType { fn count(&mut self, clause: &Clause) { match clause { Clause::Requires(..) => self.requires += 1, - Clause::Constrains(..) => self.constrains += 1, + Clause::Constrains(..) + | Clause::ConstrainsExcluded(..) + | Clause::ConstrainsParent(..) => self.constrains += 1, Clause::ForbidMultipleInstances(..) => self.forbid_multiple += 1, Clause::Lock(..) => self.lock += 1, Clause::Learnt(..) => self.learnt += 1, diff --git a/src/solver/variable_map.rs b/src/solver/variable_map.rs index 5e1bd3f..9fc143f 100644 --- a/src/solver/variable_map.rs +++ b/src/solver/variable_map.rs @@ -1,7 +1,7 @@ use std::fmt::Display; use crate::{ - DenseIndex, Interner, VariableId, + DenseIndex, Interner, VariableId, VersionSetId, internal::solver_id::SolvableIdOrRoot, solver_id::{IdMap, SolverId}, }; @@ -39,6 +39,10 @@ pub(crate) enum VariableOrigin { /// A variable that indicates that any solvable of a particular package is /// part of the solution. AtLeastOne(N), + + /// A variable that indicates that a candidate excluded by a constraint's + /// version set is installed. + ConstrainsViolation(VersionSetId), } impl Default for VariableMap { @@ -110,6 +114,12 @@ impl VariableMap { self.alloc(VariableOrigin::AtLeastOne(name)) } + /// Allocate a variable that indicates that a candidate that is excluded by + /// the given constraint's version set is installed. + pub fn alloc_constrains_violation_variable(&mut self, version_set: VersionSetId) -> VariableId { + self.alloc(VariableOrigin::ConstrainsViolation(version_set)) + } + /// Returns the origin of a variable. The origin describes the semantics of /// a variable. #[inline] @@ -169,6 +179,15 @@ impl Display for VariableDisplay<'_, I> { VariableOrigin::AtLeastOne(name) => { write!(f, "any-of({})", self.interner.display_name(name)) } + VariableOrigin::ConstrainsViolation(version_set) => { + write!( + f, + "constrains-violation({} {})", + self.interner + .display_name(self.interner.version_set_name(version_set)), + self.interner.display_version_set(version_set) + ) + } } } } diff --git a/tests/solver/main.rs b/tests/solver/main.rs index e427388..d522b23 100644 --- a/tests/solver/main.rs +++ b/tests/solver/main.rs @@ -1344,6 +1344,126 @@ fn test_constrains_transitive() { "###); } +/// The shared auxiliary-variable encoding emits the excluded candidates of a +/// constraint only once: N parents sharing a constraint over a package with M +/// excluded candidates produce M + N constrains clauses instead of N * M. +#[test] +fn test_constrains_shared_encoding_clause_count() { + let solve_and_count = |parents: usize| { + let mut provider = BundleBoxProvider::new(); + // All 10 versions of pkg are excluded, enough for the shared encoding. + for v in 1..=10u32 { + provider.add_package("pkg", v.into(), &[], &[]); + } + let parent_names = (0..parents).map(|i| format!("p{i}")).collect::>(); + for name in &parent_names { + provider.add_package(name, 1.into(), &[], &["pkg 11..100"]); + } + let requirements = + provider.requirements(&parent_names.iter().map(String::as_str).collect::>()); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + solver + .solve(problem) + .expect("nothing requires pkg, so the constraints are never violated"); + solver.clause_count() + }; + + // Each additional parent adds one requires clause and one parent clause; + // the 10 excluded-candidate clauses are emitted only once. + let single_parent = solve_and_count(1); + let many_parents = solve_and_count(5); + assert_eq!(many_parents - single_parent, 4 * 2); +} + +/// Constraints that exclude only a few candidates keep the direct pairwise +/// encoding: every parent emits one clause per excluded candidate. +#[test] +fn test_constrains_pairwise_encoding_clause_count() { + let solve_and_count = |parents: usize| { + let mut provider = BundleBoxProvider::new(); + // Only 2 versions of pkg are excluded, too few for the shared encoding. + provider.add_package("pkg", 1.into(), &[], &[]); + provider.add_package("pkg", 2.into(), &[], &[]); + let parent_names = (0..parents).map(|i| format!("p{i}")).collect::>(); + for name in &parent_names { + provider.add_package(name, 1.into(), &[], &["pkg 11..100"]); + } + let requirements = + provider.requirements(&parent_names.iter().map(String::as_str).collect::>()); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + solver + .solve(problem) + .expect("nothing requires pkg, so the constraints are never violated"); + solver.clause_count() + }; + + // Each additional parent adds one requires clause and one pairwise clause + // per excluded candidate. + let single_parent = solve_and_count(1); + let many_parents = solve_and_count(5); + assert_eq!(many_parents - single_parent, 4 * 3); +} + +/// Like `test_unsat_constrains`, but with enough excluded candidates for the +/// constraint to use the shared auxiliary-variable encoding. The rendered +/// conflict must look exactly as if the constraint was encoded pairwise. +#[test] +fn test_unsat_constrains_shared_encoding() { + let mut provider = BundleBoxProvider::from_packages(&[ + ("a", 10, vec!["b 50..100"]), + ("b", 55, vec![]), + ("b", 54, vec![]), + ("b", 53, vec![]), + ("b", 52, vec![]), + ("b", 51, vec![]), + ("b", 50, vec![]), + ("b", 42, vec![]), + ]); + + provider.add_package("c", 10.into(), &[], &["b 0..50"]); + let error = solve_unsat(provider, &["a", "c"]); + insta::assert_snapshot!(error); +} + +/// Reverse direction through the shared encoding: an installed candidate that +/// is excluded by the constraint forbids the constraint's parent. +#[test] +fn test_unsat_constrains_shared_encoding_reverse() { + // x forces b=1, while a constrains b to [5,100) which excludes b=1..4. + let mut provider = BundleBoxProvider::from_packages(&[ + ("x", 1, vec!["b 1..2"]), + ("b", 1, vec![]), + ("b", 2, vec![]), + ("b", 3, vec![]), + ("b", 4, vec![]), + ]); + provider.add_package("a", 1.into(), &[], &["b 5..100"]); + let error = solve_unsat(provider, &["x", "a"]); + insta::assert_snapshot!(error); +} + +/// Multiple parents sharing the same constraint through the shared encoding. +#[test] +fn test_unsat_constrains_shared_encoding_multiple_parents() { + let mut provider = BundleBoxProvider::from_packages(&[ + ("a", 10, vec!["b 50..100"]), + ("b", 55, vec![]), + ("b", 54, vec![]), + ("b", 53, vec![]), + ("b", 52, vec![]), + ("b", 51, vec![]), + ("b", 50, vec![]), + ("b", 42, vec![]), + ]); + + provider.add_package("c", 10.into(), &[], &["b 0..50"]); + provider.add_package("d", 10.into(), &[], &["b 0..50"]); + let error = solve_unsat(provider, &["a", "c", "d"]); + insta::assert_snapshot!(error); +} + /// Multiple constraints from different parents on the same package. #[test] fn test_constrains_multiple_parents() { diff --git a/tests/solver/snapshots/solver__unsat_constrains_shared_encoding.snap b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding.snap new file mode 100644 index 0000000..5d20b83 --- /dev/null +++ b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding.snap @@ -0,0 +1,13 @@ +--- +source: tests/solver/main.rs +assertion_line: 1385 +expression: error +--- +The following packages are incompatible +├─ a * can be installed with any of the following options: +│ └─ a 10 would require +│ └─ b >=50, <100, which can be installed with any of the following options: +│ └─ b 50 | 51 | 52 | 53 | 54 | 55 +└─ c * cannot be installed because there are no viable options: + └─ c 10 would constrain + └─ b >=0, <50, which conflicts with any installable versions previously reported diff --git a/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_multiple_parents.snap b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_multiple_parents.snap new file mode 100644 index 0000000..d5bbb8c --- /dev/null +++ b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_multiple_parents.snap @@ -0,0 +1,13 @@ +--- +source: tests/solver/main.rs +assertion_line: 1423 +expression: error +--- +The following packages are incompatible +├─ a * can be installed with any of the following options: +│ └─ a 10 would require +│ └─ b >=50, <100, which can be installed with any of the following options: +│ └─ b 50 | 51 | 52 | 53 | 54 | 55 +└─ c * cannot be installed because there are no viable options: + └─ c 10 would constrain + └─ b >=0, <50, which conflicts with any installable versions previously reported diff --git a/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_reverse.snap b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_reverse.snap new file mode 100644 index 0000000..2114a04 --- /dev/null +++ b/tests/solver/snapshots/solver__unsat_constrains_shared_encoding_reverse.snap @@ -0,0 +1,13 @@ +--- +source: tests/solver/main.rs +assertion_line: 1403 +expression: error +--- +The following packages are incompatible +├─ x * can be installed with any of the following options: +│ └─ x 1 would require +│ └─ b >=1, <2, which can be installed with any of the following options: +│ └─ b 1 +└─ a * cannot be installed because there are no viable options: + └─ a 1 would constrain + └─ b >=5, <100, which conflicts with any installable versions previously reported