smt_scope/analysis/
redundancy.rs

1use crate::{
2    items::{Blame, ENodeIdx, InstIdx, QuantPatVec, TermIdx},
3    FxHashMap, Z3Parser,
4};
5
6pub struct RedundancyAnalysis {
7    pub per_quant: QuantPatVec<QuantRedundancy>,
8}
9
10impl RedundancyAnalysis {
11    pub fn new(parser: &Z3Parser) -> Self {
12        let mut per_quant = parser.new_quant_pat_vec(|_| QuantRedundancy::default());
13        for data in parser.instantiations_data() {
14            let Some(qpat) = data.match_.kind.quant_pat() else {
15                continue;
16            };
17            let bound_terms = data.match_.kind.bound_terms(Ok, Err);
18            let quant = &mut per_quant[qpat];
19            let duplicates = quant.duplicates.entry(bound_terms).or_default();
20            duplicates.push(data.iidx);
21
22            if duplicates.len() > 1
23                || parser
24                    .get_pattern(qpat)
25                    .is_some_and(|p| parser[p].child_ids.len() <= 1)
26            {
27                continue;
28            }
29            for blame in data.match_.pattern_matches() {
30                let blame = blame.clone();
31                let sd = quant.sub_duplicates.entry(blame).or_default();
32                *sd += 1;
33            }
34        }
35        Self { per_quant }
36    }
37}
38
39#[derive(Debug, Default)]
40pub struct QuantRedundancy {
41    pub duplicates: FxHashMap<Box<[Result<ENodeIdx, TermIdx>]>, Vec<InstIdx>>,
42    pub sub_duplicates: FxHashMap<Blame, u32>,
43}
44
45impl QuantRedundancy {
46    pub fn redundant_count(&self) -> u32 {
47        self.duplicates.values().map(|v| v.len() as u32 - 1).sum()
48    }
49    pub fn redundant_ratio(&self) -> f64 {
50        let rc = self.redundant_count();
51        let total = rc + self.duplicates.len() as u32;
52        if total == 0 {
53            return 0.0;
54        }
55        rc as f64 / total as f64
56    }
57
58    pub fn unique_count(&self) -> u32 {
59        self.duplicates.len() as u32
60    }
61    pub fn unique_inputs(&self) -> u32 {
62        self.sub_duplicates.len() as u32
63    }
64    pub fn input_multiplicativity(&self) -> f64 {
65        let uis = self.unique_inputs();
66        if uis == 0 {
67            return 0.0;
68        }
69        self.unique_count() as f64 / self.unique_inputs() as f64
70    }
71}
smt_scope/analysis/redundancy.rs

smt_scope/analysis/
redundancy.rs
