From 1fbaff044d3f0d30f7486087e8416247ecfcad7e Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Thu, 28 Nov 2024 10:02:17 +0100 Subject: [PATCH 1/3] chore: add diagnostics and segmented vector --- .github/workflows/rust-compile.yml | 6 +- Cargo.lock | 37 +++++++++++ Cargo.toml | 12 +++- src/conflict.rs | 72 +++++++++++----------- src/solver/decision_map.rs | 5 ++ src/solver/decision_tracker.rs | 5 ++ src/solver/diagnostics.rs | 99 ++++++++++++++++++++++++++++++ src/solver/mod.rs | 70 ++++++++++++--------- src/solver/watch_map.rs | 10 +++ tests/solver.rs | 8 +-- 10 files changed, 248 insertions(+), 76 deletions(-) create mode 100644 src/solver/diagnostics.rs diff --git a/.github/workflows/rust-compile.yml b/.github/workflows/rust-compile.yml index 07fb9da..56d1c27 100644 --- a/.github/workflows/rust-compile.yml +++ b/.github/workflows/rust-compile.yml @@ -40,7 +40,7 @@ jobs: - name: Run rustfmt uses: actions-rust-lang/rustfmt@v1 - name: Run clippy - run: cargo clippy --workspace + run: cargo clippy --workspace --all-features test: name: Test @@ -54,6 +54,6 @@ jobs: with: components: rustfmt - name: Build - run: cargo build + run: cargo build --all-features - name: Run tests - run: cargo test --workspace -- --nocapture + run: cargo test --workspace --all-features -- --nocapture diff --git a/Cargo.lock b/Cargo.lock index a2901e4..56971d3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -686,6 +686,12 @@ version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" +[[package]] +name = "human_bytes" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "91f255a4535024abf7640cb288260811fc14794f62b063652ed349f9a6c2348e" + [[package]] name = "indexmap" version = "2.2.6" @@ -846,6 +852,15 @@ dependencies = [ "winapi", ] +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + [[package]] name = "num-traits" version = "0.2.19" @@ -1096,14 +1111,17 @@ dependencies = [ "elsa", "event-listener 5.3.1", "futures", + "human_bytes", "indexmap", "insta", "itertools", "petgraph", "proptest", "resolvo", + "segvec", "serde", "serde_json", + "tabwriter", "tokio", "tracing", "tracing-test", @@ -1170,6 +1188,16 @@ version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" +[[package]] +name = "segvec" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c3ab3d9bc0d11482ed0019aa9c2cee94a0b4890a0eb21ce2153d88b1816f877" +dependencies = [ + "either", + "num-integer", +] + [[package]] name = "serde" version = "1.0.203" @@ -1287,6 +1315,15 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tabwriter" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a327282c4f64f6dc37e3bba4c2b6842cc3a992f204fa58d917696a89f691e5f6" +dependencies = [ + "unicode-width", +] + [[package]] name = "tap" version = "1.0.1" diff --git a/Cargo.toml b/Cargo.toml index 54905b0..00d791b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,13 +11,13 @@ license = "BSD-3-Clause" edition = "2021" readme = "README.md" keywords = ["dependency", "solver", "version"] -categories= ["algorithms"] +categories = ["algorithms"] [package] name = "resolvo" version.workspace = true authors.workspace = true -description= "Fast package resolver written in Rust (CDCL based SAT solving)" +description = "Fast package resolver written in Rust (CDCL based SAT solving)" keywords.workspace = true categories.workspace = true homepage.workspace = true @@ -26,6 +26,9 @@ license.workspace = true edition.workspace = true readme.workspace = true +[features] +diagnostics = ["tabwriter", "human_bytes"] + [dependencies] ahash = "0.8.11" itertools = "0.13" @@ -40,6 +43,11 @@ indexmap = "2" tokio = { version = "1.37", features = ["rt"], optional = true } async-std = { version = "1.12", default-features = false, features = ["alloc", "default"], optional = true } version-ranges = { version = "0.1.0", optional = true } +segvec = { version = "0.2.0" } + +# Dependencies for the diagnostics feature +tabwriter = { version = "1.4.0", optional = true } +human_bytes = { version = "0.4.3", optional = true } [dev-dependencies] insta = "1.39.0" diff --git a/src/conflict.rs b/src/conflict.rs index edad5e9..10b7ffb 100644 --- a/src/conflict.rs +++ b/src/conflict.rs @@ -588,42 +588,6 @@ impl Indenter { } } -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_indenter_without_top_level_indent() { - let indenter = Indenter::new(false); - - let indenter = indenter.push_level_with_order(ChildOrder::Last); - assert_eq!(indenter.get_indent(), ""); - - let indenter = indenter.push_level_with_order(ChildOrder::Last); - assert_eq!(indenter.get_indent(), "└─ "); - } - - #[test] - fn test_indenter_with_multiple_siblings() { - let indenter = Indenter::new(true); - - let indenter = indenter.push_level_with_order(ChildOrder::Last); - assert_eq!(indenter.get_indent(), "└─ "); - - let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings); - assert_eq!(indenter.get_indent(), " ├─ "); - - let indenter = indenter.push_level_with_order(ChildOrder::Last); - assert_eq!(indenter.get_indent(), " │ └─ "); - - let indenter = indenter.push_level_with_order(ChildOrder::Last); - assert_eq!(indenter.get_indent(), " │ └─ "); - - let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings); - assert_eq!(indenter.get_indent(), " │ ├─ "); - } -} - /// A struct implementing [`fmt::Display`] that generates a user-friendly /// representation of a conflict graph pub struct DisplayUnsat<'i, I: Interner> { @@ -1012,3 +976,39 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> { Ok(()) } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_indenter_without_top_level_indent() { + let indenter = Indenter::new(false); + + let indenter = indenter.push_level_with_order(ChildOrder::Last); + assert_eq!(indenter.get_indent(), ""); + + let indenter = indenter.push_level_with_order(ChildOrder::Last); + assert_eq!(indenter.get_indent(), "└─ "); + } + + #[test] + fn test_indenter_with_multiple_siblings() { + let indenter = Indenter::new(true); + + let indenter = indenter.push_level_with_order(ChildOrder::Last); + assert_eq!(indenter.get_indent(), "└─ "); + + let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings); + assert_eq!(indenter.get_indent(), " ├─ "); + + let indenter = indenter.push_level_with_order(ChildOrder::Last); + assert_eq!(indenter.get_indent(), " │ └─ "); + + let indenter = indenter.push_level_with_order(ChildOrder::Last); + assert_eq!(indenter.get_indent(), " │ └─ "); + + let indenter = indenter.push_level_with_order(ChildOrder::HasRemainingSiblings); + assert_eq!(indenter.get_indent(), " │ ├─ "); + } +} diff --git a/src/solver/decision_map.rs b/src/solver/decision_map.rs index 5522e74..b648a8e 100644 --- a/src/solver/decision_map.rs +++ b/src/solver/decision_map.rs @@ -47,6 +47,11 @@ impl DecisionMap { } } + #[cfg(feature = "diagnostics")] + pub fn len(&self) -> usize { + self.map.len() + } + pub fn reset(&mut self, solvable_id: InternalSolvableId) { let solvable_id = solvable_id.to_usize(); if solvable_id < self.map.len() { diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs index 23995d3..cdffdaf 100644 --- a/src/solver/decision_tracker.rs +++ b/src/solver/decision_tracker.rs @@ -27,6 +27,11 @@ impl DecisionTracker { self.propagate_index = 0; } + #[cfg(feature = "diagnostics")] + pub(crate) fn len(&self) -> usize { + self.map.len() + } + #[inline(always)] pub(crate) fn assigned_value(&self, solvable_id: InternalSolvableId) -> Option { self.map.value(solvable_id) diff --git a/src/solver/diagnostics.rs b/src/solver/diagnostics.rs new file mode 100644 index 0000000..6efcc72 --- /dev/null +++ b/src/solver/diagnostics.rs @@ -0,0 +1,99 @@ +use std::io::Write; + +use ahash::HashMap; +use itertools::Itertools; + +use crate::{ + runtime::AsyncRuntime, + solver::clause::{Clause, ClauseState}, + DependencyProvider, Solver, +}; + +impl Solver { + /// Reports diagnostics about the current state of the solver. + pub(crate) fn report_diagnostics(&self) { + let mut forbid_clauses_by_name = HashMap::default(); + let mut forbid_clauses = 0usize; + let mut requires_clauses = 0usize; + let mut locked_clauses = 0usize; + let mut learned_clauses = 0usize; + let mut constrains_clauses = 0usize; + let clauses = self.clauses.kinds.borrow(); + for clause in clauses.iter() { + match clause { + Clause::ForbidMultipleInstances(_a, _b, name_id) => { + let count = forbid_clauses_by_name.entry(name_id).or_insert(0usize); + *count += 1; + forbid_clauses += 1; + } + Clause::Requires(..) => { + requires_clauses += 1; + } + Clause::Lock(..) => { + locked_clauses += 1; + } + Clause::Learnt(..) => { + learned_clauses += 1; + } + Clause::Constrains(..) => { + constrains_clauses += 1; + } + _ => {} + } + } + + let mut writer = tabwriter::TabWriter::new(Vec::new()); + writeln!( + writer, + "Total number of solvables:\t{}", + self.decision_tracker.len() + ) + .unwrap(); + writeln!( + writer, + "Total number of watches:\t{} ({})", + self.watches.len(), + human_bytes::human_bytes(self.watches.size_in_bytes() as f64) + ) + .unwrap(); + writeln!( + writer, + "Total number of clauses:\t{} ({})", + clauses.len(), + human_bytes::human_bytes( + (clauses.len() + * (std::mem::size_of::() + std::mem::size_of::())) + as f64 + ) + ) + .unwrap(); + writeln!(writer, "- Requires:\t{}", requires_clauses).unwrap(); + writeln!(writer, "- Constrains:\t{}", constrains_clauses).unwrap(); + writeln!(writer, "- Lock:\t{}", locked_clauses).unwrap(); + writeln!(writer, "- Learned:\t{}", learned_clauses).unwrap(); + writeln!(writer, "- ForbidMultiple:\t{}", forbid_clauses).unwrap(); + + for (name_id, count) in forbid_clauses_by_name + .iter() + .sorted_by_key(|(_, count)| **count) + .rev() + .take(5) + { + writeln!( + writer, + " - {}:\t{}", + self.provider().display_name(**name_id), + count + ) + .unwrap(); + } + + if forbid_clauses_by_name.len() > 5 { + writeln!(writer, " ...").unwrap(); + } + + let report = String::from_utf8(writer.into_inner().unwrap()).unwrap(); + + tracing::info!("Solver diagnostics:\n{}", report); + } +} diff --git a/src/solver/mod.rs b/src/solver/mod.rs index c01997d..d83fb85 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -8,6 +8,7 @@ use decision_tracker::DecisionTracker; use futures::{stream::FuturesUnordered, FutureExt, StreamExt}; use indexmap::{IndexMap, IndexSet}; use itertools::Itertools; +use segvec::{Linear, MemConfig, SegVec}; use watch_map::WatchMap; use crate::{ @@ -26,6 +27,8 @@ pub(crate) mod clause; mod decision; mod decision_map; mod decision_tracker; +#[cfg(feature = "diagnostics")] +mod diagnostics; mod watch_map; #[derive(Default)] @@ -123,8 +126,8 @@ impl> Problem { #[derive(Default)] pub(crate) struct Clauses { - pub(crate) kinds: RefCell>, - states: RefCell>, + pub(crate) kinds: RefCell>>, + states: RefCell>>, } impl Clauses { @@ -356,6 +359,9 @@ impl Solver { } } + #[cfg(feature = "diagnostics")] + self.report_diagnostics(); + Ok(self.chosen_solvables().collect()) } @@ -995,7 +1001,7 @@ impl Solver { break; }; - tracing::info!( + tracing::debug!( "╒══ Install {} at level {level} (derived from {})", candidate.display(self.provider()), self.clauses.kinds.borrow()[clause_id.to_usize()].display(self.provider()) @@ -1005,14 +1011,14 @@ impl Solver { match self.set_propagate_learn(level, candidate, required_by, clause_id) { Ok(new_level) => { level = new_level; - tracing::info!("╘══ Propagation completed"); + tracing::debug!("╘══ Propagation completed"); } Err(UnsolvableOrCancelled::Cancelled(value)) => { - tracing::info!("╘══ Propagation cancelled"); + tracing::debug!("╘══ Propagation cancelled"); return Err(UnsolvableOrCancelled::Cancelled(value)); } Err(UnsolvableOrCancelled::Unsolvable(conflict)) => { - tracing::info!("╘══ Propagation resulted in a conflict"); + tracing::debug!("╘══ Propagation resulted in a conflict"); return Err(UnsolvableOrCancelled::Unsolvable(conflict)); } } @@ -1288,16 +1294,16 @@ impl Solver { conflicting_clause: ClauseId, ) -> Result { { - tracing::info!( + tracing::debug!( "├┬ Propagation conflicted: could not set {solvable} to {attempted_value}", solvable = conflicting_solvable.display(self.provider()), ); - tracing::info!( + tracing::debug!( "││ During unit propagation for clause: {}", self.clauses.kinds.borrow()[conflicting_clause.to_usize()].display(self.provider()) ); - tracing::info!( + tracing::debug!( "││ Previously decided value: {}. Derived from: {}", !attempted_value, self.clauses.kinds.borrow()[self @@ -1321,7 +1327,7 @@ impl Solver { continue; } - tracing::info!( + tracing::debug!( "* ({level}) {action} {}. Reason: {}", decision.solvable_id.display(self.provider()), self.clauses.kinds.borrow()[decision.derived_from.to_usize()] @@ -1346,12 +1352,12 @@ impl Solver { level, ) .expect("bug: solvable was already decided!"); - tracing::debug!( + tracing::trace!( "│├ Propagate after learn: {} = {decision}", literal.solvable_id().display(self.provider()), ); - tracing::info!("│└ Backtracked from {old_level} -> {level}"); + tracing::debug!("│└ Backtracked from {old_level} -> {level}"); Ok(level) } @@ -1446,20 +1452,24 @@ impl Solver { ); // Get mutable access to both clauses. - let (predecessor_clause_state, clause_state) = - if let Some(prev_clause_id) = predecessor_clause_id { - let prev_idx = prev_clause_id.to_usize(); - let current_idx = clause_id.to_usize(); - if prev_idx < current_idx { - let (left, right) = clause_states.split_at_mut(current_idx); - (Some(&mut left[prev_idx]), &mut right[0]) - } else { - let (left, right) = clause_states.split_at_mut(prev_idx); - (Some(&mut right[0]), &mut left[current_idx]) - } - } else { - (None, &mut clause_states[clause_id.to_usize()]) - }; + let (predecessor_clause_state, clause_state) = if let Some(prev_clause_id) = + predecessor_clause_id + { + let prev_idx = prev_clause_id.to_usize(); + let current_idx = clause_id.to_usize(); + assert_ne!(prev_idx, current_idx); + // SAFETY: This is safe because we guarentee that `prev_idx` and `current_idx` + // are different. + unsafe { + let clause_states_ptr = + std::ops::DerefMut::deref_mut(&mut clause_states) as *mut SegVec<_, _>; + let prev_clause_state = &mut (*clause_states_ptr)[prev_idx]; + let current_clause_state = &mut (*clause_states_ptr)[current_idx]; + (Some(prev_clause_state), current_clause_state) + } + } else { + (None, &mut clause_states[clause_id.to_usize()]) + }; // Update the prev_clause_id for the next run old_predecessor_clause_id = predecessor_clause_id; @@ -1545,7 +1555,7 @@ impl Solver { // Skip logging for ForbidMultipleInstances, which is so noisy Clause::ForbidMultipleInstances(..) => {} _ => { - tracing::debug!( + tracing::trace!( "├ Propagate {} = {}. {}", remaining_watch.solvable_id().display(self.provider()), remaining_watch.satisfying_value(), @@ -1565,8 +1575,8 @@ impl Solver { /// /// Because learnt clauses are not relevant for the user, they are not added /// to the [`Conflict`]. Instead, we report the clauses that caused them. - fn analyze_unsolvable_clause( - clauses: &[Clause], + fn analyze_unsolvable_clause( + clauses: &SegVec, learnt_why: &Mapping>, clause_id: ClauseId, conflict: &mut Conflict, @@ -1599,7 +1609,7 @@ impl Solver { let mut conflict = Conflict::default(); - tracing::info!("=== ANALYZE UNSOLVABLE"); + tracing::debug!("=== ANALYZE UNSOLVABLE"); let mut involved = HashSet::default(); self.clauses.kinds.borrow()[clause_id.to_usize()].visit_literals( diff --git a/src/solver/watch_map.rs b/src/solver/watch_map.rs index 698aaf9..ac78905 100644 --- a/src/solver/watch_map.rs +++ b/src/solver/watch_map.rs @@ -18,6 +18,16 @@ impl WatchMap { } } + #[cfg(feature = "diagnostics")] + pub fn len(&self) -> usize { + self.map.len() + } + + #[cfg(feature = "diagnostics")] + pub fn size_in_bytes(&self) -> usize { + self.len() * std::mem::size_of::<(Literal, ClauseId)>() + } + pub(crate) fn start_watching(&mut self, clause: &mut ClauseState, clause_id: ClauseId) { for (watch_index, watched_literal) in clause.watched_literals.into_iter().enumerate() { let already_watching = self diff --git a/tests/solver.rs b/tests/solver.rs index 389c1c9..40cea16 100644 --- a/tests/solver.rs +++ b/tests/solver.rs @@ -123,9 +123,7 @@ impl Spec { pub fn parse_union( spec: &str, ) -> impl Iterator::Err>> + '_ { - spec.split('|') - .map(str::trim) - .map(|dep| Spec::from_str(dep)) + spec.split('|').map(str::trim).map(Spec::from_str) } } @@ -386,7 +384,7 @@ impl DependencyProvider for BundleBoxProvider { candidates .iter() .copied() - .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) == !inverse) + .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) != inverse) .collect() } @@ -538,7 +536,7 @@ impl DependencyProvider for BundleBoxProvider { } /// Create a string from a [`Transaction`] -fn transaction_to_string(interner: &impl Interner, solvables: &Vec) -> String { +fn transaction_to_string(interner: &impl Interner, solvables: &[SolvableId]) -> String { use std::fmt::Write; let mut buf = String::new(); for solvable in solvables From 33e0686eaee0bfedbef0eea7046edb6a6a72cc04 Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Thu, 28 Nov 2024 10:11:35 +0100 Subject: [PATCH 2/3] fix: number of watches reported was way to high --- src/internal/mapping.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/internal/mapping.rs b/src/internal/mapping.rs index 26df86b..4655be0 100644 --- a/src/internal/mapping.rs +++ b/src/internal/mapping.rs @@ -60,7 +60,9 @@ impl Mapping { .resize_with(chunk + 1, || std::array::from_fn(|_| None)); } let previous_value = self.chunks[chunk][offset].replace(value); - self.len += 1; + if previous_value.is_none() { + self.len += 1; + } self.max = self.max.max(idx); previous_value } From 63b9d0a2d7d543b8eeee7561798ced7c308095ac Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Thu, 28 Nov 2024 10:25:16 +0100 Subject: [PATCH 3/3] fix: watch map incorrectly reported size --- src/internal/mapping.rs | 10 ++++++++++ src/solver/watch_map.rs | 5 ++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/internal/mapping.rs b/src/internal/mapping.rs index 4655be0..6f52391 100644 --- a/src/internal/mapping.rs +++ b/src/internal/mapping.rs @@ -27,6 +27,16 @@ impl Mapping { Self::with_capacity(1) } + /// Returns the total number of values that can be stored in the mapping without reallocating. + pub fn capacity(&self) -> usize { + self.chunks.len() * VALUES_PER_CHUNK + } + + /// Returns the total number of bytes allocated by this instance. + pub fn size_in_bytes(&self) -> usize { + self.capacity() * std::mem::size_of::>() + } + /// Constructs a new arena with a capacity for `n` values pre-allocated. pub fn with_capacity(n: usize) -> Self { let n = cmp::max(1, n); diff --git a/src/solver/watch_map.rs b/src/solver/watch_map.rs index ac78905..1ea6564 100644 --- a/src/solver/watch_map.rs +++ b/src/solver/watch_map.rs @@ -1,7 +1,6 @@ -use crate::solver::clause::Literal; use crate::{ internal::{id::ClauseId, mapping::Mapping}, - solver::clause::ClauseState, + solver::clause::{ClauseState, Literal}, }; /// A map from solvables to the clauses that are watching them @@ -25,7 +24,7 @@ impl WatchMap { #[cfg(feature = "diagnostics")] pub fn size_in_bytes(&self) -> usize { - self.len() * std::mem::size_of::<(Literal, ClauseId)>() + self.map.size_in_bytes() } pub(crate) fn start_watching(&mut self, clause: &mut ClauseState, clause_id: ClauseId) {