aver/
scc.rs

1//! Generic strongly-connected-components (Tarjan).
2//!
3//! One algorithm, two callers: `call_graph::scc` (string-keyed fn names, for
4//! TCO grouping + topo order) and `analysis::shape::compute_sccs` (`FnId`-keyed,
5//! for recursion classification feeding the proof path) both wrap this. Before
6//! unification each maintained its own copy of the `strong_connect` DFS.
7//!
8//! Deterministic: vertices are sorted, each component is sorted, and the
9//! components are ordered by their least member, so two runs over the same
10//! input agree. A vertex with no self-edge is its own 1-element component;
11//! mutual recursion shows up as a component with `len() > 1`.
12
13use std::collections::{HashMap, HashSet};
14use std::hash::Hash;
15
16/// Tarjan's SCC partition of `graph` over the given `nodes`. Out-edges to
17/// vertices absent from `graph` are treated as having no further edges.
18pub fn tarjan_sccs<K>(nodes: &[K], graph: &HashMap<K, Vec<K>>) -> Vec<Vec<K>>
19where
20    K: Clone + Eq + Hash + Ord,
21{
22    struct State<K> {
23        index: usize,
24        indices: HashMap<K, usize>,
25        lowlink: HashMap<K, usize>,
26        stack: Vec<K>,
27        on_stack: HashSet<K>,
28        components: Vec<Vec<K>>,
29    }
30
31    fn strong_connect<K>(v: K, graph: &HashMap<K, Vec<K>>, st: &mut State<K>)
32    where
33        K: Clone + Eq + Hash + Ord,
34    {
35        st.indices.insert(v.clone(), st.index);
36        st.lowlink.insert(v.clone(), st.index);
37        st.index += 1;
38        st.stack.push(v.clone());
39        st.on_stack.insert(v.clone());
40
41        if let Some(neighbors) = graph.get(&v) {
42            for w in neighbors {
43                if !st.indices.contains_key(w) {
44                    strong_connect(w.clone(), graph, st);
45                    let low_v = st.lowlink[&v];
46                    let low_w = st.lowlink[w];
47                    st.lowlink.insert(v.clone(), low_v.min(low_w));
48                } else if st.on_stack.contains(w) {
49                    let low_v = st.lowlink[&v];
50                    let idx_w = st.indices[w];
51                    st.lowlink.insert(v.clone(), low_v.min(idx_w));
52                }
53            }
54        }
55
56        if st.lowlink[&v] == st.indices[&v] {
57            let mut comp = Vec::new();
58            while let Some(w) = st.stack.pop() {
59                st.on_stack.remove(&w);
60                let done = w == v;
61                comp.push(w);
62                if done {
63                    break;
64                }
65            }
66            comp.sort();
67            st.components.push(comp);
68        }
69    }
70
71    let mut sorted_nodes = nodes.to_vec();
72    sorted_nodes.sort();
73    let mut st = State {
74        index: 0,
75        indices: HashMap::new(),
76        lowlink: HashMap::new(),
77        stack: Vec::new(),
78        on_stack: HashSet::new(),
79        components: Vec::new(),
80    };
81    for node in sorted_nodes {
82        if !st.indices.contains_key(&node) {
83            strong_connect(node, graph, &mut st);
84        }
85    }
86    st.components.sort_by(|a, b| a[0].cmp(&b[0]));
87    st.components
88}
89
90/// The set of vertices that participate in mutual recursion — i.e. live in a
91/// strongly-connected component of size > 1. (Self-recursion via a self-edge
92/// is intentionally NOT captured here; callers that exclude self-edges from
93/// `graph` get exactly the mutual-recursion set.)
94pub fn mutually_recursive<K>(nodes: &[K], graph: &HashMap<K, Vec<K>>) -> HashSet<K>
95where
96    K: Clone + Eq + Hash + Ord,
97{
98    tarjan_sccs(nodes, graph)
99        .into_iter()
100        .filter(|c| c.len() > 1)
101        .flatten()
102        .collect()
103}
aver/scc.rs

aver/
scc.rs
