From b5ec0889bd070ac7a21582ff2759d5eba0aef434 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 30 Jun 2026 12:36:18 +0200 Subject: [PATCH] Put it into an iterator --- src/ast/rewriter/seq_split.cpp | 76 ++++++++++++++++++++++------------ src/ast/rewriter/seq_split.h | 65 ++++++++++++++++++++--------- src/test/seq_split.cpp | 71 ++++++++++++++++++++++++++----- 3 files changed, 154 insertions(+), 58 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index a5adcd055f..8977065fc0 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -506,8 +506,11 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, split_oracle const& oracle, split_set& out) { - return enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); + iterator it(*this, node, mode, threshold, oracle); + expr_ref d(m), n(m); + while (it.next(d, n)) + out.push_back(split_pair(d, n, m)); + return !it.gave_up(); } expr_ref seq_split::make(expr* r) { @@ -518,41 +521,61 @@ expr_ref seq_split::make(expr* r) { return mk_fromre(r); } -bool seq_split::enumerate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_yield const& yield) { +// --- Lazy enumerator -------------------------------------------------------- +// The worklist holds suspended split-sets. Each next() pops a node, head- +// normalizes it to a frontier (empty | single | union), and either returns the +// single split, pushes the two union branches back, or skips an empty. All the +// expansion work happens lazily, one split per next() call. + +seq_split::iterator::iterator(seq_split& engine, expr* node, split_mode mode, + unsigned threshold, split_oracle oracle) : + m_engine(engine), m(engine.m), m_mode(mode), m_threshold(threshold), + m_oracle(std::move(oracle)), m_work(engine.m) { SASSERT(node); - expr_ref_vector work(m); // GC-safe worklist of suspended split-sets - work.push_back(node); - unsigned count = 0; - while (!work.empty()) { - expr_ref t(work.back(), m); - work.pop_back(); + m_work.push_back(node); +} + +bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { + if (m_giveup) + return false; // a prior give-up is sticky + while (!m_work.empty()) { + expr_ref t(m_work.back(), m); + m_work.pop_back(); bool ok = true; - expr_ref hn = head_normalize(t, mode, threshold, oracle, ok); - if (!ok) - return false; // give up (unsupported / weak Boolean / overrun) + expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok); + if (!ok) { + m_giveup = true; // unsupported / weak Boolean / overrun + return false; + } expr *a = nullptr, *b = nullptr, *d = nullptr, *n = nullptr; - if (is_empty_ss(hn)) + if (m_engine.is_empty_ss(hn)) continue; - if (is_single(hn, d, n)) { - if (oracle && !oracle(d, n)) + if (m_engine.is_single(hn, d, n)) { + if (m_oracle && !m_oracle(d, n)) continue; // pruned by lookahead - if (++count > threshold) - return false; // safety cap against space bloat - if (!yield(d, n)) - return true; // caller asked to stop early (success) - continue; + if (++m_count > m_threshold) { + m_giveup = true; // safety cap against space bloat + return false; + } + out_d = d; + out_n = n; + return true; } - if (is_union(hn, a, b)) { - work.push_back(a); - work.push_back(b); + if (m_engine.is_union(hn, a, b)) { + m_work.push_back(a); + m_work.push_back(b); continue; } UNREACHABLE(); } - return true; + return false; // exhausted (m_giveup stays false) +} + +seq_split::iterator seq_split::iterate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle) { + return iterator(*this, node, mode, threshold, oracle); } // Eager wrapper: drain the lazy enumeration into `out`. Semantics (give-up cases, @@ -564,8 +587,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo if (!seq().is_re(r, seq_sort)) return false; expr_ref node = mk_fromre(r); - return enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { result.push_back(split_pair(d, n, m)); return true; }); + return materialize(node, mode, threshold, oracle, result); } // same-D / same-N merge (paper eqs. 1 & 2): diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 185627ce1c..f3b7a57675 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -57,11 +57,6 @@ enum class split_mode { weak, strong }; // default) keeps everything, so sigma is unchanged. See seq_split::compute. typedef std::function split_oracle; -// Callback invoked by seq_split::enumerate for each concrete split as it -// emerges from the lazy expansion. Returning false stops the enumeration early -// (a successful early stop); returning true asks for the next split. -typedef std::function split_yield; - class seq_split { ast_manager& m; seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access @@ -132,6 +127,7 @@ class seq_split { expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold, split_oracle const& oracle, bool& ok); // Fully drain a suspended split-set into `out` (used for inter/compl bodies). + // Runs an `iterator` to exhaustion; returns false on a give-up. bool materialize(expr* node, split_mode mode, unsigned threshold, split_oracle const& oracle, split_set& out); @@ -155,30 +151,59 @@ class seq_split { public: explicit seq_split(seq_rewriter& rw); - // Build the *suspended* sigma(r) as a split-algebra term (no expansion). - // Returns null on a non-regex argument. Drive it with `enumerate`. - expr_ref make(expr* r); - - // Lazily expand a suspended split-set, invoking `yield` for every concrete - // split . The threshold is supplied by the caller and serves only as a - // safety cap against space bloat (lazy expansion still has to materialize the - // operands of intersection / complement). An overrun, an unsupported regex - // shape, or a Boolean-closure case in weak mode makes it return false ("give - // up"). `yield` returning false stops early and is reported as success. + // Lazy split enumerator. Holds the suspended split-set worklist and produces + // the concrete splits one at a time, on demand, instead of computing + // them all up front. Obtain one from seq_split::iterate (or construct it + // directly) and pull splits with next() until it returns false; gave_up() then + // tells a normal exhaustion (false) apart from a give-up (true). // - // `oracle` (optional) prunes non-viable splits as they are yielded. It must + // The threshold is supplied by the caller and serves only as a safety cap + // against space bloat (lazy expansion still has to materialize the operands of + // intersection / complement). A threshold overrun, an unsupported regex shape, + // or a Boolean-closure case in weak mode aborts the enumeration: next() returns + // false and gave_up() returns true. To stop early, simply stop calling next(). + // + // `oracle` (optional) prunes non-viable splits as they are produced. It must // be sound to apply per split: a candidate N can still gain a prefix from a // factor appended to its right later (concat/star), so the oracle must use a // "prefix-compatible" test (prune only when N can never match the lookahead, // even partially), NOT a strict "starts-with" test. The complement body is // expanded WITHOUT the oracle (inverted orientation); the oracle is re-applied // to the complement's output fold. - bool enumerate(expr* node, split_mode mode, unsigned threshold, - split_oracle const& oracle, split_yield const& yield); + class iterator { + seq_split& m_engine; + ast_manager& m; + split_mode m_mode; + unsigned m_threshold; + split_oracle m_oracle; + expr_ref_vector m_work; // GC-safe worklist of suspended split-sets + unsigned m_count = 0; // splits produced so far (vs. threshold) + bool m_giveup = false; + public: + iterator(seq_split& engine, expr* node, split_mode mode, + unsigned threshold, split_oracle oracle); + // Compute the next split. On success returns true and sets ; on + // exhaustion or give-up returns false (see gave_up()). Calling next() + // again after it has returned false keeps returning false. + bool next(expr_ref& d, expr_ref& n); + // Valid after next() has returned false: true iff the enumeration aborted + // (unsupported regex / weak-mode Boolean / threshold overrun) rather than + // running out of splits. + bool gave_up() const { return m_giveup; } + }; + + // Build the *suspended* sigma(r) as a split-algebra term (no expansion). + // Returns null on a non-regex argument. Drive it with `iterate`. + expr_ref make(expr* r); + + // Create a lazy enumerator over a suspended split-set `node` (typically the + // result of make()). See `iterator` for the meaning of the arguments. + iterator iterate(expr* node, split_mode mode, unsigned threshold, + split_oracle const& oracle = {}); // Compute sigma(r), appending to `out` (does not clear it). Thin eager - // wrapper that drains `enumerate`; semantics match the historic engine. See - // `enumerate` for the meaning of `threshold`, `mode`, and `oracle`. + // wrapper that drains an `iterator` to exhaustion; semantics match the historic + // engine. See `iterator` for the meaning of `threshold`, `mode`, and `oracle`. bool compute(expr* r, split_set& out, unsigned threshold, split_mode mode = split_mode::strong, split_oracle const& oracle = {}); diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp index 229ec98664..29df0545c7 100644 --- a/src/test/seq_split.cpp +++ b/src/test/seq_split.cpp @@ -68,8 +68,11 @@ class seq_split_test { split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { expr_ref node = m_split.make(r); ENSURE(node); - return m_split.enumerate(node, mode, threshold, oracle, - [&](expr* d, expr* n) { out.push_back(split_pair(d, n, m)); return true; }); + seq_split::iterator it = m_split.iterate(node, mode, threshold, oracle); + expr_ref d(m), n(m); + while (it.next(d, n)) + out.push_back(split_pair(d, n, m)); + return !it.gave_up(); } // assert that the eager and lazy engines agree on sigma(r) as a *set* of @@ -154,16 +157,18 @@ public: } void test_lazy_early_stop() { - // a* has 3 splits; stop after the first one. (Note .* is the full_seq - // special case with a single split, so use a proper char-class body.) + // a* has 3 splits; pull just the first one and then stop. (Note .* is the + // full_seq special case with a single split, so use a proper char-class body.) expr_ref star(re().mk_star(rng('a', 'a')), m); expr_ref node = m_split.make(star); ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); unsigned seen = 0; - bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, - [&](expr*, expr*) { ++seen; return false; /* stop now */ }); - ENSURE(ok); // early stop is reported as success - ENSURE(seen == 1); // and nothing was produced past the stop + if (it.next(d, n)) // pull exactly one split, then walk away + ++seen; + ENSURE(!it.gave_up()); // stopping early is not a give-up + ENSURE(seen == 1); } void test_threshold_giveup() { @@ -331,13 +336,55 @@ public: expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits expr_ref node = m_split.make(as); ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); unsigned seen = 0; - bool ok = m_split.enumerate(node, split_mode::strong, UINT_MAX, {}, - [&](expr*, expr*) { ++seen; return seen < 2; }); - ENSURE(ok); + while (seen < 2 && it.next(d, n)) // pull two splits on demand, then stop + ++seen; + ENSURE(!it.gave_up()); ENSURE(seen == 2); } + void test_iterator_exhaustion() { + // Pull every split on demand; gave_up() must stay false on a clean + // exhaustion, and next() must keep returning false once drained. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits + expr_ref node = m_split.make(as); + ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {}); + expr_ref d(m), n(m); + unsigned seen = 0; + while (it.next(d, n)) + ++seen; + ENSURE(seen == 3); + ENSURE(!it.gave_up()); + // idempotent past the end + ENSURE(!it.next(d, n)); + ENSURE(!it.gave_up()); + } + + void test_iterator_giveup() { + // A threshold overrun aborts: next() returns false and gave_up() is true. + expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1 + expr_ref node = m_split.make(as); + ENSURE(node); + seq_split::iterator it = m_split.iterate(node, split_mode::strong, /*threshold*/ 1, {}); + expr_ref d(m), n(m); + unsigned seen = 0; + while (it.next(d, n)) + ++seen; + ENSURE(it.gave_up()); // aborted, not a clean exhaustion + ENSURE(seen <= 1); // produced at most the capped number + + // A weak-mode Boolean closure is likewise a give-up. + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); + expr_ref inode = m_split.make(inter); + ENSURE(inode); + seq_split::iterator wit = m_split.iterate(inode, split_mode::weak, UINT_MAX, {}); + ENSURE(!wit.next(d, n)); + ENSURE(wit.gave_up()); + } + void test_simplify() { expr_ref regs[] = { expr_ref(re().mk_star(rng('a', 'a')), m), @@ -390,6 +437,8 @@ public: test_determinism(); test_threshold_boundary(); test_early_stop_after_two(); + test_iterator_exhaustion(); + test_iterator_giveup(); test_simplify(); test_trivial_oracle(); }