smt_scope/analysis/graph/analysis/
mod.rs

1pub mod cdcl;
2pub mod cost;
3pub mod depth;
4pub mod matching_loop;
5pub mod next_nodes;
6pub mod proof;
7pub mod reconnect;
8pub mod run;
9
10use std::cmp::Reverse;
11
12#[cfg(feature = "mem_dbg")]
13use mem_dbg::{MemDbg, MemSize};
14
15use matching_loop::MlData;
16
17use crate::{F64Ord, Result, TiVec, Z3Parser};
18
19use self::{
20    cost::{DefaultCost, ProofCost},
21    depth::DefaultDepth,
22    next_nodes::NextInstsInit,
23    proof::ProofInitialiser,
24    reconnect::{BwdReachableAnalysis, ReachNonDisabled},
25};
26
27use super::{raw::RawInstGraph, InstGraph, RawNodeIndex};
28
29#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
30#[derive(Debug, Default)]
31pub struct Analysis {
32    pub reach: TiVec<RawNodeIndex, ReachNonDisabled>,
33    // Highest to lowest
34    pub cost: OrderingAnalysis,
35    // Most to least
36    pub children: OrderingAnalysis,
37    // Most to least
38    pub fwd_depth_min: OrderingAnalysis,
39    pub ml_data: Option<MlData>,
40}
41
42#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
43#[derive(Debug, Default)]
44pub struct OrderingAnalysis {
45    nodes: Vec<RawNodeIndex>,
46    sorted_to: usize,
47}
48
49impl OrderingAnalysis {
50    pub fn duplicate(&self) -> Result<Self> {
51        // Alloc `children` vector
52        let mut nodes = Vec::new();
53        nodes.try_reserve_exact(self.nodes.len())?;
54        nodes.extend(self.nodes.iter().copied());
55        Ok(Self {
56            nodes,
57            sorted_to: 0,
58        })
59    }
60
61    pub fn first_n<O: Ord>(
62        &mut self,
63        n: usize,
64        ord: impl Fn(RawNodeIndex) -> O,
65    ) -> (&[RawNodeIndex], &[RawNodeIndex]) {
66        let idx = n.min(self.nodes.len());
67        if let Some(pivot) = idx.checked_sub(self.sorted_to + 1) {
68            let unsorted = &mut self.nodes[self.sorted_to..];
69            let (larger, _, _) = unsorted.select_nth_unstable_by_key(pivot, |&a| (ord(a), a));
70            larger.sort_unstable_by_key(|&a| (ord(a), a));
71            self.sorted_to = idx;
72        }
73        self.nodes.split_at(idx)
74    }
75}
76
77impl Analysis {
78    pub fn new(nodes: impl Iterator<Item = RawNodeIndex>) -> Result<Self> {
79        // Alloc `cost` vector
80        let mut cost = Vec::new();
81        for node in nodes {
82            cost.try_reserve(1)?;
83            cost.push(node);
84        }
85        let cost = OrderingAnalysis {
86            nodes: cost,
87            sorted_to: 0,
88        };
89        // Alloc `children` vector
90        let children = cost.duplicate()?;
91        // Alloc `fwd_depth_min` vector
92        let fwd_depth_min = cost.duplicate()?;
93        Ok(Self {
94            reach: Default::default(),
95            cost,
96            children,
97            fwd_depth_min,
98            ml_data: None,
99        })
100    }
101}
102
103impl InstGraph {
104    pub fn initialise_first(&mut self, parser: &Z3Parser, n: usize) {
105        self.initialise_collect(ProofInitialiser::<false>, parser);
106        self.initialise_collect(ProofInitialiser::<true>, parser);
107        self.initialise_cdcl(parser);
108
109        self.initialise_default(parser, n);
110    }
111
112    pub fn initialise_default(&mut self, parser: &Z3Parser, n: usize) {
113        let mut reach = BwdReachableAnalysis::<ReachNonDisabled>::default();
114        self.analysis.reach = self.topo_analysis(&mut reach);
115
116        self.initialise_transfer(DefaultCost, parser);
117        self.initialise_transfer(ProofCost, parser);
118        self.initialise_collect(DefaultDepth::<true>, parser);
119        self.initialise_collect(DefaultDepth::<false>, parser);
120
121        self.initialise_transfer(NextInstsInit::<true>, parser);
122        self.initialise_transfer(NextInstsInit::<false>, parser);
123
124        self.analyse(n);
125    }
126
127    pub fn analyse(&mut self, n: usize) {
128        self.analysis.cost.sorted_to = 0;
129        self.analysis.children.sorted_to = 0;
130        self.analysis.fwd_depth_min.sorted_to = 0;
131        self.analysis.first_n_cost(&self.raw, n);
132        self.analysis.first_n_children(&self.raw, n);
133        self.analysis.first_n_fwd_depth_min(&self.raw, n);
134    }
135}
136
137impl Analysis {
138    pub fn first_n_cost(
139        &mut self,
140        raw: &RawInstGraph,
141        n: usize,
142    ) -> (&[RawNodeIndex], &[RawNodeIndex]) {
143        self.cost.first_n(n, |a| Reverse(F64Ord(raw[a].cost)))
144    }
145
146    pub fn first_n_children(
147        &mut self,
148        raw: &RawInstGraph,
149        n: usize,
150    ) -> (&[RawNodeIndex], &[RawNodeIndex]) {
151        self.children.first_n(n, |a| Reverse(raw[a].children.count))
152    }
153
154    pub fn first_n_fwd_depth_min(
155        &mut self,
156        raw: &RawInstGraph,
157        n: usize,
158    ) -> (&[RawNodeIndex], &[RawNodeIndex]) {
159        self.fwd_depth_min
160            .first_n(n, |a| Reverse(raw[a].fwd_depth.min))
161    }
162}
smt_scope/analysis/graph/analysis/mod.rs

smt_scope/analysis/graph/analysis/
mod.rs
