Skip to content

Reduce regular layered graph construction memory - #234

Open
zayenz wants to merge 3 commits into
mainfrom
feature/improved-regular-construction
Open

Reduce regular layered graph construction memory#234
zayenz wants to merge 3 commits into
mainfrom
feature/improved-regular-construction

Conversation

@zayenz

@zayenz zayenz commented Jul 28, 2026

Copy link
Copy Markdown
Member

The regular propagator constructs a layered graph for the sequence and DFA. The existing initializer reserves a state slot for every DFA state at every sequence position, so a sequence of length n and a DFA with k states needs (n + 1)k temporary State objects even when only a small part of that matrix is reachable.

This change constructs the graph from sparse forward frontiers, filters it by backward co-reachability, and allocates persistent state nodes only after the surviving layer sizes are known. State-related construction memory is therefore O(k + S), where S is the number of state nodes in the final layered graph. For an unfolded DFA, S <= k. A looping DFA can still have S = Theta(nk), but construction no longer adds a second dense state matrix.

The persistent Layer, Support, Edge, and State representation is unchanged. The existing propagator, advisors, cloning, and copy-time compression continue to use the same graph.

The added tests cover cyclic frontiers, acyclic reconvergence, position-specific domain pruning, failed acceptance, Boolean views, merged and unmerged terminal states, state-index boundaries, and randomized differential checks.

Evidence from Release builds with Apple Clang:

  • A fresh build of all libraries, tools, and examples succeeds, and the focused Int::Extensional::Reg suite passes.
  • In the unfolded size-5,000 case, the dense construction had 25,010,001 state slots for 5,001 persistent states. Median peak RSS fell from 108,000 KiB to 9,552 KiB, and median root construction time fell from 215.882 ms to 157.038 ms.
  • An all-model campaign completed 1,760 fresh-process runs with no differences in status, solutions, objectives, nodes, or failures. Across 15 real-model timing rows, the geometric-mean candidate/baseline runtime ratio was 1.010.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant