From ae6c794743121dcaec8c09a306411a30a443f655 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Wed, 17 Jul 2024 16:27:43 +0200 Subject: [PATCH 01/11] chore: Add more tracing Signed-off-by: Julien Jerphanion --- src/internal/id.rs | 6 +++ src/solver/cache.rs | 32 ++++++++++++- src/solver/clause.rs | 39 +++++++--------- src/solver/mod.rs | 104 +++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 155 insertions(+), 26 deletions(-) diff --git a/src/internal/id.rs b/src/internal/id.rs index 1ebc041..9b5ef37 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -161,6 +161,12 @@ impl From for u32 { #[derive(Copy, Clone, PartialOrd, Ord, Eq, PartialEq, Debug, Hash)] pub(crate) struct ClauseId(u32); +impl Display for ClauseId { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!(f, "ClauseId({})", self.0) + } +} + impl ClauseId { /// There is a guarentee that ClauseId(0) will always be /// "Clause::InstallRoot". This assumption is verified by the solver. diff --git a/src/solver/cache.rs b/src/solver/cache.rs index 55125fd..2946813 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -172,13 +172,24 @@ impl SolverCache { Some(candidates) => Ok(candidates), None => { let package_name = self.provider.version_set_name(version_set_id); + + tracing::debug!( + "Getting matching candidates for package: {:?}", + package_name + ); let candidates = self.get_or_cache_candidates(package_name).await?; + tracing::debug!("Got {:?} matching candidates", candidates.candidates.len()); let matching_candidates = self .provider .filter_candidates(&candidates.candidates, version_set_id, false) .await; + tracing::debug!( + "Filtered {:?} matching candidates", + matching_candidates.len() + ); + Ok(self .version_set_candidates .insert(version_set_id, matching_candidates)) @@ -198,9 +209,18 @@ impl SolverCache { Some(candidates) => Ok(candidates), None => { let package_name = self.provider.version_set_name(version_set_id); + + tracing::debug!( + "Getting NON-matching candidates for package: {:?}", + package_name + ); let candidates = self.get_or_cache_candidates(package_name).await?; + tracing::debug!( + "Got {:?} NON-matching candidates", + candidates.candidates.len() + ); - let matching_candidates = self + let matching_candidates: Vec = self .provider .filter_candidates(&candidates.candidates, version_set_id, true) .await @@ -208,6 +228,11 @@ impl SolverCache { .map(Into::into) .collect(); + tracing::debug!( + "Filtered {:?} matching candidates", + matching_candidates.len() + ); + Ok(self .version_set_inverse_candidates .insert(version_set_id, matching_candidates)) @@ -228,6 +253,11 @@ impl SolverCache { Some(candidates) => Ok(candidates), None => { let package_name = self.provider.version_set_name(version_set_id); + tracing::debug!( + "Getting sorted matching candidates for package: {:?}", + package_name + ); + let matching_candidates = self .get_or_cache_matching_candidates(version_set_id) .await?; diff --git a/src/solver/clause.rs b/src/solver/clause.rs index e859b33..d18618c 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -611,49 +611,44 @@ pub(crate) struct ClauseDisplay<'i, I: Interner> { impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match self.kind { - Clause::InstallRoot => write!(f, "install root"), + Clause::InstallRoot => write!(f, "InstallRoot"), Clause::Excluded(solvable_id, reason) => { write!( f, - "{} excluded because: {}", - solvable_id.display(self.interner), + "Excluded({:?}, {})", + solvable_id, self.interner.display_string(reason) ) } - Clause::Learnt(learnt_id) => write!(f, "learnt clause {learnt_id:?}"), + Clause::Learnt(learnt_id) => write!(f, "Learnt({:?})", learnt_id), Clause::Requires(solvable_id, version_set_id) => { write!( f, - "{} requires {} {}", - solvable_id.display(self.interner), - self.interner - .display_name(self.interner.version_set_name(version_set_id)), + "Requires({:?}, {})", + solvable_id, self.interner.display_version_set(version_set_id) ) } Clause::Constrains(s1, s2, version_set_id) => { write!( f, - "{} excludes {} by {}", - s1.display(self.interner), - s2.display(self.interner), - self.interner.display_version_set(version_set_id), + "Constrains({:?}, {:?}, {})", + s1, + s2, + self.interner.display_version_set(version_set_id) ) } - Clause::Lock(locked, forbidden) => { + Clause::ForbidMultipleInstances(s1, s2, name) => { write!( f, - "{} is locked, so {} is forbidden", - locked.display(self.interner), - forbidden.display(self.interner), + "ForbidMultipleInstances({:?}, {:?}, {})", + s1, + s2, + self.interner.display_name(name) ) } - Clause::ForbidMultipleInstances(_, _, name_id) => { - write!( - f, - "only one {} allowed", - self.interner.display_name(name_id) - ) + Clause::Lock(locked, other) => { + write!(f, "Lock({:?}, {:?})", locked, other) } } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 009eebb..2bb059b 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -1,11 +1,11 @@ -use std::{any::Any, cell::RefCell, collections::HashSet, future::ready, ops::ControlFlow}; - pub use cache::SolverCache; use clause::{Clause, ClauseState, Literal}; use decision::Decision; use decision_tracker::DecisionTracker; use futures::{stream::FuturesUnordered, FutureExt, StreamExt}; use itertools::{chain, Itertools}; +use std::fmt::Display; +use std::{any::Any, cell::RefCell, collections::HashSet, future::ready, ops::ControlFlow}; use watch_map::WatchMap; use crate::{ @@ -34,6 +34,12 @@ struct AddClauseOutput { clauses_to_watch: Vec, } +impl Display for AddClauseOutput { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "AddClauseOutput {{ new_requires_clauses: {:?}, conflicting_clauses: {:?}, negative_assertions: {:?}, clauses_to_watch: {:?} }}", self.new_requires_clauses, self.conflicting_clauses, self.negative_assertions, self.clauses_to_watch) + } +} + /// Drives the SAT solving process pub struct Solver { pub(crate) async_runtime: RT, @@ -106,11 +112,29 @@ impl From> for UnsolvableOrCancelled { } /// An error during the propagation step +#[derive(Debug)] pub(crate) enum PropagationError { Conflict(InternalSolvableId, bool, ClauseId), Cancelled(Box), } +impl Display for PropagationError { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + PropagationError::Conflict(solvable, value, clause) => { + write!( + f, + "conflict while propagating solvable {:?}, value {} caused by clause {:?}", + solvable, value, clause + ) + } + PropagationError::Cancelled(_) => { + write!(f, "propagation was cancelled") + } + } + } +} + impl Solver { /// Returns the dependency provider used by this instance. pub fn provider(&self) -> &D { @@ -179,6 +203,8 @@ impl Solver { }) .collect(); + tracing::info!("Solver steps: {:?}", steps); + Ok(steps) } @@ -196,6 +222,8 @@ impl Solver { ) -> Result> { let mut output = AddClauseOutput::default(); + tracing::info!("Add clauses for solvables"); + pub enum TaskResult<'i> { Dependencies { solvable_id: InternalSolvableId, @@ -238,6 +266,10 @@ impl Solver { "┝━ adding clauses for dependencies of {}", internal_solvable_id.display(self.provider()), ); + tracing::info!( + "Adding clauses for dependencies of {}", + internal_solvable_id.display(self.provider()) + ); // If the solvable is the root solvable, we can skip the dependency provider // and use the root requirements and constraints directly. @@ -314,6 +346,10 @@ impl Solver { "┝━ adding clauses for package '{}'", self.provider().display_name(dependency_name), ); + tracing::info!( + "Adding clauses for package '{}'", + self.provider().display_name(dependency_name), + ); pending_futures.push( async move { @@ -375,6 +411,11 @@ impl Solver { self.provider().display_name(name_id) ); + tracing::info!( + "Package candidates available for {}", + self.provider().display_name(name_id) + ); + let locked_solvable_id = package_candidates.locked; let candidates = &package_candidates.candidates; @@ -449,6 +490,13 @@ impl Solver { self.provider().display_version_set(version_set_id), ); + tracing::info!( + "Sorted candidates available for {} {}", + self.provider() + .display_name(self.provider().version_set_name(version_set_id)), + self.provider().display_version_set(version_set_id), + ); + // Queue requesting the dependencies of the candidates as well if they are // cheaply available from the dependency provider. for &candidate in candidates { @@ -503,6 +551,13 @@ impl Solver { self.provider().display_version_set(version_set_id), ); + tracing::info!( + "Non matching candidates available for {} {}", + self.provider() + .display_name(self.provider().version_set_name(version_set_id)), + self.provider().display_version_set(version_set_id), + ); + // Add forbidden clauses for the candidates for &forbidden_candidate in non_matching_candidates { let (clause, conflict) = ClauseState::constrains( @@ -523,6 +578,8 @@ impl Solver { } } + tracing::info!("Done adding clauses for solvables"); + Ok(output) } @@ -554,6 +611,12 @@ impl Solver { let mut level = 0; loop { + if level == 0 { + tracing::info!("Level 0: Resetting the decision loop"); + } else { + tracing::info!("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 { @@ -565,7 +628,7 @@ impl Solver { // 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::info!("╤══ install at level {level}",); + tracing::info!("╤══ Install at level {level}",); self.decision_tracker .try_add_decision( Decision::new(InternalSolvableId::root(), true, ClauseId::install_root()), @@ -578,15 +641,20 @@ impl Solver { .async_runtime .block_on(self.add_clauses_for_solvables(vec![InternalSolvableId::root()]))?; if let Err(clause_id) = self.process_add_clause_output(output) { + tracing::info!("Unsolvable: {:?}", clause_id); return Err(UnsolvableOrCancelled::Unsolvable( self.analyze_unsolvable(clause_id), )); } } + tracing::info!("Level {}: Propagating", level); + // Propagate decisions from assignments above let propagate_result = self.propagate(level); + tracing::info!("Propagate result: {:?}", propagate_result); + // Handle propagation errors match propagate_result { Ok(()) => {} @@ -613,7 +681,9 @@ impl Solver { // Enter the solver loop, return immediately if no new assignments have been // made. + tracing::info!("Level {}: Resolving dependencies", level); level = self.resolve_dependencies(level)?; + tracing::info!("Level {}: Done resolving dependencies", level); // We have a partial solution. E.g. there is a solution that satisfies all the // clauses that have been added so far. @@ -638,6 +708,10 @@ impl Solver { if new_solvables.is_empty() { // If no new literals were selected this solution is complete and we can return. + tracing::info!( + "Level {}: No new solvables selected, solution is complete", + level + ); return Ok(()); } @@ -707,6 +781,8 @@ impl Solver { /// it was provided by the user, and set its value to true. fn resolve_dependencies(&mut self, mut level: u32) -> Result { loop { + tracing::info!("Loop in resolve_dependencies: Level {}: Deciding", level); + // Make a decision. If no decision could be made it means the problem is // satisfyable. let Some((candidate, required_by, clause_id)) = self.decide() else { @@ -939,6 +1015,8 @@ impl Solver { /// solvable has become false, in which case it picks a new solvable to /// watch (if available) or triggers an assignment. fn propagate(&mut self, level: u32) -> Result<(), PropagationError> { + tracing::info!("Propagate"); + if let Some(value) = self.provider().should_cancel_with_value() { return Err(PropagationError::Cancelled(value)); }; @@ -946,18 +1024,33 @@ impl Solver { // Negative assertions derived from other rules (assertions are clauses that // consist of a single literal, and therefore do not have watches) for &(solvable_id, clause_id) in &self.negative_assertions { + tracing::info!( + "Negative assertions derived from other rules: {} = false", + solvable_id.display(self.provider()) + ); + let value = false; let decided = self .decision_tracker .try_add_decision(Decision::new(solvable_id, value, clause_id), level) .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?; + tracing::info!( + "Negative assertions derived from other rules: Decided: {}", + decided + ); + if decided { tracing::trace!( "├─ Propagate assertion {} = {}", solvable_id.display(self.provider()), value ); + tracing::info!( + "Negative assertions derived from other rules: Propagate assertion {} = {}", + solvable_id.display(self.provider()), + value + ); } } @@ -1002,6 +1095,11 @@ impl Solver { while let Some(decision) = self.decision_tracker.next_unpropagated() { let pkg = decision.solvable_id; + tracing::trace!( + "Exploring watched solvables for {}", + pkg.display(self.provider()) + ); + // Propagate, iterating through the linked list of clauses that watch this // solvable let mut old_predecessor_clause_id: Option; From 4434ca3b930477d218e02eed8b2cb7a3583d17c6 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Wed, 17 Jul 2024 17:39:44 +0200 Subject: [PATCH 02/11] Replace some `info!`, `debug!` with `trace!` Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/problem.rs | 6 ++-- src/solver/mod.rs | 76 +++++++++++++++++------------------------------ 2 files changed, 30 insertions(+), 52 deletions(-) diff --git a/src/problem.rs b/src/problem.rs index a084453..91432a5 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -56,7 +56,7 @@ impl Problem { match clause { Clause::InstallRoot => (), Clause::Excluded(solvable, reason) => { - tracing::info!("{solvable:?} is excluded"); + tracing::trace!("{solvable:?} is excluded"); let package_node = Self::add_node(&mut graph, &mut nodes, *solvable); let excluded_node = excluded_nodes .entry(*reason) @@ -76,7 +76,7 @@ impl Problem { unreachable!("The version set was used in the solver, so it must have been cached. Therefore cancellation is impossible here and we cannot get an `Err(...)`") }); if candidates.is_empty() { - tracing::info!( + tracing::trace!( "{package_id:?} requires {version_set_id:?}, which has no candidates" ); graph.add_edge( @@ -86,7 +86,7 @@ impl Problem { ); } else { for &candidate_id in candidates { - tracing::info!("{package_id:?} requires {candidate_id:?}"); + tracing::trace!("{package_id:?} requires {candidate_id:?}"); let candidate_node = Self::add_node(&mut graph, &mut nodes, candidate_id.into()); diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 2bb059b..1f0aa84 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -203,7 +203,10 @@ impl Solver { }) .collect(); - tracing::info!("Solver steps: {:?}", steps); + tracing::trace!("Solvables found:"); + for step in &steps { + tracing::trace!(" - {}", step.display(self.provider())); + } Ok(steps) } @@ -222,7 +225,7 @@ impl Solver { ) -> Result> { let mut output = AddClauseOutput::default(); - tracing::info!("Add clauses for solvables"); + tracing::trace!("Add clauses for solvables"); pub enum TaskResult<'i> { Dependencies { @@ -266,10 +269,6 @@ impl Solver { "┝━ adding clauses for dependencies of {}", internal_solvable_id.display(self.provider()), ); - tracing::info!( - "Adding clauses for dependencies of {}", - internal_solvable_id.display(self.provider()) - ); // If the solvable is the root solvable, we can skip the dependency provider // and use the root requirements and constraints directly. @@ -343,11 +342,7 @@ impl Solver { let dependency_name = self.provider().version_set_name(version_set_id); if clauses_added_for_package.insert(dependency_name) { tracing::trace!( - "┝━ adding clauses for package '{}'", - self.provider().display_name(dependency_name), - ); - tracing::info!( - "Adding clauses for package '{}'", + "┝━ Adding clauses for package '{}'", self.provider().display_name(dependency_name), ); @@ -407,11 +402,6 @@ impl Solver { } => { // Get the solvable information and request its requirements and constraints tracing::trace!( - "package candidates available for {}", - self.provider().display_name(name_id) - ); - - tracing::info!( "Package candidates available for {}", self.provider().display_name(name_id) ); @@ -484,13 +474,6 @@ impl Solver { candidates, } => { tracing::trace!( - "sorted candidates available for {} {}", - self.provider() - .display_name(self.provider().version_set_name(version_set_id)), - self.provider().display_version_set(version_set_id), - ); - - tracing::info!( "Sorted candidates available for {} {}", self.provider() .display_name(self.provider().version_set_name(version_set_id)), @@ -551,13 +534,6 @@ impl Solver { self.provider().display_version_set(version_set_id), ); - tracing::info!( - "Non matching candidates available for {} {}", - self.provider() - .display_name(self.provider().version_set_name(version_set_id)), - self.provider().display_version_set(version_set_id), - ); - // Add forbidden clauses for the candidates for &forbidden_candidate in non_matching_candidates { let (clause, conflict) = ClauseState::constrains( @@ -578,7 +554,7 @@ impl Solver { } } - tracing::info!("Done adding clauses for solvables"); + tracing::trace!("Done adding clauses for solvables"); Ok(output) } @@ -612,9 +588,9 @@ impl Solver { loop { if level == 0 { - tracing::info!("Level 0: Resetting the decision loop"); + tracing::trace!("Level 0: Resetting the decision loop"); } else { - tracing::info!("Level {}: Starting the decision loop", level); + tracing::trace!("Level {}: Starting the decision loop", level); } // A level of 0 means the decision loop has been completely reset because a @@ -628,7 +604,7 @@ impl Solver { // 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::info!("╤══ Install at level {level}",); + tracing::trace!("╤══ Install at level {level}",); self.decision_tracker .try_add_decision( Decision::new(InternalSolvableId::root(), true, ClauseId::install_root()), @@ -641,19 +617,19 @@ impl Solver { .async_runtime .block_on(self.add_clauses_for_solvables(vec![InternalSolvableId::root()]))?; if let Err(clause_id) = self.process_add_clause_output(output) { - tracing::info!("Unsolvable: {:?}", clause_id); + tracing::trace!("Unsolvable: {:?}", clause_id); return Err(UnsolvableOrCancelled::Unsolvable( self.analyze_unsolvable(clause_id), )); } } - tracing::info!("Level {}: Propagating", level); + tracing::trace!("Level {}: Propagating", level); // Propagate decisions from assignments above let propagate_result = self.propagate(level); - tracing::info!("Propagate result: {:?}", propagate_result); + tracing::trace!("Propagate result: {:?}", propagate_result); // Handle propagation errors match propagate_result { @@ -681,9 +657,9 @@ impl Solver { // Enter the solver loop, return immediately if no new assignments have been // made. - tracing::info!("Level {}: Resolving dependencies", level); + tracing::trace!("Level {}: Resolving dependencies", level); level = self.resolve_dependencies(level)?; - tracing::info!("Level {}: Done resolving dependencies", level); + tracing::trace!("Level {}: Done resolving dependencies", level); // We have a partial solution. E.g. there is a solution that satisfies all the // clauses that have been added so far. @@ -708,15 +684,16 @@ impl Solver { if new_solvables.is_empty() { // If no new literals were selected this solution is complete and we can return. - tracing::info!( + tracing::trace!( "Level {}: No new solvables selected, solution is complete", level ); return Ok(()); } + tracing::debug!("==== Found newly selected solvables"); tracing::debug!( - "====\n==Found newly selected solvables\n- {}\n====", + " - {}", new_solvables .iter() .copied() @@ -726,6 +703,7 @@ impl Solver { self.clauses.borrow()[derived_from].display(self.provider()), ))) ); + tracing::debug!("===="); // Concurrently get the solvable's clauses let output = self.async_runtime.block_on(self.add_clauses_for_solvables( @@ -734,7 +712,7 @@ impl Solver { // Serially process the outputs, to reduce the need for synchronization for &clause_id in &output.conflicting_clauses { - tracing::debug!("├─ added clause {clause} introduces a conflict which invalidates the partial solution", + tracing::debug!("├─ Added clause {clause} introduces a conflict which invalidates the partial solution", clause=self.clauses.borrow()[clause_id].display(self.provider())); } @@ -781,7 +759,7 @@ impl Solver { /// it was provided by the user, and set its value to true. fn resolve_dependencies(&mut self, mut level: u32) -> Result { loop { - tracing::info!("Loop in resolve_dependencies: Level {}: Deciding", level); + tracing::trace!("Loop in resolve_dependencies: Level {}: Deciding", level); // Make a decision. If no decision could be made it means the problem is // satisfyable. @@ -852,7 +830,7 @@ impl Solver { } if let Some((count, (candidate, _solvable_id, clause_id))) = best_decision { - tracing::info!( + tracing::trace!( "deciding to assign {}, ({}, {} possible candidates)", self.provider().display_solvable(candidate), self.clauses.borrow()[clause_id].display(self.provider()), @@ -889,7 +867,7 @@ impl Solver { ) -> Result { level += 1; - tracing::info!( + tracing::trace!( "╤══ Install {} at level {level} (required by {})", solvable.display(self.provider()), required_by.display(self.provider()) @@ -1015,7 +993,7 @@ impl Solver { /// solvable has become false, in which case it picks a new solvable to /// watch (if available) or triggers an assignment. fn propagate(&mut self, level: u32) -> Result<(), PropagationError> { - tracing::info!("Propagate"); + tracing::trace!("Propagate"); if let Some(value) = self.provider().should_cancel_with_value() { return Err(PropagationError::Cancelled(value)); @@ -1024,7 +1002,7 @@ impl Solver { // Negative assertions derived from other rules (assertions are clauses that // consist of a single literal, and therefore do not have watches) for &(solvable_id, clause_id) in &self.negative_assertions { - tracing::info!( + tracing::trace!( "Negative assertions derived from other rules: {} = false", solvable_id.display(self.provider()) ); @@ -1035,7 +1013,7 @@ impl Solver { .try_add_decision(Decision::new(solvable_id, value, clause_id), level) .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?; - tracing::info!( + tracing::trace!( "Negative assertions derived from other rules: Decided: {}", decided ); @@ -1046,7 +1024,7 @@ impl Solver { solvable_id.display(self.provider()), value ); - tracing::info!( + tracing::trace!( "Negative assertions derived from other rules: Propagate assertion {} = {}", solvable_id.display(self.provider()), value From 767c25f0547633b8c25184d94bc3a2ffbbe240e6 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 11:54:22 +0200 Subject: [PATCH 03/11] Improve display of solvables Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/internal/id.rs | 6 ++++++ src/solver/clause.rs | 25 +++++++++++++++++++------ src/solver/mod.rs | 4 ++-- 3 files changed, 27 insertions(+), 8 deletions(-) diff --git a/src/internal/id.rs b/src/internal/id.rs index 9b5ef37..22f642b 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -60,6 +60,12 @@ impl ArenaId for VersionSetId { #[cfg_attr(feature = "serde", serde(transparent))] pub struct SolvableId(pub u32); +impl SolvableId { + pub(crate) const fn as_internal(self) -> InternalSolvableId { + InternalSolvableId(self.0 + 1) + } +} + /// Internally used id for solvables that can also represent root and null. #[repr(transparent)] #[derive(Copy, Clone, Eq, PartialEq, Hash, Debug, Ord, PartialOrd)] diff --git a/src/solver/clause.rs b/src/solver/clause.rs index d18618c..8ea3b99 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -615,16 +615,18 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { Clause::Excluded(solvable_id, reason) => { write!( f, - "Excluded({:?}, {})", + "Excluded({}({:?}), {})", + solvable_id.display(self.interner), solvable_id, self.interner.display_string(reason) ) } - Clause::Learnt(learnt_id) => write!(f, "Learnt({:?})", learnt_id), + Clause::Learnt(learnt_id) => write!(f, "Learnt({learnt_id:?})"), Clause::Requires(solvable_id, version_set_id) => { write!( f, - "Requires({:?}, {})", + "Requires({}({:?}), {})", + solvable_id.display(self.interner), solvable_id, self.interner.display_version_set(version_set_id) ) @@ -632,8 +634,10 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { Clause::Constrains(s1, s2, version_set_id) => { write!( f, - "Constrains({:?}, {:?}, {})", + "Constrains({}({:?}), {}({:?}), {})", + s1.display(self.interner), s1, + s2.display(self.interner), s2, self.interner.display_version_set(version_set_id) ) @@ -641,14 +645,23 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { Clause::ForbidMultipleInstances(s1, s2, name) => { write!( f, - "ForbidMultipleInstances({:?}, {:?}, {})", + "ForbidMultipleInstances({}({:?}), {}({:?}), {})", + s1.display(self.interner), s1, + s2.display(self.interner), s2, self.interner.display_name(name) ) } Clause::Lock(locked, other) => { - write!(f, "Lock({:?}, {:?})", locked, other) + write!( + f, + "Lock({}({:?}), {}({:?}))", + locked.display(self.interner), + locked, + other.display(self.interner), + other, + ) } } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 1f0aa84..daec0c5 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -190,7 +190,7 @@ impl Solver { // Run SAT self.run_sat()?; - let steps = self + let steps: Vec = self .decision_tracker .stack() .filter_map(|d| { @@ -205,7 +205,7 @@ impl Solver { tracing::trace!("Solvables found:"); for step in &steps { - tracing::trace!(" - {}", step.display(self.provider())); + tracing::trace!(" - {}", step.as_internal().display(self.provider())); } Ok(steps) From 5e1052257eda1cdaf4c21be70a7ff755b00beb80 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 11:58:57 +0200 Subject: [PATCH 04/11] Remove the implementation of the Display trait for ClauseId Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/internal/id.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/internal/id.rs b/src/internal/id.rs index 22f642b..48e78e8 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -167,12 +167,6 @@ impl From for u32 { #[derive(Copy, Clone, PartialOrd, Ord, Eq, PartialEq, Debug, Hash)] pub(crate) struct ClauseId(u32); -impl Display for ClauseId { - fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { - write!(f, "ClauseId({})", self.0) - } -} - impl ClauseId { /// There is a guarentee that ClauseId(0) will always be /// "Clause::InstallRoot". This assumption is verified by the solver. From 7dc53461497fad35f74c445fc995270c4a501d44 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 12:04:39 +0200 Subject: [PATCH 05/11] Display name of package Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/solver/cache.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/solver/cache.rs b/src/solver/cache.rs index 2946813..39ba0f2 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -171,13 +171,14 @@ impl SolverCache { match self.version_set_candidates.get(&version_set_id) { Some(candidates) => Ok(candidates), None => { - let package_name = self.provider.version_set_name(version_set_id); + let package_name_id = self.provider.version_set_name(version_set_id); tracing::debug!( "Getting matching candidates for package: {:?}", - package_name + self.provider.display_name(package_name_id).to_string() ); - let candidates = self.get_or_cache_candidates(package_name).await?; + + let candidates = self.get_or_cache_candidates(package_name_id).await?; tracing::debug!("Got {:?} matching candidates", candidates.candidates.len()); let matching_candidates = self @@ -208,13 +209,14 @@ impl SolverCache { match self.version_set_inverse_candidates.get(&version_set_id) { Some(candidates) => Ok(candidates), None => { - let package_name = self.provider.version_set_name(version_set_id); + let package_name_id = self.provider.version_set_name(version_set_id); tracing::debug!( "Getting NON-matching candidates for package: {:?}", - package_name + self.provider.display_name(package_name_id).to_string() ); - let candidates = self.get_or_cache_candidates(package_name).await?; + + let candidates = self.get_or_cache_candidates(package_name_id).await?; tracing::debug!( "Got {:?} NON-matching candidates", candidates.candidates.len() @@ -252,16 +254,16 @@ impl SolverCache { match self.version_set_to_sorted_candidates.get(&version_set_id) { Some(candidates) => Ok(candidates), None => { - let package_name = self.provider.version_set_name(version_set_id); + let package_name_id = self.provider.version_set_name(version_set_id); tracing::debug!( "Getting sorted matching candidates for package: {:?}", - package_name + self.provider.display_name(package_name_id).to_string() ); let matching_candidates = self .get_or_cache_matching_candidates(version_set_id) .await?; - let candidates = self.get_or_cache_candidates(package_name).await?; + let candidates = self.get_or_cache_candidates(package_name_id).await?; // Sort all the candidates in order in which they should be tried by the solver. let mut sorted_candidates = Vec::new(); From fdc4765b911ce2782d694deb643bac9cd266aaec Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 11:58:57 +0200 Subject: [PATCH 06/11] Remove the implementation of the Display trait for AddClauseOutput Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/solver/mod.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/solver/mod.rs b/src/solver/mod.rs index daec0c5..b457ec6 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -34,12 +34,6 @@ struct AddClauseOutput { clauses_to_watch: Vec, } -impl Display for AddClauseOutput { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AddClauseOutput {{ new_requires_clauses: {:?}, conflicting_clauses: {:?}, negative_assertions: {:?}, clauses_to_watch: {:?} }}", self.new_requires_clauses, self.conflicting_clauses, self.negative_assertions, self.clauses_to_watch) - } -} - /// Drives the SAT solving process pub struct Solver { pub(crate) async_runtime: RT, From 801bb6f8d0f7f136180e9c1145fc968c45d33ca9 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 12:10:42 +0200 Subject: [PATCH 07/11] Use trace! over debug! Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/solver/cache.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/solver/cache.rs b/src/solver/cache.rs index 39ba0f2..62081cf 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -173,20 +173,20 @@ impl SolverCache { None => { let package_name_id = self.provider.version_set_name(version_set_id); - tracing::debug!( + tracing::trace!( "Getting matching candidates for package: {:?}", self.provider.display_name(package_name_id).to_string() ); let candidates = self.get_or_cache_candidates(package_name_id).await?; - tracing::debug!("Got {:?} matching candidates", candidates.candidates.len()); + tracing::trace!("Got {:?} matching candidates", candidates.candidates.len()); let matching_candidates = self .provider .filter_candidates(&candidates.candidates, version_set_id, false) .await; - tracing::debug!( + tracing::trace!( "Filtered {:?} matching candidates", matching_candidates.len() ); @@ -211,13 +211,13 @@ impl SolverCache { None => { let package_name_id = self.provider.version_set_name(version_set_id); - tracing::debug!( + tracing::trace!( "Getting NON-matching candidates for package: {:?}", self.provider.display_name(package_name_id).to_string() ); let candidates = self.get_or_cache_candidates(package_name_id).await?; - tracing::debug!( + tracing::trace!( "Got {:?} NON-matching candidates", candidates.candidates.len() ); @@ -230,7 +230,7 @@ impl SolverCache { .map(Into::into) .collect(); - tracing::debug!( + tracing::trace!( "Filtered {:?} matching candidates", matching_candidates.len() ); @@ -255,7 +255,7 @@ impl SolverCache { Some(candidates) => Ok(candidates), None => { let package_name_id = self.provider.version_set_name(version_set_id); - tracing::debug!( + tracing::trace!( "Getting sorted matching candidates for package: {:?}", self.provider.display_name(package_name_id).to_string() ); From 7eef3fe9f577cef526f225ab07d4287d827b019b Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 12:12:32 +0200 Subject: [PATCH 08/11] Revert changes and use info! for previous tracing Signed-off-by: Julien Jerphanion --- src/problem.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/problem.rs b/src/problem.rs index 91432a5..a084453 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -56,7 +56,7 @@ impl Problem { match clause { Clause::InstallRoot => (), Clause::Excluded(solvable, reason) => { - tracing::trace!("{solvable:?} is excluded"); + tracing::info!("{solvable:?} is excluded"); let package_node = Self::add_node(&mut graph, &mut nodes, *solvable); let excluded_node = excluded_nodes .entry(*reason) @@ -76,7 +76,7 @@ impl Problem { unreachable!("The version set was used in the solver, so it must have been cached. Therefore cancellation is impossible here and we cannot get an `Err(...)`") }); if candidates.is_empty() { - tracing::trace!( + tracing::info!( "{package_id:?} requires {version_set_id:?}, which has no candidates" ); graph.add_edge( @@ -86,7 +86,7 @@ impl Problem { ); } else { for &candidate_id in candidates { - tracing::trace!("{package_id:?} requires {candidate_id:?}"); + tracing::info!("{package_id:?} requires {candidate_id:?}"); let candidate_node = Self::add_node(&mut graph, &mut nodes, candidate_id.into()); From a08a3add476d2bfcd64a93271d4379c90aab5100 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 12:14:08 +0200 Subject: [PATCH 09/11] Format Signed-off-by: Julien Jerphanion --- src/solver/cache.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/cache.rs b/src/solver/cache.rs index 62081cf..ee299d9 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -175,7 +175,7 @@ impl SolverCache { tracing::trace!( "Getting matching candidates for package: {:?}", - self.provider.display_name(package_name_id).to_string() + self.provider.display_name(package_name_id).to_string() ); let candidates = self.get_or_cache_candidates(package_name_id).await?; @@ -213,7 +213,7 @@ impl SolverCache { tracing::trace!( "Getting NON-matching candidates for package: {:?}", - self.provider.display_name(package_name_id).to_string() + self.provider.display_name(package_name_id).to_string() ); let candidates = self.get_or_cache_candidates(package_name_id).await?; @@ -257,7 +257,7 @@ impl SolverCache { let package_name_id = self.provider.version_set_name(version_set_id); tracing::trace!( "Getting sorted matching candidates for package: {:?}", - self.provider.display_name(package_name_id).to_string() + self.provider.display_name(package_name_id).to_string() ); let matching_candidates = self From a37a65a1fc702c423e243192da631443d64f2827 Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 16:39:58 +0200 Subject: [PATCH 10/11] Address review comments Signed-off-by: Julien Jerphanion Co-authored-by: Bas Zalmstra --- src/internal/id.rs | 6 ------ src/solver/cache.rs | 4 ++-- src/solver/mod.rs | 27 ++++----------------------- 3 files changed, 6 insertions(+), 31 deletions(-) diff --git a/src/internal/id.rs b/src/internal/id.rs index 48e78e8..1ebc041 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -60,12 +60,6 @@ impl ArenaId for VersionSetId { #[cfg_attr(feature = "serde", serde(transparent))] pub struct SolvableId(pub u32); -impl SolvableId { - pub(crate) const fn as_internal(self) -> InternalSolvableId { - InternalSolvableId(self.0 + 1) - } -} - /// Internally used id for solvables that can also represent root and null. #[repr(transparent)] #[derive(Copy, Clone, Eq, PartialEq, Hash, Debug, Ord, PartialOrd)] diff --git a/src/solver/cache.rs b/src/solver/cache.rs index ee299d9..cd4cc9b 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -174,8 +174,8 @@ impl SolverCache { let package_name_id = self.provider.version_set_name(version_set_id); tracing::trace!( - "Getting matching candidates for package: {:?}", - self.provider.display_name(package_name_id).to_string() + "Getting matching candidates for package: {}", + self.provider.display_name(package_name_id) ); let candidates = self.get_or_cache_candidates(package_name_id).await?; diff --git a/src/solver/mod.rs b/src/solver/mod.rs index b457ec6..44a62dd 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -199,7 +199,10 @@ impl Solver { tracing::trace!("Solvables found:"); for step in &steps { - tracing::trace!(" - {}", step.as_internal().display(self.provider())); + tracing::trace!( + " - {}", + InternalSolvableId::from(step.clone()).display(self.provider()) + ); } Ok(steps) @@ -987,8 +990,6 @@ impl Solver { /// solvable has become false, in which case it picks a new solvable to /// watch (if available) or triggers an assignment. fn propagate(&mut self, level: u32) -> Result<(), PropagationError> { - tracing::trace!("Propagate"); - if let Some(value) = self.provider().should_cancel_with_value() { return Err(PropagationError::Cancelled(value)); }; @@ -996,28 +997,13 @@ impl Solver { // Negative assertions derived from other rules (assertions are clauses that // consist of a single literal, and therefore do not have watches) for &(solvable_id, clause_id) in &self.negative_assertions { - tracing::trace!( - "Negative assertions derived from other rules: {} = false", - solvable_id.display(self.provider()) - ); - let value = false; let decided = self .decision_tracker .try_add_decision(Decision::new(solvable_id, value, clause_id), level) .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?; - tracing::trace!( - "Negative assertions derived from other rules: Decided: {}", - decided - ); - if decided { - tracing::trace!( - "├─ Propagate assertion {} = {}", - solvable_id.display(self.provider()), - value - ); tracing::trace!( "Negative assertions derived from other rules: Propagate assertion {} = {}", solvable_id.display(self.provider()), @@ -1067,11 +1053,6 @@ impl Solver { while let Some(decision) = self.decision_tracker.next_unpropagated() { let pkg = decision.solvable_id; - tracing::trace!( - "Exploring watched solvables for {}", - pkg.display(self.provider()) - ); - // Propagate, iterating through the linked list of clauses that watch this // solvable let mut old_predecessor_clause_id: Option; From 9edf75c9f540ba1b3cb3aec07fa8554c71ce93bf Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Thu, 18 Jul 2024 16:46:18 +0200 Subject: [PATCH 11/11] Use a dereference instead of a clone Signed-off-by: Julien Jerphanion --- src/solver/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 44a62dd..61fe85a 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -201,7 +201,7 @@ impl Solver { for step in &steps { tracing::trace!( " - {}", - InternalSolvableId::from(step.clone()).display(self.provider()) + InternalSolvableId::from(*step).display(self.provider()) ); }