smt_scope/analysis/
misc.rs

1use crate::{
2    items::{QuantIdx, QuantPatVec},
3    Z3Parser,
4};
5
6pub struct LogInfo {
7    pub match_: MatchesInfo,
8    pub inst: InstsInfo,
9    pub quants: QuantsInfo,
10}
11
12#[derive(Default, Clone, Copy)]
13/// Counts of different match-line kinds. Essentially how many instantiations
14/// were from each of the different categories.
15pub struct MatchesInfo {
16    pub mbqi: usize,
17    pub theory_solving: usize,
18    pub axioms: usize,
19    pub quantifiers: usize,
20}
21
22#[derive(Default, Clone, Copy)]
23/// Counts of different instantiation stats.
24pub struct InstsInfo {
25    pub insts: usize,
26    pub enodes: usize,
27    pub geqs: usize,
28    pub treqs: usize,
29    pub geqs_trivial: usize,
30    pub treqs_error: usize,
31    pub proofs: usize,
32    /// Proof nodes which are not trivial and not QI related
33    pub proofs_nt_nq: usize,
34    pub cdcls: usize,
35}
36
37impl InstsInfo {
38    pub fn total(&self) -> usize {
39        self.enodes + self.geqs + self.treqs + self.insts
40    }
41    pub fn geqs_nontrivial(&self) -> usize {
42        self.geqs - self.geqs_trivial
43    }
44    pub fn treqs_nontrivial(&self) -> usize {
45        self.treqs
46    }
47
48    pub fn new(parser: &Z3Parser) -> Self {
49        let equalities = &parser.egraph.equalities;
50        let geqs_trivial = equalities.given.iter().filter(|eq| eq.is_trivial()).count();
51        let treqs_error = equalities
52            .transitive
53            .iter()
54            .filter(|eq| eq.given_len.is_none())
55            .count();
56        let proofs = parser.proofs().iter();
57        Self {
58            insts: parser.instantiations().len(),
59            enodes: parser.egraph.enodes.len(),
60            geqs: equalities.given.len(),
61            treqs: equalities.transitive.len(),
62            geqs_trivial,
63            treqs_error,
64            proofs: parser.proofs().len(),
65            proofs_nt_nq: proofs
66                .filter(|p| !p.kind.is_quant_inst() && !p.kind.is_trivial())
67                .count(),
68            cdcls: parser.cdcls().len(),
69        }
70    }
71}
72
73/// How many times each quantifier was instantiated
74pub struct QuantsInfo(pub QuantPatVec<usize>);
75
76impl LogInfo {
77    pub fn new(parser: &Z3Parser) -> Self {
78        let mut quants = QuantsInfo(parser.new_quant_pat_vec(|_| 0));
79        let mut match_ = MatchesInfo::default();
80        for data in parser.instantiations_data() {
81            if let Some(qpat) = data.match_.kind.quant_pat() {
82                quants.0[qpat] += 1;
83            }
84            use crate::items::MatchKind::*;
85            match &data.match_.kind {
86                MBQI { .. } => match_.mbqi += 1,
87                TheorySolving { .. } => match_.theory_solving += 1,
88                Axiom { .. } => match_.axioms += 1,
89                Quantifier { .. } => match_.quantifiers += 1,
90            }
91        }
92        let inst = InstsInfo::new(parser);
93
94        Self {
95            match_,
96            inst,
97            quants,
98        }
99    }
100
101    pub fn quants_iter(&self) -> impl Iterator<Item = (QuantIdx, usize)> + '_ {
102        self.quants
103            .0
104             .0
105            .iter_enumerated()
106            .map(|(i, count)| (i, count.iter_enumerated().map(|(_, c)| c).sum()))
107    }
108
109    pub fn quant_insts(&self, qidx: QuantIdx) -> usize {
110        self.quants.0 .0[qidx]
111            .iter_enumerated()
112            .map(|(_, c)| *c)
113            .sum()
114    }
115}
smt_scope/analysis/misc.rs

smt_scope/analysis/
misc.rs
