diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index afe18ad3f3..5052162240 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -41,6 +41,7 @@ z3_add_component(rewriter seq_axioms.cpp seq_eq_solver.cpp seq_derive.cpp + seq_split.cpp seq_subset.cpp seq_derive.cpp seq_monadic.cpp diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index dbe3e694f2..24a2d1285c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -25,6 +25,7 @@ Notes: #include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/seq_subset.h" +#include "ast/rewriter/seq_split.h" #include "util/params.h" #include "util/lbool.h" #include "util/sign.h" @@ -125,6 +126,7 @@ class seq_rewriter { seq_util m_util; seq_subset m_subset; + seq_split m_split; arith_util m_autil; bool_rewriter m_br; seq::derive m_derive; @@ -324,7 +326,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_derive(m, *this), // m_re2aut(m), + m_util(m), m_subset(m_util.re), m_split(*this), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m) { } @@ -391,6 +393,37 @@ 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, + split_mode const 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); } + + // Build the *suspended* sigma(r) split-set term (no expansion); drive it with + // iterate_split. Returns null on a non-regex argument. See seq_split.h. + expr_ref make_split(expr* r) { return m_split.make(r); } + + // Create a lazy enumerator over a suspended split-set `node` (typically the + // result of make_split()). See seq_split::iterator for the arguments. + seq_split::iterator iterate_split(expr* node, unsigned threshold, + split_mode const mode = split_mode::strong, + split_oracle const& oracle = {}) { + return m_split.iterate(node, mode, threshold, oracle); + } + + // Decompose a membership constraint into a boundary (head, tail) and a set of + // regex splits; see seq_split::split_membership. + std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { + return m_split.split_membership(str, regex, threshold, result); + } + + // split-algebra performance counters + split_stats const& get_split_stats() const { return m_split.stats(); } + void reset_split_stats() { m_split.reset_stats(); } + /* * Construct r1 XOR r2 applying the structural rewrites in * mk_re_xor (r XOR r = empty, comp/empty/full normalisation, AC diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp new file mode 100644 index 0000000000..a39c8cf434 --- /dev/null +++ b/src/ast/rewriter/seq_split.cpp @@ -0,0 +1,1030 @@ + +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_split.cpp + +Abstract: + + Regex split decomposition (the split function sigma). See seq_split.h. + +Author: + + Clemens Eisenhofer 2026-6-10 + +--*/ + +#include "ast/rewriter/seq_split.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_range_collapse.h" +#include "ast/ast_pp.h" +#include "util/obj_hashtable.h" +#include "util/obj_pair_hashtable.h" + +seq_split::seq_split(seq_rewriter& rw) : + 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; } + +// Add unless the (optional) lookahead oracle prunes it. +void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const { + ++m_stats.m_pushes; + if (!oracle || oracle(d, n)) + out.push_back(split_pair(d, n, m)); + else + ++m_stats.m_oracle_prunes; +} + +// 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 { + ++m_stats.m_intersect; + const seq_util::rex& r = re(); + // Dedup the cross-product: a split-set denotes the UNION of its pairs, + // so identical (perfectly-shared) pairs are redundant. Skipping them keeps + // the De Morgan fold from accumulating exponentially many equal splits. + obj_pair_hashtable seen; + 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); + ++m_stats.m_intersect_pairs; + std::pair key(di.get(), ni.get()); + if (seen.contains(key)) { + ++m_stats.m_dedup_drops; + continue; + } + seen.insert(key); + push(result, oracle, di, ni); + if (result.size() > threshold) { + ++m_stats.m_threshold_overruns; + 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 { + + ++m_stats.m_complement; + 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; + // Do not simplify(acc) here. It does bound |acc| (each round + // intersects acc with a 2-element set, so the fold is 2^|sp| without it), + // but merge_by collapses pairs by unioning their other component, so + // re-merging every round nests unions ~rounds*|acc| deep and the + // recursive is_subset / mk_regex_union_normalize then overflow the stack. + // |acc| is bounded by the caller's cap instead; see BOOL_CLOSURE_CAP. + if (acc.size() > threshold) { + ++m_stats.m_threshold_overruns; + return false; + } + } + result.append(acc); + return true; +} + +// Single-character regex for a cofactor path condition `pred` (a Boolean over the +// character (:var 0)). Materialized via the canonical seq::range_predicate as a +// union-of-ranges regex (fully supported by the derivative / emptiness / primitive +// path, and canonical so equivalent classes share AST identity). Falls back to +// of_pred(lambda) only for predicates outside the recognized range fragment. +expr_ref seq_split::mk_charclass_re(expr* pred, sort* seq_sort) { + seq_util& sq = seq(); + sort* cs = sq.mk_char_sort(); + expr_ref var0(m.mk_var(0, cs), m); + seq::range_predicate rp(sq.max_char()); + if (seq::guard_to_range_predicate(sq, var0, pred, rp)) + return seq::range_predicate_to_regex(sq, rp, seq_sort); + symbol nm("c"); + expr_ref lam(m.mk_lambda(1, &cs, &nm, pred), m); + return expr_ref(re().mk_of_pred(lam), m); +} + +// r == E(r) | RE(LF(delta(r))): peel one character through the symbolic derivative +// (Brzozowski cofactors) and recurse. Shared by the complement and intersection +// cases to avoid the De Morgan / cross-product blow-up. delta distributes over +// both ~ and &, so LF(delta(r)) = { (alpha_i, tgt_i) } with tgt_i the (complement / +// intersection of) character-derivatives. Records `r` in `deriv_memo` as a cycle +// guard. Returns a null expr_ref when nullability of `r` is not statically +// decidable (the caller then falls back to its structural rule). +expr_ref seq_split::try_derivative_split(expr* r, sort* seq_sort, obj_hashtable& deriv_memo) { + seq_util::rex& rex = re(); + expr_ref nb = m_rw.is_nullable(r); + if (!m.is_true(nb) && !m.is_false(nb)) + return expr_ref(m); // undecidable -> fall back + deriv_memo.insert(r); + sort* re_sort = rex.mk_re(seq_sort); + expr_ref unfolded(m); + if (m.is_true(nb)) + unfolded = rex.mk_epsilon(seq_sort); // E(r) = eps + else + unfolded = rex.mk_empty(re_sort); // E(r) = bot + expr_ref_pair_vector cofs(m); + m_rw.brz_derivative_cofactors(r, cofs); // { (alpha_i, tgt_i) } = LF(delta(r)) + for (auto const& [cond, tgt] : cofs) { + expr_ref alpha = mk_charclass_re(cond, seq_sort); // single-char regex + expr_ref term(rex.mk_concat(alpha, tgt), m); // alpha_i . tgt_i + unfolded = expr_ref(rex.mk_union(unfolded, term), m); + } + return mk_fromre(unfolded); +} + +// The complemented body `a` "starts with an unbounded loop" (R*.S / R+.S) when its +// leftmost concat factor is a star or plus. delta(~(R*.S)) regenerates R*.S (the +// R* self-loops) and never collapses to a bare ~(R*), so the forward derivative +// peel of such a complement does NOT terminate. Route these through the De Morgan +// rule instead (which sends R* to the star rule / Nielsen star-introduction). +// Bounded loops (re.loop m m, e.g. the L15 counted-membership benchmarks) DO +// terminate under the derivative and are intentionally NOT matched here. +static bool complement_body_diverges(seq_util::rex& rex, expr* a) { + while (rex.is_concat(a) && to_app(a)->get_num_args() > 0) + a = to_app(a)->get_arg(0); // descend to the leftmost factor + return rex.is_star(a) || rex.is_plus(a); +} + +// One level of the sigma rules. 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, unsigned threshold, bool& ok, obj_hashtable& deriv_memo) { + ok = true; + ++m_stats.m_sigma_expand; + seq_util& sq = seq(); + seq_util::rex& rex = re(); + + sort* seq_sort = nullptr; + if (!sq.is_re(r, seq_sort)) { + ok = false; + return expr_ref(m); + } + ensure_decls(seq_sort); + + // bottom: sigma(empty) = {} + if (rex.is_empty(r)) + return mk_empty(); + + // epsilon: sigma(eps) = { } + if (rex.is_epsilon(r)) { + const expr_ref eps(rex.mk_epsilon(seq_sort), m); + return mk_single(eps, eps); + } + + 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; + 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(cur, str2)) { + str += str2; + continue; + } + // not a constant string; unsupported for now + 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); + acc = mk_union(acc, mk_single(p, q)); + } + return acc; + } + + // 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, m); + const expr_ref eps(rex.mk_epsilon(seq_sort), m); + return mk_union(mk_single(eps, ex), mk_single(ex, eps)); + } + + // .* : sigma(.*) = { <.*, .*> } + if (rex.is_full_seq(r)) { + const expr_ref ex(r, m); + return mk_single(ex, ex); + } + + // 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); + expr_ref acc = mk_empty(); + for (expr* arg : *ap) { + acc = mk_union(acc, mk_fromre(arg)); + } + return acc; + } + + // concat: sigma(r0...r_{n-1}) = U_i (r0...r_{i-1}) . sigma(ri) . (r_{i+1}...r_{n-1}) + // 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++) { + 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), m) : expr_ref(arg, m); + } + } + 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); + } + } + expr_ref term = mk_lcat(left, mk_rcat(mk_fromre(ap->get_arg(i)), right)); + acc = mk_union(acc, term); + } + 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); + 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* + return mk_lcat(star, mk_rcat(mk_fromre(a), star)); + } + + // intersection: prefer the derivative rule r = E(r) | RE(LF(delta(r))) (delta + // distributes over &) to avoid the Split(r0) cap ... cap Split(r_{n-1}) cross- + // product blow-up; fall back to the eager cross-product on a cyclic revisit. + if (rex.is_intersection(r)) { + if (!deriv_memo.contains(r)) { + expr_ref d = try_derivative_split(r, seq_sort, deriv_memo); + if (d.get()) return d; + } + app* ap = to_app(r); + const unsigned n = ap->get_num_args(); + 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). Prefer the symbolic-derivative rule to avoid the De + // Morgan 2^k blow-up: r = E(~a) | RE(LF(delta(~a))), peel one character and + // recurse. Fall back to the De Morgan rule sigma(~a)=~sigma(a) when the body + // starts with an unbounded loop R*.S / R+.S (the derivative regenerates R*.S + // and diverges -- a termination flaw of the peel, see complement_body_diverges) + // or on a cyclic revisit (both keep it terminating). + if (rex.is_complement(r, a)) { + if (!complement_body_diverges(rex, a) && !deriv_memo.contains(r)) { + expr_ref d = try_derivative_split(r, seq_sort, deriv_memo); + if (d.get()) return d; + } + return mk_compl(mk_fromre(a)); // De Morgan fallback + } + + // abbreviation + // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b). + if (rex.is_diff(r, a, b)) + return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b))); + + // abbreviation + // optional: a? = eps | a ; sigma(a?) = sigma(eps | a) = eps cup sigma(a) + if (rex.is_opt(r, a)) { + const expr_ref eps(rex.mk_epsilon(seq_sort), m); + return mk_union(mk_single(eps, eps), mk_fromre(a)); + } + + // loop: r{l,h} = \bigcup_{l <= j <= h} r^j. + // A split either singles out the i-th copy of a (0 <= i < h) as + // for in sigma(a), + // where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining + // j in [l,h] with j > i, into a single loop [ when l == 0] + unsigned l, h; + if (rex.is_loop(r, a, l, h)) { + // The rule unfolds eagerly into h branches; cap this *before* building + // them (the iterator's threshold only counts emitted splits, which + // would be too late for a huge bound like r{0,10^8}). + if (h > threshold) { + TRACE(seq, tout << "seq_split: loop bound " << h << " exceeds threshold\n";); + ok = false; + return expr_ref(m); + } + expr_ref acc = mk_empty(); + if (l == 0) { + const expr_ref eps(rex.mk_epsilon(seq_sort), m); + acc = mk_single(eps, eps); + } + for (unsigned i = 0; i < h; i++) { + const expr_ref pre(rex.mk_loop_proper(a, i, i), m); + const unsigned lo_i = l > i + 1 ? l - i - 1 : 0; + const unsigned hi_i = h - i - 1; + const expr_ref post(rex.mk_loop_proper(a, lo_i, hi_i), m); + acc = mk_union(acc, mk_lcat(pre, mk_rcat(mk_fromre(a), post))); + } + return acc; + } + + // one-sided loop r{l,} / ite / other shapes: not handled (bail). + TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";); + 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, + obj_hashtable& deriv_memo) { + 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, threshold, ok, deriv_memo); + if (!ok) + return expr_ref(m); + if (is_frontier(e)) + return e; + return head_normalize(e, mode, threshold, oracle, ok, deriv_memo); + } + + // 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, deriv_memo); + 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, deriv_memo); + 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); + } + // The operand split-sets are materialized eagerly, so they are capped + // rather than by the (deliberately huge) cap that bounds + // how many splits the lazy enumeration may emit + const unsigned cap = std::min(threshold, BOOL_CLOSURE_CAP); + split_set sa, sb, tmp; + if (!materialize(a, mode, cap, oracle, sa) || + !materialize(b, mode, cap, oracle, sb)) { + ok = false; + return expr_ref(m); + } + // simplify(sa)/simplify(sb) before the cross product would cut the + // |sa|*|sb| pairs considerably, but merge_by builds unions of unbounded + // depth and the recursive seq_subset::is_subset then overflows the stack. + // Needs a depth-guarded is_subset first. + if (!intersect(sa, sb, tmp, cap, 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(). + const unsigned cap = std::min(threshold, BOOL_CLOSURE_CAP); + split_set sa, res; + if (!materialize(a, mode, cap, split_oracle{}, sa)) { + ok = false; + return expr_ref(m); + } + // As in the inter case, simplify(sa) here would cut the number of fold + // rounds but currently risks a stack overflow; see the note above. + if (!complement(m_seq_sort, sa, res, cap, oracle)) { + ok = false; + return expr_ref(m); + } + return from_split_set(res); + } + + // Not a recognized split-algebra node. This is only reachable when the + // suspended term was built for a different sequence sort: ensure_decls + // rebuilds the sort-dependent declarations (single / from_re / lcat / rcat) + // on a sort switch, so older terms stop matching the recognizers. Degrade + // to a give-up instead of asserting. + TRACE(seq, tout << "seq_split: stale split-set node " << mk_pp(t, m) << "\n";); + ok = false; + return expr_ref(m); +} + +bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle, split_set& out) { + ++m_stats.m_materialize; + 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)); + if (out.size() > m_stats.m_max_split_set) + m_stats.m_max_split_set = out.size(); + return !it.gave_up(); +} + +expr_ref seq_split::make(expr* r) { + SASSERT(r); + ++m_stats.m_make; + sort* seq_sort = nullptr; + if (!seq().is_re(r, seq_sort)) + return expr_ref(m); + return mk_fromre(r); +} + +// --- 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); + 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 = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok, m_deriv_memo); + if (!ok) { + m_giveup = true; // unsupported / weak Boolean / overrun + ++m_engine.m_stats.m_giveups; + return false; + } + + expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; + if (m_engine.is_empty_ss(hn)) + continue; + if (m_engine.is_single(hn, d, n)) { + if (m_oracle && !m_oracle(d, n)) { + ++m_engine.m_stats.m_oracle_prunes; + continue; // pruned by lookahead + } + if (++m_count > m_threshold) { + m_giveup = true; // safety cap against space bloat + ++m_engine.m_stats.m_giveups; + ++m_engine.m_stats.m_threshold_overruns; + return false; + } + out_d = d; + out_n = n; + ++m_engine.m_stats.m_splits; + return true; + } + if (m_engine.is_union(hn, a, b)) { + m_work.push_back(a); + m_work.push_back(b); + continue; + } + UNREACHABLE(); + } + 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, +// 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 materialize(node, mode, threshold, oracle, result); +} + +// 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 { + 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), m); + 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 { + ++m_stats.m_simplify; + 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. Size-capped: each check runs two language-inclusion + // tests, so the O(n^2) pass is only affordable on small sets. + 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 { + 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)); + } + + expr* ch = nullptr; + 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()) { + // The term was entirely constant, so the derivative loop above already + // reduced the membership to nullability of `regex`. Return it as the + // single split over (head, tail) = ("", "") rather than + // discarding that work -- a null head is reserved for give-ups. + sort* srt = str->get_sort(); + const expr_ref empty_str(seq().str.mk_empty(srt), m); + result.push_back(split_pair(re().mk_epsilon(srt), regex, m)); + return { empty_str, empty_str }; + } + + // Choose the factorization boundary so the tail starts with the + // longest run of concrete characters c. A run may mix constant-character + // units and string literals and is weighted by the number of characters + // it contributes. + // 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). + auto token_chars = [&](expr* t, unsigned& chars) { + zstring s2; + expr* ch2; + if (seq().str.is_string(t, s2)) { + chars = s2.length(); + return true; + } + if (seq().str.is_unit(t, ch2) && seq().is_const_char(ch2)) { + chars = 1; + return true; + } + return false; + }; + const unsigned total = tokens.size(); + unsigned run_start = 0, run_len = 0, run_chars = 0; + for (i = 1; i < total; ) { + unsigned chars = 0, block_chars = 0; + if (!token_chars(tokens.get(i), chars)) { + i++; + continue; + } + unsigned j = i; + while (j < total && token_chars(tokens.get(j), chars)) { + block_chars += chars; + j++; + } + if (block_chars > run_chars) { + run_chars = block_chars; + 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 = tokens.get(0); + for (i = 1; i < p; i++) { + head = seq().str.mk_concat(head, 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 (i = 0; i < run_len; i++) { + expr* t = tokens.get(run_start + i); + zstring s2; + if (seq().str.is_string(t, s2)) { + c = c + s2; + continue; + } + unsigned cv; + VERIFY(seq().str.is_unit(t, 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 { expr_ref(m), expr_ref(m) }; + } + + simplify(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 (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 { 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))) + 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..6ed2eb01ad --- /dev/null +++ b/src/ast/rewriter/seq_split.h @@ -0,0 +1,297 @@ +/*++ +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 "util/obj_hashtable.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). +// 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; + +// Lightweight performance counters for the split algebra (behaviour-neutral; +// read via seq_rewriter::get_split_stats). See seq_split.cpp for where each fires. +struct split_stats { + unsigned m_make = 0; // make(): suspended sigma(r) built + unsigned m_sigma_expand = 0; // expand_fromre(): one sigma rule level + unsigned m_materialize = 0; // materialize(): a split-set drained + unsigned m_splits = 0; // splits produced by iterator::next() + unsigned m_pushes = 0; // candidate offered to push() + unsigned m_oracle_prunes = 0; // candidates dropped by the lookahead oracle + unsigned m_intersect = 0; // intersect() calls + unsigned m_intersect_pairs = 0; // pairs formed by intersect() cross-products + unsigned m_complement = 0; // complement() calls + unsigned m_giveups = 0; // iterator give-ups (unsupported/weak/overrun) + unsigned m_threshold_overruns = 0; // threshold hits (intersect/complement/iterator) + unsigned m_max_split_set = 0; // largest materialized split-set seen + unsigned m_dedup_drops = 0; // duplicate pairs skipped in intersect + unsigned m_simplify = 0; // simplify() calls + void reset() { *this = split_stats(); } +}; + +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 + mutable split_stats m_stats; // performance counters (see -st) + + seq_util& seq() const; + seq_util::rex& re() const; + + // (Re)build the local declarations for `seq_sort` if not already current. + // NB: rebuilding for a new sequence sort invalidates suspended split-set + // terms built for the previous sort (head_normalize degrades to a give-up + // on such stale terms); an iterator must not be used across a sort switch. + 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 or on a + // loop bound exceeding `threshold` (the loop rule unfolds eagerly into one + // branch per copy, so it must be capped before allocation). + expr_ref expand_fromre(expr* r, unsigned threshold, bool& ok, obj_hashtable& deriv_memo); + + // Build the single-character regex for a cofactor path condition `pred` (a + // Boolean over the character (:var 0)). Prefer a canonical range / + // union-of-ranges (see seq::range_predicate_to_regex); fall back to + // of_pred(lambda) only for predicates outside the recognized range fragment. + expr_ref mk_charclass_re(expr* pred, sort* seq_sort); + + // r == E(r) | RE(LF(delta(r))): build the suspended split-set for `r` by + // peeling one character through the symbolic derivative (Brzozowski cofactors) + // and recursing. Used for complement and intersection to avoid the De Morgan + // / cross-product blow-up. Records `r` in `deriv_memo` (cycle guard). Returns + // a null expr_ref when nullability of `r` is not statically decidable. + expr_ref try_derivative_split(expr* r, sort* seq_sort, obj_hashtable& deriv_memo); + + // 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, + obj_hashtable& deriv_memo); + + // 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); + + // 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; + + // Cap on the split-sets materialized for the *Boolean-closure* cases + // (intersection / complement), which cannot be produced lazily and are + // therefore drained in full inside head_normalize. This is a different + // quantity from the caller's `threshold`, which bounds how many splits the + // lazy enumeration may EMIT and is typically huge (a consumer walking the + // splits one at a time may legitimately want arbitrarily many). Reusing + // that value here let the De Morgan fold -- whose `acc` is intersected with a + // 2-element set per element, hence doubles -- run to 2^20 pairs before + // aborting, which is several seconds of pure waste. Overrunning this cap is + // a give-up, so the caller falls through to its other rules; that is sound + // and strictly better than the hang. + static const unsigned BOOL_CLOSURE_CAP = 256; + +public: + explicit seq_split(seq_rewriter& rw); + + // Performance counters. + split_stats const& stats() const { return m_stats; } + void reset_stats() { m_stats.reset(); } + + // 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). + // + // 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, + // a loop bound exceeding the threshold, 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. + 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; + // Complement ~-regex states already expanded via the symbolic-derivative + // rule; re-encountering one (a cycle) falls back to the De Morgan rule so + // the lazy unfolding terminates. Per-iterator (iterators run concurrently). + obj_hashtable m_deriv_memo; + 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 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 = {}); + + // 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 `str in regex` into a boundary + // (head, tail) with str = head . c . tail (c a constant run consumed into + // the splits by derivatives) and a split-set such that the membership + // holds iff head in D and tail in N for some in `result`. + // A null head signals a give-up (threshold / unsupported shape). An + // entirely-constant `str` is fully consumed by derivatives and returns + // ("", "") with the single split . + 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; + + +}; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 6bd0d0bdba..daef3bf6e0 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -133,6 +133,7 @@ add_executable(test-z3 scoped_vector.cpp seq_rewriter.cpp seq_monadic.cpp + seq_split.cpp seq_monadic_bench.cpp simple_parser.cpp scanner_io.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index b8d18d3b40..4e981e21b4 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -117,6 +117,7 @@ X(regex_range_collapse) \ X(seq_rewriter) \ X(seq_monadic) \ + X(seq_split) \ X(seq_monadic_bench) \ X(check_assumptions) \ X(smt_context) \ diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp new file mode 100644 index 0000000000..79ffd11f61 --- /dev/null +++ b/src/test/seq_split.cpp @@ -0,0 +1,460 @@ +/*++ +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); + 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 + // 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; 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; + 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() { + 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() { + // ~(.*) is the complemented-star (~(R*)) case: it has no terminating + // derivative peel, so it falls back to the eager De Morgan node ~sigma(a), + // which weak mode refuses (producing even one split would materialize the + // operand split-set). Strong mode performs the eager De Morgan complement. + expr_ref compl_(re().mk_complement(re().mk_star(dot())), m); + // An intersection is expanded lazily through the symbolic derivative + // r = E(r) | RE(LF(delta(r))) (delta distributes over &): one character + // peel, no operand materialization, so weak mode now handles it too. + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); + + split_set s; + ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); // De Morgan node: weak refuses + s.reset(); + ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); // strong: eager De Morgan + + // intersection is derivative-expanded (lazy): succeeds in BOTH modes + s.reset(); + ENSURE(eager(inter, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(lazy(inter, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(eager(inter, 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); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); + unsigned seen = 0; + 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 eager Boolean closure is likewise a give-up: ~(.*) is the + // complemented-star case with no terminating derivative peel, so it needs + // the eager De Morgan node, which weak mode refuses. (An intersection, by + // contrast, is now derivative-expanded and succeeds in weak mode.) + expr_ref cstar(re().mk_complement(re().mk_star(dot())), m); + expr_ref cnode = m_split.make(cstar); + ENSURE(cnode); + seq_split::iterator wit = m_split.iterate(cnode, 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), + 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_iterator_exhaustion(); + test_iterator_giveup(); + test_simplify(); + test_trivial_oracle(); + } +}; + +void tst_seq_split() { + seq_split_test t; + t.run(); +}