Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: Add more tracing #55

Merged
merged 11 commits into from
Jul 18, 2024
Merged

chore: Add more tracing #55

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
ae6c794
chore: Add more tracing
jjerphan Jul 17, 2024
4434ca3
Replace some `info!`, `debug!` with `trace!`
jjerphan Jul 17, 2024
767c25f
Improve display of solvables
jjerphan Jul 18, 2024
5e10522
Remove the implementation of the Display trait for ClauseId
jjerphan Jul 18, 2024
7dc5346
Display name of package
jjerphan Jul 18, 2024
fdc4765
Remove the implementation of the Display trait for AddClauseOutput
jjerphan Jul 18, 2024
801bb6f
Use trace! over debug!
jjerphan Jul 18, 2024
7eef3fe
Revert changes and use info! for previous tracing
jjerphan Jul 18, 2024
a08a3ad
Format
jjerphan Jul 18, 2024
a37a65a
Address review comments
jjerphan Jul 18, 2024
9edf75c
Use a dereference instead of a clone
jjerphan Jul 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 39 additions & 7 deletions src/solver/cache.rs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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