From 42c03139481ac32b55c725c5d5071d913db53b15 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 09:58:51 -0700 Subject: [PATCH 1/4] 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) From 8e11ae58e9dcf41450fbb8d133675fcffd853263 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 10:06:26 -0700 Subject: [PATCH 2/4] move light_ant_derivative_cofactors into the derivative engine (#10371) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 61 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_derive.h | 19 ++++++++++ src/ast/rewriter/seq_rewriter.cpp | 61 ------------------------------- src/ast/rewriter/seq_rewriter.h | 4 +- 4 files changed, 83 insertions(+), 62 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 9892ffd35c..8bfe4bf96b 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/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 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 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 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)); + } + } diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index e0559bdf1d..08e8631315 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/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); + }; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 508e2dea6d..6b71e47db5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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 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 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 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; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c9c5ea989f..5bad5ae3dc 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/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. From 9e7363bd272cfef869d5cb986ec2ab20f0072574 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 10:08:11 -0700 Subject: [PATCH 3/4] fix unsound regex info for the legacy argument form of re.loop (#10370) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `re.loop` has two accepted AST forms: bounds as decl parameters, `((_ re.loop lo hi) r)` (1 argument, 2 parameters), and bounds as arguments, `(re.loop r lo hi)` (3 arguments, 0 parameters). The plugin accepts arities 1, 2 and 3, and `is_loop` has separate overloads for each form. Only the parameter form was recognized downstream. ### The soundness bug `mk_info_rec`'s `OP_RE_LOOP` case read the bounds solely from `get_decl()->get_num_parameters()`, which is 0 for the argument form, so it silently fell back to the locals `lower_bound = 0, upper_bound = UINT_MAX`. `info::loop` computes ```cpp loop_nullable = (nullable == l_true || lower == 0) ? l_true : nullable; ``` so `lower == 0` forces nullability, and `min_length` collapses to `min_length * 0 = 0`. Net effect: `(re.loop (str.to_re "ab") 1 3)` was reported as `nullable = l_true, min_length = 0`. At the SMT level ```smt2 (declare-const x String) (assert (str.in_re x (re.loop (str.to_re "ab") 1 3))) (assert (= (str.len x) 0)) (check-sat) ``` answered **sat** rather than unsat. The indexed form of the same regex correctly answers unsat. `seq_rewriter::mk_re_loop` already normalizes the argument form to `mk_loop_proper`, which is why this was never observable on the usual paths — it only surfaces where the rewriter is bypassed, as in `seq_monadic`. The `info.nullable` fast path added in #10366 didn't create the bug but widened the path that reaches it. ### The performance bug `derive_core` had no case for the argument form either, so the derivative got stuck as an uninterpreted `re.derivative` term. Instrumenting all three sites that can emit a symbolic `re.derivative` showed that **every one of the 4171 stuck terms** in the regex corpus came from this fall-through (the 512-deep recursion cap and the unnormalizable `re.reverse` site never fired), and 4096 of them came from a single legacy-form loop, whose search then burned its full budget before giving up. ### The fix * `mk_info_rec` branches on `get_num_args()`; for the argument form it reads the bounds from `get_arg(1)`/`get_arg(2)` when they are unsigned numerals, and returns `unknown_info` when they are not. * `derive_core` normalizes the numeral argument forms to `mk_loop_proper`/`mk_loop` and recurses. The block is gated on the cheap `re().is_loop(r)` kind check so that regexes falling through to the later cases don't pay for the `rational` locals. Arguably the right long-term place to normalize is the parser, so the legacy form never reaches the AST at all. Keeping the `mk_info_rec` half is still worthwhile as a guard for API-constructed terms, and the regression test builds the term directly via `mk_app`, so it stays meaningful either way. ### Regression test `src/test/seq_rewriter.cpp` gains a case asserting that `get_info` agrees on the two forms (`nullable == l_false`, `min_length == 2`). Verified to actually catch the bug: reverting `seq_decl_plugin.cpp` and rebuilding gives `ASSERTION VIOLATION` with `nullable=l_true min_length=0`. ### Evaluation Full run over 1545 regex benchmarks with declared statuses, in both transition modes: | | light-ant | brz | |---|---|---| | decided (before → after) | 1462 → **1463** | 1464 → **1465** | | soundness mismatches | 0 → 0 | 0 → 0 | | verdict changes | 1 | 1 (same file) | The one changed file is `L4-01-loop-sat.smt2`: **undef @ 8625 ms → sat @ 0.20 ms**. The corpus contains 1 legacy-form file and 236 indexed-form files, which share the modified `OP_RE_LOOP` path, hence the full A/B rather than a spot check. Timing is neutral. Measured with an interleaved base/fix/base/fix protocol over two saved binaries, since same-binary run-to-run variance (±8%) turned out to exceed the effect: paired best-of-2 over the 315 files taking >1 ms gives a **median ratio of 0.998** (p25/p75 = 0.889/1.075), overall 0.976. `tst_seq_rewriter` passes, `seq_monadic` is ALL PASS in both modes, and the 22172-file QF_S corpus shows no verdict changes and no mismatches. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2 --- src/ast/rewriter/seq_derive.cpp | 16 ++++++++++++++++ src/ast/seq_decl_plugin.cpp | 29 ++++++++++++++++++++++++----- src/test/seq_rewriter.cpp | 28 +++++++++++++++++++++++++++- 3 files changed, 67 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 8bfe4bf96b..39f2ea2a44 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -288,6 +288,22 @@ namespace seq { return mk_deriv_concat(d1, tail); } + // Legacy form where the loop bounds are arguments rather than + // decl parameters: (re.loop r lo hi) and (re.loop r lo). The parser + // accepts these and seq_rewriter normalizes them, but unrewritten + // terms reach here directly. Rewrite to the parameterized form. + if (re().is_loop(r)) { + expr* lo_e = nullptr, * hi_e = nullptr; + rational nlo, nhi; + if (re().is_loop(r, r1, lo_e, hi_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned() && + m_autil.is_numeral(hi_e, nhi) && nhi.is_unsigned()) + return derive_rec(re().mk_loop_proper(r1, nlo.get_unsigned(), nhi.get_unsigned())); + if (re().is_loop(r, r1, lo_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned()) + return derive_rec(re().mk_loop(r1, nlo.get_unsigned())); + } + // δ(r1 \ r2) = δ(r1) ∩ ~δ(r2) if (re().is_diff(r, r1, r2)) { expr_ref d1 = derive_rec(r1); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index d0f45485dd..36310fd3c3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1733,11 +1733,30 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { return i1.complement(); case OP_RE_LOOP: i1 = get_info_rec(e->get_arg(0)); - if (e->get_decl()->get_num_parameters() >= 1) - lower_bound = e->get_decl()->get_parameter(0).get_int(); - if (e->get_decl()->get_num_parameters() == 2) - upper_bound = e->get_decl()->get_parameter(1).get_int(); - return i1.loop(lower_bound, upper_bound); + if (e->get_num_args() == 1) { + if (e->get_decl()->get_num_parameters() >= 1) + lower_bound = e->get_decl()->get_parameter(0).get_int(); + if (e->get_decl()->get_num_parameters() == 2) + upper_bound = e->get_decl()->get_parameter(1).get_int(); + return i1.loop(lower_bound, upper_bound); + } + else { + // legacy form carrying the bounds as arguments: + // (re.loop r lo) and (re.loop r lo hi) + arith_util autil(m); + rational n; + if (e->get_num_args() != 2 && e->get_num_args() != 3) + return unknown_info; + if (!autil.is_numeral(e->get_arg(1), n) || !n.is_unsigned()) + return unknown_info; + lower_bound = n.get_unsigned(); + if (e->get_num_args() == 3) { + if (!autil.is_numeral(e->get_arg(2), n) || !n.is_unsigned()) + return unknown_info; + upper_bound = n.get_unsigned(); + } + return i1.loop(lower_bound, upper_bound); + } case OP_RE_DIFF: if (e->get_num_args() != 2) return unknown_info; diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 55c318aa86..ebfdb09e11 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -16,7 +16,8 @@ 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 + 22. re.loop with bounds as arguments agrees with the indexed form + 23. (Σ*·S)* is flattened to () | Σ*·S --*/ #include "ast/arith_decl_plugin.h" @@ -323,5 +324,30 @@ void tst_seq_rewriter() { } } + // ----------------------------------------------------------------------- + // 22. re.loop with the bounds given as arguments must be interpreted the + // same as the indexed form. get_info used to read the bounds only + // from the decl parameters, which the argument form does not carry, + // so it silently fell back to lo = 0 and reported (ab){1,3} as + // nullable with min_length 0. seq_rewriter normalizes the argument + // form, so this is only observable on paths that bypass it. + // ----------------------------------------------------------------------- + { + arith_util a_util(m); + expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m); + expr_ref indexed(su.re.mk_loop_proper(ab, 1, 3), m); + expr* args[3] = { ab.get(), a_util.mk_int(1), a_util.mk_int(3) }; + expr_ref as_args(m.mk_app(su.get_family_id(), OP_RE_LOOP, 0, nullptr, 3, args), m); + + auto i1 = su.re.get_info(indexed); + auto i2 = su.re.get_info(as_args); + std::cout << "re.loop indexed: " << mk_pp(indexed, m) + << " nullable=" << i1.nullable << " min_length=" << i1.min_length << "\n"; + std::cout << "re.loop arguments: " << mk_pp(as_args, m) + << " nullable=" << i2.nullable << " min_length=" << i2.min_length << "\n"; + ENSURE(i1.nullable == l_false && i1.min_length == 2); + ENSURE(i2.nullable == l_false && i2.min_length == 2); + } + std::cout << "tst_seq_rewriter: all tests passed\n"; } From 2441ae2f3097e386c70bc636287b5f3d27f5d5ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Aug 2026 10:11:15 -0700 Subject: [PATCH 4/4] Update seq_monadic.cpp --- src/ast/rewriter/seq_monadic.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index ecd1903997..2dc65ebaaf 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -40,6 +40,11 @@ TODOs: explored and we can check the variable intersection membership constraints if the new expansion is feasible. Constant characters are consumed at the same time to also prune the choice. +- separate out "live-state" and enumerator over reachable live states: + - make it share live states between callers. + - make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states. + - make use of DFS exploration of derivatives to extract live states without visiting all states up front. + - use it in seq_regex legacy mode that also has this notion.