Skip to content

Commit

Permalink
chore: Add more tracing (prefix-dev#55)
Browse files Browse the repository at this point in the history 
Adds more tracing
  • Loading branch information
@jjerphan
jjerphan authored Jul 18, 2024
1 parent 8e47d5b commit 94169d7
Show file tree
Hide file tree
Showing 3 changed files with 125 additions and 34 deletions.
46 changes: 39 additions & 7 deletions src/solver/cache.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
);

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))
Expand All @@ -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))
Expand All @@ -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();
Expand Down
38 changes: 23 additions & 15 deletions src/solver/clause.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
)
}
}
Expand Down
75 changes: 63 additions & 12 deletions src/solver/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -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::{
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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| {
Expand All @@ -179,6 +197,14 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
})
.collect();

tracing::trace!("Solvables found:");
for step in &steps {
tracing::trace!(
" - {}",
InternalSolvableId::from(*step).display(self.provider())
);
}

Ok(steps)
}

Expand All @@ -196,6 +222,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,
Expand Down Expand Up @@ -311,7 +339,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),
);

Expand Down Expand Up @@ -371,7 +399,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)
);

Expand Down Expand Up @@ -443,7 +471,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),
Expand Down Expand Up @@ -523,6 +551,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}

tracing::trace!("Done adding clauses for solvables");

Ok(output)
}

Expand Down Expand Up @@ -554,6 +584,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 {
Expand All @@ -565,7 +601,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()),
Expand All @@ -578,15 +614,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(()) => {}
Expand All @@ -613,7 +654,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.
Expand All @@ -638,11 +681,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()
Expand All @@ -652,6 +700,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(
Expand All @@ -660,7 +709,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()));
}

Expand Down Expand Up @@ -707,6 +756,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 {
Expand Down Expand Up @@ -776,7 +827,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()),
Expand Down Expand Up @@ -813,7 +864,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())
Expand Down Expand Up @@ -954,7 +1005,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {

if decided {
tracing::trace!(
"├─ Propagate assertion {} = {}",
"Negative assertions derived from other rules: Propagate assertion {} = {}",
solvable_id.display(self.provider()),
value
);
Expand Down

0 comments on commit 94169d7

Please sign in to comment.