From a88dfa64ac0c19e25f41a1a044806559128b1455 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 26 Jun 2026 17:37:40 +0200 Subject: [PATCH] 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(); +}