move light_ant_derivative_cofactors into the derivative engine (#10371)

Follow-up cleanup requested in review of the seq_monadic work. Based
directly on master, independent of #10370.

`light_ant_derivative_cofactors` was implemented in `seq_rewriter`, even
though it is purely a derivative operation: it post-processes the output
of `derive::derivative_cofactors` and uses no rewriter state beyond the
shared `bool_rewriter`. The two sibling entry points, `get_cofactors`
and `brz_derivative_cofactors`, were already thin forwarders into
`seq::derive`, so this one was the odd one out.

### Change

The body moves to `seq::derive`, next to `get_cofactors` and
`derivative_cofactors`, so all three cofactor entry points live in one
place. `seq_rewriter` keeps `light_ant_derivative_cofactors` as an
inline forwarder in the header, matching how the other two are exposed —
no caller changes anywhere (`seq_monadic`, `smt/seq_regex`,
`seq_range_collapse`, `seq_regex_bisim`, and the unit tests all keep
calling it through the rewriter).

| file | |
|---|---|
| `seq_derive.h` | declaration + doc comment |
| `seq_derive.cpp` | +61, the body |
| `seq_rewriter.cpp` | −61, the body |
| `seq_rewriter.h` | forwarder becomes inline, like its two siblings |

The one non-mechanical detail: the splitting step builds its
concatenation with `seq_rewriter::mk_regex_concat`, which stays in the
rewriter because other rewriter code uses it. `derive` already holds the
`m_re` back-reference and calls through it for `mk_inter`, `mk_xor0` and
`is_subset`, so the moved code does the same rather than duplicating the
constructor. The terms produced are identical.

### Verification

Pure refactoring, so this was checked for exact equivalence rather than
for improvement.

* **0 verdict differences** against master over 1545 regex benchmarks,
in light-ant (the mode that exercises this path) and in brz. Decided
counts unchanged at 1462 / 1464.
* `seq_monadic` ALL PASS in both transition modes; `seq_rewriter`,
`seq_regex_bisim` and `regex_range_collapse` all pass.

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

src/ast/rewriter/seq_derive.cpp

@@ -1567,5 +1567,66 @@ namespace seq {
         get_cofactors(m_ele, d, result);
     }
 
+    void derive::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
+        expr_ref_pair_vector brz(m);
+        derivative_cofactors(r, brz);
+
+        obj_map<expr, unsigned> target_index;
+        expr_ref_vector guards(m);
+        expr_ref_vector targets(m);
+
+        auto add = [&](expr* guard, expr* target) {
+            unsigned index = 0;
+            if (target_index.find(target, index)) {
+                expr_ref merged(m);
+                m_br.mk_or(guards.get(index), guard, merged);
+                guards.set(index, merged);
+            }
+            else {
+                target_index.insert(target, targets.size());
+                targets.push_back(target);
+                guards.push_back(guard);
+            }
+        };
+
+        for (auto const& [guard, target] : brz) {
+            ptr_vector<expr> pending;
+            pending.push_back(target);
+            while (!pending.empty()) {
+                expr* t = pending.back();
+                pending.pop_back();
+                expr* left = nullptr, * right = nullptr;
+                if (re().is_union(t, left, right)) {
+                    pending.push_back(right);
+                    pending.push_back(left);
+                }
+                else if (re().is_concat(t, left, right) && re().is_union(left)) {
+                    ptr_vector<expr> heads;
+                    heads.push_back(left);
+                    while (!heads.empty()) {
+                        expr* head = heads.back();
+                        heads.pop_back();
+                        expr* a = nullptr, * b = nullptr;
+                        if (re().is_union(head, a, b)) {
+                            heads.push_back(b);
+                            heads.push_back(a);
+                        }
+                        else {
+                            expr_ref split = m_re.mk_regex_concat(head, right);
+                            add(guard, split);
+                        }
+                    }
+                }
+                else {
+                    add(guard, t);
+                }
+            }
+        }
+
+        result.reset();
+        for (unsigned i = 0; i < targets.size(); ++i)
+            result.push_back(guards.get(i), targets.get(i));
+    }
+
 }
 

src/ast/rewriter/seq_derive.h

@@ -261,6 +261,25 @@ namespace seq {
          */
         void derivative_cofactors(expr* r, expr_ref_pair_vector& result);
 
+        /**
+         * Compute the Brzozowski cofactors of r (derivative_cofactors above),
+         * then expose the nondeterminism that a union leaf hides: a target of
+         * the form (s1 | ... | sn), or (s1 | ... | sn) . tail, is split into
+         * one cofactor per alternative si (resp. si . tail). Splitting is
+         * applied recursively, so nested unions are flattened as well.
+         *
+         * Splitting can make two originally distinct cofactors reach the same
+         * target; such cofactors are merged back into a single pair whose
+         * guard is the disjunction of the original guards. The result is
+         * therefore still a list of distinct targets, but each one is a
+         * single Antimirov-style alternative rather than a union state.
+         *
+         * The guards are not required to be mutually exclusive after merging,
+         * and the transition relation is genuinely nondeterministic: a
+         * character may be accepted by several of the returned guards.
+         */
+        void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result);
+
     };
 
 }

src/ast/rewriter/seq_rewriter.cpp

@@ -2931,67 +2931,6 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
     return result;
 }
 
-void seq_rewriter::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
-    expr_ref_pair_vector brz(m());
-    m_derive.derivative_cofactors(r, brz);
-
-    obj_map<expr, unsigned> target_index;
-    expr_ref_vector guards(m());
-    expr_ref_vector targets(m());
-
-    auto add = [&](expr* guard, expr* target) {
-        unsigned index = 0;
-        if (target_index.find(target, index)) {
-            expr_ref merged(m());
-            m_br.mk_or(guards.get(index), guard, merged);
-            guards.set(index, merged);
-        }
-        else {
-            target_index.insert(target, targets.size());
-            targets.push_back(target);
-            guards.push_back(guard);
-        }
-    };
-
-    for (auto const& [guard, target] : brz) {
-        ptr_vector<expr> pending;
-        pending.push_back(target);
-        while (!pending.empty()) {
-            expr* t = pending.back();
-            pending.pop_back();
-            expr* left = nullptr, * right = nullptr;
-            if (re().is_union(t, left, right)) {
-                pending.push_back(right);
-                pending.push_back(left);
-            }
-            else if (re().is_concat(t, left, right) && re().is_union(left)) {
-                ptr_vector<expr> heads;
-                heads.push_back(left);
-                while (!heads.empty()) {
-                    expr* head = heads.back();
-                    heads.pop_back();
-                    expr* a = nullptr, * b = nullptr;
-                    if (re().is_union(head, a, b)) {
-                        heads.push_back(b);
-                        heads.push_back(a);
-                    }
-                    else {
-                        expr_ref split = mk_regex_concat(head, right);
-                        add(guard, split);
-                    }
-                }
-            }
-            else {
-                add(guard, t);
-            }
-        }
-    }
-
-    result.reset();
-    for (unsigned i = 0; i < targets.size(); ++i)
-        result.push_back(guards.get(i), targets.get(i));
-}
-
 expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     expr_ref _r1(r1, m()), _r2(r2, m());
     expr *a1, *b1, *a2, *b2;

src/ast/rewriter/seq_rewriter.h

@@ -480,7 +480,9 @@ public:
     form (s1 | ... | sn) or (s1 | ... | sn) . tail. Cofactors with the same
     resulting target are merged by disjoining their guards.
     */
-    void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result);
+    void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
+        m_derive.light_ant_derivative_cofactors(r, result);
+    }
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.