From 2107341a6e83a036383a8e78ded5433f7cf9fe3b Mon Sep 17 00:00:00 2001 From: Julien Jerphanion Date: Wed, 17 Jul 2024 16:27:43 +0200 Subject: [PATCH] chore: Add more tracing Signed-off-by: Julien Jerphanion --- build.sh | 31 +++++++++++++ src/internal/id.rs | 6 +++ src/solver/cache.rs | 32 ++++++++++++- src/solver/clause.rs | 39 +++++++--------- src/solver/mod.rs | 104 +++++++++++++++++++++++++++++++++++++++++-- 5 files changed, 186 insertions(+), 26 deletions(-) create mode 100755 build.sh diff --git a/build.sh b/build.sh new file mode 100755 index 0000000..06ee6ee --- /dev/null +++ b/build.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +set -euxo pipefail + +export PREFIX=/home/jjerphan/.local/miniforge3/envs/mamba +export BUILD_PREFIX=$PREFIX +export CARGO_BUILD_TARGET=x86_64-unknown-linux-gnu + +cmake -B build \ + -GNinja \ + -DRust_CARGO_TARGET=${CARGO_BUILD_TARGET} \ + -DCMAKE_AR=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-ar \ + -DCMAKE_CXX_COMPILER_AR=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-gcc-ar \ + -DCMAKE_C_COMPILER_AR=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-gcc-ar \ + -DCMAKE_RANLIB=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-ranlib \ + -DCMAKE_CXX_COMPILER_RANLIB=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-gcc-ranlib \ + -DCMAKE_C_COMPILER_RANLIB=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-gcc-ranlib \ + -DCMAKE_LINKER=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-ld \ + -DCMAKE_STRIP=$BUILD_PREFIX/bin/x86_64-conda-linux-gnu-strip \ + -DCMAKE_BUILD_TYPE=Debug \ + -DCMAKE_FIND_ROOT_PATH_MODE_PROGRAM=NEVER \ + -DCMAKE_FIND_ROOT_PATH_MODE_LIBRARY=ONLY \ + -DCMAKE_FIND_ROOT_PATH_MODE_INCLUDE=ONLY \ + -DCMAKE_FIND_ROOT_PATH="$PREFIX;$BUILD_PREFIX/x86_64-conda-linux-gnu/sysroot" \ + -DCMAKE_INSTALL_PREFIX=$PREFIX \ + -DCMAKE_INSTALL_LIBDIR=lib \ + -DCMAKE_PROGRAM_PATH="$BUILD_PREFIX/bin;$PREFIX/bin" \ + -DRust_CARGO_TARGET=${CARGO_BUILD_TARGET} + +cd build +ninja install 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;