flatten (Sigma*.S)* to () | Sigma*.S (#10373)

## Summary

Two related changes:

1. Rewrite `(Σ*·S)*` to the flat form `() | Σ*·S` in
`seq_rewriter::mk_re_star`.
2. Make `seq_monadic_bench` normalize its inputs, so that rewriter-level
changes are
   observable at all.

## The rewrite

`Σ*·S` is idempotent under concatenation. Any word of `(Σ*·S)·(Σ*·S)`
factors as
`(Σ*·S·Σ*)·S`, and the leading `Σ*·S·Σ*` is absorbed by `Σ*`, so the
word is again in
`Σ*·S`. Hence `L·L ⊆ L`, and therefore `L* = () | L`.

This is the same absorption argument the subset checker already
implements — see the
"prefix absorption" rule `P·R' ⊆ Σ*·R'` in `seq_subset.cpp`. It was
simply never applied
to the star.

The two forms denote the same language but are not equally cheap to
determinize. Under
the star, every residual carries a trailing `(Σ*·S)*` factor, so the
derivative automaton
keeps a separate copy of the `S`-tracking states for each unfolding. The
flat form drops
that factor and the copies collapse.

Measured live-state counts of the derivative automaton:

| regex | star form | flat form |
|---|---|---|
| `nonA ∩ (Σ*·b·Σ^5)*` | 904 | **65** |
| `core ∩ (Σ*·b·Σ^5)*` | 1807 | **129** |

roughly a 14x reduction.

The shape is not exotic: it is what a "contains" pattern under a star
looks like, and it
occurs in 27 of the 1545 regex benchmarks I track.

## The bench change

`seq_monadic_bench` handed `seq_monadic` the raw parsed regex, whereas
in the solver
`seq_regex` only ever sees terms that `asserted_formulas` has already
rewritten. The
bench therefore could not observe a rewriter-level change at all — the
rewrite above
measured as *exactly zero* difference across all 1545 benchmarks in both
modes until the
bench was made to normalize.

Each `str.in_re` regex argument now goes through `th_rewriter` before
reaching
`seq_monadic`, placed ahead of the multi-membership merge so that
`mk_regex_inter_normalize` also receives normalized operands.

This is closer to production but not identical to it:
`asserted_formulas` rewrites whole
assertions and can propagate across them, while this rewrites each
membership's regex in
isolation.

## Measurements

Combined effect over 1545 regex benchmarks, against master:

| mode | decided | gained | lost | mismatches | status conflicts |
|---|---|---|---|---|---|
| light-ant | 1464 → **1467** | 4 | 1 | 0 | 0 |
| brz | 1466 → **1469** | 4 | 1 | 0 | 0 |

Gained in both modes:

- `MargusRegex/levels/L4-01-loop-sat`
- `ClemensRegex/generated/split_membership_medium_sat_0012`
- `ClemensRegex/generated/split_membership_medium_sat_0000`
- `ClemensRegex/generated_easy/split_membership_easy_unsat_0009`

The single loss per mode comes from the normalization, not the rewrite,
and is marginal in
both cases: `easy_unsat_0006` (light-ant) took 5.5 s and
`medium_sat_0036` (brz) took
3.9 s on master, and both now trip a cap slightly earlier. Each is
mode-specific —
`easy_unsat_0006` is still decided in `brz`, and `medium_sat_0036` was
already undecided in
`light-ant` on master.

Runtime, paired best-of-2 over two interleaved rounds:

| | outside `ClemensRegex/generated` | `ClemensRegex/generated` |
|---|---|---|
| light-ant | +2.2% | +12.0% |
| brz | −0.2% | +11.3% |

Outside the `generated` family this is inside the ±8% run-to-run noise
of the measurement
machine. Within that family the increase is expected and is what buys
the extra
decisions: those files previously tripped the `state_cap` bail early,
and with the smaller
automaton the search gets further before exhausting the budget. The cost
stays bounded by
the existing budget.

The rule fires only on the `Σ*·S` shape:

```
(simplify (re.* (re.++ re.all (str.to_re "b"))))
  → (re.union (re.++ re.all (str.to_re "b")) (str.to_re ""))

(simplify (re.* (re.++ (str.to_re "a") (str.to_re "b"))))
  → (re.* (str.to_re "ab"))
```

## Tests

Adds case 22 to `src/test/seq_rewriter.cpp`: checks that `(Σ*·b)*` is no
longer a star
after rewriting, and pins the semantics with three solver queries —
`"ab"` and `""` are
members, `"ba"` is not.

`seq_rewriter`, `seq_monadic`, `seq_regex_bisim` and
`regex_range_collapse` all pass in
both `light-ant` and `brz` modes.

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

src/ast/rewriter/seq_rewriter.cpp

@@ -4286,6 +4286,16 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         result = re().mk_star(re().mk_union(b1, c1));
         return BR_REWRITE2;
     }
+    // (Σ*·S)* = () | Σ*·S.
+    // Σ*·S is idempotent under concatenation: Σ*·S·Σ*·S = (Σ*·S·Σ*)·S ⊆ Σ*·S,
+    // since any prefix is absorbed by Σ*. Hence L·L ⊆ L and L* = () | L.
+    // Keeping the flat form avoids a large blowup in the derivative automaton.
+    if (re().is_concat(a, b, c) && re().is_full_seq(b)) {
+        sort* seq_sort = nullptr;
+        VERIFY(m_util.is_re(a, seq_sort));
+        result = re().mk_union(re().mk_epsilon(seq_sort), a);
+        return BR_REWRITE1;
+    }
     if (m().is_ite(a, c, b1, c1)) {
         if ((re().is_full_char(b1) || re().is_full_seq(b1)) &&
             (re().is_full_char(c1) || re().is_full_seq(c1))) {

src/test/seq_monadic_bench.cpp

@@ -25,6 +25,7 @@ Abstract:
 #include "ast/arith_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/seq_monadic.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
@@ -100,6 +101,7 @@ lbool run_file(
     seq_util u(m);
     arith_util a(m);
     seq_rewriter rw(m);
+    th_rewriter trw(m);
     trail_stack undo_trail;
     seq_monadic mon(rw, undo_trail, mode);
 
@@ -197,6 +199,13 @@ lbool run_file(
             return;
         }
         obj_map<expr, expr*>& map = is_var ? var_re : term_re;
+        // Normalize the regex the way asserted_formulas normalizes assertions
+        // before seq_regex hands them to seq_monadic. Without this the bench
+        // measures raw parsed regexes, which no production path ever sees.
+        expr_ref normalized(r, m);
+        trw(normalized);
+        pin.push_back(normalized);
+        r = normalized;
         expr* previous = nullptr;
         if (map.find(s, previous)) {
             expr_ref intersection = rw.mk_regex_inter_normalize(previous, r);

src/test/seq_rewriter.cpp

@@ -16,6 +16,7 @@ Tests:
  18. Solver: (str.in_re x (re.range x x)) unsat when len(x)=2
  19. Solver: inverted symbolic bounds make membership unsatisfiable
  20. Solver: contradictory constant lexical bounds are unsatisfiable
+ 22. (Σ*·S)* is flattened to () | Σ*·S
 --*/
 
 #include "ast/arith_decl_plugin.h"
@@ -276,7 +277,33 @@ void tst_seq_rewriter() {
             ENSURE(res == l_true);
         }
 
-        // 20. unsat: contradictory constant lexical bounds.
+        // 22. (Σ*·S)* is rewritten to the flat form () | Σ*·S.
+        //     Σ*·S is idempotent under concatenation — Σ*·S·Σ*·S = (Σ*·S·Σ*)·S
+        //     is again of the form Σ*·S — so its Kleene star contributes
+        //     nothing beyond the empty word. The star form is exponentially
+        //     more expensive to determinize, so the flat form is kept.
+        {
+            expr_ref sigma_star(su.re.mk_full_seq(re_sort), m);
+            expr_ref b_re(su.re.mk_to_re(su.str.mk_string(zstring('b'))), m);
+            expr_ref star(su.re.mk_star(su.re.mk_concat(sigma_star, b_re)), m);
+            expr_ref e(star);
+            rw(e);
+            std::cout << "(sigma* b)* flattened: " << mk_pp(e, m) << "\n";
+            ENSURE(!su.re.is_star(e));
+
+            // Semantics: L* = words ending in "b", plus the empty word.
+            auto member = [&](char const* w) {
+                smt_params sp;
+                smt::context ctx(m, sp);
+                ctx.assert_expr(su.re.mk_in_re(su.str.mk_string(w), star));
+                return ctx.check();
+            };
+            ENSURE(member("ab") == l_true);
+            ENSURE(member("") == l_true);
+            ENSURE(member("ba") == l_false);
+        }
+
+
         //     "2024-01-01" < x < "2024-12-31" and x < "2023-01-01".
         //     Since "2023-01-01" < "2024-01-01", no such x exists.
         if (false)