Skip to main content

Module scc

Module scc 

Source
Expand description

Generic strongly-connected-components (Tarjan).

One algorithm, two callers: call_graph::scc (string-keyed fn names, for TCO grouping + topo order) and analysis::shape::compute_sccs (FnId-keyed, for recursion classification feeding the proof path) both wrap this. Before unification each maintained its own copy of the strong_connect DFS.

Deterministic: vertices are sorted, each component is sorted, and the components are ordered by their least member, so two runs over the same input agree. A vertex with no self-edge is its own 1-element component; mutual recursion shows up as a component with len() > 1.

Functions§

mutually_recursive
The set of vertices that participate in mutual recursion — i.e. live in a strongly-connected component of size > 1. (Self-recursion via a self-edge is intentionally NOT captured here; callers that exclude self-edges from graph get exactly the mutual-recursion set.)
tarjan_sccs
Tarjan’s SCC partition of graph over the given nodes. Out-edges to vertices absent from graph are treated as having no further edges.