mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-18 21:15:47 +00:00
Code Activity

Put it into an iterator

Browse source
This commit is contained in:
CEisenhofer 2026-06-30 12:36:18 +02:00
parent a88dfa64ac
commit b5ec0889bd
3 changed files with 154 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

76
src/ast/rewriter/seq_split.cpp
View file

@ -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):

65
src/ast/rewriter/seq_split.h
View file

@ -57,11 +57,6 @@ enum class split_mode { weak, strong };
// default) keeps everything, so sigma is unchanged. See seq_split::compute.
typedef std::function<bool(expr* D, expr* N)> split_oracle;
// Callback invoked by seq_split::enumerate for each concrete split <D, N> 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<bool(expr* D, expr* N)> 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 <D, N>. 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 <D, N> 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 <d, n>; 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 = {});