From 871a2b3bc89134676649966b470aa5246944c0d3 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 12 Jun 2026 15:18:14 +0200 Subject: [PATCH 1/6] Porting seq_split to master --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/seq_rewriter.cpp | 113 +++---- src/ast/rewriter/seq_rewriter.h | 13 +- src/ast/rewriter/seq_split.cpp | 501 ++++++++++++++++++++++++++++++ src/ast/rewriter/seq_split.h | 118 +++++++ 5 files changed, 682 insertions(+), 64 deletions(-) create mode 100644 src/ast/rewriter/seq_split.cpp create mode 100644 src/ast/rewriter/seq_split.h diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index cfcc179bca..be8449978d 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -40,6 +40,7 @@ z3_add_component(rewriter seq_axioms.cpp seq_eq_solver.cpp seq_subset.cpp + seq_split.cpp seq_rewriter.cpp seq_regex_bisim.cpp seq_skolem.cpp diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1654c57771..0028562ff1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3999,58 +3999,54 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { //do not concatenate [], it is a deade-end return result; } - else { - // Classical Brzozowski union: keep the derivative tree free of - // antimirov-union nodes so the bisimulation procedure sees a - // single regex tree whose leaves are XOR pairs. - return mk_der_union(result, mk_der_concat(is_n, dr2)); - } + // Classical Brzozowski union: keep the derivative tree free of + // antimirov-union nodes so the bisimulation procedure sees a + // single regex tree whose leaves are XOR pairs. + return mk_der_union(result, mk_der_concat(is_n, dr2)); } - else if (re().is_star(r, r1)) { + if (re().is_star(r, r1)) { return mk_der_concat(mk_derivative_rec(ele, r1), r); } - else if (re().is_plus(r, r1)) { + if (re().is_plus(r, r1)) { expr_ref star(re().mk_star(r1), m()); return mk_derivative_rec(ele, star); } - else if (re().is_union(r, r1, r2)) { + if (re().is_union(r, r1, r2)) { return mk_der_union(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - else if (re().is_intersection(r, r1, r2)) { + if (re().is_intersection(r, r1, r2)) { return mk_der_inter(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - else if (re().is_diff(r, r1, r2)) { + if (re().is_diff(r, r1, r2)) { return mk_der_inter(mk_derivative_rec(ele, r1), mk_der_compl(mk_derivative_rec(ele, r2))); } - else if (re().is_xor(r, r1, r2)) { + if (re().is_xor(r, r1, r2)) { return mk_der_xor(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - else if (m().is_ite(r, p, r1, r2)) { + if (m().is_ite(r, p, r1, r2)) { // there is no BDD normalization here result = m().mk_ite(p, mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); return result; } - else if (re().is_opt(r, r1)) { + if (re().is_opt(r, r1)) { return mk_derivative_rec(ele, r1); } - else if (re().is_complement(r, r1)) { + if (re().is_complement(r, r1)) { return mk_der_compl(mk_derivative_rec(ele, r1)); } - else if (re().is_loop(r, r1, lo)) { + if (re().is_loop(r, r1, lo)) { if (lo > 0) { lo--; } result = mk_derivative_rec(ele, r1); - //do not concatenate with [] (emptyset) + // do not concatenate with [] (emptyset) if (re().is_empty(result)) { return result; } - else { - //do not create loop r1{0,}, instead create r1* - return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo))); - } + // do not create loop r1{0,}, instead create r1* + return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo))); } - else if (re().is_loop(r, r1, lo, hi)) { + if (re().is_loop(r, r1, lo, hi)) { if (hi == 0) { return mk_empty(); } @@ -4059,19 +4055,16 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { lo--; } result = mk_derivative_rec(ele, r1); - //do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain + // do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain if (re().is_empty(result) || hi == 0) { return result; } - else { - return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); - } + return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); } - else if (re().is_full_seq(r) || - re().is_empty(r)) { + if (re().is_full_seq(r) || re().is_empty(r)) { return expr_ref(r, m()); } - else if (re().is_to_re(r, r1)) { + if (re().is_to_re(r, r1)) { // r1 is a string here (not a regexp) expr_ref hd(m()), tl(m()); if (get_head_tail(r1, hd, tl)) { @@ -4084,16 +4077,16 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_concat(result, r1); return result; } - else if (str().is_empty(r1)) { - //observe: str().is_empty(r1) checks that r = () = epsilon - //while mk_empty() = [], because deriv(epsilon) = [] = nothing + if (str().is_empty(r1)) { + // observe: str().is_empty(r1) checks that r = () = epsilon + // while mk_empty() = [], because deriv(epsilon) = [] = nothing return mk_empty(); } - else if (str().is_itos(r1)) { + if (str().is_itos(r1)) { // - // here r1 = (str.from_int r2) and r2 is non-ground + // here r1 = (str.from_int r2) and r2 is non-ground // or else the expression would have been simplified earlier - // so r1 must be nonempty and must consists of decimal digits + // so r1 must be nonempty and must consists of decimal digits // '0' <= elem <= '9' // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // @@ -4105,19 +4098,17 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { auto a3 = m().mk_eq(hd, ele); auto inner = m().mk_and(a2, a3); m_br.mk_and(a0, a1, inner, result); - tl = re().mk_to_re(mk_seq_rest(r1)); - return re_and(result, tl); - } - else { - // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence - // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) - hd = mk_seq_first(r1); - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); } + // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence + // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) + hd = mk_seq_first(r1); + m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); + tl = re().mk_to_re(mk_seq_rest(r1)); + return re_and(result, tl); } - else if (re().is_reverse(r, r1)) { + if (re().is_reverse(r, r1)) { if (re().is_to_re(r1, r2)) { // First try to extract hd and tl such that r = hd ++ tl and |tl|=1 expr_ref hd(m()), tl(m()); @@ -4129,22 +4120,20 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd))); return result; } - else if (str().is_empty(r2)) { + if (str().is_empty(r2)) { return mk_empty(); } - else { - // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else [])) - // hd = first of reverse(r2) i.e. last of r2 - // tl = rest of reverse(r2) i.e. butlast of r2 - //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); - hd = mk_seq_last(r2); - // factor nested constructor calls to enforce deterministic argument evaluation order - auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); - auto a_eq = m().mk_eq(hd, ele); - m_br.mk_and(a_non_empty, a_eq, result); - tl = re().mk_to_re(mk_seq_butlast(r2)); - return re_and(result, re().mk_reverse(tl)); - } + // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else [])) + // hd = first of reverse(r2) i.e. last of r2 + // tl = rest of reverse(r2) i.e. butlast of r2 + // hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); + hd = mk_seq_last(r2); + // factor nested constructor calls to enforce deterministic argument evaluation order + auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); + auto a_eq = m().mk_eq(hd, ele); + m_br.mk_and(a_non_empty, a_eq, result); + tl = re().mk_to_re(mk_seq_butlast(r2)); + return re_and(result, re().mk_reverse(tl)); } } else if (re().is_range(r, r1, r2)) { @@ -4163,11 +4152,9 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_inter(p1, p2); return result; } - else { - return mk_empty(); - } + return mk_empty(); } - expr* e1 = nullptr, * e2 = nullptr; + expr *e1 = nullptr, *e2 = nullptr; if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) { SASSERT(u().is_char(e1)); // Use mk_der_cond to normalize @@ -4185,7 +4172,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } else if (re().is_of_pred(r, p)) { array_util array(m()); - expr* args[2] = { p, ele }; + expr *args[2] = {p, ele}; result = array.mk_select(2, args); // Use mk_der_cond to normalize STRACE(seq_verbose, tout << "deriv of_pred" << std::endl;); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 618124e10b..1ae892a100 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -18,6 +18,7 @@ Notes: --*/ #pragma once +#include "seq_split.h" #include "ast/seq_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" @@ -130,6 +131,7 @@ class seq_rewriter { seq_util m_util; seq_subset m_subset; + seq_split m_split; arith_util m_autil; bool_rewriter m_br; // re2automaton m_re2aut; @@ -346,7 +348,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), // m_re2aut(m), + m_util(m), m_subset(m_util.re), m_split(*this), m_autil(m), m_br(m, p), // m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) { } @@ -397,6 +399,15 @@ public: return result; } + // Split decomposition (sigma) of a regex; see seq_split.h. `oracle` (optional) + // prunes non-viable splits during generation. + bool split(expr* r, split_set& out, unsigned threshold, + const split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { + return m_split.compute(r, out, threshold, mode, oracle); + } + + void simplify_split(split_set& s) { m_split.simplify(s); } + /** * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences */ diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp new file mode 100644 index 0000000000..f2026b67e9 --- /dev/null +++ b/src/ast/rewriter/seq_split.cpp @@ -0,0 +1,501 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_split.cpp + +Abstract: + + Regex split decomposition (the split function sigma). See seq_split.h. + +Author: + + Nikolaj Bjorner (nbjorner) 2026-6-10 + Clemens Eisenhofer 2026-6-10 + +--*/ + +#include "ast/rewriter/seq_split.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/ast_pp.h" +#include "util/obj_hashtable.h" +#include "util/stack.h" + +seq_split::seq_split(seq_rewriter& rw) : + m_rw(rw), m_subset(rw.u().re) {} + +ast_manager& seq_split::m() const { return m_rw.m(); } +seq_util& seq_split::seq() const { return m_rw.u(); } +seq_util::rex& seq_split::re() const { return m_rw.u().re; } + +// Add unless the (optional) lookahead oracle prunes it. +void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const { + if (!oracle || oracle(d, n)) + out.push_back(split_pair(d, n, m())); +} + +// Cross-product intersection of two split-sets (split algebra): +// S1 cap S2 = { | in S1, in S2 }. +// Pairs where any component is bottom (the empty regex) are dropped. +bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& result, + unsigned threshold, split_oracle const& oracle) const { + const seq_util::rex& r = re(); + for (auto const& p1 : s1) { + for (auto const& p2 : s2) { + if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) || + r.is_empty(p1.m_n) || r.is_empty(p2.m_n)) + continue; + const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m()); + const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m()); + push(result, oracle, di, ni); + if (result.size() > threshold) + return false; + } + } + return true; +} + +// Complement of a split-set via De Morgan: ~S = cap_{s in S} ~s with +// ~ = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }. +// May produce up to 2^|sp| pairs (bounded by the threshold). A threshold +// overrun must abort entirely: a partial fold is a strictly weaker (unsound) +// split-set, since each ~sp[i] further constrains ~S. +bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& result, + const unsigned threshold, split_oracle const& oracle) const { + + seq_util::rex& r = re(); + sort* re_sort = r.mk_re(seq_sort); + const expr_ref full(r.mk_full_seq(re_sort), m()); // .* + if (sp.empty()) { // ~{} = <.*, .*> + push(result, oracle, full, full); + return true; + } + // The acc/next pairs carry genuine output-orientation N components (the De + // Morgan ~ = {<~D,.*>, <.*,~N>}), so the oracle prunes them soundly and + // keeps the 2^|sp| fold from blowing up. + split_set acc; + push(acc, oracle, r.mk_complement(sp[0].m_d), full); + push(acc, oracle, full, r.mk_complement(sp[0].m_n)); + for (unsigned i = 1; i < sp.size(); ++i) { + split_set next; + push(next, oracle, r.mk_complement(sp[i].m_d), full); + push(next, oracle, full, r.mk_complement(sp[i].m_n)); + split_set tmp; + if (!intersect(acc, next, tmp, threshold, oracle)) + return false; + acc = std::move(tmp); + if (acc.empty()) // intersection empty => ~S is empty + break; + if (acc.size() > threshold) + return false; + } + result.append(acc); + return true; +} + +bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mode mode, + split_oracle const& oracle) { + SASSERT(r); + seq_util& sq = seq(); + seq_util::rex& rex = re(); + ast_manager& mm = m(); + + sort* seq_sort = nullptr; + if (!sq.is_re(r, seq_sort)) + return false; + + // bottom: sigma(empty) = {} (the empty split-set) + if (rex.is_empty(r)) + return true; + + // epsilon: sigma(eps) = { } + if (rex.is_epsilon(r)) { + const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + push(result, oracle, eps, eps); + return true; + } + + expr* a = nullptr, *b = nullptr; + + // to_re(s): split the literal word s at every position. + expr* s = nullptr; + if (rex.is_to_re(r, s)) { + zstring str; + if (sq.str.is_string(s, str)) { + for (unsigned i = 0; i <= str.length(); ++i) { + const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), mm); + const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), mm); + push(result, oracle, p, q); + } + return true; + } + // a single symbolic unit behaves like one token: { , } + if (sq.str.is_unit(s)) { + const expr_ref ex(r, mm); + const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + push(result, oracle, eps, ex); + push(result, oracle, ex, eps); + return true; + } + // to_re over a non-literal sequence: not handled. + return false; + } + + // single-character class alpha (., [lo-hi], of_pred): + // sigma(alpha) = { , } + if (rex.is_full_char(r) || rex.is_range(r) || rex.is_of_pred(r)) { + const expr_ref ex(r, mm); + const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + push(result, oracle, eps, ex); + push(result, oracle, ex, eps); + return true; + } + + // .* : sigma(.*) = { <.*, .*> } + if (rex.is_full_seq(r)) { + const expr_ref ex(r, mm); + push(result, oracle, ex, ex); + return true; + } + + // union: sigma(r0 | ... | r_{n-1}) = U sigma(ri) (re.union may be n-ary) + if (rex.is_union(r)) { + app* ap = to_app(r); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + if (!compute(ap->get_arg(i), result, threshold, mode, oracle)) + return false; + } + return true; + } + + // concat: sigma(r0...r_{n-1}) = U_i (r0...r_{i-1}) . sigma(ri) . (r_{i+1}...r_{n-1}) + // (re.++ may be n-ary) + if (rex.is_concat(r)) { + app* ap = to_app(r); + const unsigned n = ap->get_num_args(); + for (unsigned i = 0; i < n; ++i) { + // Sound to pass the oracle into the sub-computation: N_inner.Sigma* + // over-approximates the final N_inner.right, so a prune here is a + // prune of the final pair too (prefix-compatible test). + split_set sigma_arg; + if (!compute(ap->get_arg(i), sigma_arg, threshold, mode, oracle)) + return false; + + expr_ref left(mm), right(mm); + if (i == 0) + left = rex.mk_epsilon(seq_sort); + else { + for (unsigned j = 0; j < i; ++j) { + expr* arg = ap->get_arg(j); + left = left ? expr_ref(rex.mk_concat(left, arg), mm) : expr_ref(arg, mm); + } + } + if (i == n - 1) + right = rex.mk_epsilon(seq_sort); + else { + right = ap->get_arg(i + 1); + for (unsigned j = i + 2; j < n; ++j) { + expr* arg = ap->get_arg(j); + right = rex.mk_concat(right, arg); + } + } + + for (auto const& [d, nn] : sigma_arg) { + const expr_ref p = m_rw.mk_re_append(left, d); + const expr_ref q = m_rw.mk_re_append(nn, right); + push(result, oracle, p, q); + } + } + return true; + } + + // star: sigma(a*) = { } cup a*.sigma(a).a* + if (rex.is_star(r, a)) { + const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + push(result, oracle, eps, eps); + split_set sa; + if (!compute(a, sa, threshold, mode, oracle)) + return false; + for (auto const& [d, n] : sa) { + const expr_ref p = m_rw.mk_re_append(r, d); // a*.D + const expr_ref q = m_rw.mk_re_append(n, r); // N.a* + push(result, oracle, p, q); + } + return true; + } + + // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) + if (rex.is_plus(r, a)) { + const expr_ref star(rex.mk_star(a), mm); // a* + split_set sa; + if (!compute(a, sa, threshold, mode, oracle)) + return false; + for (auto const& [d, n] : sa) { + const expr_ref p = m_rw.mk_re_append(star, d); + const expr_ref q = m_rw.mk_re_append(n, star); + push(result, oracle, p, q); + } + return true; + } + + // intersection: sigma(r0 & ... & r_{n-1}) = cap sigma(ri) (re.inter may be n-ary) + if (rex.is_intersection(r)) { + if (mode == split_mode::weak) + return false; + app* ap = to_app(r); + const unsigned n = ap->get_num_args(); + split_set current; + if (!compute(ap->get_arg(0), current, threshold, mode, oracle)) + return false; + // A give-up on any conjunct must propagate as a give-up: silently treating + // it as the empty split-set would collapse the whole intersection to bottom + // and be misreported as an (unsound) conflict. + for (unsigned i = 1; i < n && !current.empty(); ++i) { + split_set arg_i, tmp; + if (!compute(ap->get_arg(i), arg_i, threshold, mode, oracle)) + return false; + if (!intersect(current, arg_i, tmp, threshold, oracle)) + return false; + current = std::move(tmp); + } + result.append(current); + return true; + } + + // complement: sigma(~a) = ~sigma(a). + // The body is computed WITHOUT the oracle (the body's pairs are inverted, so + // their N is unrelated to the output N); the oracle is re-applied in complement(). + if (rex.is_complement(r, a)) { + if (mode == split_mode::weak) + return false; + split_set sa; + if (!compute(a, sa, threshold, mode)) + return false; + return complement(seq_sort, sa, result, threshold, oracle); + } + + // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b). + // sigma(b) (used only inside the complement) is computed WITHOUT the oracle. + if (rex.is_diff(r, a, b)) { + if (mode == split_mode::weak) + return false; + split_set sa, sb, sb_compl, tmp; + if (!compute(a, sa, threshold, mode, oracle)) + return false; + if (!compute(b, sb, threshold, mode)) + return false; + if (!complement(seq_sort, sb, sb_compl, threshold, oracle)) + return false; + if (!intersect(sa, sb_compl, tmp, threshold, oracle)) + return false; + result.append(tmp); + return true; + } + + // bounded loop / ite / other: not handled (paper "v1: bail"). + TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, mm) << "\n";); + return false; +} + +// same-D / same-N merge (paper eqs. 1 & 2): +// { , } -> (by_left = true, group by D) +// { , } -> (by_left = false, group by N) +// Only fires on syntactically-identical (perfectly-shared) key components, so +// it is a conservative instance of the rule. +void seq_split::merge_by(split_set& pairs, const bool by_left) const { + ast_manager& mm = m(); + obj_map idx; // key component -> position in `out` + split_set out; + for (auto const& p : pairs) { + expr* key = by_left ? p.m_d.get() : p.m_n.get(); + expr* other = by_left ? p.m_n.get() : p.m_d.get(); + unsigned pos; + if (idx.find(key, pos)) { + expr* prev = by_left ? out[pos].m_n.get() : out[pos].m_d.get(); + const expr_ref u(m_rw.mk_regex_union_normalize(prev, other), mm); + if (by_left) + out[pos].m_n = u; + else + out[pos].m_d = u; + } + else { + idx.insert(key, out.size()); + out.push_back(p); + } + } + pairs.swap(out); +} + +void seq_split::simplify(split_set& pairs) const { + seq_util::rex& r = re(); + + // 1. drop pairs with a bottom (empty-language) component. + unsigned w = 0; + for (unsigned i = 0; i < pairs.size(); ++i) { + if (r.is_empty(pairs[i].m_d) || r.is_empty(pairs[i].m_n)) + continue; + if (w != i) + pairs[w] = pairs[i]; + ++w; + } + pairs.shrink(w); + if (pairs.size() <= 1) + return; + + // 2. same-D / same-N merge rules. + merge_by(pairs, true); + merge_by(pairs, false); + if (pairs.size() <= 1) + return; + + // 3. subsumption: drop when L(D_i) subseteq L(D_j) and + // L(N_i) subseteq L(N_j) for some kept j. seq_subset is conservative + // (returns true only for definite containment), so we never drop a + // needed split. + //if (pairs.size() > 64) + // return; + + struct row { expr* d; expr* n; unsigned idx; }; + vector rows; + for (unsigned i = 0; i < pairs.size(); ++i) + rows.push_back({ pairs[i].m_d.get(), pairs[i].m_n.get(), i }); + + auto subsumes = [&](row const& a, row const& b) { + return m_subset.is_subset(b.d, a.d) && m_subset.is_subset(b.n, a.n); + }; + + vector kept; + for (row const& row_r : rows) { + bool redundant = false; + for (row const& k : kept) + if (subsumes(k, row_r)) { redundant = true; break; } + if (redundant) + continue; + // drop already-kept rows strictly subsumed by row_r + unsigned kw = 0; + for (unsigned t = 0; t < kept.size(); ++t) { + if (subsumes(row_r, kept[t])) + continue; + kept[kw++] = kept[t]; + } + kept.shrink(kw); + kept.push_back(row_r); + } + + split_set result; + for (row const& k : kept) + result.push_back(pairs[k.idx]); + pairs.swap(result); +} + +std::pair seq_split::split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { + ast_manager& m = this->m(); + expr_ref_vector tokens(m); + + vector stack; + stack.push_back(str); + + while (!stack.empty()) { + expr* cur = stack.back(); + stack.pop_back(); + expr* l, *r; + if (seq().str.is_concat(cur, l, r)) { + stack.push_back(r); + stack.push_back(l); + } + else + tokens.push_back(expr_ref(cur, m)); + } + + SASSERT(!tokens.empty()); + expr* first = tokens.get(0); + SASSERT(seq().is_char(first)); // constants are consumed earlier + + // Choose the factorization boundary so the tail starts with the + // longest run of concrete characters c. + // This gives the split-engine lookahead oracle the most pruning information. + // head = u' (tokens before the run), tail = c · u''' (tokens from the run onward). + const unsigned total = tokens.size(); + unsigned run_start = 0, run_len = 0; + for (unsigned i = 0; i < total; ) { + if (!seq().is_char(tokens.get(i))) { + i++; + continue; + } + unsigned j = i; + while (j < total && seq().is_char(tokens.get(j))) { + j++; + } + if (j - i > run_len) { + run_len = j - i; + run_start = i; + } + i = j; + } + // No constant run => fall back to splitting off the first token. + const unsigned p = run_len == 0 ? 1 : run_start; + SASSERT(p >= 1); + expr* head = first; + for (unsigned i = 1; i < p; i++) { + head = seq().str.mk_concat(head, tokens.get(i)); + } + expr* tail = tokens.get(p); + for (unsigned i = p + run_len; i < tokens.size(); i++) { + tail = seq().str.mk_concat(tail, tokens.get(i)); + } + SASSERT(head && tail); + + // Build the constant lookahead c and (if non-empty) an oracle that + // prunes splits whose postfix cannot match c. + zstring c; + for (unsigned i = 0; i < run_len; ++i) { + expr* ch; unsigned cv; + VERIFY(seq().str.is_unit(tokens.get(run_start + i), ch)); + VERIFY(seq().is_const_char(ch, cv)); + c = c + zstring(cv); + } + split_oracle oracle; + if (!c.empty()) + oracle = [this, &c](expr*, expr* n) { return split_lookahead_viable(n, c); }; + + // Decompose the regex into a split-set via the shared seq_split engine + if (!m_rw.split(regex, result, threshold, split_mode::strong, oracle)) { + result.clear(); + return { nullptr, nullptr }; + } + + m_rw.simplify_split(result); + + // Eagerly consume the constant run c from the tail by taking the c-derivative + // of each postfix + if (!c.empty()) { + unsigned w = 0; + for (unsigned i = 0; i < result.size(); ++i) { + expr* d = result[i].m_n; + for (unsigned k = 0; d && !seq().re.is_empty(d) && k < c.length(); ++k) { + d = m_rw.mk_derivative(seq().mk_char(c[k]), d); + } + SASSERT(d); + if (re().is_empty(d)) + continue; // postfix can't start with c => infeasible split, drop + result[w++] = split_pair(result[i].m_d, d, m); + } + result.shrink(w); + } + + return { head, tail }; +} + +bool seq_split::split_lookahead_viable(expr* regex, zstring const& c) const { + SASSERT(regex); + for (unsigned i = 0; i < c.length(); i++) { + if (m().is_true(m_rw.is_nullable(regex))) + return true; // N accepts the prefix c[0..i) => a suffix completes it + regex = m_rw.mk_derivative(seq().mk_char(c[i]), regex); + SASSERT(regex); + if (re().is_empty(regex)) + return false; // N went (syntactically) dead before reaching c + } + return !re().is_empty(regex); +} \ No newline at end of file diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h new file mode 100644 index 0000000000..5ba4cabdef --- /dev/null +++ b/src/ast/rewriter/seq_split.h @@ -0,0 +1,118 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_split.h + +Abstract: + + Regex split decomposition: the split function sigma from the paper + "Solving by Splitting". For a regular expression r, sigma(r) is a finite + "split-set" of pairs { } such that + + u.v in L(r) iff exists i: u in L(D_i) and v in L(N_i). + + The split algebra (intersection, De Morgan complement, left/right + concatenation with a regex) and the cardinality-reducing simplification + heuristics (drop bottom, same-D/same-N merge, subsumption via seq_subset) + follow the paper. + +Author: + + Clemens Eisenhofer 2026-6-10 + +--*/ +#pragma once + +#include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_subset.h" +#include + +class seq_rewriter; + +// An individual split : the left (prefix) regex D and right (suffix) +// regex N. u.v in L(r) for this split iff u in L(D) and v in L(N). +struct split_pair { + expr_ref m_d; + expr_ref m_n; + split_pair(expr* d, expr* n, ast_manager& m) : m_d(d, m), m_n(n, m) { + SASSERT(d && n); + } +}; + +// A split-set is a union of individual splits. +typedef vector split_set; + +// Controls how aggressively sigma expands the Boolean-closure cases: +// strong - fully expand complement / intersection via the split algebra +// (De Morgan / cross product). This is the behaviour the nseq +// solver relies on. +// weak - do not perform the (potentially 2^k) Boolean-closure expansion; +// give up (return false) on complement / intersection instead. +enum class split_mode { weak, strong }; + +// Optional lookahead oracle. Called for each candidate split as it is +// generated; returns true to keep it, false to prune it. An empty oracle (the +// default) keeps everything, so sigma is unchanged. See seq_split::compute. +typedef std::function split_oracle; + +class seq_split { + seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access + seq_subset m_subset; // language-subset checks for subsumption + + ast_manager& m() const; + seq_util& seq() const; + seq_util::rex& re() const; + + // Push onto `out`, unless `oracle` rejects it. + void push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const; + + // S1 cap S2 = { } dropping any pair with a bottom + // component (and any rejected by `oracle`). Returns false on threshold overrun. + bool intersect(split_set const& s1, split_set const& s2, split_set& result, + unsigned threshold, split_oracle const& oracle) const; + + // De Morgan complement of a split-set: ~S = cap_{s in S} ~s with + // ~ = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }. + bool complement(sort* seq_sort, split_set const& sp, split_set& result, + unsigned threshold, split_oracle const& oracle) const; + + // same-D / same-N merge: groups pairs that share a (syntactically identical) + // left (resp. right) component and unions the other component. + void merge_by(split_set& pairs, bool by_left) const; + +public: + explicit seq_split(seq_rewriter& rw); + + // Compute sigma(r), appending to `out` (does not clear it). `threshold` + // bounds the number of produced splits; an overrun, an unsupported regex + // shape (bounded loop / ite), or a Boolean-closure case in weak mode makes + // it return false ("give up"). + // + // `oracle` (optional) prunes non-viable splits *during* generation. It must + // be sound to apply at every generation step: a candidate N can still gain a + // prefix from a factor appended to its right later (concat/star), so the + // oracle must use a "prefix-compatible" test (prune only when N can never + // match the lookahead, even partially), NOT a strict "starts-with" test. + // The complement body is computed WITHOUT the oracle (inverted orientation); + // the oracle is re-applied to the complement's output fold. + bool compute(expr* r, split_set& out, unsigned threshold, + split_mode mode = split_mode::strong, split_oracle const& oracle = {}); + + // In-place simplification of a split-set: drop bottom components, apply the + // same-D / same-N merge rules, and drop splits subsumed by another (using + // seq_subset). Size-capped to keep the O(n^2) subsumption affordable. + void simplify(split_set& s) const; + + // decompose a membership constraint into a set of pairs of regex splits + std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const; + + // Lookahead oracle for the split engine: is the split's right component + // `n_regex` prefix-compatible with the constant character sequence `c`? + // This is sound to apply during split generation — it never drops a viable split. + // Thus, it might not eliminate all cases in order to stay sound + bool split_lookahead_viable(expr* regex, zstring const& c) const; + + +}; From 1feb610daac85119358fbd7bfe8d19dbba30514b Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 12 Jun 2026 17:05:38 +0200 Subject: [PATCH 2/6] Probably quite instable, but included the splitting into the legacy solver --- src/ast/rewriter/seq_rewriter.h | 5 ++ src/ast/rewriter/seq_split.cpp | 104 ++++++++++++++++++++++--------- src/params/smt_params_helper.pyg | 2 + src/params/theory_seq_params.cpp | 2 + src/params/theory_seq_params.h | 2 + src/smt/seq_regex.cpp | 25 ++++++++ 6 files changed, 110 insertions(+), 30 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 1ae892a100..0d21f94ba5 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -408,6 +408,11 @@ public: void simplify_split(split_set& s) { m_split.simplify(s); } + // decompose a membership constraint into a set of pairs of regex splits + std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { + return m_split.split_membership(str, regex, threshold, result); + } + /** * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences */ diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index f2026b67e9..8095cff951 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -122,24 +122,38 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo expr* s = nullptr; if (rex.is_to_re(r, s)) { zstring str; - if (sq.str.is_string(s, str)) { - for (unsigned i = 0; i <= str.length(); ++i) { - const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), mm); - const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), mm); - push(result, oracle, p, q); + vector stack; + stack.push_back(s); + + while (!stack.empty()) { + expr* cur = stack.back(); + stack.pop_back(); + if (seq().str.is_concat(cur, a, b)) { + stack.push_back(b); + stack.push_back(a); + } + else { + expr* ch; + unsigned cv; + if (seq().str.is_unit(cur, ch) && seq().is_const_char(ch, cv)) { + str += zstring(cv); + continue; + } + zstring str2; + if (sq.str.is_string(s, str2)) { + str = str2; + continue; + } + // not a constant string; unsupported for now + return false; } - return true; } - // a single symbolic unit behaves like one token: { , } - if (sq.str.is_unit(s)) { - const expr_ref ex(r, mm); - const expr_ref eps(rex.mk_epsilon(seq_sort), mm); - push(result, oracle, eps, ex); - push(result, oracle, ex, eps); - return true; + for (unsigned i = 0; i <= str.length(); ++i) { + const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), mm); + const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), mm); + push(result, oracle, p, q); } - // to_re over a non-literal sequence: not handled. - return false; + return true; } // single-character class alpha (., [lo-hi], of_pred): @@ -391,8 +405,8 @@ void seq_split::simplify(split_set& pairs) const { std::pair seq_split::split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { ast_manager& m = this->m(); - expr_ref_vector tokens(m); + expr_ref_vector tokens(m); vector stack; stack.push_back(str); @@ -408,9 +422,36 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi tokens.push_back(expr_ref(cur, m)); } - SASSERT(!tokens.empty()); - expr* first = tokens.get(0); - SASSERT(seq().is_char(first)); // constants are consumed earlier + expr* ch; + unsigned i = 0; + + while (i < tokens.size() && (seq().str.is_string(tokens.get(i)) || (seq().str.is_unit(tokens.get(i), ch) && seq().is_const_char(ch)))) { + zstring s; + if (seq().str.is_string(tokens.get(i), s)) { + if (s.empty()) { + i++; + continue; + } + ch = seq().mk_char(s[0]); + tokens[i] = seq().str.mk_string(s.extract(1, s.length() - 1)); + } + else + i++; + regex = m_rw.mk_derivative(ch, regex); + } + + if (i > 0) { + unsigned j = 0; + for (; i < tokens.size(); i++, j++) { + tokens[j] = tokens.get(i); + } + tokens.shrink(j); + } + + // TODO: Do this for the back as well (also, why did no rule before do that?) + + if (tokens.empty()) + return { nullptr, nullptr }; // Choose the factorization boundary so the tail starts with the // longest run of concrete characters c. @@ -418,13 +459,13 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi // head = u' (tokens before the run), tail = c · u''' (tokens from the run onward). const unsigned total = tokens.size(); unsigned run_start = 0, run_len = 0; - for (unsigned i = 0; i < total; ) { - if (!seq().is_char(tokens.get(i))) { + for (i = 1; i < total; ) { + if (!(seq().str.is_unit(tokens.get(i), ch) && seq().is_const_char(ch))) { i++; continue; } unsigned j = i; - while (j < total && seq().is_char(tokens.get(j))) { + while (j < total && seq().str.is_unit(tokens.get(j), ch) && seq().is_const_char(ch)) { j++; } if (j - i > run_len) { @@ -436,21 +477,24 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi // No constant run => fall back to splitting off the first token. const unsigned p = run_len == 0 ? 1 : run_start; SASSERT(p >= 1); - expr* head = first; - for (unsigned i = 1; i < p; i++) { + expr* head = tokens.get(0); + for (i = 1; i < p; i++) { head = seq().str.mk_concat(head, tokens.get(i)); } - expr* tail = tokens.get(p); - for (unsigned i = p + run_len; i < tokens.size(); i++) { - tail = seq().str.mk_concat(tail, tokens.get(i)); + expr* tail = seq().str.mk_empty(head->get_sort()); + if (tokens.size() > p + run_len) { + tail = tokens.get(p + run_len); + for (i = p + run_len + 1; i < tokens.size(); i++) { + tail = seq().str.mk_concat(tail, tokens.get(i)); + } } SASSERT(head && tail); // Build the constant lookahead c and (if non-empty) an oracle that // prunes splits whose postfix cannot match c. zstring c; - for (unsigned i = 0; i < run_len; ++i) { - expr* ch; unsigned cv; + for (i = 0; i < run_len; ++i) { + unsigned cv; VERIFY(seq().str.is_unit(tokens.get(run_start + i), ch)); VERIFY(seq().is_const_char(ch, cv)); c = c + zstring(cv); @@ -471,7 +515,7 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi // of each postfix if (!c.empty()) { unsigned w = 0; - for (unsigned i = 0; i < result.size(); ++i) { + for (i = 0; i < result.size(); ++i) { expr* d = result[i].m_n; for (unsigned k = 0; d && !seq().re.is_empty(d) && k < c.length(); ++k) { d = m_rw.mk_derivative(seq().mk_char(c[k]), d); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index cd52b989cc..d3f164f3bb 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -138,6 +138,8 @@ def_module_params(module_name='smt', ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'), ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'), + ('seq.regex_factorization_threshold', UINT, 10, 'maximum number of cases to factor a regex into in a single step'), + ('seq.regex_factorization_enabled', BOOL, False, 'apply regex factorization (sigma splitting)'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'), ('sls.parallel', BOOL, True, 'use sls co-processor in parallel or sequential with SMT engine'), diff --git a/src/params/theory_seq_params.cpp b/src/params/theory_seq_params.cpp index 54bf691620..960f145a66 100644 --- a/src/params/theory_seq_params.cpp +++ b/src/params/theory_seq_params.cpp @@ -23,4 +23,6 @@ void theory_seq_params::updt_params(params_ref const & _p) { m_seq_validate = p.seq_validate(); m_seq_max_unfolding = p.seq_max_unfolding(); m_seq_min_unfolding = p.seq_min_unfolding(); + m_seq_regex_factorization_enabled = p.seq_regex_factorization_enabled(); + m_seq_regex_factorization_threshold = p.seq_regex_factorization_threshold(); } diff --git a/src/params/theory_seq_params.h b/src/params/theory_seq_params.h index f964088eb8..067a65a663 100644 --- a/src/params/theory_seq_params.h +++ b/src/params/theory_seq_params.h @@ -26,6 +26,8 @@ struct theory_seq_params { bool m_seq_validate = false; unsigned m_seq_max_unfolding = UINT_MAX/4; unsigned m_seq_min_unfolding = 1; + bool m_seq_regex_factorization_enabled = false; + unsigned m_seq_regex_factorization_threshold = 1; theory_seq_params(params_ref const & p = params_ref()) { updt_params(p); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 0e9a03b633..af8b280d80 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -128,6 +128,31 @@ namespace smt { return; } + if (th.get_fparams().m_seq_regex_factorization_enabled) { + unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; + if (threshold == 0) + threshold = UINT_MAX; + split_set result; + auto [head, tail] = seq_rw().split_membership(s, r, threshold, result); + if (head) { + SASSERT(tail); + // propagate all cases + expr_ref_vector cases(m); + expr_ref_vector branches(m); + for (auto [pre, post] : result) { + expr_ref mem_head(re().mk_in_re(head, pre), m); + expr_ref mem_tail(re().mk_in_re(tail, post), m); + cases.push_back(m.mk_and(mem_head, mem_tail)); + } + const expr_ref cases_expr(m.mk_or(cases), m); + ctx.internalize(cases_expr, false); + std::cout << mk_pp(s, m) << " in " << mk_pp(r, m) << " =>\n" << mk_pp(cases_expr, m) << std::endl; + th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); + return; + } + // fallthrough; decomposition failed + } + // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection // for example: From bbe473cb8ed236c54bd1701b75e1cfc752ba3003 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 26 Jun 2026 16:12:52 +0200 Subject: [PATCH 3/6] Bug fixes --- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/rewriter/seq_split.cpp | 50 +++++++++++++++------------------ src/ast/rewriter/seq_split.h | 4 +-- 3 files changed, 25 insertions(+), 31 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 0d21f94ba5..7d995da985 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -409,7 +409,7 @@ public: void simplify_split(split_set& s) { m_split.simplify(s); } // decompose a membership constraint into a set of pairs of regex splits - std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { + std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { return m_split.split_membership(str, regex, threshold, result); } diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 8095cff951..5d86af2310 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -11,7 +11,6 @@ Abstract: Author: - Nikolaj Bjorner (nbjorner) 2026-6-10 Clemens Eisenhofer 2026-6-10 --*/ @@ -23,16 +22,15 @@ Author: #include "util/stack.h" seq_split::seq_split(seq_rewriter& rw) : - m_rw(rw), m_subset(rw.u().re) {} + m(rw.m()), m_rw(rw), m_subset(rw.u().re) {} -ast_manager& seq_split::m() const { return m_rw.m(); } seq_util& seq_split::seq() const { return m_rw.u(); } seq_util::rex& seq_split::re() const { return m_rw.u().re; } // Add unless the (optional) lookahead oracle prunes it. void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const { if (!oracle || oracle(d, n)) - out.push_back(split_pair(d, n, m())); + out.push_back(split_pair(d, n, m)); } // Cross-product intersection of two split-sets (split algebra): @@ -46,8 +44,8 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) || r.is_empty(p1.m_n) || r.is_empty(p2.m_n)) continue; - const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m()); - const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m()); + const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m); + const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m); push(result, oracle, di, ni); if (result.size() > threshold) return false; @@ -66,7 +64,7 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul seq_util::rex& r = re(); sort* re_sort = r.mk_re(seq_sort); - const expr_ref full(r.mk_full_seq(re_sort), m()); // .* + const expr_ref full(r.mk_full_seq(re_sort), m); // .* if (sp.empty()) { // ~{} = <.*, .*> push(result, oracle, full, full); return true; @@ -99,7 +97,6 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo SASSERT(r); seq_util& sq = seq(); seq_util::rex& rex = re(); - ast_manager& mm = m(); sort* seq_sort = nullptr; if (!sq.is_re(r, seq_sort)) @@ -111,7 +108,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // epsilon: sigma(eps) = { } if (rex.is_epsilon(r)) { - const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + const expr_ref eps(rex.mk_epsilon(seq_sort), m); push(result, oracle, eps, eps); return true; } @@ -149,8 +146,8 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo } } for (unsigned i = 0; i <= str.length(); ++i) { - const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), mm); - const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), mm); + const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), m); + const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), m); push(result, oracle, p, q); } return true; @@ -159,8 +156,8 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // single-character class alpha (., [lo-hi], of_pred): // sigma(alpha) = { , } if (rex.is_full_char(r) || rex.is_range(r) || rex.is_of_pred(r)) { - const expr_ref ex(r, mm); - const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + const expr_ref ex(r, m); + const expr_ref eps(rex.mk_epsilon(seq_sort), m); push(result, oracle, eps, ex); push(result, oracle, ex, eps); return true; @@ -168,7 +165,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // .* : sigma(.*) = { <.*, .*> } if (rex.is_full_seq(r)) { - const expr_ref ex(r, mm); + const expr_ref ex(r, m); push(result, oracle, ex, ex); return true; } @@ -196,13 +193,13 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo if (!compute(ap->get_arg(i), sigma_arg, threshold, mode, oracle)) return false; - expr_ref left(mm), right(mm); + expr_ref left(m), right(m); if (i == 0) left = rex.mk_epsilon(seq_sort); else { for (unsigned j = 0; j < i; ++j) { expr* arg = ap->get_arg(j); - left = left ? expr_ref(rex.mk_concat(left, arg), mm) : expr_ref(arg, mm); + left = left ? expr_ref(rex.mk_concat(left, arg), m) : expr_ref(arg, m); } } if (i == n - 1) @@ -226,7 +223,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // star: sigma(a*) = { } cup a*.sigma(a).a* if (rex.is_star(r, a)) { - const expr_ref eps(rex.mk_epsilon(seq_sort), mm); + const expr_ref eps(rex.mk_epsilon(seq_sort), m); push(result, oracle, eps, eps); split_set sa; if (!compute(a, sa, threshold, mode, oracle)) @@ -241,7 +238,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) if (rex.is_plus(r, a)) { - const expr_ref star(rex.mk_star(a), mm); // a* + const expr_ref star(rex.mk_star(a), m); // a* split_set sa; if (!compute(a, sa, threshold, mode, oracle)) return false; @@ -308,7 +305,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo } // bounded loop / ite / other: not handled (paper "v1: bail"). - TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, mm) << "\n";); + TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";); return false; } @@ -318,7 +315,6 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo // Only fires on syntactically-identical (perfectly-shared) key components, so // it is a conservative instance of the rule. void seq_split::merge_by(split_set& pairs, const bool by_left) const { - ast_manager& mm = m(); obj_map idx; // key component -> position in `out` split_set out; for (auto const& p : pairs) { @@ -327,7 +323,7 @@ void seq_split::merge_by(split_set& pairs, const bool by_left) const { unsigned pos; if (idx.find(key, pos)) { expr* prev = by_left ? out[pos].m_n.get() : out[pos].m_d.get(); - const expr_ref u(m_rw.mk_regex_union_normalize(prev, other), mm); + const expr_ref u(m_rw.mk_regex_union_normalize(prev, other), m); if (by_left) out[pos].m_n = u; else @@ -403,9 +399,7 @@ void seq_split::simplify(split_set& pairs) const { pairs.swap(result); } -std::pair seq_split::split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { - ast_manager& m = this->m(); - +std::pair seq_split::split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { expr_ref_vector tokens(m); vector stack; stack.push_back(str); @@ -451,7 +445,7 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi // TODO: Do this for the back as well (also, why did no rule before do that?) if (tokens.empty()) - return { nullptr, nullptr }; + return { expr_ref(m), expr_ref(m) }; // Choose the factorization boundary so the tail starts with the // longest run of concrete characters c. @@ -506,7 +500,7 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi // Decompose the regex into a split-set via the shared seq_split engine if (!m_rw.split(regex, result, threshold, split_mode::strong, oracle)) { result.clear(); - return { nullptr, nullptr }; + return { expr_ref(m), expr_ref(m) }; } m_rw.simplify_split(result); @@ -528,13 +522,13 @@ std::pair seq_split::split_membership(expr* str, expr* regex, unsi result.shrink(w); } - return { head, tail }; + return { expr_ref(head, m), expr_ref(tail, m) }; } bool seq_split::split_lookahead_viable(expr* regex, zstring const& c) const { SASSERT(regex); for (unsigned i = 0; i < c.length(); i++) { - if (m().is_true(m_rw.is_nullable(regex))) + if (m.is_true(m_rw.is_nullable(regex))) return true; // N accepts the prefix c[0..i) => a suffix completes it regex = m_rw.mk_derivative(seq().mk_char(c[i]), regex); SASSERT(regex); diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 5ba4cabdef..05e40aefbd 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -58,10 +58,10 @@ enum class split_mode { weak, strong }; typedef std::function split_oracle; class seq_split { + ast_manager& m; seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access seq_subset m_subset; // language-subset checks for subsumption - ast_manager& m() const; seq_util& seq() const; seq_util::rex& re() const; @@ -106,7 +106,7 @@ public: void simplify(split_set& s) const; // decompose a membership constraint into a set of pairs of regex splits - std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const; + std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const; // Lookahead oracle for the split engine: is the split's right component // `n_regex` prefix-compatible with the constant character sequence `c`? From 5693aa706a3277677f7cfe83f3d0b4322091ee49 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 26 Jun 2026 17:09:57 +0200 Subject: [PATCH 4/6] Undid rewriter refactoring --- src/ast/rewriter/seq_rewriter.cpp | 113 +++++++++++++++++------------- 1 file changed, 63 insertions(+), 50 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0028562ff1..1654c57771 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3999,54 +3999,58 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { //do not concatenate [], it is a deade-end return result; } - // Classical Brzozowski union: keep the derivative tree free of - // antimirov-union nodes so the bisimulation procedure sees a - // single regex tree whose leaves are XOR pairs. - return mk_der_union(result, mk_der_concat(is_n, dr2)); + else { + // Classical Brzozowski union: keep the derivative tree free of + // antimirov-union nodes so the bisimulation procedure sees a + // single regex tree whose leaves are XOR pairs. + return mk_der_union(result, mk_der_concat(is_n, dr2)); + } } - if (re().is_star(r, r1)) { + else if (re().is_star(r, r1)) { return mk_der_concat(mk_derivative_rec(ele, r1), r); } - if (re().is_plus(r, r1)) { + else if (re().is_plus(r, r1)) { expr_ref star(re().mk_star(r1), m()); return mk_derivative_rec(ele, star); } - if (re().is_union(r, r1, r2)) { + else if (re().is_union(r, r1, r2)) { return mk_der_union(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - if (re().is_intersection(r, r1, r2)) { + else if (re().is_intersection(r, r1, r2)) { return mk_der_inter(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - if (re().is_diff(r, r1, r2)) { + else if (re().is_diff(r, r1, r2)) { return mk_der_inter(mk_derivative_rec(ele, r1), mk_der_compl(mk_derivative_rec(ele, r2))); } - if (re().is_xor(r, r1, r2)) { + else if (re().is_xor(r, r1, r2)) { return mk_der_xor(mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); } - if (m().is_ite(r, p, r1, r2)) { + else if (m().is_ite(r, p, r1, r2)) { // there is no BDD normalization here result = m().mk_ite(p, mk_derivative_rec(ele, r1), mk_derivative_rec(ele, r2)); return result; } - if (re().is_opt(r, r1)) { + else if (re().is_opt(r, r1)) { return mk_derivative_rec(ele, r1); } - if (re().is_complement(r, r1)) { + else if (re().is_complement(r, r1)) { return mk_der_compl(mk_derivative_rec(ele, r1)); } - if (re().is_loop(r, r1, lo)) { + else if (re().is_loop(r, r1, lo)) { if (lo > 0) { lo--; } result = mk_derivative_rec(ele, r1); - // do not concatenate with [] (emptyset) + //do not concatenate with [] (emptyset) if (re().is_empty(result)) { return result; } - // do not create loop r1{0,}, instead create r1* - return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo))); + else { + //do not create loop r1{0,}, instead create r1* + return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo))); + } } - if (re().is_loop(r, r1, lo, hi)) { + else if (re().is_loop(r, r1, lo, hi)) { if (hi == 0) { return mk_empty(); } @@ -4055,16 +4059,19 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { lo--; } result = mk_derivative_rec(ele, r1); - // do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain + //do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain if (re().is_empty(result) || hi == 0) { return result; } - return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); + else { + return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); + } } - if (re().is_full_seq(r) || re().is_empty(r)) { + else if (re().is_full_seq(r) || + re().is_empty(r)) { return expr_ref(r, m()); } - if (re().is_to_re(r, r1)) { + else if (re().is_to_re(r, r1)) { // r1 is a string here (not a regexp) expr_ref hd(m()), tl(m()); if (get_head_tail(r1, hd, tl)) { @@ -4077,16 +4084,16 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_concat(result, r1); return result; } - if (str().is_empty(r1)) { - // observe: str().is_empty(r1) checks that r = () = epsilon - // while mk_empty() = [], because deriv(epsilon) = [] = nothing + else if (str().is_empty(r1)) { + //observe: str().is_empty(r1) checks that r = () = epsilon + //while mk_empty() = [], because deriv(epsilon) = [] = nothing return mk_empty(); } - if (str().is_itos(r1)) { + else if (str().is_itos(r1)) { // - // here r1 = (str.from_int r2) and r2 is non-ground + // here r1 = (str.from_int r2) and r2 is non-ground // or else the expression would have been simplified earlier - // so r1 must be nonempty and must consists of decimal digits + // so r1 must be nonempty and must consists of decimal digits // '0' <= elem <= '9' // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // @@ -4098,17 +4105,19 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { auto a3 = m().mk_eq(hd, ele); auto inner = m().mk_and(a2, a3); m_br.mk_and(a0, a1, inner, result); + tl = re().mk_to_re(mk_seq_rest(r1)); + return re_and(result, tl); + } + else { + // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence + // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) + hd = mk_seq_first(r1); + m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); } - // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence - // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) - hd = mk_seq_first(r1); - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); - tl = re().mk_to_re(mk_seq_rest(r1)); - return re_and(result, tl); } - if (re().is_reverse(r, r1)) { + else if (re().is_reverse(r, r1)) { if (re().is_to_re(r1, r2)) { // First try to extract hd and tl such that r = hd ++ tl and |tl|=1 expr_ref hd(m()), tl(m()); @@ -4120,20 +4129,22 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd))); return result; } - if (str().is_empty(r2)) { + else if (str().is_empty(r2)) { return mk_empty(); } - // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else [])) - // hd = first of reverse(r2) i.e. last of r2 - // tl = rest of reverse(r2) i.e. butlast of r2 - // hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); - hd = mk_seq_last(r2); - // factor nested constructor calls to enforce deterministic argument evaluation order - auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); - auto a_eq = m().mk_eq(hd, ele); - m_br.mk_and(a_non_empty, a_eq, result); - tl = re().mk_to_re(mk_seq_butlast(r2)); - return re_and(result, re().mk_reverse(tl)); + else { + // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else [])) + // hd = first of reverse(r2) i.e. last of r2 + // tl = rest of reverse(r2) i.e. butlast of r2 + //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); + hd = mk_seq_last(r2); + // factor nested constructor calls to enforce deterministic argument evaluation order + auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); + auto a_eq = m().mk_eq(hd, ele); + m_br.mk_and(a_non_empty, a_eq, result); + tl = re().mk_to_re(mk_seq_butlast(r2)); + return re_and(result, re().mk_reverse(tl)); + } } } else if (re().is_range(r, r1, r2)) { @@ -4152,9 +4163,11 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { result = mk_der_inter(p1, p2); return result; } - return mk_empty(); + else { + return mk_empty(); + } } - expr *e1 = nullptr, *e2 = nullptr; + expr* e1 = nullptr, * e2 = nullptr; if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) { SASSERT(u().is_char(e1)); // Use mk_der_cond to normalize @@ -4172,7 +4185,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } else if (re().is_of_pred(r, p)) { array_util array(m()); - expr *args[2] = {p, ele}; + expr* args[2] = { p, ele }; result = array.mk_select(2, args); // Use mk_der_cond to normalize STRACE(seq_verbose, tout << "deriv of_pred" << std::endl;); From a88dfa64ac0c19e25f41a1a044806559128b1455 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 26 Jun 2026 17:37:40 +0200 Subject: [PATCH 5/6] Lazy decomposition Test-cases --- src/ast/rewriter/seq_split.cpp | 467 +++++++++++++++++++++++++-------- src/ast/rewriter/seq_split.h | 104 +++++++- src/smt/seq_regex.cpp | 1 - src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/seq_split.cpp | 401 ++++++++++++++++++++++++++++ 6 files changed, 859 insertions(+), 116 deletions(-) create mode 100644 src/test/seq_split.cpp diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 5d86af2310..a5adcd055f 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -22,7 +22,154 @@ Author: #include "util/stack.h" seq_split::seq_split(seq_rewriter& rw) : - m(rw.m()), m_rw(rw), m_subset(rw.u().re) {} + m(rw.m()), m_rw(rw), m_subset(rw.u().re), + m_set_sort(m), + m_d_empty(m), m_d_single(m), m_d_fromre(m), m_d_union(m), + m_d_inter(m), m_d_compl(m), m_d_lcat(m), m_d_rcat(m), + m_empty_app(m) {} + +// --------------------------------------------------------------------------- +// Suspended split-set representation (split algebra over `expr`). +// --------------------------------------------------------------------------- + +void seq_split::ensure_decls(sort* seq_sort) { + SASSERT(seq_sort); + if (m_seq_sort == seq_sort) + return; + sort* re_sort = re().mk_re(seq_sort); + m_set_sort = m.mk_uninterpreted_sort(symbol("seq.split.set")); + sort* ss = m_set_sort; + m_d_empty = m.mk_func_decl(symbol("seq.split.empty"), 0u, nullptr, ss); + m_d_single = m.mk_func_decl(symbol("seq.split.single"), re_sort, re_sort, ss); + m_d_fromre = m.mk_func_decl(symbol("seq.split.from_re"), re_sort, ss); + m_d_union = m.mk_func_decl(symbol("seq.split.union"), ss, ss, ss); + m_d_inter = m.mk_func_decl(symbol("seq.split.inter"), ss, ss, ss); + m_d_compl = m.mk_func_decl(symbol("seq.split.compl"), ss, ss); + m_d_lcat = m.mk_func_decl(symbol("seq.split.lcat"), re_sort, ss, ss); + m_d_rcat = m.mk_func_decl(symbol("seq.split.rcat"), ss, re_sort, ss); + m_empty_app = m.mk_const(m_d_empty); + m_seq_sort = seq_sort; +} + +// --- smart constructors ---------------------------------------------------- + +expr_ref seq_split::mk_empty() { + SASSERT(m_empty_app); + return m_empty_app; +} + +expr_ref seq_split::mk_single(expr* d, expr* n) { + SASSERT(d && n); + if (re().is_empty(d) || re().is_empty(n)) + return mk_empty(); + return expr_ref(m.mk_app(m_d_single, d, n), m); +} + +expr_ref seq_split::mk_fromre(expr* r) { + SASSERT(r); + sort* seq_sort = nullptr; + VERIFY(seq().is_re(r, seq_sort)); + ensure_decls(seq_sort); + if (re().is_empty(r)) + return mk_empty(); + return expr_ref(m.mk_app(m_d_fromre, r), m); +} + +expr_ref seq_split::mk_union(expr* a, expr* b) { + SASSERT(a && b); + if (is_empty_ss(a)) + return expr_ref(b, m); + if (is_empty_ss(b)) + return expr_ref(a, m); + return expr_ref(m.mk_app(m_d_union, a, b), m); +} + +expr_ref seq_split::mk_inter(expr* a, expr* b) { + SASSERT(a && b); + if (is_empty_ss(a) || is_empty_ss(b)) + return mk_empty(); + return expr_ref(m.mk_app(m_d_inter, a, b), m); +} + +expr_ref seq_split::mk_compl(expr* a) { + SASSERT(a); + return expr_ref(m.mk_app(m_d_compl, a), m); +} + +expr_ref seq_split::mk_lcat(expr* r, expr* s) { + SASSERT(r && s); + if (is_empty_ss(s)) + return mk_empty(); + if (re().is_epsilon(r)) // eps . S = S + return expr_ref(s, m); + return expr_ref(m.mk_app(m_d_lcat, r, s), m); +} + +expr_ref seq_split::mk_rcat(expr* s, expr* r) { + SASSERT(r && s); + if (is_empty_ss(s)) + return mk_empty(); + if (re().is_epsilon(r)) // S . eps = S + return expr_ref(s, m); + return expr_ref(m.mk_app(m_d_rcat, s, r), m); +} + +// --- recognizers ----------------------------------------------------------- + +bool seq_split::is_empty_ss(expr* e) const { + return is_app(e) && to_app(e)->get_decl() == m_d_empty; +} +bool seq_split::is_single(expr* e, expr*& d, expr*& n) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_single) + return false; + d = to_app(e)->get_arg(0); + n = to_app(e)->get_arg(1); + return true; +} +bool seq_split::is_fromre(expr* e, expr*& r) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_fromre) + return false; + r = to_app(e)->get_arg(0); + return true; +} +bool seq_split::is_union(expr* e, expr*& a, expr*& b) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_union) + return false; + a = to_app(e)->get_arg(0); + b = to_app(e)->get_arg(1); + return true; +} +bool seq_split::is_inter(expr* e, expr*& a, expr*& b) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_inter) + return false; + a = to_app(e)->get_arg(0); + b = to_app(e)->get_arg(1); + return true; +} +bool seq_split::is_compl(expr* e, expr*& a) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_compl) + return false; + a = to_app(e)->get_arg(0); + return true; +} +bool seq_split::is_lcat(expr* e, expr*& r, expr*& s) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_lcat) + return false; + r = to_app(e)->get_arg(0); + s = to_app(e)->get_arg(1); + return true; +} +bool seq_split::is_rcat(expr* e, expr*& s, expr*& r) const { + if (!is_app(e) || to_app(e)->get_decl() != m_d_rcat) + return false; + s = to_app(e)->get_arg(0); + r = to_app(e)->get_arg(1); + return true; +} +bool seq_split::is_frontier(expr* e) const { + expr *a = nullptr, *b = nullptr; + return is_empty_ss(e) || is_single(e, a, b) || is_union(e, a, b); +} seq_util& seq_split::seq() const { return m_rw.u(); } seq_util::rex& seq_split::re() const { return m_rw.u().re; } @@ -92,25 +239,30 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul return true; } -bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mode mode, - split_oracle const& oracle) { - SASSERT(r); +// One level of the sigma rules. Mirrors the historic eager `compute`, except it +// emits *suspended* split-algebra terms (from_re / lcat / rcat / inter / compl) for +// the subterms instead of recursing. `mode` is irrelevant here: weak vs. strong is +// decided when `head_normalize` reaches an inter / compl node. +expr_ref seq_split::expand_fromre(expr* r, bool& ok) { + ok = true; seq_util& sq = seq(); seq_util::rex& rex = re(); sort* seq_sort = nullptr; - if (!sq.is_re(r, seq_sort)) - return false; + if (!sq.is_re(r, seq_sort)) { + ok = false; + return expr_ref(m); + } + ensure_decls(seq_sort); - // bottom: sigma(empty) = {} (the empty split-set) + // bottom: sigma(empty) = {} if (rex.is_empty(r)) - return true; + return mk_empty(); // epsilon: sigma(eps) = { } if (rex.is_epsilon(r)) { const expr_ref eps(rex.mk_epsilon(seq_sort), m); - push(result, oracle, eps, eps); - return true; + return mk_single(eps, eps); } expr* a = nullptr, *b = nullptr; @@ -142,15 +294,17 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo continue; } // not a constant string; unsupported for now - return false; + ok = false; + return expr_ref(m); } } + expr_ref acc = mk_empty(); for (unsigned i = 0; i <= str.length(); ++i) { const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), m); const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), m); - push(result, oracle, p, q); + acc = mk_union(acc, mk_single(p, q)); } - return true; + return acc; } // single-character class alpha (., [lo-hi], of_pred): @@ -158,41 +312,32 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo if (rex.is_full_char(r) || rex.is_range(r) || rex.is_of_pred(r)) { const expr_ref ex(r, m); const expr_ref eps(rex.mk_epsilon(seq_sort), m); - push(result, oracle, eps, ex); - push(result, oracle, ex, eps); - return true; + return mk_union(mk_single(eps, ex), mk_single(ex, eps)); } // .* : sigma(.*) = { <.*, .*> } if (rex.is_full_seq(r)) { const expr_ref ex(r, m); - push(result, oracle, ex, ex); - return true; + return mk_single(ex, ex); } - // union: sigma(r0 | ... | r_{n-1}) = U sigma(ri) (re.union may be n-ary) + // union: sigma(r0 | ... | r_{n-1}) = U from_re(ri) (re.union may be n-ary) if (rex.is_union(r)) { app* ap = to_app(r); - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - if (!compute(ap->get_arg(i), result, threshold, mode, oracle)) - return false; + expr_ref acc = mk_empty(); + for (expr* arg : *ap) { + acc = mk_union(acc, mk_fromre(arg)); } - return true; + return acc; } // concat: sigma(r0...r_{n-1}) = U_i (r0...r_{i-1}) . sigma(ri) . (r_{i+1}...r_{n-1}) - // (re.++ may be n-ary) + // emitted as U_i lcat(left, rcat(from_re(ri), right)) (re.++ may be n-ary) if (rex.is_concat(r)) { app* ap = to_app(r); const unsigned n = ap->get_num_args(); + expr_ref acc = mk_empty(); for (unsigned i = 0; i < n; ++i) { - // Sound to pass the oracle into the sub-computation: N_inner.Sigma* - // over-approximates the final N_inner.right, so a prune here is a - // prune of the final pair too (prefix-compatible test). - split_set sigma_arg; - if (!compute(ap->get_arg(i), sigma_arg, threshold, mode, oracle)) - return false; - expr_ref left(m), right(m); if (i == 0) left = rex.mk_epsilon(seq_sort); @@ -211,102 +356,216 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo right = rex.mk_concat(right, arg); } } - - for (auto const& [d, nn] : sigma_arg) { - const expr_ref p = m_rw.mk_re_append(left, d); - const expr_ref q = m_rw.mk_re_append(nn, right); - push(result, oracle, p, q); - } + expr_ref term = mk_lcat(left, mk_rcat(mk_fromre(ap->get_arg(i)), right)); + acc = mk_union(acc, term); } - return true; + return acc; } // star: sigma(a*) = { } cup a*.sigma(a).a* if (rex.is_star(r, a)) { const expr_ref eps(rex.mk_epsilon(seq_sort), m); - push(result, oracle, eps, eps); - split_set sa; - if (!compute(a, sa, threshold, mode, oracle)) - return false; - for (auto const& [d, n] : sa) { - const expr_ref p = m_rw.mk_re_append(r, d); // a*.D - const expr_ref q = m_rw.mk_re_append(n, r); // N.a* - push(result, oracle, p, q); - } - return true; + expr_ref body = mk_lcat(r, mk_rcat(mk_fromre(a), r)); // a*.from_re(a).a* + return mk_union(mk_single(eps, eps), body); } // plus: a+ = a.a* ; sigma(a+) = a*.sigma(a).a* (star rule without ) if (rex.is_plus(r, a)) { const expr_ref star(rex.mk_star(a), m); // a* - split_set sa; - if (!compute(a, sa, threshold, mode, oracle)) - return false; - for (auto const& [d, n] : sa) { - const expr_ref p = m_rw.mk_re_append(star, d); - const expr_ref q = m_rw.mk_re_append(n, star); - push(result, oracle, p, q); - } - return true; + return mk_lcat(star, mk_rcat(mk_fromre(a), star)); } - // intersection: sigma(r0 & ... & r_{n-1}) = cap sigma(ri) (re.inter may be n-ary) + // intersection: sigma(r0 & ... & r_{n-1}) = cap from_re(ri) (re.inter may be n-ary) if (rex.is_intersection(r)) { - if (mode == split_mode::weak) - return false; app* ap = to_app(r); const unsigned n = ap->get_num_args(); - split_set current; - if (!compute(ap->get_arg(0), current, threshold, mode, oracle)) - return false; - // A give-up on any conjunct must propagate as a give-up: silently treating - // it as the empty split-set would collapse the whole intersection to bottom - // and be misreported as an (unsound) conflict. - for (unsigned i = 1; i < n && !current.empty(); ++i) { - split_set arg_i, tmp; - if (!compute(ap->get_arg(i), arg_i, threshold, mode, oracle)) - return false; - if (!intersect(current, arg_i, tmp, threshold, oracle)) - return false; - current = std::move(tmp); - } - result.append(current); - return true; + expr_ref acc = mk_fromre(ap->get_arg(0)); + for (unsigned i = 1; i < n; ++i) + acc = mk_inter(acc, mk_fromre(ap->get_arg(i))); + return acc; } // complement: sigma(~a) = ~sigma(a). - // The body is computed WITHOUT the oracle (the body's pairs are inverted, so - // their N is unrelated to the output N); the oracle is re-applied in complement(). - if (rex.is_complement(r, a)) { - if (mode == split_mode::weak) - return false; - split_set sa; - if (!compute(a, sa, threshold, mode)) - return false; - return complement(seq_sort, sa, result, threshold, oracle); - } + if (rex.is_complement(r, a)) + return mk_compl(mk_fromre(a)); // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b). - // sigma(b) (used only inside the complement) is computed WITHOUT the oracle. - if (rex.is_diff(r, a, b)) { - if (mode == split_mode::weak) - return false; - split_set sa, sb, sb_compl, tmp; - if (!compute(a, sa, threshold, mode, oracle)) - return false; - if (!compute(b, sb, threshold, mode)) - return false; - if (!complement(seq_sort, sb, sb_compl, threshold, oracle)) - return false; - if (!intersect(sa, sb_compl, tmp, threshold, oracle)) - return false; - result.append(tmp); - return true; - } + if (rex.is_diff(r, a, b)) + return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b))); // bounded loop / ite / other: not handled (paper "v1: bail"). TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";); - return false; + ok = false; + return expr_ref(m); +} + +// r . hs : push the left regex onto the D component of a head-normal split-set. +expr_ref seq_split::distribute_lcat(expr* r, expr* hs) { + expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; + if (is_empty_ss(hs)) + return mk_empty(); + if (is_single(hs, d, n)) + return mk_single(m_rw.mk_re_append(r, d), n); // r.D + if (is_union(hs, a, b)) + return mk_union(mk_lcat(r, a), mk_lcat(r, b)); + UNREACHABLE(); + return expr_ref(hs, m); +} + +// hs . r : push the right regex onto the N component of a head-normal split-set. +expr_ref seq_split::distribute_rcat(expr* hs, expr* r) { + expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; + if (is_empty_ss(hs)) + return mk_empty(); + if (is_single(hs, d, n)) + return mk_single(d, m_rw.mk_re_append(n, r)); // N.r + if (is_union(hs, a, b)) + return mk_union(mk_rcat(a, r), mk_rcat(b, r)); + UNREACHABLE(); + return expr_ref(hs, m); +} + +expr_ref seq_split::from_split_set(split_set const& s) { + expr_ref acc = mk_empty(); + for (auto const& p : s) + acc = mk_union(acc, mk_single(p.m_d, p.m_n)); + return acc; +} + +expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, + split_oracle const& oracle, bool& ok) { + ok = true; + expr *a = nullptr, *b = nullptr, *r = nullptr, *s = nullptr; + + // already a frontier node + if (is_frontier(t)) + return expr_ref(t, m); + + // from_re(r): one level of sigma; recurse to settle a non-frontier head + // (plus / inter / compl / diff expand to lcat / inter / compl nodes). + if (is_fromre(t, r)) { + expr_ref e = expand_fromre(r, ok); + if (!ok) + return expr_ref(m); + if (is_frontier(e)) + return e; + return head_normalize(e, mode, threshold, oracle, ok); + } + + // r.S : head-normalize S, then distribute r over the frontier. + if (is_lcat(t, r, s)) { + expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); + if (!ok) + return expr_ref(m); + return distribute_lcat(r, hs); + } + if (is_rcat(t, s, r)) { + expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); + if (!ok) + return expr_ref(m); + return distribute_rcat(hs, r); + } + + // inter / compl are eager by nature: a single split of S1 cap S2 (or ~S) + // cannot be produced without materializing the operand split-sets. + if (is_inter(t, a, b)) { + if (mode == split_mode::weak) { + ok = false; + return expr_ref(m); + } + split_set sa, sb, tmp; + if (!materialize(a, mode, threshold, oracle, sa) || + !materialize(b, mode, threshold, oracle, sb) || + !intersect(sa, sb, tmp, threshold, oracle)) { + ok = false; + return expr_ref(m); + } + return from_split_set(tmp); + } + if (is_compl(t, a)) { + if (mode == split_mode::weak) { + ok = false; + return expr_ref(m); + } + // The body is materialized WITHOUT the oracle (its pairs are inverted, so + // their N is unrelated to the output N); the oracle is re-applied in + // complement(). + split_set sa, res; + if (!materialize(a, mode, threshold, split_oracle{}, sa) || + !complement(m_seq_sort, sa, res, threshold, oracle)) { + ok = false; + return expr_ref(m); + } + return from_split_set(res); + } + + UNREACHABLE(); + ok = false; + return expr_ref(m); +} + +bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle, split_set& out) { + return enumerate(node, mode, threshold, oracle, + [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); +} + +expr_ref seq_split::make(expr* r) { + SASSERT(r); + sort* seq_sort = nullptr; + if (!seq().is_re(r, seq_sort)) + return expr_ref(m); + return mk_fromre(r); +} + +bool seq_split::enumerate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle, split_yield const& yield) { + SASSERT(node); + expr_ref_vector work(m); // GC-safe worklist of suspended split-sets + work.push_back(node); + unsigned count = 0; + while (!work.empty()) { + expr_ref t(work.back(), m); + work.pop_back(); + + bool ok = true; + expr_ref hn = head_normalize(t, mode, threshold, oracle, ok); + if (!ok) + return false; // give up (unsupported / weak Boolean / overrun) + + expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; + if (is_empty_ss(hn)) + continue; + if (is_single(hn, d, n)) { + if (oracle && !oracle(d, n)) + continue; // pruned by lookahead + if (++count > threshold) + return false; // safety cap against space bloat + if (!yield(d, n)) + return true; // caller asked to stop early (success) + continue; + } + if (is_union(hn, a, b)) { + work.push_back(a); + work.push_back(b); + continue; + } + UNREACHABLE(); + } + return true; +} + +// Eager wrapper: drain the lazy enumeration into `out`. Semantics (give-up cases, +// oracle discipline) match the historic engine. +bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mode mode, + split_oracle const& oracle) { + SASSERT(r); + sort* seq_sort = nullptr; + if (!seq().is_re(r, seq_sort)) + return false; + expr_ref node = mk_fromre(r); + return enumerate(node, mode, threshold, oracle, + [&](expr* d, expr* n) { result.push_back(split_pair(d, n, m)); return true; }); } // same-D / same-N merge (paper eqs. 1 & 2): @@ -503,7 +762,7 @@ std::pair seq_split::split_membership(expr* str, expr* regex return { expr_ref(m), expr_ref(m) }; } - m_rw.simplify_split(result); + simplify(result); // Eagerly consume the constant run c from the tail by taking the c-derivative // of each postfix diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 05e40aefbd..185627ce1c 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -57,14 +57,84 @@ enum class split_mode { weak, strong }; // default) keeps everything, so sigma is unchanged. See seq_split::compute. typedef std::function split_oracle; +// Callback invoked by seq_split::enumerate for each concrete split as it +// emerges from the lazy expansion. Returning false stops the enumeration early +// (a successful early stop); returning true asks for the next split. +typedef std::function split_yield; + class seq_split { ast_manager& m; seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access seq_subset m_subset; // language-subset checks for subsumption + // --- Suspended split-set representation ------------------------------- + // A split-set computation is kept as an `expr` term over a small family of + // locally-declared, uninterpreted function symbols (the split algebra of the + // paper / split-algebra.md). Nothing here is ever asserted to the solver; + // the terms are only used as scratch structure to drive lazy expansion. + // + // empty : SplitSet -- {} (bottom) + // single : Re x Re -> SplitSet -- a single split + // from_re : Re -> SplitSet -- the *suspended* sigma(r) + // union : SplitSet x SplitSet -> SplitSet + // inter : SplitSet x SplitSet -> SplitSet + // compl : SplitSet -> SplitSet + // lcat : Re x SplitSet -> SplitSet -- r . S (left-concat onto D) + // rcat : SplitSet x Re -> SplitSet -- S . r (right-concat onto N) + sort* m_seq_sort = nullptr; // sequence sort the decls are built for + sort_ref m_set_sort; // the uninterpreted SplitSet sort + func_decl_ref m_d_empty, m_d_single, m_d_fromre, m_d_union, + m_d_inter, m_d_compl, m_d_lcat, m_d_rcat; + expr_ref m_empty_app; // cached nullary `empty` term + seq_util& seq() const; seq_util::rex& re() const; + // (Re)build the local declarations for `seq_sort` if not already current. + void ensure_decls(sort* seq_sort); + + // Smart constructors: apply the cheap normalizations the eager engine relies + // on (drop-bottom, eps cancellation, union absorption of empty). + expr_ref mk_empty(); + expr_ref mk_single(expr* d, expr* n); + expr_ref mk_fromre(expr* r); + expr_ref mk_union(expr* a, expr* b); + expr_ref mk_inter(expr* a, expr* b); + expr_ref mk_compl(expr* a); + expr_ref mk_lcat(expr* r, expr* s); + expr_ref mk_rcat(expr* s, expr* r); + + // Recognizers over the local decls. + bool is_empty_ss(expr* e) const; + bool is_single(expr* e, expr*& d, expr*& n) const; + bool is_fromre(expr* e, expr*& r) const; + bool is_union (expr* e, expr*& a, expr*& b) const; + bool is_inter (expr* e, expr*& a, expr*& b) const; + bool is_compl (expr* e, expr*& a) const; + bool is_lcat (expr* e, expr*& r, expr*& s) const; + bool is_rcat (expr* e, expr*& s, expr*& r) const; + // A term whose head is empty | single | union (ready for the worklist loop). + bool is_frontier(expr* e) const; + + // One level of the sigma rules: from_re(r) -> a SplitSet term built from the + // immediate subterms. `ok` is set false on an unsupported shape. + expr_ref expand_fromre(expr* r, bool& ok); + // Distribute a left/right concatenation over a head-normal split-set. + expr_ref distribute_lcat(expr* r, expr* hs); + expr_ref distribute_rcat(expr* hs, expr* r); + // Materialized split-set -> a `union` of `single`s. + expr_ref from_split_set(split_set const& s); + // Reduce `t` until its head is empty | single | union (one outermost level + // for the lazy nodes; inter/compl are expanded eagerly via `materialize`, + // since the paper's De Morgan / cross-product cannot yield a split lazily). + // `ok` is set false on a give-up (unsupported shape, weak-mode Boolean, or + // threshold overrun). + expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold, + split_oracle const& oracle, bool& ok); + // Fully drain a suspended split-set into `out` (used for inter/compl bodies). + bool materialize(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle, split_set& out); + // Push onto `out`, unless `oracle` rejects it. void push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const; @@ -85,18 +155,30 @@ class seq_split { public: explicit seq_split(seq_rewriter& rw); - // Compute sigma(r), appending to `out` (does not clear it). `threshold` - // bounds the number of produced splits; an overrun, an unsupported regex - // shape (bounded loop / ite), or a Boolean-closure case in weak mode makes - // it return false ("give up"). + // Build the *suspended* sigma(r) as a split-algebra term (no expansion). + // Returns null on a non-regex argument. Drive it with `enumerate`. + expr_ref make(expr* r); + + // Lazily expand a suspended split-set, invoking `yield` for every concrete + // split . The threshold is supplied by the caller and serves only as a + // safety cap against space bloat (lazy expansion still has to materialize the + // operands of intersection / complement). An overrun, an unsupported regex + // shape, or a Boolean-closure case in weak mode makes it return false ("give + // up"). `yield` returning false stops early and is reported as success. // - // `oracle` (optional) prunes non-viable splits *during* generation. It must - // be sound to apply at every generation step: a candidate N can still gain a - // prefix from a factor appended to its right later (concat/star), so the - // oracle must use a "prefix-compatible" test (prune only when N can never - // match the lookahead, even partially), NOT a strict "starts-with" test. - // The complement body is computed WITHOUT the oracle (inverted orientation); - // the oracle is re-applied to the complement's output fold. + // `oracle` (optional) prunes non-viable splits as they are yielded. It must + // be sound to apply per split: a candidate N can still gain a prefix from a + // factor appended to its right later (concat/star), so the oracle must use a + // "prefix-compatible" test (prune only when N can never match the lookahead, + // even partially), NOT a strict "starts-with" test. The complement body is + // expanded WITHOUT the oracle (inverted orientation); the oracle is re-applied + // to the complement's output fold. + bool enumerate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle, split_yield const& yield); + + // Compute sigma(r), appending to `out` (does not clear it). Thin eager + // wrapper that drains `enumerate`; semantics match the historic engine. See + // `enumerate` for the meaning of `threshold`, `mode`, and `oracle`. bool compute(expr* r, split_set& out, unsigned threshold, split_mode mode = split_mode::strong, split_oracle const& oracle = {}); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index af8b280d80..c20bdf3114 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -146,7 +146,6 @@ namespace smt { } const expr_ref cases_expr(m.mk_or(cases), m); ctx.internalize(cases_expr, false); - std::cout << mk_pp(s, m) << " in " << mk_pp(r, m) << " =>\n" << mk_pp(cases_expr, m) << std::endl; th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); return; } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 39050620ad..c98b7a6649 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -132,6 +132,7 @@ add_executable(test-z3 simplifier.cpp sls_test.cpp sls_seq_plugin.cpp + seq_split.cpp small_object_allocator.cpp smt2print_parse.cpp smt_context.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 1727cb9dc0..dfc6d481c1 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -193,6 +193,7 @@ X(ho_matcher) \ X(finite_set) \ X(finite_set_rewriter) \ + X(seq_split) \ X(fpa) #define FOR_EACH_TEST(X, X_ARGV) \ diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp new file mode 100644 index 0000000000..229ec98664 --- /dev/null +++ b/src/test/seq_split.cpp @@ -0,0 +1,401 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_split.cpp + +Abstract: + + Unit tests for the regex split engine (the split function sigma) in ast/rewriter/seq_split.cpp. + +Author: + + Clemens Eisenhofer 2026-6-22 + +--*/ + +#include "ast/ast.h" +#include "ast/reg_decl_plugins.h" +#include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_split.h" +#include +#include + + +struct plugin_registrar { + plugin_registrar(ast_manager& m) { reg_decl_plugins(m); } +}; + +class seq_split_test { + ast_manager m; + plugin_registrar m_reg; + seq_rewriter m_rw; + seq_split m_split; + seq_util u; + sort_ref m_str; // the sequence (String) sort + sort_ref m_re; // the RegEx sort over m_str + + seq_util::rex& re() { return u.re; } + + expr_ref eps() { return expr_ref(re().mk_epsilon(m_str), m); } // mk_epsilon takes the seq sort + expr_ref dot() { return expr_ref(re().mk_full_char(m_re), m); } // mk_full_char takes the RegEx sort + expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } // .* + expr_ref empty_re() { return expr_ref(re().mk_empty(m_re), m); } // the bottom regex + expr_ref rappend(expr* a, expr* b) { return m_rw.mk_re_append(a, b); } // the engine's regex concat + expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); } + expr_ref rng(char lo, char hi) { + return expr_ref(re().mk_range(u.str.mk_string(zstring(std::string(1, lo).c_str())), + u.str.mk_string(zstring(std::string(1, hi).c_str()))), m); + } + + typedef std::set> pair_set; + + pair_set as_set(split_set const& s) { + pair_set out; + for (auto const& p : s) + out.insert({ p.m_d.get(), p.m_n.get() }); + return out; + } + + bool eager(expr* r, split_set& out, unsigned threshold = UINT_MAX, + split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { + return m_split.compute(r, out, threshold, mode, oracle); + } + + bool lazy(expr* r, split_set& out, unsigned threshold = UINT_MAX, + split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { + expr_ref node = m_split.make(r); + ENSURE(node); + return m_split.enumerate(node, mode, threshold, oracle, + [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); + } + + // assert that the eager and lazy engines agree on sigma(r) as a *set* of + // splits, and report the common cardinality. + unsigned check_agree(expr* r) { + split_set se, sl; + bool oke = eager(r, se); + bool okl = lazy(r, sl); + ENSURE(oke == okl); + if (!oke) + return 0; + ENSURE(as_set(se) == as_set(sl)); + return (unsigned)as_set(se).size(); + } + +public: + seq_split_test() : m_reg(m), m_rw(m), m_split(m_rw), u(m), m_str(m), m_re(m) { + m_str = u.str.mk_string_sort(); + m_re = re().mk_re(m_str); + } + + void test_eager_epsilon() { + split_set s; + ENSURE(eager(eps(), s)); + ENSURE(as_set(s) == pair_set({ { eps().get(), eps().get() } })); + } + + void test_eager_char() { + // sigma(.) = { , <., eps> } + expr_ref a = dot(); + split_set s; + ENSURE(eager(a, s)); + pair_set expected({ { eps().get(), a.get() }, { a.get(), eps().get() } }); + ENSURE(as_set(s) == expected); + } + + void test_eager_word() { + // sigma("ab") = { <"", "ab">, <"a","b">, <"ab",""> } + split_set s; + ENSURE(eager(word("ab"), s)); + pair_set expected({ + { word("").get(), word("ab").get() }, + { word("a").get(), word("b").get() }, + { word("ab").get(), word("").get() }, + }); + ENSURE(as_set(s) == expected); + } + + void test_eager_union() { + // sigma(a | b) = sigma(a) cup sigma(b) + expr_ref a = rng('a', 'a'), b = rng('b', 'b'); + expr_ref u_re(re().mk_union(a, b), m); + split_set s; + ENSURE(eager(u_re, s)); + pair_set expected({ + { eps().get(), a.get() }, { a.get(), eps().get() }, + { eps().get(), b.get() }, { b.get(), eps().get() }, + }); + ENSURE(as_set(s) == expected); + } + + void test_agree_all() { + expr_ref a = rng('a', 'a'), b = rng('b', 'b'); + expr_ref star(re().mk_star(a), m); + expr_ref plus(re().mk_plus(a), m); + expr_ref concat(re().mk_concat(a, b), m); + expr_ref uni(re().mk_union(a, b), m); + expr_ref inter(re().mk_inter(re().mk_star(a), re().mk_star(b)), m); + expr_ref compl_(re().mk_complement(re().mk_star(a)), m); + expr_ref diff(re().mk_diff(re().mk_star(a), re().mk_star(b)), m); + + ENSURE(check_agree(eps()) == 1); + ENSURE(check_agree(a) == 2); + ENSURE(check_agree(word("ab")) == 3); + ENSURE(check_agree(uni) == 4); + ENSURE(check_agree(star) == 3); // { , , } + (void)check_agree(plus); + (void)check_agree(concat); + (void)check_agree(inter); // strong-mode intersection + (void)check_agree(compl_); // strong-mode De Morgan complement + (void)check_agree(diff); + } + + void test_lazy_early_stop() { + // a* has 3 splits; stop after the first one. (Note .* is the full_seq + // special case with a single split, so use a proper char-class body.) + expr_ref star(re().mk_star(rng('a', 'a')), m); + expr_ref node = m_split.make(star); + ENSURE(node); + unsigned seen = 0; + bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, + [&](expr*, expr*) { ++seen; return false; /* stop now */ }); + ENSURE(ok); // early stop is reported as success + ENSURE(seen == 1); // and nothing was produced past the stop + } + + void test_threshold_giveup() { + expr_ref star(re().mk_star(rng('a', 'a')), m); // 3 splits + split_set s; + ENSURE(!lazy(star, s, /*threshold*/ 1)); + // the eager wrapper honours the same cap + split_set s2; + ENSURE(!eager(star, s2, /*threshold*/ 1)); + } + + void test_weak_vs_strong() { + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); + expr_ref compl_(re().mk_complement(re().mk_star(dot())), m); + + split_set s; + ENSURE(!eager(inter, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(!lazy(inter, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak)); + + // strong mode succeeds for both + s.reset(); + ENSURE(eager(inter, s, UINT_MAX, split_mode::strong)); + s.reset(); + ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); + } + + void test_make_non_regex() { + expr_ref not_a_regex(u.str.mk_string(zstring("a")), m); // String, not RegEx + expr_ref node = m_split.make(not_a_regex); + ENSURE(!node); + } + + void test_oracle_prunes() { + // sigma(.) without an oracle = { , <.,eps> }; an oracle that keeps + // only splits whose suffix is epsilon must drop one of the two. + expr_ref a = dot(); + expr_ref e = eps(); + split_oracle keep_eps_suffix = [&](expr*, expr* n) { return n == e.get(); }; + + split_set se, sl; + ENSURE(eager(a, se, UINT_MAX, split_mode::strong, keep_eps_suffix)); + ENSURE(lazy(a, sl, UINT_MAX, split_mode::strong, keep_eps_suffix)); + pair_set expected({ { a.get(), e.get() } }); + ENSURE(as_set(se) == expected); + ENSURE(as_set(sl) == expected); + } + + void test_eager_full_seq() { + // sigma(.*) = { <.*, .*> } + expr_ref ds = dotstar(); + split_set s; + ENSURE(eager(ds, s)); + ENSURE(as_set(s) == pair_set({ { ds.get(), ds.get() } })); + } + + void test_eager_bottom() { + // sigma(empty) = {} + split_set s; + ENSURE(eager(empty_re(), s)); + ENSURE(s.empty()); + + split_set sl; + ENSURE(lazy(empty_re(), sl)); + ENSURE(sl.empty()); + } + + void test_eager_empty_word() { + // sigma(to_re("")) = { <"", ""> } (a single, trivial split) + split_set s; + ENSURE(eager(word(""), s)); + ENSURE(as_set(s) == pair_set({ { word("").get(), word("").get() } })); + } + + void test_eager_star_content() { + // sigma(a*) = { , , } + expr_ref a = rng('a', 'a'); + expr_ref as(re().mk_star(a), m); + split_set s; + ENSURE(eager(as, s)); + pair_set expected({ + { eps().get(), eps().get() }, + { rappend(as, eps()).get(), rappend(a, as).get() }, + { rappend(as, a).get(), rappend(eps(), as).get() }, + }); + ENSURE(as_set(s) == expected); + } + + void test_eager_plus_content() { + // sigma(a+) = a*.sigma(a).a* (the star rule without ) + expr_ref a = rng('a', 'a'); + expr_ref as(re().mk_star(a), m); + expr_ref ap(re().mk_plus(a), m); + split_set s; + ENSURE(eager(ap, s)); + pair_set expected({ + { rappend(as, eps()).get(), rappend(a, as).get() }, + { rappend(as, a).get(), rappend(eps(), as).get() }, + }); + ENSURE(as_set(s) == expected); + } + + void test_eager_concat_content() { + // sigma(a.b) = sigma(a).b cup a.sigma(b) + expr_ref a = rng('a', 'a'), b = rng('b', 'b'); + expr_ref ab(re().mk_concat(a, b), m); + split_set s; + ENSURE(eager(ab, s)); + pair_set expected({ + { eps().get(), rappend(a, b).get() }, // + { a.get(), rappend(eps(), b).get() }, // + { rappend(a, eps()).get(), b.get() }, // + { rappend(a, b).get(), eps().get() }, // + }); + ENSURE(as_set(s) == expected); + } + + void test_nary_union() { + // sigma(a|b|c) has 2 splits per char-class + expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); + expr_ref u3(re().mk_union(a, re().mk_union(b, c)), m); + ENSURE(check_agree(u3) == 6); + } + + void test_nary_concat() { + // sigma(a.b.c) + expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c'); + expr_ref c3(re().mk_concat(a, re().mk_concat(b, c)), m); + ENSURE(check_agree(c3) >= 4); + } + + void test_nested_complement() { + // sigma(~~(a*)) + expr_ref cc(re().mk_complement(re().mk_complement(re().mk_star(rng('a', 'a')))), m); + (void)check_agree(cc); + } + + void test_determinism() { + expr_ref r(re().mk_concat(rng('a', 'a'), re().mk_star(rng('b', 'b'))), m); + split_set s1, s2; + ENSURE(lazy(r, s1)); + ENSURE(lazy(r, s2)); + ENSURE(as_set(s1) == as_set(s2)); + } + + void test_threshold_boundary() { + expr_ref as(re().mk_star(rng('a', 'a')), m); // exactly 3 splits + split_set s; + ENSURE(eager(as, s)); + unsigned k = (unsigned)as_set(s).size(); + ENSURE(k == 3); + + split_set ok_e, ok_l, bad_e, bad_l; + ENSURE(eager(as, ok_e, k)); + ENSURE(lazy(as, ok_l, k)); + ENSURE(!eager(as, bad_e, k - 1)); // one below threshold; give up + ENSURE(!lazy(as, bad_l, k - 1)); + } + + void test_early_stop_after_two() { + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + expr_ref node = m_split.make(as); + ENSURE(node); + unsigned seen = 0; + bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, + [&](expr*, expr*) { ++seen; return seen < 2; }); + ENSURE(ok); + ENSURE(seen == 2); + } + + void test_simplify() { + expr_ref regs[] = { + expr_ref(re().mk_star(rng('a', 'a')), m), + expr_ref(re().mk_complement(re().mk_star(rng('a', 'a'))), m), + expr_ref(re().mk_concat(rng('a', 'a'), rng('b', 'b')), m), + }; + for (auto& r : regs) { + split_set s; + ENSURE(eager(r, s)); + unsigned before = (unsigned)s.size(); + m_split.simplify(s); + ENSURE(s.size() <= before); + ENSURE(!s.empty()); + // idempotent + split_set s2(s); + m_split.simplify(s2); + ENSURE(as_set(s) == as_set(s2)); + } + } + + void test_trivial_oracle() { + expr_ref r(re().mk_star(rng('a', 'a')), m); + split_oracle keep_all = [](expr*, expr*) { return true; }; + split_set s_no, s_yes; + ENSURE(eager(r, s_no)); + ENSURE(eager(r, s_yes, UINT_MAX, split_mode::strong, keep_all)); + ENSURE(as_set(s_no) == as_set(s_yes)); + } + + void run() { + test_eager_epsilon(); + test_eager_char(); + test_eager_word(); + test_eager_union(); + test_agree_all(); + test_lazy_early_stop(); + test_threshold_giveup(); + test_weak_vs_strong(); + test_make_non_regex(); + test_oracle_prunes(); + test_eager_full_seq(); + test_eager_bottom(); + test_eager_empty_word(); + test_eager_star_content(); + test_eager_plus_content(); + test_eager_concat_content(); + test_nary_union(); + test_nary_concat(); + test_nested_complement(); + test_determinism(); + test_threshold_boundary(); + test_early_stop_after_two(); + test_simplify(); + test_trivial_oracle(); + } +}; + +void tst_seq_split() { + seq_split_test t; + t.run(); +} From b5ec0889bd070ac7a21582ff2759d5eba0aef434 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 30 Jun 2026 12:36:18 +0200 Subject: [PATCH 6/6] Put it into an iterator --- src/ast/rewriter/seq_split.cpp | 76 ++++++++++++++++++++++------------ src/ast/rewriter/seq_split.h | 65 ++++++++++++++++++++--------- src/test/seq_split.cpp | 71 ++++++++++++++++++++++++++----- 3 files changed, 154 insertions(+), 58 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index a5adcd055f..8977065fc0 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -506,8 +506,11 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, split_oracle const& oracle, split_set& out) { - return enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); + iterator it(*this, node, mode, threshold, oracle); + expr_ref d(m), n(m); + while (it.next(d, n)) + out.push_back(split_pair(d, n, m)); + return !it.gave_up(); } expr_ref seq_split::make(expr* r) { @@ -518,41 +521,61 @@ expr_ref seq_split::make(expr* r) { return mk_fromre(r); } -bool seq_split::enumerate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_yield const& yield) { +// --- Lazy enumerator -------------------------------------------------------- +// The worklist holds suspended split-sets. Each next() pops a node, head- +// normalizes it to a frontier (empty | single | union), and either returns the +// single split, pushes the two union branches back, or skips an empty. All the +// expansion work happens lazily, one split per next() call. + +seq_split::iterator::iterator(seq_split& engine, expr* node, split_mode mode, + unsigned threshold, split_oracle oracle) : + m_engine(engine), m(engine.m), m_mode(mode), m_threshold(threshold), + m_oracle(std::move(oracle)), m_work(engine.m) { SASSERT(node); - expr_ref_vector work(m); // GC-safe worklist of suspended split-sets - work.push_back(node); - unsigned count = 0; - while (!work.empty()) { - expr_ref t(work.back(), m); - work.pop_back(); + m_work.push_back(node); +} + +bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { + if (m_giveup) + return false; // a prior give-up is sticky + while (!m_work.empty()) { + expr_ref t(m_work.back(), m); + m_work.pop_back(); bool ok = true; - expr_ref hn = head_normalize(t, mode, threshold, oracle, ok); - if (!ok) - return false; // give up (unsupported / weak Boolean / overrun) + expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok); + if (!ok) { + m_giveup = true; // unsupported / weak Boolean / overrun + return false; + } expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; - if (is_empty_ss(hn)) + if (m_engine.is_empty_ss(hn)) continue; - if (is_single(hn, d, n)) { - if (oracle && !oracle(d, n)) + if (m_engine.is_single(hn, d, n)) { + if (m_oracle && !m_oracle(d, n)) continue; // pruned by lookahead - if (++count > threshold) - return false; // safety cap against space bloat - if (!yield(d, n)) - return true; // caller asked to stop early (success) - continue; + if (++m_count > m_threshold) { + m_giveup = true; // safety cap against space bloat + return false; + } + out_d = d; + out_n = n; + return true; } - if (is_union(hn, a, b)) { - work.push_back(a); - work.push_back(b); + if (m_engine.is_union(hn, a, b)) { + m_work.push_back(a); + m_work.push_back(b); continue; } UNREACHABLE(); } - return true; + return false; // exhausted (m_giveup stays false) +} + +seq_split::iterator seq_split::iterate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle) { + return iterator(*this, node, mode, threshold, oracle); } // Eager wrapper: drain the lazy enumeration into `out`. Semantics (give-up cases, @@ -564,8 +587,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo if (!seq().is_re(r, seq_sort)) return false; expr_ref node = mk_fromre(r); - return enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { result.push_back(split_pair(d, n, m)); return true; }); + return materialize(node, mode, threshold, oracle, result); } // same-D / same-N merge (paper eqs. 1 & 2): diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 185627ce1c..f3b7a57675 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -57,11 +57,6 @@ enum class split_mode { weak, strong }; // default) keeps everything, so sigma is unchanged. See seq_split::compute. typedef std::function split_oracle; -// Callback invoked by seq_split::enumerate for each concrete split as it -// emerges from the lazy expansion. Returning false stops the enumeration early -// (a successful early stop); returning true asks for the next split. -typedef std::function split_yield; - class seq_split { ast_manager& m; seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access @@ -132,6 +127,7 @@ class seq_split { expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold, split_oracle const& oracle, bool& ok); // Fully drain a suspended split-set into `out` (used for inter/compl bodies). + // Runs an `iterator` to exhaustion; returns false on a give-up. bool materialize(expr* node, split_mode mode, unsigned threshold, split_oracle const& oracle, split_set& out); @@ -155,30 +151,59 @@ class seq_split { public: explicit seq_split(seq_rewriter& rw); - // Build the *suspended* sigma(r) as a split-algebra term (no expansion). - // Returns null on a non-regex argument. Drive it with `enumerate`. - expr_ref make(expr* r); - - // Lazily expand a suspended split-set, invoking `yield` for every concrete - // split . The threshold is supplied by the caller and serves only as a - // safety cap against space bloat (lazy expansion still has to materialize the - // operands of intersection / complement). An overrun, an unsupported regex - // shape, or a Boolean-closure case in weak mode makes it return false ("give - // up"). `yield` returning false stops early and is reported as success. + // Lazy split enumerator. Holds the suspended split-set worklist and produces + // the concrete splits one at a time, on demand, instead of computing + // them all up front. Obtain one from seq_split::iterate (or construct it + // directly) and pull splits with next() until it returns false; gave_up() then + // tells a normal exhaustion (false) apart from a give-up (true). // - // `oracle` (optional) prunes non-viable splits as they are yielded. It must + // The threshold is supplied by the caller and serves only as a safety cap + // against space bloat (lazy expansion still has to materialize the operands of + // intersection / complement). A threshold overrun, an unsupported regex shape, + // or a Boolean-closure case in weak mode aborts the enumeration: next() returns + // false and gave_up() returns true. To stop early, simply stop calling next(). + // + // `oracle` (optional) prunes non-viable splits as they are produced. It must // be sound to apply per split: a candidate N can still gain a prefix from a // factor appended to its right later (concat/star), so the oracle must use a // "prefix-compatible" test (prune only when N can never match the lookahead, // even partially), NOT a strict "starts-with" test. The complement body is // expanded WITHOUT the oracle (inverted orientation); the oracle is re-applied // to the complement's output fold. - bool enumerate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_yield const& yield); + class iterator { + seq_split& m_engine; + ast_manager& m; + split_mode m_mode; + unsigned m_threshold; + split_oracle m_oracle; + expr_ref_vector m_work; // GC-safe worklist of suspended split-sets + unsigned m_count = 0; // splits produced so far (vs. threshold) + bool m_giveup = false; + public: + iterator(seq_split& engine, expr* node, split_mode mode, + unsigned threshold, split_oracle oracle); + // Compute the next split. On success returns true and sets ; on + // exhaustion or give-up returns false (see gave_up()). Calling next() + // again after it has returned false keeps returning false. + bool next(expr_ref& d, expr_ref& n); + // Valid after next() has returned false: true iff the enumeration aborted + // (unsupported regex / weak-mode Boolean / threshold overrun) rather than + // running out of splits. + bool gave_up() const { return m_giveup; } + }; + + // Build the *suspended* sigma(r) as a split-algebra term (no expansion). + // Returns null on a non-regex argument. Drive it with `iterate`. + expr_ref make(expr* r); + + // Create a lazy enumerator over a suspended split-set `node` (typically the + // result of make()). See `iterator` for the meaning of the arguments. + iterator iterate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle = {}); // Compute sigma(r), appending to `out` (does not clear it). Thin eager - // wrapper that drains `enumerate`; semantics match the historic engine. See - // `enumerate` for the meaning of `threshold`, `mode`, and `oracle`. + // wrapper that drains an `iterator` to exhaustion; semantics match the historic + // engine. See `iterator` for the meaning of `threshold`, `mode`, and `oracle`. bool compute(expr* r, split_set& out, unsigned threshold, split_mode mode = split_mode::strong, split_oracle const& oracle = {}); diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp index 229ec98664..29df0545c7 100644 --- a/src/test/seq_split.cpp +++ b/src/test/seq_split.cpp @@ -68,8 +68,11 @@ class seq_split_test { split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { expr_ref node = m_split.make(r); ENSURE(node); - return m_split.enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); + seq_split::iterator it = m_split.iterate(node, mode, threshold, oracle); + expr_ref d(m), n(m); + while (it.next(d, n)) + out.push_back(split_pair(d, n, m)); + return !it.gave_up(); } // assert that the eager and lazy engines agree on sigma(r) as a *set* of @@ -154,16 +157,18 @@ public: } void test_lazy_early_stop() { - // a* has 3 splits; stop after the first one. (Note .* is the full_seq - // special case with a single split, so use a proper char-class body.) + // a* has 3 splits; pull just the first one and then stop. (Note .* is the + // full_seq special case with a single split, so use a proper char-class body.) expr_ref star(re().mk_star(rng('a', 'a')), m); expr_ref node = m_split.make(star); ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); unsigned seen = 0; - bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, - [&](expr*, expr*) { ++seen; return false; /* stop now */ }); - ENSURE(ok); // early stop is reported as success - ENSURE(seen == 1); // and nothing was produced past the stop + if (it.next(d, n)) // pull exactly one split, then walk away + ++seen; + ENSURE(!it.gave_up()); // stopping early is not a give-up + ENSURE(seen == 1); } void test_threshold_giveup() { @@ -331,13 +336,55 @@ public: expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits expr_ref node = m_split.make(as); ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); unsigned seen = 0; - bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, - [&](expr*, expr*) { ++seen; return seen < 2; }); - ENSURE(ok); + while (seen < 2 && it.next(d, n)) // pull two splits on demand, then stop + ++seen; + ENSURE(!it.gave_up()); ENSURE(seen == 2); } + void test_iterator_exhaustion() { + // Pull every split on demand; gave_up() must stay false on a clean + // exhaustion, and next() must keep returning false once drained. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + expr_ref node = m_split.make(as); + ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); + unsigned seen = 0; + while (it.next(d, n)) + ++seen; + ENSURE(seen == 3); + ENSURE(!it.gave_up()); + // idempotent past the end + ENSURE(!it.next(d, n)); + ENSURE(!it.gave_up()); + } + + void test_iterator_giveup() { + // A threshold overrun aborts: next() returns false and gave_up() is true. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1 + expr_ref node = m_split.make(as); + ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, /*threshold*/ 1, {}); + expr_ref d(m), n(m); + unsigned seen = 0; + while (it.next(d, n)) + ++seen; + ENSURE(it.gave_up()); // aborted, not a clean exhaustion + ENSURE(seen <= 1); // produced at most the capped number + + // A weak-mode Boolean closure is likewise a give-up. + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); + expr_ref inode = m_split.make(inter); + ENSURE(inode); + seq_split::iterator wit = m_split.iterate(inode, split_mode::weak, UINT_MAX, {}); + ENSURE(!wit.next(d, n)); + ENSURE(wit.gave_up()); + } + void test_simplify() { expr_ref regs[] = { expr_ref(re().mk_star(rng('a', 'a')), m), @@ -390,6 +437,8 @@ public: test_determinism(); test_threshold_boundary(); test_early_stop_after_two(); + test_iterator_exhaustion(); + test_iterator_giveup(); test_simplify(); test_trivial_oracle(); }