nfa: +refactor Bucket the antichain of processed macrostates by cardinality

[Adda0]

"is_included_antichains()" kept the macrostates processed for one state of the
smaller automaton in one unsorted vector, so both the subsumption test and the
pruning read every stored entry. Cardinality alone decides which entries can
be related to a candidate: a subset is never larger, a superset is never
smaller, and at equal cardinality both relations reduce to equality. The
processed entries are now bucketed by the cardinality of their macrostate, so
the subsumption test reads only the buckets below "|succ|" plus one equality
scan, and pruning reads only the buckets above it.

Only the cardinalities that actually hold an entry get a bucket, and the
buckets are kept ordered by cardinality. Indexing the buckets by cardinality
instead would cost a bucket header per unused size: with 10 000 states in the
initial macrostate that is 240 KiB per state of the smaller automaton (+303
MiB of peak RSS at 2 000 such states, measured), and both the subsumption test
and the pruning would walk those empty buckets.

The comment claiming the lists were sorted by set size was wrong (they were
only appended to) and is gone, together with the commented-out variants of the
orderings that were tried.

Measured on random instances where many macrostates share one state of the
smaller automaton, inclusion holding in all cases: 8.0 s -> 5.8 s (8 states,
128 noise states, 8 instances) and 294.1 s -> 180.9 s (12 states, 288 noise
states, 5 instances).

Fixes #785.

Fixes #785

[greptile-apps]

Confidence Score: 5/5

[Medium risk] Refactors the antichain algorithm for language inclusion checking.

This PR appears safe to merge; the bucket changes preserve the inclusion checks and fix the earlier overhead.

What we checked:

• Equal-size sets prune incorrectly: StateSet stores sorted, unique states, so an equal-size subset must be equal. The caller rejects an existing subset before pruning, making it safe to prune only larger buckets.

Summary

This PR groups processed macrostates by size and stores only occupied sizes.

• Subset checks skip larger buckets. Pruning skips smaller and equal-size buckets.
• A seeded test compares both inclusion algorithms in both directions.
• The earlier empty-bucket overhead is fixed. No new actionable issues were found.

_{Reviews (2) · Last reviewed commit: "nfa: +refactor Bucket the antichain of p..." · Reviewed by Greptile}

[Adda0]

I benchmarked this branch against the commit it branched off (f5457ea3d240 vs bfed5b61ab67), both built Release with the same compiler, 60 s timeout, 8 jobs, on the nfa-bench families that exercise inclusion and Boolean combinations.

bench-double-automata-inclusion (136 instances, all finished on both):

engine	mean	median	max	total
base	0.3707	0.24	11.41	50.42
head	0.3691	0.24	11.38	50.20

43 instances faster, 49 slower, median speed-up 1.00 (min 0.50, max 2.00).

bench-double-bool-comb-cox (80 instances, 60 finished, the same 20 time out on both):

engine	mean	median	max	total	PAR2
base	0.1582	0.155	0.35	9.49	30.12
head	0.1547	0.150	0.33	9.28	30.12

24 faster, 18 slower, median speed-up 1.00 (min 0.67, max 1.67).

bench-variadic-bool-comb-ere (384 instances, all finished on both, measuring the operations inside each .emp program):

metric	base	head
overall (total)	2.898 s	2.862 s
intersection (mean)	106.0 µs	106.8 µs
emptiness_check (mean)	7.958 µs	7.969 µs

197 faster, 187 slower, median speed-up 1.004.

No instance changed its answer, no timeout appeared or disappeared, and no family moved outside measurement noise. So the change is performance-neutral on these benchmarks -- that is not a refutation of the speed-up claimed in #785: these families answer in roughly 2 ms at the median and never build the long processed lists the bucketing is meant to shorten, and the ere family does not call is_included_antichains() at all, so it only sees the shared code. Reproducing the reported gain needs the generator from #785 rather than nfa-bench.

Worth noting on the correctness side: the neutral result means the bucketing costs nothing on inputs it cannot help, which is the property one would want from it.