From 42c03139481ac32b55c725c5d5071d913db53b15 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 09:58:51 -0700 Subject: [PATCH] flatten (Sigma*.S)* to () | Sigma*.S (#10373) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## 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 | 10 ++++++++++ src/test/seq_monadic_bench.cpp | 9 +++++++++ src/test/seq_rewriter.cpp | 29 ++++++++++++++++++++++++++++- 3 files changed, 47 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d5f42cbbe9..508e2dea6d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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))) { diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index ed56846553..09fca17cec 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/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& 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); diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 9557b9cfc6..55c318aa86 100644 --- a/src/test/seq_rewriter.cpp +++ b/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)