bindings/python: +feat Release the GIL in the long-running operations (…

…#955)

No call of the bindings released the GIL, so Python threads running
automata operations serialised on it. The heavy entry points are now
declared `except + nogil` and called under `with nogil:`: determinize
(with and without the subset map), union, intersection (with and
without the product map), concatenate (with and without the state
maps), complement, revert, remove_epsilon, minimize, reduce (with and
without the state map), reduce_residual_after/with, compute_relation,
is_included (with and without a counterexample), equivalence_check,
and noodlify, noodlify_mult_eps, noodlify_for_equation_sides and
noodlify_for_transducer. The `params` dictionaries are converted to a
`ParameterMap` before the GIL is dropped, through a shared
`encode_params()` that strings.pyx cimports. The C++ library does not
synchronise anything, so the declarations document that the automata
and alphabets passed in must not be mutated by another thread meanwhile.

noodlify_for_equation_sides and noodlify_for_transducer unify the
initial and final states of their input automata in place. Each input
with more than one initial or final state is now copied before the
call, so the call never writes an automaton shared with the caller or
with a concurrent call, and the caller's automata are no longer
modified. `SparseSet::size()` is declared as the method it is; the
declaration as a field could not be called.

The result of `compute_relation` is assigned straight into the
returned `BinaryRelation` instead of being copied cell by cell through
untyped `get`/`set` calls. `BinaryRelation.to_matrix()` reads the
relation through typed C++ calls.

noodlify_for_equation is left as it is; #880 rewrites it.

Part of #755.

### Measurements

Release bindings (CPython 3.14, Cython 3.3), this branch vs `devel`,
alternating runs, throwaway scripts (not committed). Machine shared with
other builds, so absolute times are noisy; the contrast is what matters.

GIL release, `determinize()` of a random NFA (300 states, 1200
transitions, 2 symbols), `taskset -c 4,5,6`, 5 alternating runs:

| | devel | this branch |
|---|---|---|
| 3 threads at once / 1 call, wall-time ratio (median) | 5.69 | 1.66 |
| 3 threads at once, wall time (median) | 1.73 s | 0.869 s |

Main thread counting in a pure-Python loop while a second thread runs
one `determinize()` (`taskset -c 4,5`, 3 alternating runs, median):
devel 0.47 M iterations/s (the main thread barely runs), this branch
5.86 M iterations/s (idle baseline 9.5–14.5 M/s).

The GIL measurements were taken on devel `ba4a338a78`; the rebase onto
the current `devel` did not change the binding code they measure.

`compute_relation()` and `to_matrix()` on a random NFA with N=1500
states (6000 transitions, 2 symbols, 50 final states), `taskset -c 6`,
each value a median of 5 calls, 5 alternating runs, median shown,
measured on devel `1ff4da094c` (which already declares
`compute_relation` to return by value, #939; the commits since, #871,
#947 and #872, do not touch the bindings):

| | devel | this branch |
|---|---|---|
| `compute_relation()` | 733 ms | 450 ms |
| `BinaryRelation.to_matrix()` | 139 ms | 15 ms |

### Tests

`test_nfa.py`: determinize (with subset map), intersection, minimize and
reduce run in three threads at once and must match the single-threaded
results; `test_heavy_operations_let_other_threads_run` checks, for
determinize (with and without the subset map), minimize, complement,
reduce, compute_relation and intersection, that the main thread runs
Python code while the call is still running in another thread
(`runs_without_the_gil` fixture in `conftest.py`: with
`sys.setswitchinterval(60)` the main thread can only run before the
worker finishes if the call releases the GIL). Replacing `with nogil:`
by `if True:` in `determinize` or `reduce` makes the matching case fail.

`test_strings.py`: the four noodlify variants run in three threads at
once on shared inputs with two initial and two final states, and every
returned automaton, epsilon counter and input/output index must match
the single-threaded results; `noodlify_for_equation_sides` and
`noodlify_for_transducer` must leave their inputs unchanged and must let
the main thread run during the call. Dropping the input copy makes the
unchanged-inputs test fail, and replacing `with nogil:` by `if True:` in
`noodlify_for_equation_sides` makes its thread test fail. Existing
`compute_relation`/`to_matrix` tests cover the relation copy.

On devel `8b4c09bbc6`: Python bindings 153 passed, 3 skipped, 2 xfailed;
C++ suite (debug and release) 363 passed, 2 skipped, 4 failed as
expected.

### Merge order and overlap

- #868 (static buffers of `StatePost::find` and `OrdVector::insert`,
#731), on which this PR was stacked, is merged; this PR now targets
`devel` directly.
- #880 rewrites `noodlify_for_equation`; this PR leaves that function
alone.
- #939 (32-bit `State`) already added `except +` to the externs this PR
redeclares, and declares `compute_relation` to return by value; this PR
only adds `nogil` to them.
- Independent of the other #755 PRs.

parser: +feat Convert RE2 programs directly to NFAs without epsilon t…

…ransitions (#950)

create_nfa() always translated the RE2 program with an epsilon
transition for every nop, capture and empty-width instruction and for
every continuation of an instruction list, trimmed the result, and then
ran the global remove_epsilon() to get the epsilon-free NFA every
default caller asks for. The epsilon-free branch of the converter
(create_state_cache_without_epsilon(), get_mapped_states() and the
reversed edge copying) was never reached and, as its FIXME said, did not
work.

The epsilon-free conversion is now direct. A state stands for the
instruction list the program continues at: the start and the target of
each byte range. Its closure follows the non-consuming instructions and
the list continuations to byte ranges and matches; the state gets the
byte-range transitions of the closure and is final when the closure
contains a match. A worklist from the start creates states only for
reachable lists, so RE2's unanchored prefix never becomes a state. On
the regexes of the test suite and of the new benchmark, the conversion
leaves no useless state behind; only branches that can never match,
such as '[^\x00-\xff]' in Latin1, do, so trim stays enabled by default.

The explicit epsilon translation stays as the keep_epsilon mode, with
the caller's epsilon symbol, rewritten as a plain worklist over the
reachable instructions. The broken branch, its state cache and the
FIXME are gone.

Tests: a seeded differential test generates regexes covering every
instruction form (byte ranges with and without case folding, captures,
alternation lists, empty branches, greedy, non-greedy and counted
repetitions, '(?s:.)' loops compiled to AltMatch, anchors) and checks
the direct conversion, untrimmed and reduced, against the epsilon
translation followed by remove_epsilon(), and against the language of
the generated syntax tree on all words up to length 4. The bundled RE2
has no matcher, so RE2 itself cannot serve as the oracle.
bench-regex-conversion times the conversions, remove_epsilon(), trim()
and reduce() separately.

Part of #793.

### Measurements

Release build, g++, pinned to one core (`taskset -c 13`). `perf`
harness: median wall time of a `create_nfa(regex, false, 306, reduce)`
call. Each value is the median of 5 alternating base/new processes with
3 calls each. Base = `devel` at b6f7fd1; new = this stack on the same
base. It has since been rebased onto `devel` at 8b4c09b; the only
conflict was #939's casts in the removed `convert_pro_to_nfa`, and the
converter itself is unchanged. The number of states and transitions of
the trimmed result is identical between base and new for every regex.

Without reduction (`reduce = false`, the path used by `replace.cc`):

| regex | base [ms] | new [ms] | states / transitions |
|---|---:|---:|---|
| `(?:[a-z]b\|c[d-f]){1000}` | 9.74 | 2.44 | 3001 / 31000 |
| 2000-character literal | 1.62 | 0.53 | 2001 / 2000 |
| `a?` × 300 followed by `b` | 0.88 | 0.47 | 302 / 601 |
| `(?:a?b?c?){100}d` | 7504 | 2.14 | 302 / 45451 |
| `(?:((a)*)*b\|(c(d)*)){200}` | 4.07 | 0.60 | 801 / 2594 |
| `(?:(?:ab\|cd)*?e+?(?:f\|g\|)){200}` | 1.72 | 0.47 | 801 / 2197 |
| `a*b\|c(de)*` | 0.0147 | 0.0084 | 6 / 8 |
| `[a-z0-9._%+-]+@[a-z0-9.-]+\.[a-z]{2,}` | 0.060 | 0.025 | 7 / 238 |

With the default reduction:

| regex | base [ms] | new [ms] |
|---|---:|---:|
| `(?:((a)*)*b\|(c(d)*)){200}` | 23.1 | 19.5 |
| `(?:(?:ab\|cd)*?e+?(?:f\|g\|)){200}` | 23.2 | 21.3 |
| `a*b\|c(de)*` | 0.031 | 0.025 |
| `[a-z0-9._%+-]+@[a-z0-9.-]+\.[a-z]{2,}` | 0.262 | 0.220 |

`(?:a?b?c?){100}d` hits the forward-chain case of `remove_epsilon()`
(#240): 7.0 s of the 7.5 s go to `remove_epsilon()` (see the stage
timers below). Note that the base language of the lazy
`(?:(?:ab|cd)*?e+?…)` regex differs, because the base still had the bug
fixed by #948.

Stage timers from the new `bench-regex-conversion` (seconds, one run):

| regex | convert_with_epsilon | remove_epsilon | convert_direct | trim
| reduce |
|---|---:|---:|---:|---:|---:|
| `(?:[a-z]b\|c[d-f]){1000}` | 0.0047 | 0.0052 | 0.0025 | 0.0005 |
1.9173 |
| 2000-character literal | 0.0005 | 0.0004 | 0.0003 | 0.0001 | 0.0186 |
| `a?` × 300 followed by `b` | 0.0005 | 0.0002 | 0.0004 | 0.0000 |
0.0031 |
| `(?:a?b?c?){100}d` | 0.0002 | 6.9871 | 0.0019 | 0.0004 | 0.0200 |
| `(?:((a)*)*b\|(c(d)*)){200}` | 0.0009 | 0.0019 | 0.0006 | 0.0001 |
0.0220 |
| `(?:(?:ab\|cd)*?e+?(?:f\|g\|)){200}` | 0.0006 | 0.0008 | 0.0004 |
0.0000 | 0.0206 |

Useless states (#793 item 6): over the 136 regexes used in the tests
(`create_nfa`/`create_from_regex` literals and regex lists) plus the 8
benchmark regexes, the untrimmed direct conversion had 7788 states, and
`trim()` removed none of them.

Language equivalence against the old conversion: every regex of that
corpus was converted with devel and with this stack, written as `.mata`
files and compared with `are_equivalent()`, both reduced and unreduced.
270 of 272 automata are equivalent. The two that differ are `b\w+?`
(plain and reduced), whose devel result at the time was the bug fixed by
#948. The randomized differential test adds 400 generated regexes on
every run.

### Scope

Last of three PRs for #793; the first two, #948 and #949, are merged.

Not in this PR:
- RE2 acceptance as an oracle (plan step 7): the bundled RE2 is trimmed
to its parser and compiler and has no matcher. The test uses the
language of the generated syntax tree instead.
- Instrumentation counters in the library (plan step 6): the counts
above come from the benchmark and from a throwaway harness.
- Separate timers for parsing and compiling: the public API runs both
inside `create_nfa()`, so they are part of the conversion timers.

Found while testing, and left out of scope: the bundled RE2 parser drops
the folded case of a letter that it merges into a character class that
already holds that letter. `a|(?i:a)` parses to `[a]`, and `[ab]|(?i:a)`
parses to `[a-b]`, so `A` is rejected. The generator avoids this case.

nfa: +refactor Compute useful states with two reachability passes (#886)

Replace the Tarjan-based implementation of get_useful_states() with a
simpler and faster two-pass algorithm: a forward reachability pass from
initial states, followed by a backward BFS from final states over a
predecessor CSR (compressed sparse row) index. The new implementation:

- Adds a label-free predecessor CSR index with a source filter to only
index forward-reachable transitions
- Implements forward reachability from a custom initial set
- Walks backward over predecessors to find all useful states
- Honors custom initial and final sets for noodlification use cases

LOCAL BENCHMARK (Release build, 1M-state DAG with 2M transitions):
- Old Tarjan-based: 22.2 ms/iter
- New two-pass: 8.8 ms/iter
- Speedup: 2.52×

Keeps Tarjan in place for its remaining callers (is_acyclic, is_flat,
tarjan_scc_discover).

Permanent test added: 'mata::nfa::get_useful_states() with brute-force
oracle' validates correctness against an independent oracle on
randomized graphs (50 test cases with 5-50 states and random edges) and
verifies trim() state renamings.

Part of #786. Not included: the benchmark against the compact templated
Tarjan of #224 (b) and recording the decision in the issue (item 3), and
the
optional sharing of the predecessor index through #811 (item 5).

nft: +refactor Specialize the position encoding and the stop test in …

…the multiword post() (#945)

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::array`s.
- `RankedPositions<std::dynamic_extent>`: the generic mixed-radix decode
of #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

- #939 and #889 have landed. #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.

utils, tests: +feat Assert the universal iterator precondition and ad…

…d randomized oracle tests (#953)

The two remaining actionable items of #797: item 6 (precondition of the
universal iterator) and item 7 (randomized oracle tests for the utility
headers). The #769 container fixes these oracles depend on landed in
#946. Item 3 (packing a 32-bit `State` pair in `PairHash`) stays blocked
on #789 / #939 and is not part of this pull request.

## Item 6: precondition of `SynchronizedUniversalIterator::advance()`

Universal synchronization over zero inputs is not meaningful.
`advance()` now documents "at least one input pushed since construction
or the last `reset()`" as its precondition and asserts it in debug
builds (`MATA_ASSERT(!this->positions.empty())`). Release builds keep
returning `false`. The library callers (NFT intersection and
composition) always push two inputs. The header now also includes the
`<cstddef>`, `<vector>` and `assert.hh` it uses.

The existing unit tests that called `advance()` on an iterator without
inputs now check only the state after `reset()`. The release fallback
has its own `#ifdef NDEBUG` test case.

## Item 7: seeded randomized oracle tests

Every value is drawn from raw `std::mt19937` output over a fixed seed
range, as in `tests/nfa/nfa-differential.cc`, so the tests are
deterministic across standard libraries:

| Test case | Oracle | Seeds |
|---|---|---|
| `OrdVector against std::set (randomized)`: construction (vector,
`std::set`, iterator range), `set_union` and `insert(OrdVector)`,
`intersection`, `difference`, `is_subset_of`,
`is_intersection_empty_with`, `are_disjoint`, `==`/`<`,
`contains`/`count`/`find`, `min`/`max`, random insert/erase sequences,
`erase_if` | `std::set` and `std::ranges` set algorithms | 500 |
| `filter() and filter_indexes() against std::erase_if (randomized)`:
the free functions and the `OrdVector` wrappers | `std::erase_if`, an
index mask | 500 |
| `SparseSet against std::set (randomized)`: 60-step traces of
`insert`/`erase`/`complement`/`filter`/`rename` (a permutation of `[0,
61)`)/`truncate`/`sort`, then `size`, `empty`, `max`, membership over
the whole domain, `are_disjoint`, `intersects_with`, copies |
`std::set`. Contents are compared as sorted element lists:
`SparseSet::operator==` compares the internal buffers, which is a
separate #769 item left untouched here. | 300 |
| `SynchronizedUniversalIterator against a brute-force intersection
(randomized)`: 2–5 inputs, also after `reset()`, with the collected
count required to stay within the oracle's size so a stalling iterator
fails instead of timing out | `std::ranges::set_intersection` | 300 |
| `SynchronizedExistentialIterator against a brute-force merge
(randomized)`: 1–5 inputs, per-value count of synchronized positions,
also after `reset()`, with the collected count likewise bounded by the
oracle's size | `std::ranges::set_union`, `binary_search` | 300 |

## Verification

* `nix fmt` on the touched files: `(0 changed)`.
* `just cpp::build debug` + `./build/debug/g++/tests/tests` on the
pushed head, rebased onto `devel` `8b4c09b` (GCC, Nix dev shell): `test
cases: 374 | 368 passed | 2 skipped | 4 failed as expected`,
`assertions: 4754234 | 4754197 passed | 37 failed as expected`. Release
build: `test cases: 375 | 369 passed | 2 skipped | 4 failed as
expected`, `assertions: 4754239 | 4754202 passed | 37 failed as
expected` (the extra case is the release-only zero-input test). The 4
expected failures are the existing `[!shouldfail]` cases in
`tests/nft/nft-differential.cc`.
* **The assertion fires in debug.** A probe that calls `advance()` on an
empty `SynchronizedUniversalIterator`, compiled without `NDEBUG`, prints
`include/mata/utils/synchronized-iterator.hh:117: advance: Assertion
'!this->positions.empty()' failed.` and exits with 134 (SIGABRT).
Compiled with `-DNDEBUG`, it returns `false`.
* **The oracles catch real bugs.** I compiled the three test files
against a copy of the headers with the following re-introduced: the
`devel` `filter`/`filter_indexes` (`reserve(last)`), the `devel`
universal restart check, a `SparseSet::complement` that keeps values
above the new domain, an `OrdVector::difference` that drops the last
element, and an existential iterator that keeps at most two synchronized
positions. All five randomized test cases failed (10 of 21 test cases,
2237 assertions); with the real headers all pass.
* Performance: these are test and debug-only changes, so release code is
unchanged and nothing needs measuring.

---

Part of #797.

nfa,nft: +refactor Answer emptiness with a reachability search instea…

…d of Tarjan (#872)

`is_lang_empty()` without a counterexample ran
`has_no_accepting_path()`,
which drove Tarjan's SCC discovery and paid for its per-state
bookkeeping
even when the whole reachable part had to be traversed. Emptiness only
needs reachability that stops at the first final state. The
counterexample
variant walked a `std::list` worklist with an `std::unordered_set` of
processed states and an `std::map<State, State>` of predecessors.

Both are now a breadth-first search over a `std::vector` queue: a
visited
bit vector in `has_no_accepting_path()`, and a `predecessors` vector
with
`Limits::max_state` marking unvisited states in
`Automaton::is_lang_empty()`.
The witness is still built by the same BFS, so it stays shortest in the
number of transitions, and the word is still read by the leaf's own
`get_word_for_path()`, which is what makes the NFT witness level-aware.
Finality is tested once per dequeued state rather than once per incoming
transition, and the FIFO order keeps the scan of `delta` close to
ascending;
a LIFO worklist measured 1.5x slower than Tarjan on the DAG below.

In `noodlify_for_equation()` the check right after `trim()` is now
`initial.empty()`: every state left by `trim()` lies on an accepting
path.
The postcondition is documented on `Automaton::trim()`.

Measured (Release `-O3 -DNDEBUG`, GCC 16.2, pinned to one core, 3 runs,
automata copied once so the posts are compact):

| automaton | before | after |
| random 200k states / 2M transitions, empty | 175-222 ms | 48-53 ms |
| the same with a counterexample | 452-573 ms | 50-54 ms |
| DAG 1M states / 2M transitions, empty | 37.3-37.9 ms| 25.9-26.2 ms |
| trimmed 200k-state non-empty automaton | 3.2-3.3 ms | 1.9 ms |

The last row is the per-call cost that `initial.empty()` removes from
the
three `noodlify_for_equation()` overloads entirely.

`is_lang_empty_scc()` stays as a source-compatible alias and is
documented
as deprecated, since it no longer runs Tarjan.

Fixes #748.
Part of #726.

utils, ci: +refactor Adopt moved vectors and gate the whole-container…

… assertions (#947)

`OrdVector` could only be built from a vector by copying it: every
constructor took the source by const reference and then sorted the copy.
Add `OrdVector(VectorType&&)`, which adopts the vector and sorts and
deduplicates it in place, and `OrdVector(sorted_unique, VectorType&&)`,
which adopts an already sorted, duplicate-free vector and only checks
that under the expensive assertions. `Delta::get_used_symbols_vec()`
gathers into a local vector, so it now moves it in; the
`_STATIC_STRUCTURES_` branch keeps copying, because that buffer is
reused across calls. (The original revision also moved the gathered
vector in `Nfa::post()`, but #958 moved that body into `Delta::post`
with a `PostWorkspace` whose merge buffer is reused across calls, so
copying there is now intentional and this PR leaves it alone.)

`set_union(lhs, rhs, result)` appends to `result` and derives its return
value from `result.size() > lhs.size()`, which only holds when `result`
starts out empty. Make that a precondition, assert it, and document the
return value as "`rhs` has an element that is not in `lhs`". With the
precondition stated, the overload is the reusable union-into-buffer
helper: a caller passes a cleared buffer and keeps its capacity. The
FIXME above the return described an iterator return value the function
does not have; drop it together with the superseded commented-out loop.

The header checked `is_sorted()` on entry and exit of almost every
operation, so a Debug `find()` scanned the whole vector instead of
bisecting it, and `insert()` scanned it twice. Move the whole-container
checks to `MATA_EXPENSIVE_ASSERT`, which the CMake option
`MATA_EXPENSIVE_ASSERTS` turns on, and keep an O(1) check of the
inserted element against its two neighbours in `MATA_ASSERT`.
`insert(std::span<const Key>)`, which #868 added on `devel` meanwhile,
gets the same treatment. A new CI job (`expensive-asserts` in
`code-quality.yml`) builds the unit tests in Debug with
`MATA_EXPENSIVE_ASSERTS=ON` and runs them, so the invariants are still
checked on every pull request.

Part of #746 (the koniksedy follow-up items 4–6; the optional `final`
item 3 is not done).
Part of #847 (all three items; #868 took the `insert(const OrdVector&)`
doc comment meanwhile).

### Measurements

Throwaway harness, GCC 16.2, pinned to one core (`taskset -c 5`),
alternating base/head runs, 3 rounds. Base = `devel` at 2a95b88, head =
this change on the same base. Result digests identical between base and
head. The `Nfa::post` rows of the earlier measurement are dropped: that
code moved to `Delta::post` with a reused `PostWorkspace` (#958), which
this change no longer touches.

**Release** (`-O3 -DNDEBUG`, linked against
`build/release/g++/src/libmata.a`), random NFA with 20 000 states, 400
000 transitions, 8 symbols; 700 runs of `get_used_symbols_vec` per round
(7 medians of 100), plus global `operator new` count:

| round | devel | this PR | heap allocations devel → PR |
|---|---|---|---|
| 1 | 409.20 ms | 408.89 ms | 10 504 → 9 804 |
| 2 | 400.19 ms | 393.84 ms | 10 504 → 9 804 |
| 3 | 430.94 ms | 410.18 ms | 10 504 → 9 804 |

So Release runtime is unchanged within noise; the PR saves the copy
allocations.

**Debug** measurements from the earlier revision (the gated code is
unchanged): 20 000 `insert(const Key&)` of increasing keys, then 200 000
`find()` on the resulting 20 000-element `OrdVector`; 3 alternating
rounds.

| | `insert` ×20 000 | `find` ×200 000 |
|---|---|---|
| devel | 6498.9 / 3305.7 / 3262.2 ms | 95 389.2 / 32 442.2 / 32 145.8
ms |
| this PR | 14.2 / 3.2 / 3.5 ms | 92.9 / 32.2 / 33.1 ms |
| this PR, `-DMATA_EXPENSIVE_ASSERTS` | 9311.6 / 3151.3 / 3208.7 ms | 67
170.4 / 32 138.8 / 32 704.3 ms |

So Debug lookups get back the complexity of Release ones, and the opt-in
mode reproduces the old checking cost.

### Verification
- `nix develop --command nix fmt`: 0 changed.
- `just tests-cpp::check` (debug and release), on `devel` at 2a95b88,
both summaries: `test cases: 367 | 361 passed | 2 skipped | 4 failed as
expected`, `assertions: 2749369 | 2749332 passed | 37 failed as
expected`. The `-Wconversion` warnings in the log are on `devel` (32-bit
`State` from #868); this change adds none.
- Debug build with `-DMATA_EXPENSIVE_ASSERTS=ON` (the new CI job's
configuration), verified on the previous push (on `devel` at b6f7fd1):
`ctest` 100% passed out of 314; the `expensive-asserts` CI job passed on
the first push.
- The new tests bite: making `OrdVector(VectorType&&)` copy
(`vec_(vec)`) and returning `result.size() >= lhs.size()` from
`set_union` failed `tests/ord-vector.cc` assertions and passed again
after restoring.

### Overlap with open PRs
None left: #868 (`insert(std::span<const Key>)`, 64-bit-state CI job)
and #946 (`filter`/`filter_indexes` tests) merged into `devel`; the
rebase folds this PR's `OrdVector` test cases next to the #946 ones and
places the `expensive-asserts` CI job next to #868's `state-bits-64`
one, and gates #868's whole-container assertions in
`insert(std::span<const Key>)` the same way.

nfa: +refactor Compute distances to final over a predecessor CSR inst…

…ead of a reverted automaton (#871)

Automaton::distances_to_final() was implemented as
reverted().distances_from_initial(): it built a complete reversed
automaton
with one sorted Delta::add per transition, only to run a BFS that needs
predecessor lists and nothing more. is_included_antichains calls it for
both
automata on every call, so are_equivalence pays it up to four times, and
for
inclusion checks that are decided quickly the reverts are most of the
runtime.

distances_to_final() now counts the in-degrees, prefix-sums them, fills
one
flat predecessor vector and BFS-es from the final states with a vector
as the
queue: O(|Q| + |delta|) with four allocations, no sorted inserts and no
reversed delta. The returned vector is identical to the old
implementation;
a randomized regression test compares the result against the previous
revert-and-BFS computation on 30 random automata.

Measured locally (Release, GCC 16.2, -O3 -DNDEBUG, median of 7 runs, two
distance computations each on two random 5000-state NFAs with the output
shown):

  out-degree 3:  4.442 ms -> 0.511 ms
  out-degree 12: 8.978 ms -> 1.035 ms

Not part of this pull request from #740: get_terminating_states() still
reverts the
automaton (proposed change 3), the antichain are_equivalent() still
computes
each automaton's distances once per direction (proposed change 4), and
the
hand-written edge-case tests and the get_terminating_states() comparison
listed under the issue's verification are not added.

Part of #740.

nfa: +refactor Scan each macrostate once in universality and complete…

…ness (#888)

One synchronized pass per macrostate instead of an alphabet loop:

is_universal_antichains: Push posts of all macrostate states into one
SynchronizedExistentialSymbolPostIterator and walk it in lockstep with
the
sorted alphabet. Foreign symbols (outside alphabet range) are skipped;
missing alphabet symbols are detected as gaps and become counterexamples
immediately. Successors computed via unify_targets. Replace std::list
containers with vectors, pruned in one pass each with std::erase_if as
in
antichain inclusion, and move popped macrostates instead of copying. The
macrostate signature pre-filter of the subsumption test is kept.

is_complete: Use vector FIFO queue (head cursor) and byte array for
visited states instead of std::list and std::unordered_set. Compare each
state's sorted symbol posts with required symbols using two-pointer
merge.
Throw on foreign symbols with
same precedence as today, and finish scanning a state's post before
returning false on missing symbols. Keep BFS order and same state
deciding.

Witness mode: Record parent and symbol only at discovery (when cex !=
nullptr), documented as DFS so not necessarily shortest counterexample.

Part of #788. Left for later: storing interned macrostate IDs and
reusing
the cardinality-bucket dominance helpers of antichain inclusion (#785),
which waits on macrostate interning (#783); the counters and benchmarks
of the issue's execution plan. No speedup is measured in this change.

nfa, nft: +fix Check state overflow in the in-place and rvalue concat…

…enation and union paths (#959)

#939 made `State` 32-bit by default and added `check_num_of_states()` to
every path that computes a result state count. The paths it checked were
then refactored upstream (#889, #956 landed the consuming/rvalue
overloads of `concatenate()` and `unite_nondet_with()`), and the
refactored bodies allocate and shift by a `size_t` offset without the
check, so two large automata whose combined state count exceeds
`Limits::max_state` would wrap instead of throwing:

- `Nft::unite_nondet_with(Nft&&)` — appended without
`check_num_of_states()` and inserted `num_of_states_this + state` with
an unchecked `size_t → State` conversion.
- `Nfa::concatenate(Nfa&&)` / `Nft::concatenate(Nft&&)` and the
`concatenate_eps_consuming()` bodies — offsets passed to
`append_shifted()` and `add_state(result_num_of_states - 1)` without the
guard.

This re-applies the #939 invariants to those paths:
`check_num_of_states()` before any operand is consumed, and
`static_cast<State>` on every offset/index that reaches state
arithmetic. The throwing points are already declared `except +` in the
Python bindings, so the error surfaces there as `OverflowError`.

One commit on the devel that already contains #939; it is the delta of
the final rebase round that the squash-merge of #939 did not pick up.

Part of #789.

---
Release: test cases 362 | 356 passed | 2 skipped | 4 failed as expected
(assertions 2749336 | 2749299 passed | 37 failed as expected)
Debug: same counts
64-bit build (MATA_STATE_BITS=64, Release): 362 | 356 passed | 2 skipped
| 4 failed as expected