mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Bug fixes in the regex factoring

Browse source
This commit is contained in:
Clemens Eisenhofer 2026-07-10 20:15:48 +02:00
parent fa93f20d2e
commit 2b48f7dc23
2 changed files with 80 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -244,7 +244,7 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul
// 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) {
expr_ref seq_split::expand_fromre(expr* r, unsigned threshold, bool& ok) {
ok = true;
seq_util& sq = seq();
seq_util::rex& rex = re();
@ -290,8 +290,8 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
continue;
}
zstring str2;
if (sq.str.is_string(s, str2)) {
str = str2;
if (sq.str.is_string(cur, str2)) {
str += str2;
continue;
}
// not a constant string; unsupported for now
@ -410,6 +410,14 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
// j in [l,h] with j > i, into a single loop [<eps,eps> 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);
@ -425,7 +433,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
return acc;
}
// bounded loop / ite / other: not handled (paper "v1: bail").
// 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);
@ -476,7 +484,7 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold,
// 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);
expr_ref e = expand_fromre(r, threshold, ok);
if (!ok)
return expr_ref(m);
if (is_frontier(e))
@ -531,7 +539,12 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold,
return from_split_set(res);
}
UNREACHABLE();
// 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);
}
@ -675,9 +688,10 @@ void seq_split::simplify(split_set& pairs) const {
// 3. subsumption: drop <D_i,N_i> when L(D_i) subseteq L(D_j) and
// L(N_i) subseteq L(N_j) for some kept j. seq_subset is conservative
// (returns true only for definite containment), so we never drop a
// needed split.
//if (pairs.size() > 64)
// return;
// 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<row> rows;
@ -757,25 +771,51 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
// TODO: Do this for the back as well (also, why did no rule before do that?)
if (tokens.empty())
return { expr_ref(m), expr_ref(m) };
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 <eps, regex> 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.
// 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;
unsigned run_start = 0, run_len = 0, run_chars = 0;
for (i = 1; i < total; ) {
if (!(seq().str.is_unit(tokens.get(i), ch) && seq().is_const_char(ch))) {
unsigned chars = 0, block_chars = 0;
if (!token_chars(tokens.get(i), chars)) {
i++;
continue;
}
unsigned j = i;
while (j < total && seq().str.is_unit(tokens.get(j), ch) && seq().is_const_char(ch)) {
while (j < total && token_chars(tokens.get(j), chars)) {
block_chars += chars;
j++;
}
if (j - i > run_len) {
if (block_chars > run_chars) {
run_chars = block_chars;
run_len = j - i;
run_start = i;
}
@ -801,8 +841,14 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
// 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(tokens.get(run_start + i), ch));
VERIFY(seq().str.is_unit(t, ch));
VERIFY(seq().is_const_char(ch, cv));
c = c + zstring(cv);
}

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

@ -86,6 +86,9 @@ class seq_split {
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
@ -112,8 +115,10 @@ class seq_split {
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);
// 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);
// 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);
@ -160,8 +165,9 @@ public:
// 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().
// 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
@ -212,7 +218,13 @@ public:
// seq_subset). Size-capped to keep the O(n^2) subsumption affordable.
void simplify(split_set& s) const;
// decompose a membership constraint into a set of pairs of regex splits
// 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 <D, N> 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 <eps, derivative-consumed regex>.
std::pair<expr_ref, expr_ref> split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const;
// Lookahead oracle for the split engine: is the split's right component