smt_scope/analysis/
problem_behaviour.rs

1use crate::{items::QuantPat, Z3Parser};
2
3use super::{analysis::matching_loop::MlData, InstGraph, RedundancyAnalysis};
4
5#[derive(Debug, Default)]
6pub struct ProblemBehaviours {
7    /// All confirmed problem behaviours.
8    pub errors: Vec<ProblemBehaviour>,
9    /// All suspicious behaviours.
10    pub warnings: Vec<ProblemBehaviour>,
11}
12
13impl ProblemBehaviours {
14    pub fn find(ml: &MlData, redundancy: &RedundancyAnalysis) -> Self {
15        let mut self_ = Self::default();
16        for (idx, ml) in ml.matching_loops.iter().enumerate() {
17            let kind = PbKind::MatchingLoop {
18                max_len: ml.leaves.0[0].0,
19                idx,
20            };
21            if ml.graph.is_some() {
22                self_.errors.push(ProblemBehaviour { kind, sus: false });
23            } else {
24                self_.warnings.push(ProblemBehaviour { kind, sus: true });
25            }
26        }
27        for (qpat, red) in redundancy.per_quant.iter_enumerated() {
28            let multiplicativity = red.input_multiplicativity();
29            let kind = PbKind::Multiplicative {
30                qpat,
31                multiplicativity,
32            };
33            if multiplicativity >= 4.0 {
34                self_.errors.push(ProblemBehaviour { kind, sus: false });
35            } else if multiplicativity >= 2.0 {
36                self_.warnings.push(ProblemBehaviour { kind, sus: true });
37            }
38        }
39        self_
40    }
41}
42
43#[derive(Debug)]
44pub struct ProblemBehaviour {
45    pub kind: PbKind,
46    /// Is this behaviour confirmed problem (false), or only suspicious (true)?
47    pub sus: bool,
48}
49
50#[derive(Debug)]
51pub enum PbKind {
52    MatchingLoop {
53        max_len: u32,
54        idx: usize,
55    },
56    Multiplicative {
57        qpat: QuantPat,
58        multiplicativity: f64,
59    },
60}
61
62impl ProblemBehaviour {
63    pub fn kind_str(&self) -> &'static str {
64        match &self.kind {
65            PbKind::MatchingLoop { .. } => "matching loop",
66            PbKind::Multiplicative { .. } => "multiplicative",
67        }
68    }
69
70    pub fn detail(&self) -> String {
71        match &self.kind {
72            PbKind::MatchingLoop { max_len, .. } => format!("{max_len} iters"),
73            PbKind::Multiplicative {
74                multiplicativity, ..
75            } => {
76                format!("{multiplicativity:.1}x")
77            }
78        }
79    }
80
81    pub fn quant_pats(&self, parser: &Z3Parser, inst: &InstGraph) -> Vec<QuantPat> {
82        match &self.kind {
83            PbKind::MatchingLoop { idx, .. } => {
84                let ml_data = inst.analysis.ml_data.as_ref().unwrap();
85                ml_data.matching_loops[*idx].quants(parser, ml_data)
86            }
87            PbKind::Multiplicative { qpat, .. } => vec![*qpat],
88        }
89    }
90}
smt_scope/analysis/problem_behaviour.rs

smt_scope/analysis/
problem_behaviour.rs
