diff --git a/cpp/include/resolvo.h b/cpp/include/resolvo.h index 48844d6..97d00f5 100644 --- a/cpp/include/resolvo.h +++ b/cpp/include/resolvo.h @@ -4,6 +4,7 @@ #include "resolvo_internal.h" namespace resolvo { +using cbindgen_private::Problem; using cbindgen_private::Requirement; /** @@ -30,8 +31,8 @@ inline Requirement requirement_union(VersionSetUnionId id) { * stored in `result`. If the solve was unsuccesfull an error describing the reason is returned and * the result vector will be empty. */ -inline String solve(DependencyProvider &provider, Slice requirements, - Slice constraints, Vector &result) { +inline String solve(DependencyProvider &provider, const Problem &problem, + Vector &result) { cbindgen_private::DependencyProvider bridge{ static_cast(&provider), private_api::bridge_display_solvable, @@ -50,7 +51,7 @@ inline String solve(DependencyProvider &provider, Slice requirement }; String error; - cbindgen_private::resolvo_solve(&bridge, requirements, constraints, &error, &result); + cbindgen_private::resolvo_solve(&bridge, &problem, &error, &result); return error; } } // namespace resolvo diff --git a/cpp/src/lib.rs b/cpp/src/lib.rs index 4aa9998..a0ab2ac 100644 --- a/cpp/src/lib.rs +++ b/cpp/src/lib.rs @@ -473,28 +473,45 @@ impl<'d> resolvo::DependencyProvider for &'d DependencyProvider { } } +#[repr(C)] +pub struct Problem<'a> { + pub requirements: Slice<'a, Requirement>, + pub constraints: Slice<'a, VersionSetId>, + pub soft_requirements: Slice<'a, SolvableId>, +} + #[no_mangle] #[allow(unused)] pub extern "C" fn resolvo_solve( provider: &DependencyProvider, - requirements: Slice, - constraints: Slice, + problem: &Problem, error: &mut String, result: &mut Vector, ) -> bool { - let requirements = requirements - .into_iter() - .copied() - .map(Into::into) - .collect::>(); - let constraints = constraints - .into_iter() - .copied() - .map(Into::into) - .collect::>(); - let mut solver = resolvo::Solver::new(provider); - match solver.solve(requirements, constraints) { + + let problem = resolvo::Problem { + requirements: problem + .requirements + .into_iter() + .copied() + .map(Into::into) + .collect(), + constraints: problem + .constraints + .into_iter() + .copied() + .map(Into::into) + .collect(), + soft_requirements: problem + .soft_requirements + .into_iter() + .copied() + .map(Into::into) + .collect(), + }; + + match solver.solve(problem) { Ok(solution) => { *result = solution.into_iter().map(Into::into).collect(); true diff --git a/cpp/tests/solve.cpp b/cpp/tests/solve.cpp index 13a05fa..1bb02b7 100644 --- a/cpp/tests/solve.cpp +++ b/cpp/tests/solve.cpp @@ -216,19 +216,27 @@ SCENARIO("Solve") { auto c_1 = db.alloc_candidate("c", 1, {}); + const auto d_1 = db.alloc_candidate("d", 1, {}); + // Construct a problem to be solved by the solver resolvo::Vector requirements = {db.alloc_requirement("a", 1, 3)}; - resolvo::Vector constraints = {db.alloc_version_set("b", 1, 3), - db.alloc_version_set("c", 1, 3)}; + resolvo::Vector constraints = { + db.alloc_version_set("b", 1, 3), + db.alloc_version_set("c", 1, 3), + db.alloc_version_set("d", 2, 2), + }; + resolvo::Vector soft_requirements{c_1, d_1}; // Solve the problem resolvo::Vector result; - resolvo::solve(db, requirements, constraints, result); + resolvo::Problem problem = {requirements, constraints, soft_requirements}; + resolvo::solve(db, problem, result); // Check the result - REQUIRE(result.size() == 2); + REQUIRE(result.size() == 3); REQUIRE(result[0] == a_2); REQUIRE(result[1] == b_2); + REQUIRE(result[2] == c_1); } SCENARIO("Solve Union") { @@ -264,7 +272,9 @@ SCENARIO("Solve Union") { // Solve the problem resolvo::Vector result; - resolvo::solve(db, requirements, constraints, result); + resolvo::Problem problem = {requirements, constraints, {}}; + resolvo::solve(db, problem, result); + ; // Check the result REQUIRE(result.size() == 4); diff --git a/src/problem.rs b/src/conflict.rs similarity index 88% rename from src/problem.rs rename to src/conflict.rs index 3033244..5996dbe 100644 --- a/src/problem.rs +++ b/src/conflict.rs @@ -20,12 +20,12 @@ use crate::{ /// Represents the cause of the solver being unable to find a solution #[derive(Debug)] -pub struct Problem { +pub struct Conflict { /// The clauses involved in an unsatisfiable conflict clauses: Vec, } -impl Problem { +impl Conflict { pub(crate) fn default() -> Self { Self { clauses: Vec::new(), @@ -38,18 +38,18 @@ impl Problem { } } - /// Generates a graph representation of the problem (see [`ProblemGraph`] + /// Generates a graph representation of the conflict (see [`ConflictGraph`] /// for details) pub fn graph( &self, solver: &Solver, - ) -> ProblemGraph { - let mut graph = DiGraph::::default(); + ) -> ConflictGraph { + let mut graph = DiGraph::::default(); let mut nodes: HashMap = HashMap::default(); let mut excluded_nodes: HashMap = HashMap::default(); let root_node = Self::add_node(&mut graph, &mut nodes, InternalSolvableId::root()); - let unresolved_node = graph.add_node(ProblemNode::UnresolvedDependency); + let unresolved_node = graph.add_node(ConflictNode::UnresolvedDependency); for clause_id in &self.clauses { let clause = &solver.clauses.borrow()[*clause_id].kind; @@ -60,12 +60,12 @@ impl Problem { let package_node = Self::add_node(&mut graph, &mut nodes, *solvable); let excluded_node = excluded_nodes .entry(*reason) - .or_insert_with(|| graph.add_node(ProblemNode::Excluded(*reason))); + .or_insert_with(|| graph.add_node(ConflictNode::Excluded(*reason))); graph.add_edge( package_node, *excluded_node, - ProblemEdge::Conflict(ConflictCause::Excluded), + ConflictEdge::Conflict(ConflictCause::Excluded), ); } Clause::Learnt(..) => unreachable!(), @@ -82,7 +82,7 @@ impl Problem { graph.add_edge( package_node, unresolved_node, - ProblemEdge::Requires(version_set_id), + ConflictEdge::Requires(version_set_id), ); } else { for &candidate_id in candidates { @@ -93,7 +93,7 @@ impl Problem { graph.add_edge( package_node, candidate_node, - ProblemEdge::Requires(version_set_id), + ConflictEdge::Requires(version_set_id), ); } } @@ -101,14 +101,14 @@ impl Problem { &Clause::Lock(locked, forbidden) => { let node2_id = Self::add_node(&mut graph, &mut nodes, forbidden); let conflict = ConflictCause::Locked(locked); - graph.add_edge(root_node, node2_id, ProblemEdge::Conflict(conflict)); + graph.add_edge(root_node, node2_id, ConflictEdge::Conflict(conflict)); } &Clause::ForbidMultipleInstances(instance1_id, instance2_id, _) => { let node1_id = Self::add_node(&mut graph, &mut nodes, instance1_id); let node2_id = Self::add_node(&mut graph, &mut nodes, instance2_id); let conflict = ConflictCause::ForbidMultipleInstances; - graph.add_edge(node1_id, node2_id, ProblemEdge::Conflict(conflict)); + graph.add_edge(node1_id, node2_id, ConflictEdge::Conflict(conflict)); } &Clause::Constrains(package_id, dep_id, version_set_id) => { let package_node = Self::add_node(&mut graph, &mut nodes, package_id); @@ -117,7 +117,7 @@ impl Problem { graph.add_edge( package_node, dep_node, - ProblemEdge::Conflict(ConflictCause::Constrains(version_set_id)), + ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)), ); } } @@ -142,7 +142,7 @@ impl Problem { } assert_eq!(graph.node_count(), visited_nodes.len()); - ProblemGraph { + ConflictGraph { graph, root_node, unresolved_node, @@ -150,16 +150,16 @@ impl Problem { } fn add_node( - graph: &mut DiGraph, + graph: &mut DiGraph, nodes: &mut HashMap, solvable_id: InternalSolvableId, ) -> NodeIndex { *nodes .entry(solvable_id) - .or_insert_with(|| graph.add_node(ProblemNode::Solvable(solvable_id))) + .or_insert_with(|| graph.add_node(ConflictNode::Solvable(solvable_id))) } - /// Display a user-friendly error explaining the problem + /// Display a user-friendly error explaining the conflict pub fn display_user_friendly<'a, D: DependencyProvider, RT: AsyncRuntime>( &self, solver: &'a Solver, @@ -169,9 +169,9 @@ impl Problem { } } -/// A node in the graph representation of a [`Problem`] +/// A node in the graph representation of a [`Conflict`] #[derive(Copy, Clone, Eq, PartialEq)] -pub(crate) enum ProblemNode { +pub(crate) enum ConflictNode { /// Node corresponding to a solvable Solvable(InternalSolvableId), /// Node representing a dependency without candidates @@ -180,23 +180,23 @@ pub(crate) enum ProblemNode { Excluded(StringId), } -impl ProblemNode { +impl ConflictNode { fn solvable_id(self) -> InternalSolvableId { match self { - ProblemNode::Solvable(solvable_id) => solvable_id, - ProblemNode::UnresolvedDependency => { + ConflictNode::Solvable(solvable_id) => solvable_id, + ConflictNode::UnresolvedDependency => { panic!("expected solvable node, found unresolved dependency") } - ProblemNode::Excluded(_) => { + ConflictNode::Excluded(_) => { panic!("expected solvable node, found excluded node") } } } } -/// An edge in the graph representation of a [`Problem`] +/// An edge in the graph representation of a [`Conflict`] #[derive(Copy, Clone, Hash, Eq, PartialEq, Ord, PartialOrd)] -pub(crate) enum ProblemEdge { +pub(crate) enum ConflictEdge { /// The target node is a candidate for the dependency specified by the /// [`Requirement`] Requires(Requirement), @@ -204,18 +204,18 @@ pub(crate) enum ProblemEdge { Conflict(ConflictCause), } -impl ProblemEdge { +impl ConflictEdge { fn try_requires(self) -> Option { match self { - ProblemEdge::Requires(match_spec_id) => Some(match_spec_id), - ProblemEdge::Conflict(_) => None, + ConflictEdge::Requires(match_spec_id) => Some(match_spec_id), + ConflictEdge::Conflict(_) => None, } } fn requires(self) -> Requirement { match self { - ProblemEdge::Requires(match_spec_id) => match_spec_id, - ProblemEdge::Conflict(_) => panic!("expected requires edge, found conflict"), + ConflictEdge::Requires(match_spec_id) => match_spec_id, + ConflictEdge::Conflict(_) => panic!("expected requires edge, found conflict"), } } } @@ -241,22 +241,22 @@ pub(crate) enum ConflictCause { /// - They all have the same name /// - They all have the same predecessor nodes /// - They all have the same successor nodes -pub(crate) struct MergedProblemNode { +pub(crate) struct MergedConflictNode { pub ids: Vec, } -/// Graph representation of [`Problem`] +/// Graph representation of [`Conflict`] /// /// The root of the graph is the "root solvable". Note that not all the /// solvable's requirements are included in the graph, only those that are /// directly or indirectly involved in the conflict. -pub struct ProblemGraph { - graph: DiGraph, +pub struct ConflictGraph { + graph: DiGraph, root_node: NodeIndex, unresolved_node: Option, } -impl ProblemGraph { +impl ConflictGraph { /// Writes a graphviz graph that represents this instance to the specified /// output. pub fn graphviz( @@ -276,7 +276,7 @@ impl ProblemGraph { write!(f, "digraph {{")?; for nx in graph.node_indices() { let id = match graph.node_weight(nx).as_ref().unwrap() { - ProblemNode::Solvable(id) => *id, + ConflictNode::Solvable(id) => *id, _ => continue, }; @@ -294,26 +294,28 @@ impl ProblemGraph { let target = *graph.node_weight(edge.target()).unwrap(); let color = match edge.weight() { - ProblemEdge::Requires(_) if target != ProblemNode::UnresolvedDependency => { + ConflictEdge::Requires(_) if target != ConflictNode::UnresolvedDependency => { "black" } _ => "red", }; let label = match edge.weight() { - ProblemEdge::Requires(requirement) => requirement.display(interner).to_string(), - ProblemEdge::Conflict(ConflictCause::Constrains(version_set_id)) => { + ConflictEdge::Requires(requirement) => { + requirement.display(interner).to_string() + } + ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)) => { interner.display_version_set(*version_set_id).to_string() } - ProblemEdge::Conflict(ConflictCause::ForbidMultipleInstances) - | ProblemEdge::Conflict(ConflictCause::Locked(_)) => { + ConflictEdge::Conflict(ConflictCause::ForbidMultipleInstances) + | ConflictEdge::Conflict(ConflictCause::Locked(_)) => { "already installed".to_string() } - ProblemEdge::Conflict(ConflictCause::Excluded) => "excluded".to_string(), + ConflictEdge::Conflict(ConflictCause::Excluded) => "excluded".to_string(), }; let target = match target { - ProblemNode::Solvable(mut solvable_2) => { + ConflictNode::Solvable(mut solvable_2) => { // If the target node has been merged, replace it by the first id in the // group if let Some(solvable_id) = solvable_2.as_solvable() { @@ -329,8 +331,8 @@ impl ProblemGraph { solvable_2.display(interner).to_string() } - ProblemNode::UnresolvedDependency => "unresolved".to_string(), - ProblemNode::Excluded(reason) => { + ConflictNode::UnresolvedDependency => "unresolved".to_string(), + ConflictNode::Excluded(reason) => { format!("reason: {}", interner.display_string(reason)) } }; @@ -348,15 +350,15 @@ impl ProblemGraph { /// Simplifies and collapses nodes so that these can be considered the same /// candidate - fn simplify(&self, interner: &impl Interner) -> HashMap> { + fn simplify(&self, interner: &impl Interner) -> HashMap> { let graph = &self.graph; // Gather information about nodes that can be merged let mut maybe_merge = HashMap::default(); for node_id in graph.node_indices() { let candidate = match graph[node_id] { - ProblemNode::UnresolvedDependency | ProblemNode::Excluded(_) => continue, - ProblemNode::Solvable(solvable_id) => { + ConflictNode::UnresolvedDependency | ConflictNode::Excluded(_) => continue, + ConflictNode::Solvable(solvable_id) => { if solvable_id.is_root() { continue; } else { @@ -395,7 +397,7 @@ impl ProblemGraph { let mut merged_candidates = HashMap::default(); for m in maybe_merge.into_values() { if m.len() > 1 { - let m = Rc::new(MergedProblemNode { + let m = Rc::new(MergedConflictNode { ids: m.into_iter().map(|(_, snd)| snd).collect(), }); for &id in &m.ids { @@ -427,7 +429,7 @@ impl ProblemGraph { let excluding_edges = self .graph .edges_directed(nx, Direction::Incoming) - .any(|e| matches!(e.weight(), ProblemEdge::Conflict(ConflictCause::Excluded))); + .any(|e| matches!(e.weight(), ConflictEdge::Conflict(ConflictCause::Excluded))); if excluding_edges { // Nodes with incoming disabling edges aren't installable continue; @@ -436,7 +438,7 @@ impl ProblemGraph { let outgoing_conflicts = self .graph .edges_directed(nx, Direction::Outgoing) - .any(|e| matches!(e.weight(), ProblemEdge::Conflict(_))); + .any(|e| matches!(e.weight(), ConflictEdge::Conflict(_))); if outgoing_conflicts { // Nodes with outgoing conflicts aren't installable continue; @@ -447,8 +449,8 @@ impl ProblemGraph { .graph .edges_directed(nx, Direction::Outgoing) .map(|e| match e.weight() { - ProblemEdge::Requires(version_set_id) => (version_set_id, e.target()), - ProblemEdge::Conflict(_) => unreachable!(), + ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()), + ConflictEdge::Conflict(_) => unreachable!(), }) .chunk_by(|(&version_set_id, _)| version_set_id); @@ -482,7 +484,7 @@ impl ProblemGraph { let outgoing_conflicts = self .graph .edges_directed(nx, Direction::Outgoing) - .any(|e| matches!(e.weight(), ProblemEdge::Conflict(_))); + .any(|e| matches!(e.weight(), ConflictEdge::Conflict(_))); if outgoing_conflicts { // Nodes with outgoing conflicts aren't missing continue; @@ -493,8 +495,8 @@ impl ProblemGraph { .graph .edges_directed(nx, Direction::Outgoing) .map(|e| match e.weight() { - ProblemEdge::Requires(version_set_id) => (version_set_id, e.target()), - ProblemEdge::Conflict(_) => unreachable!(), + ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()), + ConflictEdge::Conflict(_) => unreachable!(), }) .chunk_by(|(&version_set_id, _)| version_set_id); @@ -620,17 +622,17 @@ mod tests { } /// A struct implementing [`fmt::Display`] that generates a user-friendly -/// representation of a problem graph +/// representation of a conflict graph pub struct DisplayUnsat<'i, I: Interner> { - graph: ProblemGraph, - merged_candidates: HashMap>, + graph: ConflictGraph, + merged_candidates: HashMap>, installable_set: HashSet, missing_set: HashSet, interner: &'i I, } impl<'i, I: Interner> DisplayUnsat<'i, I> { - pub(crate) fn new(graph: ProblemGraph, interner: &'i I) -> Self { + pub(crate) fn new(graph: ConflictGraph, interner: &'i I) -> Self { let merged_candidates = graph.simplify(interner); let installable_set = graph.get_installable_set(); let missing_set = graph.get_missing_set(); @@ -647,7 +649,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { fn fmt_graph( &self, f: &mut Formatter<'_>, - top_level_edges: &[EdgeReference<'_, ProblemEdge>], + top_level_edges: &[EdgeReference<'_, ConflictEdge>], top_level_indent: bool, ) -> fmt::Result { pub enum DisplayOp { @@ -705,7 +707,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let target_nx = graph.edge_endpoints(edges[0]).unwrap().1; let missing = - edges.len() == 1 && graph[target_nx] == ProblemNode::UnresolvedDependency; + edges.len() == 1 && graph[target_nx] == ConflictNode::UnresolvedDependency; if missing { // No candidates for requirement if top_level { @@ -845,8 +847,8 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let excluded = graph .edges_directed(candidate, Direction::Outgoing) .find_map(|e| match e.weight() { - ProblemEdge::Conflict(ConflictCause::Excluded) => { - let ProblemNode::Excluded(reason) = graph[e.target()] else { + ConflictEdge::Conflict(ConflictCause::Excluded) => { + let ConflictNode::Excluded(reason) = graph[e.target()] else { unreachable!(); }; Some(reason) @@ -854,12 +856,13 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { _ => None, }); let already_installed = graph.edges(candidate).any(|e| { - e.weight() == &ProblemEdge::Conflict(ConflictCause::ForbidMultipleInstances) + e.weight() + == &ConflictEdge::Conflict(ConflictCause::ForbidMultipleInstances) }); let constrains_conflict = graph.edges(candidate).any(|e| { matches!( e.weight(), - ProblemEdge::Conflict(ConflictCause::Constrains(_)) + ConflictEdge::Conflict(ConflictCause::Constrains(_)) ) }); let is_leaf = graph.edges(candidate).next().is_none(); @@ -881,7 +884,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let mut version_sets = graph .edges(candidate) .flat_map(|e| match e.weight() { - ProblemEdge::Conflict(ConflictCause::Constrains( + ConflictEdge::Conflict(ConflictCause::Constrains( version_set_id, )) => Some(version_set_id), _ => None, @@ -972,8 +975,8 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> { let indent = indenter.get_indent(); let conflict = match e.weight() { - ProblemEdge::Requires(_) => continue, - ProblemEdge::Conflict(conflict) => conflict, + ConflictEdge::Requires(_) => continue, + ConflictEdge::Conflict(conflict) => conflict, }; // The only possible conflict at the root level is a Locked conflict diff --git a/src/lib.rs b/src/lib.rs index 5ca2ba1..ece1a5e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -10,8 +10,8 @@ #![deny(missing_docs)] +pub mod conflict; pub(crate) mod internal; -pub mod problem; mod requirement; pub mod runtime; pub mod snapshot; @@ -29,7 +29,7 @@ pub use internal::{ }; use itertools::Itertools; pub use requirement::Requirement; -pub use solver::{Solver, SolverCache, UnsolvableOrCancelled}; +pub use solver::{Problem, Solver, SolverCache, UnsolvableOrCancelled}; /// An object that is used by the solver to query certain properties of /// different internalized objects. diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs index 080061a..abbfd12 100644 --- a/src/solver/decision_tracker.rs +++ b/src/solver/decision_tracker.rs @@ -27,10 +27,6 @@ impl DecisionTracker { self.propagate_index = 0; } - pub(crate) fn is_empty(&self) -> bool { - self.stack.is_empty() - } - pub(crate) fn assigned_value(&self, solvable_id: InternalSolvableId) -> Option { self.map.value(solvable_id) } @@ -77,6 +73,11 @@ impl DecisionTracker { } pub(crate) fn undo_until(&mut self, level: u32) { + if level == 0 { + self.clear(); + return; + } + while let Some(decision) = self.stack.last() { if self.level(decision.solvable_id) <= level { break; diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 45205cc..66bed80 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -9,12 +9,12 @@ use std::{any::Any, cell::RefCell, collections::HashSet, future::ready, ops::Con use watch_map::WatchMap; use crate::{ + conflict::Conflict, internal::{ arena::Arena, id::{ClauseId, InternalSolvableId, LearntClauseId, NameId, SolvableId}, mapping::Mapping, }, - problem::Problem, runtime::{AsyncRuntime, NowOrNeverRuntime}, Candidates, Dependencies, DependencyProvider, KnownDependencies, Requirement, VersionSetId, }; @@ -34,7 +34,30 @@ struct AddClauseOutput { clauses_to_watch: Vec, } -/// Drives the SAT solving process +/// Describes the problem that is to be solved by the solver. +#[derive(Default)] +pub struct Problem { + /// The requirements that _must_ have one candidate solvable be included in the + /// solution. + pub requirements: Vec, + + /// Additional constraints imposed on individual packages that the solvable (if any) + /// chosen for that package _must_ adhere to. + pub constraints: Vec, + + /// A set of additional requirements that the solver should _try_ and fulfill once it has + /// found a solution to the main problem. + /// + /// An unsatisfiable soft requirement does not cause a conflict; the solver will try + /// and fulfill as many soft requirements as possible and skip the unsatisfiable ones. + /// + /// Soft requirements are currently only specified as individual solvables to be + /// included in the solution, however in the future they will be able to be specified + /// as version sets. + pub soft_requirements: Vec, +} + +/// Drives the SAT solving process. pub struct Solver { pub(crate) async_runtime: RT, pub(crate) cache: SolverCache, @@ -88,13 +111,13 @@ impl Solver { #[derive(Debug)] pub enum UnsolvableOrCancelled { /// The problem was unsolvable. - Unsolvable(Problem), + Unsolvable(Conflict), /// The solving process was cancelled. Cancelled(Box), } -impl From for UnsolvableOrCancelled { - fn from(value: Problem) -> Self { +impl From for UnsolvableOrCancelled { + fn from(value: Conflict) -> Self { UnsolvableOrCancelled::Unsolvable(value) } } @@ -155,57 +178,70 @@ impl Solver { } } - /// Solves for the provided `root_requirements` and `root_constraints`. The - /// `root_requirements` are package that will be included in the - /// solution. `root_constraints` are additional constrains which do not - /// necesarily need to be included in the solution. + /// Solves the given [`Problem`]. /// - /// Returns a [`Problem`] if no solution was found, which provides ways to - /// inspect the causes and report them to the user. - pub fn solve( - &mut self, - root_requirements: Vec, - root_constraints: Vec, - ) -> Result, UnsolvableOrCancelled> { - // Clear state + /// The solver first solves for the root requirements and constraints, and then + /// tries to include in the solution as many of the soft requirements as it can. + /// Each soft requirement is subject to all the clauses and decisions introduced + /// for all the previously decided solvables in the solution. + /// + /// Unless the corresponding package has been requested by a version set in another + /// solvable's clauses, each soft requirement is _not_ subject to the + /// package-level clauses introduced in [`DependencyProvider::get_candidates`] since the + /// solvables have been requested specifically (not through a version set) in the solution. + /// + /// # Returns + /// + /// If a solution was found, returns a [`Vec`] of the solvables included in the solution. + /// + /// If no solution to the _root_ requirements and constraints was found, returns a + /// [`Conflict`] wrapped in a [`UnsolvableOrCancelled::Unsolvable`], which provides ways to + /// inspect the causes and report them to the user. If a soft requirement is unsolvable, + /// it is simply not included in the solution. + /// + /// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]), + /// returns an [`UnsolvableOrCancelled::Cancelled`] containing the cancellation value. + pub fn solve(&mut self, problem: Problem) -> Result, UnsolvableOrCancelled> { self.decision_tracker.clear(); self.negative_assertions.clear(); self.learnt_clauses.clear(); self.learnt_why = Mapping::new(); self.clauses = Default::default(); - self.root_requirements = root_requirements; - self.root_constraints = root_constraints; + self.root_requirements = problem.requirements; + self.root_constraints = problem.constraints; // The first clause will always be the install root clause. Here we verify that // this is indeed the case. let root_clause = self.clauses.borrow_mut().alloc(ClauseState::root()); assert_eq!(root_clause, ClauseId::install_root()); - // Run SAT - self.run_sat()?; + assert!( + self.run_sat(InternalSolvableId::root())?, + "bug: Since root is the first requested solvable, \ + should have returned Err instead of Ok(false) if root is unsolvable" + ); - let steps: Vec = self - .decision_tracker - .stack() - .filter_map(|d| { - if d.value { - d.solvable_id.as_solvable() - } else { - // Ignore things that are set to false - None - } - }) - .collect(); + for additional in problem.soft_requirements { + let additional = additional.into(); - tracing::trace!("Solvables found:"); - for step in &steps { - tracing::trace!( - " - {}", - InternalSolvableId::from(*step).display(self.provider()) - ); + if self.decision_tracker.assigned_value(additional).is_none() { + self.run_sat(additional)?; + } } - Ok(steps) + Ok(self.chosen_solvables().collect()) + } + + /// Returns the solvables that the solver has chosen to include in the solution so far. + fn chosen_solvables(&self) -> impl Iterator + '_ { + self.decision_tracker.stack().filter_map(|d| { + if d.value { + d.solvable_id.as_solvable() + } else { + // Ignore things that are set to false + None + } + }) } /// Adds clauses for a solvable. These clauses include requirements and @@ -410,15 +446,6 @@ impl Solver { let locked_solvable_id = package_candidates.locked; let candidates = &package_candidates.candidates; - // Check the assumption that no decision has been made about any of the - // solvables. - for &candidate in candidates { - debug_assert!( - self.decision_tracker.assigned_value(candidate.into()).is_none(), - "a decision has been made about a candidate of a package that was not properly added yet." - ); - } - // Each candidate gets a clause to disallow other candidates. for (i, &candidate) in candidates.iter().enumerate() { for &other_candidate in &candidates[i + 1..] { @@ -581,32 +608,49 @@ impl Solver { /// implementation of this step. /// /// The solver loop can be found in [`Solver::resolve_dependencies`]. - fn run_sat(&mut self) -> Result<(), UnsolvableOrCancelled> { - assert!(self.decision_tracker.is_empty()); - let mut level = 0; + /// + /// Returns `Ok(true)` if a solution was found for `solvable`. If a solution was not + /// found, returns `Ok(false)` if some decisions have already been made by the solver + /// (i.e. the decision tracker stack is not empty). Otherwise, returns + /// [`UnsolvableOrCancelled::Unsolvable`] as an `Err` on no solution. + /// + /// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]), + /// returns [`UnsolvableOrCancelled::Cancelled`] as an `Err`. + fn run_sat(&mut self, solvable: InternalSolvableId) -> Result { + let starting_level = self + .decision_tracker + .stack() + .next_back() + .map(|decision| self.decision_tracker.level(decision.solvable_id)) + .unwrap_or(0); + + let mut level = starting_level; loop { - if level == 0 { - tracing::trace!("Level 0: Resetting the decision loop"); + if level == starting_level { + tracing::trace!("Level {starting_level}: Resetting the decision loop"); } else { tracing::trace!("Level {}: Starting the decision loop", level); } - // 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; + // A level of starting_level means the decision loop has been completely reset + // because a partial solution was invalidated by newly added clauses. + if level == starting_level { + // Level starting_level + 1 is the initial decision level + level = starting_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 // solution that satisfies the user requirements. - tracing::trace!("╤══ Install at level {level}",); + tracing::trace!( + "╤══ Install {} at level {level}", + solvable.display(self.provider()) + ); self.decision_tracker .try_add_decision( - Decision::new(InternalSolvableId::root(), true, ClauseId::install_root()), + Decision::new(solvable, true, ClauseId::install_root()), level, ) .expect("already decided"); @@ -614,12 +658,9 @@ impl Solver { // Add the clauses for the root solvable. let output = self .async_runtime - .block_on(self.add_clauses_for_solvables(vec![InternalSolvableId::root()]))?; + .block_on(self.add_clauses_for_solvables([solvable]))?; if let Err(clause_id) = self.process_add_clause_output(output) { - tracing::trace!("Unsolvable: {:?}", clause_id); - return Err(UnsolvableOrCancelled::Unsolvable( - self.analyze_unsolvable(clause_id), - )); + return self.run_sat_process_unsolvable(solvable, starting_level, clause_id); } } @@ -634,17 +675,19 @@ impl Solver { match propagate_result { Ok(()) => {} Err(PropagationError::Conflict(_, _, clause_id)) => { - if level == 1 { - return Err(UnsolvableOrCancelled::Unsolvable( - self.analyze_unsolvable(clause_id), - )); + if level == starting_level + 1 { + return self.run_sat_process_unsolvable( + solvable, + starting_level, + clause_id, + ); } else { // 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.borrow()[clause_id].display(self.provider())); - level = 0; - self.decision_tracker.clear(); + level = starting_level; + self.decision_tracker.undo_until(starting_level); continue; } } @@ -687,7 +730,7 @@ impl Solver { "Level {}: No new solvables selected, solution is complete", level ); - return Ok(()); + return Ok(true); } tracing::debug!("==== Found newly selected solvables"); @@ -716,12 +759,41 @@ impl Solver { } if let Err(_first_conflicting_clause_id) = self.process_add_clause_output(output) { - self.decision_tracker.clear(); - level = 0; + self.decision_tracker.undo_until(starting_level); + level = starting_level; } } } + /// Decides how to terminate the solver algorithm when the given `solvable` was + /// deemed unsolvable by [`Solver::run_sat`]. + /// + /// Returns an `Err` value of [`UnsolvableOrCancelled::Unsolvable`] only if `solvable` is + /// the very first solvable we are solving for. Otherwise, undoes all the decisions made + /// when trying to solve for `solvable`, sets it to `false` and returns `Ok(false)`. + fn run_sat_process_unsolvable( + &mut self, + solvable: InternalSolvableId, + starting_level: u32, + clause_id: ClauseId, + ) -> Result { + if starting_level == 0 { + tracing::trace!("Unsolvable: {:?}", clause_id); + Err(UnsolvableOrCancelled::Unsolvable( + self.analyze_unsolvable(clause_id), + )) + } else { + self.decision_tracker.undo_until(starting_level); + self.decision_tracker + .try_add_decision( + Decision::new(solvable, false, ClauseId::install_root()), + starting_level + 1, + ) + .expect("bug: already decided - decision should have been undone"); + Ok(false) + } + } + fn process_add_clause_output(&mut self, mut output: AddClauseOutput) -> Result<(), ClauseId> { let mut clauses = self.clauses.borrow_mut(); for clause_id in output.clauses_to_watch { @@ -855,7 +927,7 @@ impl Solver { /// CDCL algorithm. /// /// Returns the new level after this set-propagate-learn round, or a - /// [`Problem`] if we discovered that the requested jobs are + /// [`Conflict`] if we discovered that the requested jobs are /// unsatisfiable. fn set_propagate_learn( &mut self, @@ -915,7 +987,7 @@ impl Solver { conflicting_solvable: InternalSolvableId, attempted_value: bool, conflicting_clause: ClauseId, - ) -> Result { + ) -> Result { { tracing::info!( "├─ Propagation conflicted: could not set {solvable} to {attempted_value}", @@ -1161,15 +1233,15 @@ impl Solver { Ok(()) } - /// Adds the clause with `clause_id` to the current `Problem` + /// Adds the clause with `clause_id` to the current [`Conflict`] /// /// Because learnt clauses are not relevant for the user, they are not added - /// to the `Problem`. Instead, we report the clauses that caused them. + /// to the [`Conflict`]. Instead, we report the clauses that caused them. fn analyze_unsolvable_clause( clauses: &Arena, learnt_why: &Mapping>, clause_id: ClauseId, - problem: &mut Problem, + conflict: &mut Conflict, seen: &mut HashSet, ) { let clause = &clauses[clause_id]; @@ -1183,21 +1255,21 @@ impl Solver { .get(learnt_clause_id) .expect("no cause for learnt clause available") { - Self::analyze_unsolvable_clause(clauses, learnt_why, cause, problem, seen); + Self::analyze_unsolvable_clause(clauses, learnt_why, cause, conflict, seen); } } - _ => problem.add_clause(clause_id), + _ => conflict.add_clause(clause_id), } } - /// Create a [`Problem`] based on the id of the clause that triggered an + /// Create a [`Conflict`] based on the id of the clause that triggered an /// unrecoverable conflict - fn analyze_unsolvable(&mut self, clause_id: ClauseId) -> Problem { + fn analyze_unsolvable(&mut self, clause_id: ClauseId) -> Conflict { let last_decision = self.decision_tracker.stack().last().unwrap(); let highest_level = self.decision_tracker.level(last_decision.solvable_id); debug_assert_eq!(highest_level, 1); - let mut problem = Problem::default(); + let mut conflict = Conflict::default(); tracing::info!("=== ANALYZE UNSOLVABLE"); @@ -1215,7 +1287,7 @@ impl Solver { &self.clauses.borrow(), &self.learnt_why, clause_id, - &mut problem, + &mut conflict, &mut seen, ); @@ -1236,7 +1308,7 @@ impl Solver { &self.clauses.borrow(), &self.learnt_why, why, - &mut problem, + &mut conflict, &mut seen, ); @@ -1253,7 +1325,7 @@ impl Solver { ); } - problem + conflict } /// Analyze the causes of the conflict and learn from it diff --git a/tests/solver.rs b/tests/solver.rs index f5708d0..6aa1cea 100644 --- a/tests/solver.rs +++ b/tests/solver.rs @@ -22,8 +22,8 @@ use itertools::Itertools; use resolvo::{ snapshot::{DependencySnapshot, SnapshotProvider}, utils::{Pool, Range}, - Candidates, Dependencies, DependencyProvider, Interner, KnownDependencies, NameId, Requirement, - SolvableId, Solver, SolverCache, StringId, UnsolvableOrCancelled, VersionSetId, + Candidates, Dependencies, DependencyProvider, Interner, KnownDependencies, NameId, Problem, + Requirement, SolvableId, Solver, SolverCache, StringId, UnsolvableOrCancelled, VersionSetId, VersionSetUnionId, }; use tracing_test::traced_test; @@ -179,6 +179,7 @@ struct BundleBoxProvider { // duplicate requests. requested_candidates: RefCell>, requested_dependencies: RefCell>, + interned_solvables: RefCell>, } #[derive(Debug, Clone)] @@ -313,6 +314,18 @@ impl BundleBoxProvider { .collect::>(); DependencySnapshot::from_provider(self, name_ids, [], []).unwrap() } + + pub fn intern_solvable(&self, name_id: NameId, pack: Pack) -> SolvableId { + *self + .interned_solvables + .borrow_mut() + .entry((name_id, pack)) + .or_insert_with_key(|&(name_id, pack)| self.pool.intern_solvable(name_id, pack)) + } + + pub fn solvable_id(&self, name: impl Into, version: impl Into) -> SolvableId { + self.intern_solvable(self.pool.intern_package_name(name.into()), version.into()) + } } impl Interner for BundleBoxProvider { @@ -411,7 +424,7 @@ impl DependencyProvider for BundleBoxProvider { let locked = self.locked.get(package_name); let excluded = self.excluded.get(package_name); for pack in package.keys() { - let solvable = self.pool.intern_solvable(name, *pack); + let solvable = self.intern_solvable(name, *pack); candidates.candidates.push(solvable); if Some(pack) == favor { candidates.favored = Some(solvable); @@ -539,15 +552,19 @@ fn transaction_to_string(interner: &impl Interner, solvables: &Vec) buf } -/// Unsat so that we can view the problem +/// Unsat so that we can view the conflict fn solve_unsat(provider: BundleBoxProvider, specs: &[&str]) -> String { let requirements = provider.requirements(specs); let mut solver = Solver::new(provider); - match solver.solve(requirements, Vec::new()) { + let problem = Problem { + requirements, + ..Default::default() + }; + match solver.solve(problem) { Ok(_) => panic!("expected unsat, but a solution was found"), - Err(UnsolvableOrCancelled::Unsolvable(problem)) => { - // Write the problem graphviz to stderr - let graph = problem.graph(&solver); + Err(UnsolvableOrCancelled::Unsolvable(conflict)) => { + // Write the conflict graphviz to stderr + let graph = conflict.graph(&solver); let mut output = stderr(); writeln!(output, "UNSOLVABLE:").unwrap(); graph @@ -556,7 +573,7 @@ fn solve_unsat(provider: BundleBoxProvider, specs: &[&str]) -> String { writeln!(output, "\n").unwrap(); // Format a user friendly error message - problem.display_user_friendly(&solver).to_string() + conflict.display_user_friendly(&solver).to_string() } Err(UnsolvableOrCancelled::Cancelled(reason)) => *reason.downcast().unwrap(), } @@ -575,11 +592,15 @@ fn solve_snapshot(mut provider: BundleBoxProvider, specs: &[&str]) -> String { let requirements = provider.parse_requirements(specs); let mut solver = Solver::new(provider).with_runtime(runtime); - match solver.solve(requirements, Vec::new()) { + let problem = Problem { + requirements, + ..Default::default() + }; + match solver.solve(problem) { Ok(solvables) => transaction_to_string(solver.provider(), &solvables), - Err(UnsolvableOrCancelled::Unsolvable(problem)) => { - // Write the problem graphviz to stderr - let graph = problem.graph(&solver); + Err(UnsolvableOrCancelled::Unsolvable(conflict)) => { + // Write the conflict graphviz to stderr + let graph = conflict.graph(&solver); let mut output = stderr(); writeln!(output, "UNSOLVABLE:").unwrap(); graph @@ -588,7 +609,7 @@ fn solve_snapshot(mut provider: BundleBoxProvider, specs: &[&str]) -> String { writeln!(output, "\n").unwrap(); // Format a user friendly error message - problem.display_user_friendly(&solver).to_string() + conflict.display_user_friendly(&solver).to_string() } Err(UnsolvableOrCancelled::Cancelled(reason)) => *reason.downcast().unwrap(), } @@ -598,9 +619,13 @@ fn solve_snapshot(mut provider: BundleBoxProvider, specs: &[&str]) -> String { #[test] fn test_unit_propagation_1() { let provider = BundleBoxProvider::from_packages(&[("asdf", 1, vec![])]); - let root_requirements = provider.requirements(&["asdf"]); + let requirements = provider.requirements(&["asdf"]); let mut solver = Solver::new(provider); - let solved = solver.solve(root_requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -620,7 +645,11 @@ fn test_unit_propagation_nested() { ]); let requirements = provider.requirements(&["asdf"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 2); @@ -647,7 +676,11 @@ fn test_resolve_multiple() { ]); let requirements = provider.requirements(&["asdf", "efgh"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 2); @@ -705,7 +738,11 @@ fn test_resolve_with_nonexisting() { ]); let requirements = provider.requirements(&["asdf"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -739,7 +776,11 @@ fn test_resolve_with_nested_deps() { ]); let requirements = provider.requirements(&["apache-airflow"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -763,7 +804,11 @@ fn test_resolve_with_unknown_deps() { provider.add_package("opentelemetry-api", Pack::new(2), &[], &[]); let requirements = provider.requirements(&["opentelemetry-api"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -808,7 +853,11 @@ fn test_resolve_locked_top_level() { let requirements = provider.requirements(&["asdf"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -830,7 +879,11 @@ fn test_resolve_ignored_locked_top_level() { let requirements = provider.requirements(&["asdf"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let pool = &solver.provider().pool; assert_eq!(solved.len(), 1); @@ -888,7 +941,11 @@ fn test_resolve_cyclic() { BundleBoxProvider::from_packages(&[("a", 2, vec!["b 0..10"]), ("b", 5, vec!["a 2..4"])]); let requirements = provider.requirements(&["a 0..100"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, Vec::new()).unwrap(); + let problem = Problem { + requirements, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let result = transaction_to_string(solver.provider(), &solved); insta::assert_snapshot!(result, @r###" @@ -1171,7 +1228,12 @@ fn test_constraints() { let requirements = provider.requirements(&["a 0..10"]); let constraints = provider.requirements(&["b 1..2", "c"]); let mut solver = Solver::new(provider); - let solved = solver.solve(requirements, constraints).unwrap(); + let problem = Problem { + requirements, + constraints, + ..Default::default() + }; + let solved = solver.solve(problem).unwrap(); let result = transaction_to_string(solver.provider(), &solved); insta::assert_snapshot!(result, @r###" @@ -1180,6 +1242,107 @@ fn test_constraints() { "###); } +#[test] +fn test_solve_with_additional() { + let mut provider = BundleBoxProvider::from_packages(&[ + ("a", 1, vec!["b 0..10"]), + ("b", 1, vec![]), + ("b", 2, vec![]), + ("c", 1, vec![]), + ("d", 1, vec![]), + ("e", 1, vec!["d"]), + ("locked", 1, vec![]), + ("locked", 2, vec![]), + ]); + + provider.set_locked("locked", 2); + + let requirements = provider.requirements(&["a 0..10"]); + let constraints = provider.requirements(&["b 1..2", "c"]); + + let extra_solvables = [ + provider.solvable_id("b", 2), + provider.solvable_id("c", 1), + provider.solvable_id("e", 1), + // Does not obey the locked clause since it has not been requested + // in a version set by another solvable + provider.solvable_id("locked", 1), + provider.solvable_id("unknown-deps", Pack::new(1).with_unknown_deps()), + ]; + + let mut solver = Solver::new(provider); + + let problem = Problem { + requirements, + constraints, + soft_requirements: extra_solvables.to_vec(), + }; + let solved = solver.solve(problem).unwrap(); + + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r###" + a=1 + b=1 + c=1 + d=1 + e=1 + locked=1 + "###); +} + +#[test] +fn test_solve_with_additional_with_constrains() { + let mut provider = BundleBoxProvider::from_packages(&[ + ("a", 1, vec!["b 0..10"]), + ("b", 1, vec![]), + ("b", 2, vec![]), + ("b", 3, vec![]), + ("c", 1, vec![]), + ("d", 1, vec!["f"]), + ("e", 1, vec!["c"]), + ]); + + provider.add_package("f", 1.into(), &[], &["c 2..3"]); + provider.add_package("g", 1.into(), &[], &["b 2..3"]); + provider.add_package("h", 1.into(), &[], &["b 1..2"]); + provider.add_package("i", 1.into(), &[], &[]); + provider.add_package("j", 1.into(), &["i"], &[]); + provider.add_package("k", 1.into(), &["i"], &[]); + provider.add_package("l", 1.into(), &["j", "k"], &[]); + + let requirements = provider.requirements(&["a 0..10", "e"]); + let constraints = provider.requirements(&["b 1..2", "c", "k 2..3"]); + + let extra_solvables = [ + provider.solvable_id("d", 1), + provider.solvable_id("g", 1), + provider.solvable_id("h", 1), + provider.solvable_id("j", 1), + provider.solvable_id("l", 1), + provider.solvable_id("k", 1), + ]; + + let mut solver = Solver::new(provider); + + let problem = Problem { + requirements, + constraints, + soft_requirements: extra_solvables.to_vec(), + }; + let solved = solver.solve(problem).unwrap(); + + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r###" + a=1 + b=1 + c=1 + e=1 + h=1 + i=1 + j=1 + "###); +} + #[test] fn test_snapshot() { let provider = BundleBoxProvider::from_packages(&[ @@ -1241,14 +1404,15 @@ fn serialize_snapshot(snapshot: &DependencySnapshot, destination: impl AsRef String { let mut solver = Solver::new(provider); - match solver.solve( - root_reqs.iter().copied().map(Into::into).collect(), - Vec::new(), - ) { + let problem = Problem { + requirements: root_reqs.iter().copied().map(Into::into).collect(), + ..Default::default() + }; + match solver.solve(problem) { Ok(solvables) => transaction_to_string(solver.provider(), &solvables), - Err(UnsolvableOrCancelled::Unsolvable(problem)) => { - // Write the problem graphviz to stderr - let graph = problem.graph(&solver); + Err(UnsolvableOrCancelled::Unsolvable(conflict)) => { + // Write the conflict graphviz to stderr + let graph = conflict.graph(&solver); let mut output = stderr(); writeln!(output, "UNSOLVABLE:").unwrap(); graph @@ -1257,7 +1421,7 @@ fn solve_for_snapshot(provider: SnapshotProvider, root_reqs: &[VersionSetId]) -> writeln!(output, "\n").unwrap(); // Format a user friendly error message - problem.display_user_friendly(&solver).to_string() + conflict.display_user_friendly(&solver).to_string() } Err(UnsolvableOrCancelled::Cancelled(reason)) => *reason.downcast().unwrap(), }