nft: +refactor Specialize the position encoding and the stop test in the multiword post()

[Adda0]

Part of #806. Implements the remaining unblocked items — the overflow arena (item 5), the 1-/2-level specialisation with a used-levels prefix table (item 6), and the internal rank-based stop hook for is_in_lang_by_levels (item 4). Item 7 (per-transition precompute) is skipped: it is blocked on #807.

What changes

Position policies in src/nft/nft.cc. The multiword post() search is now templated on a position representation over the used levels only (projected-out levels never move, so a configuration no longer stores their zeros):

• RankedPositions<1>: the rank is the position itself — no decoding at all.
• RankedPositions<2>: one division per popped configuration; fixed-width tuples are std::arrays.
• RankedPositions<std::dynamic_extent>: the generic mixed-radix decode of nft: +feat Rank reading-head positions and move long searches to a visited bitmap in post() #926.
• InternedPositions: tuples hash-consed into fixed-width blocks of one append-only arena, with cached hashes and an open-addressed id table. A successor is built in reused scratch storage and looked up there, so a tuple is copied only when it is new (item 5 — previously every consuming step copied a full std::vector before the unordered_map probe, which allocated a node per new tuple).

A span's stride sum is a precomputed prefix-sums difference, and its used levels are located through a per-level count table instead of scanning all levels (item 6).

Rank-based stop (item 4). Nft::is_in_lang_by_levels() used to pass post() an early-exit predicate that compared full position vectors — forcing a decode of every discovered configuration. It now calls the protected reaches_final_by_levels_(), whose stop test is levels[target] == 0 && (match_prefix || positions_id == end_id) && final.contains(target): no decoding, on ids only. The public is_early_exit_config path keeps its behaviour: it still gets the positions of all levels, rebuilt from the used-level tuple with zeros on the projected-out levels.

Tests (tests/nft/post.cc). A plain vector-tuple reference search written from the documented tape semantics is checked against post() (result and visited zero-level states) and against is_in_lang_by_levels() (prefix and full membership) on randomized level-respecting NFTs with jumps, DONT_CARE and EPSILON transitions, under random level masks covering the 0/1/2/many-used-levels paths, plus a 33-level run whose 2^33 tuples force the interned arena, and deterministic tuple-count boundary tests (255^4 fits the rank, 256^4 does not). The public is_early_exit_config predicate is checked against the same reference under noncontiguous level masks with one, two and three used levels (the three rank encodings) and a 32-of-33-levels mask (the interned arena): it must see exactly the reference's configurations, with zeros on the projected-out levels, and halt the search at a chosen configuration without being called again. Each new check was shown to bite by temporarily breaking the corresponding code path.

Measured effect

Re-measured on top of devel 1ff4da0 (32-bit State by default since #939, single inline SymbolPost target since #940); the later #871, #947 and #872 change no code on this path in a release build (#947 only regates OrdVector assertions). build/release (g++ 16.2, -O3) libraries of this branch and of devel, linked into the same scratch harness, taskset -c 2, min of 7 calls per run, min over three alternating devel/PR runs; both binaries return the same result on every workload. All workloads use JumpMode::AppendDontCares, since is_in_lang_by_levels() sends RepeatSymbol to its dedicated worklist and never reaches post():

Workload	devel	this PR	speedup
membership, 1 level, self-loop, word 100 000 (100 001 configs)	6.14 ms	3.39 ms	~1.8×
membership, 2 levels, free interleaving of two 500-long words (501² tuples, rejected)	64.9 ms	44.5 ms	~1.5×
exhaustive post(), 3 levels, free interleaving of three 12-long words (13³ tuples)	0.727 ms	0.488 ms	~1.5×
membership, 3 levels, 40 000-long lockstep cycle (rank overflows, ~120 000 interned tuples, rejected)	44.9 ms	15.4 ms	~2.9×
post() with an is_early_exit_config predicate that never stops, 2 levels, 501² tuples (752 502 calls)	63.3 ms	51.5 ms	~1.2×

The overflow fallback is where item 5 pays off most (node-data arenas with cached hashes instead of a vector copy plus an unordered_map node per step/miss), consistent with the issue's 1.5–5× target; the ranked paths gain a smaller constant factor from the fixed-width decodes, and membership additionally skips the decode for the stop test. The public predicate path still rebuilds the positions of all levels per configuration, so it gains least. The devel times of the interned workload vary between runs (44.9–59.6 ms); the PR's between 15.4 and 20.3 ms.

Rebase notes

• nfa: +feat Make State 32-bit by default and check state overflow #939 and nft: +fix Validate level metadata in unwind_jumps instead of the silent fallback #889 have landed. nfa: +feat Make State 32-bit by default and check state overflow #939 replaced the MATA_ASSERT on the state count in the old post() with an std::overflow_error in 64-bit-State builds; the rebase moves that check into post_by_words(), after the empty-delta shortcut as on devel, so it covers every Positions instantiation of the templated searcher.

CI note: macOS runners are queue-starved repo-wide, Linux coverage is the gate.

Test-generator note

The randomized differential generator exposed a latent, pre-existing post() behaviour worth knowing about: for a transition between two states on the same nonzero level (a malformed, not level-respecting NFT), the span is empty — it reads nothing — yet the current-symbol pruning still filters it out by symbol. devel behaves identically (verified against the devel binary on a witness: visited {0,1} vs an exhaustive reference BFS {0,1,2}); this PR does not change that. The generator now only emits well-formed jumps (a whole cycle only from level 0), keeping that out of the differential.

[greptile-apps]

Confidence Score: 4/5

[Medium impact] Refactors the multiword search logic in the automaton library.

The PR appears safe to merge, with a non-blocking request to test the changed public callback branch.

Findings

1.  Callback changes lack coverage ▶

Summary

Refactors multiword post() to store positions only for used levels.

• Multiword post() searches track positions with compact ids.
• General membership searches stop by checking position ids.

No behavioral defect was established. One non-blocking test gap remains for the changed public callback branch. Tests were not run during this review.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart TD
  A["Multiword post()"] --> C["Build used-level query"]
  B["is_in_lang_by_levels() general search"] --> C
  C --> D{"Tuple count fits the rank?"}
  D -->|Yes| E["RankedPositions: one, two, or many levels"]
  D -->|No| F["InternedPositions: tuple arena"]
  E --> G["Search state and position-id pairs"]
  F --> G
  G --> H{"Stop mode"}
  H --> I["Membership: compare position ids"]
  H --> J["Public callback: rebuild all level positions"]
  H --> K["No stop: collect reachable states"]

Loading

_{Reviews (1) · Last reviewed commit: "nft: +refactor Specialize the position e..." · Reviewed by Greptile}

[Adda0]

Rebased onto devel after #939 (32-bit State) landed. #939 added an overflow check inside search_by_words, a function this PR introduces with a local num_of_states variable, so the check called num_of_states() on a size_t and failed to compile. It now compares the local variable. Verified with the default 32-bit build (just tests-cpp::check, debug and release: 371 test cases, 365 passed, 2 skipped, 4 failed as expected) and with -DMATA_STATE_BITS=64 (ctest: 100% of 371 passed).