Consume live states lazily in dfs_atoms (#10381)

Builds on `seq-live-states`. `reachable_live` returns a lazy iterator,
but `dfs_atoms` drained it into a `ptr_vector` before exploring
anything:

```cpp
auto live = m_live_states.reachable_live(R);
for (expr* q : live)
    targets.push_back(q);
```

so the search was always driven to completion and the laziness had no
effect at its only consumer. This explores each live state as it is
produced and stops at the first `l_true`, so a root whose live set is
exponential is tractable whenever a witness appears early. The
`failed()` check moves after the loop, since a cap or resource overrun
only matters if no branch succeeded.

### Results

1545 regex benchmarks, 20s timeout, decided = `sat` or `unsat`. Relative
to `seq-live-states`:

| mode | decided | time |
|---|---|---|
| brz | 1466 → **1472** | 0.978 |
| light-ant | 1463 → **1469** | 0.886 |

No verdict changes and no losses in either mode; it is also slightly
faster, since the states that are never expanded are never paid for.

The six gains per mode include the `noodler_killer` nth-from-the-end
family, where the live set is exponential but a witness is found after a
few dozen states. `noodler_killer_1_nth_from_end` goes from `undef` to
`sat` in 0.165 ms.

Relative to `master` the branch with this change is +8/−3 (brz) and
+7/−3 (light-ant), at 0.86x the time.

### Two follow-ups, not addressed here

**The 3 files that regress against `master`**
(`split_membership_medium_sat_0000`, `easy_sat_0019`, `medium_sat_0046`)
all bail on **budget**, not the state cap — the signature of exploration
order rather than a cap that is too tight. `m_live_frontier` is appended
by `mark_live`, which propagates backward through predecessors, so an
ancestor is emitted after the descendant that revealed it; `master`
emits in strict BFS interning order. I prototyped replacing backward
propagation with a root-independent per-state liveness memo to restore
BFS order: it fixes all 3 (`medium_sat_0046` returns in 9 ms) but loses
`medium_sat_0003`/`0026`/`0036`/`0052`, which the current order wins,
and costs 31% on light-ant because per-state forward liveness is
quadratic where backward propagation is linear. The two orders prefer
different things — nearest the root vs nearest a nullable state — and
neither dominates, so this needs a real decision rather than a swap.
Happy to share that prototype.

**Splitting `get_cached_cofactors` into `m_brz_cofactor_cache` /
`m_ant_cofactor_cache`** fixes a latent bug on `master`, where the cache
was keyed on `r` alone and a brz cofactor list could be served to a
light-ant query. That fix is independent of the traversal rewrite and
might be worth landing separately.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2

src/ast/rewriter/seq_monadic.cpp

@@ -444,27 +444,13 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
     // A variable: the last atom is a plain membership in R, otherwise the variable drives
     // the derivative automaton from R to some live state q, which splits the search.
     bool last_atom = (i + 1 == atoms.size());
-    ptr_vector<expr> targets;
-    if (last_atom)
-        targets.push_back(nullptr);
-    else {
-        auto live = m_live_states.reachable_live(R);
-        for (expr* q : live)
-            targets.push_back(q);
-        if (live.failed()) {
-            m_stats.inc_bail(
-                live.failure_reason() == seq::live_states::failure::state_cap ?
-                bail_reason::state_cap : bail_reason::resource);
-            return l_undef;
-        }
-    }
-
     unsigned vi = var_index(a.var.get());
     uint64_t pos = (static_cast<uint64_t>(mi) << 32) | i;
     uint64_t last = 0;
     bool finalize = m_last_occ.find(a.var.get(), last) && last == pos;
-    bool any_undef = false;
-    for (expr* target : targets) {
+
+    // Explores one split target; the caller stops at the first l_true.
+    auto explore = [&](expr* target) -> lbool {
         m_groups[vi].push_back(component{ a.var.get(), R, target });
         // The group's emptiness test has to be run at some point anyway; running it as
         // soon as the group is complete (or as soon as it holds several components, where
@@ -485,6 +471,19 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
                 --m_undef_vars;
         }
         m_groups[vi].pop_back();
+        return r;
+    };
+
+    if (last_atom)
+        return explore(nullptr);
+
+    // The live states are consumed as they are produced, so a satisfying branch under an
+    // early state means the rest of the reachable set is never expanded.  That is what
+    // makes a root with an exponential live set tractable when a witness is found early.
+    bool any_undef = false;
+    auto live = m_live_states.reachable_live(R);
+    for (expr* q : live) {
+        lbool r = explore(q);
         if (r == l_true)
             return l_true;
         if (r == l_undef) {
@@ -493,6 +492,14 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
             any_undef = true;
         }
     }
+    // Short of the full reachable set the unexplored split states could still hold a
+    // solution, so the l_false the loop would otherwise report is not justified.
+    if (live.failed()) {
+        m_stats.inc_bail(
+            live.failure_reason() == seq::live_states::failure::state_cap ?
+            bail_reason::state_cap : bail_reason::resource);
+        return l_undef;
+    }
     return any_undef ? l_undef : l_false;
 }