smt_scope/analysis/graph/
disable.rs

1use crate::Z3Parser;
2
3use super::{
4    raw::{NodeState, RawInstGraph},
5    InstGraph, RawNodeIndex,
6};
7
8impl InstGraph {
9    /// Updates which nodes are disabled based on the predicate `f`. The
10    /// `hidden` of all nodes is reset to `false` so any filters will need to be
11    /// reapplied. The default analyses are also reapplied.
12    pub fn reset_disabled_to(
13        &mut self,
14        parser: &Z3Parser,
15        f: impl Fn(RawNodeIndex, &RawInstGraph) -> bool,
16    ) {
17        let (_, disabled_changed) = self.raw.reset_disabled_to_raw(f);
18        if disabled_changed {
19            self.initialise_default(parser, super::DEFAULT_N);
20        }
21    }
22
23    pub fn disabled_nodes(&self) -> impl Iterator<Item = RawNodeIndex> + '_ {
24        self.raw.node_indices().filter(|&n| self.raw[n].disabled())
25    }
26}
27
28impl RawInstGraph {
29    /// Updates which nodes are disabled based on the predicate `f`. The
30    /// `hidden` of all non-disabled nodes is reset to `false` so any filters
31    /// will need to be reapplied. It returns two booleans: the first indicates
32    /// if any state was modified, the second indicates if any node was
33    /// enabled/disabled.
34    ///
35    /// Analyses should be reapplied after this function is called! (unless the
36    /// second boolean is false)
37    pub fn reset_disabled_to_raw(
38        &mut self,
39        f: impl Fn(RawNodeIndex, &RawInstGraph) -> bool,
40    ) -> (bool, bool) {
41        let mut modified_disabled = false;
42        let mut modified = false;
43        for node in self.graph.node_indices().map(RawNodeIndex) {
44            let disable = f(node, self);
45            let node = &mut self.graph[node.0];
46            modified_disabled |= disable != node.disabled();
47            let state = if disable {
48                NodeState::Disabled
49            } else {
50                NodeState::Visible
51            };
52            modified |= self.stats.set_state(node, state);
53        }
54        (modified, modified_disabled)
55    }
56}
smt_scope/analysis/graph/disable.rs

smt_scope/analysis/graph/
disable.rs
