Svex-compose-bit-sccs
- Signature
(svex-compose-bit-sccs x trav-index stack
trav-indices finalized-updates params)
→
(mv err min-lowlink new-trav-index new-stack
new-trav-indices new-finalized-updates)
- Arguments
- x — current expression/bit (pseudo-node) to be traversed.
Guard (svex/index-p x).
- trav-index — next unused traversal index.
Guard (natp trav-index).
- stack — Stack of elements not yet assigned to an SCC.
Guard (svex/index-nat-alist-p stack).
- trav-indices — Traversal indices of nodes that have been visited.
Guard (svex/index-nat-alist-p trav-indices).
- finalized-updates — Accumulator of finalized update functions.
Guard (svex-alist-p finalized-updates).
- params — Guard (svex-scc-consts-p params).
- Returns
- min-lowlink — Type (maybe-natp min-lowlink).
- new-trav-index — Type (natp new-trav-index).
- new-stack — Type (svex/index-nat-alist-p new-stack).
- new-trav-indices — Type (svex/index-nat-alist-p new-trav-indices).
- new-finalized-updates — Type (svex-alist-p new-finalized-updates).
Implementation notes.
A node is a variable/bit-index pair that is a looping bit from final-masks.
A pseudo-node is an svex/integer pair, representing either a bit of that svex
expression (if the index is nonnegative) or a tail of that expression (if
negative -- the lognot is the number of bits to shift).
