chore: Add more tracing

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)]

src/solver/cache.rs

@@ -171,14 +171,26 @@ impl<D: DependencyProvider> SolverCache<D> {
         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 candidates = self.get_or_cache_candidates(package_name).await?;
+                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()
+                );
+
+                let candidates = self.get_or_cache_candidates(package_name_id).await?;
+                tracing::trace!("Got {:?} matching candidates", candidates.candidates.len());
 
                 let matching_candidates = self
                     .provider
                     .filter_candidates(&candidates.candidates, version_set_id, false)
                     .await;
 
+                tracing::trace!(
+                    "Filtered {:?} matching candidates",
+                    matching_candidates.len()
+                );
+
                 Ok(self
                     .version_set_candidates
                     .insert(version_set_id, matching_candidates))
@@ -197,17 +209,32 @@ impl<D: DependencyProvider> SolverCache<D> {
         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 candidates = self.get_or_cache_candidates(package_name).await?;
+                let package_name_id = self.provider.version_set_name(version_set_id);
 
-                let matching_candidates = self
+                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::trace!(
+                    "Got {:?} NON-matching candidates",
+                    candidates.candidates.len()
+                );
+
+                let matching_candidates: Vec<SolvableId> = self
                     .provider
                     .filter_candidates(&candidates.candidates, version_set_id, true)
                     .await
                     .into_iter()
                     .map(Into::into)
                     .collect();
 
+                tracing::trace!(
+                    "Filtered {:?} matching candidates",
+                    matching_candidates.len()
+                );
+
                 Ok(self
                     .version_set_inverse_candidates
                     .insert(version_set_id, matching_candidates))
@@ -227,11 +254,16 @@ impl<D: DependencyProvider> SolverCache<D> {
         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::trace!(
+                    "Getting sorted matching candidates for package: {:?}",
+                    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();

src/solver/clause.rs

@@ -611,48 +611,56 @@ 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: {}",
+                    "Excluded({}({:?}), {})",
                     solvable_id.display(self.interner),
+                    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 {} {}",
+                    "Requires({}({:?}), {})",
                     solvable_id.display(self.interner),
-                    self.interner
-                        .display_name(self.interner.version_set_name(version_set_id)),
+                    solvable_id,
                     self.interner.display_version_set(version_set_id)
                 )
             }
             Clause::Constrains(s1, s2, version_set_id) => {
                 write!(
                     f,
-                    "{} excludes {} by {}",
+                    "Constrains({}({:?}), {}({:?}), {})",
                     s1.display(self.interner),
+                    s1,
                     s2.display(self.interner),
-                    self.interner.display_version_set(version_set_id),
+                    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.display(self.interner),
+                    s1,
+                    s2.display(self.interner),
+                    s2,
+                    self.interner.display_name(name)
                 )
             }
-            Clause::ForbidMultipleInstances(_, _, name_id) => {
+            Clause::Lock(locked, other) => {
                 write!(
                     f,
-                    "only one {} allowed",
-                    self.interner.display_name(name_id)
+                    "Lock({}({:?}), {}({:?}))",
+                    locked.display(self.interner),
+                    locked,
+                    other.display(self.interner),
+                    other,
                 )
             }
         }

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::{
@@ -106,11 +106,29 @@ impl From<Box<dyn Any>> for UnsolvableOrCancelled {
 }
 
 /// An error during the propagation step
+#[derive(Debug)]
 pub(crate) enum PropagationError {
     Conflict(InternalSolvableId, bool, ClauseId),
     Cancelled(Box<dyn Any>),
 }
 
+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<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     /// Returns the dependency provider used by this instance.
     pub fn provider(&self) -> &D {
@@ -166,7 +184,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         // Run SAT
         self.run_sat()?;
 
-        let steps = self
+        let steps: Vec<SolvableId> = self
             .decision_tracker
             .stack()
             .filter_map(|d| {
@@ -179,6 +197,11 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             })
             .collect();
 
+        tracing::trace!("Solvables found:");
+        for step in &steps {
+            tracing::trace!(" - {}", step.as_internal().display(self.provider()));
+        }
+
         Ok(steps)
     }
 
@@ -196,6 +219,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     ) -> Result<AddClauseOutput, Box<dyn Any>> {
         let mut output = AddClauseOutput::default();
 
+        tracing::trace!("Add clauses for solvables");
+
         pub enum TaskResult<'i> {
             Dependencies {
                 solvable_id: InternalSolvableId,
@@ -311,7 +336,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                         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 '{}'",
+                                "┝━ Adding clauses for package '{}'",
                                 self.provider().display_name(dependency_name),
                             );
 
@@ -371,7 +396,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 } => {
                     // Get the solvable information and request its requirements and constraints
                     tracing::trace!(
-                        "package candidates available for {}",
+                        "Package candidates available for {}",
                         self.provider().display_name(name_id)
                     );
 
@@ -443,7 +468,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                     candidates,
                 } => {
                     tracing::trace!(
-                        "sorted candidates available for {} {}",
+                        "Sorted candidates available for {} {}",
                         self.provider()
                             .display_name(self.provider().version_set_name(version_set_id)),
                         self.provider().display_version_set(version_set_id),
@@ -523,6 +548,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             }
         }
 
+        tracing::trace!("Done adding clauses for solvables");
+
         Ok(output)
     }
 
@@ -554,6 +581,12 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         let mut level = 0;
 
         loop {
+            if level == 0 {
+                tracing::trace!("Level 0: 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 {
@@ -565,7 +598,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                 // 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 <root> at level {level}",);
+                tracing::trace!("╤══ Install <root> at level {level}",);
                 self.decision_tracker
                     .try_add_decision(
                         Decision::new(InternalSolvableId::root(), true, ClauseId::install_root()),
@@ -578,15 +611,20 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                     .async_runtime
                     .block_on(self.add_clauses_for_solvables(vec![InternalSolvableId::root()]))?;
                 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),
                     ));
                 }
             }
 
+            tracing::trace!("Level {}: Propagating", level);
+
             // Propagate decisions from assignments above
             let propagate_result = self.propagate(level);
 
+            tracing::trace!("Propagate result: {:?}", propagate_result);
+
             // Handle propagation errors
             match propagate_result {
                 Ok(()) => {}
@@ -613,7 +651,9 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
 
             // Enter the solver loop, return immediately if no new assignments have been
             // made.
+            tracing::trace!("Level {}: Resolving dependencies", level);
             level = self.resolve_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.
@@ -638,11 +678,16 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
 
             if new_solvables.is_empty() {
                 // If no new literals were selected this solution is complete and we can return.
+                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()
@@ -652,6 +697,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                         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(
@@ -660,7 +706,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
 
             // 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()));
             }
 
@@ -707,6 +753,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     /// it was provided by the user, and set its value to true.
     fn resolve_dependencies(&mut self, mut level: u32) -> Result<u32, UnsolvableOrCancelled> {
         loop {
+            tracing::trace!("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 {
@@ -776,7 +824,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         }
 
         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()),
@@ -813,7 +861,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     ) -> Result<u32, UnsolvableOrCancelled> {
         level += 1;
 
-        tracing::info!(
+        tracing::trace!(
             "╤══ Install {} at level {level} (required by {})",
             solvable.display(self.provider()),
             required_by.display(self.provider())
@@ -939,25 +987,42 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
     /// 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));
         };
 
         // 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()),
+                    value
+                );
             }
         }
 
@@ -1002,6 +1067,11 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         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<ClauseId>;