chore: add diagnostics and segmented vector

.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

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"

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(), "   │        ├─ ");
+    }
+}

src/internal/mapping.rs

@@ -27,6 +27,16 @@ impl<TId: ArenaId, TValue> Mapping<TId, TValue> {
         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::<Option<TValue>>()
+    }
+
     /// 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);
@@ -60,7 +70,9 @@ impl<TId: ArenaId, TValue> Mapping<TId, TValue> {
                 .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
     }

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() {

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<bool> {
         self.map.value(solvable_id)

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<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
+    /// 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::<Clause>() + std::mem::size_of::<ClauseState>()))
+                    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);
+    }
+}