resolvo 0.10.2

Fast package resolver written in Rust (CDCL based SAT solving)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

use std::io::Write;

use ahash::HashMap;
use itertools::Itertools;

use crate::{
    DependencyProvider, Solver,
    runtime::AsyncRuntime,
    solver::clause::{Clause, WatchedLiterals},
};

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.state.clauses.kinds;
        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.state.decision_tracker.len()
        )
        .unwrap();
        writeln!(
            writer,
            "Total number of watches:\t{} ({})",
            self.state.watches.len(),
            human_bytes::human_bytes(self.state.watches.size_in_bytes() as f64)
        )
        .unwrap();
        writeln!(
            writer,
            "Total number of variables:\t{} ({})",
            self.state.variable_map.count(),
            human_bytes::human_bytes(self.state.variable_map.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::<WatchedLiterals>()))
                    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);
    }
}