mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00
Code Activity

Prune seq_monadic product states that can no longer reach their goal (#10386)

Browse source 
Answers Nikolaj's question on #10384: *"is a cheap non-reachability
check possible and beneficial? When we explore (R, Q) we take
derivatives of R and check if Q is reached. Do we ensure that the
current derivative can always reach Q?"*

**We did not.** `product_nonempty` tests each popped state for
acceptance — for a component with a target that means syntactic equality
with the target — but nothing checked that the target was still
reachable. The only pruning was empty-guard, `is_empty`, and `visited`;
`reachable_live` enforces liveness toward *acceptance*, never toward the
specific goal Q.

## How much is wasted

Measured with an exact oracle (materialize `reachable_live` per source
state and test goal membership), on ClemensRegex/generated:

| mode | product states expanded | provably cannot reach their goal |
|---|---|---|
| brz | 10.40M | 7.17M (**68.9%**) |
| light-ant | 9.95M | 6.21M (**62.4%**) |

## The check

Some features can be *inherited* by a derivative but never *created* by
one:

- the **characters** of a string literal — `d(to_re("bc")) =
to_re("c")`;
- the **body** of a star or bounded loop — `d(r*) = d(r)·r*` and
`d(r{k,l}) = d(r)·r{k-1,l-1}` keep `r` verbatim. Note the loop *node* is
not preserved, so the body is the atom.

Hashing these into a 256-bit Bloom filter gives `atoms(d_a(t)) ⊆
atoms(t)`, hence `atoms(d_w(t)) ⊆ atoms(t)` for every word `w`. If the
goal's atoms are not contained in the state's, the goal is unreachable.

Two things are needed for soundness, both found by dumping
counterexamples rather than by reasoning:

1. **The abstraction must be directional.** The test is `under(goal) ⊆
over(source)`; an unmodelled construct contributes everything to `over`
and nothing to `under`. Saturating both sides makes an unmodelled *goal*
look unreachable. Getting this wrong produced 751k false prunes.
2. **Normalization synthesizes nodes.** `mk_re_complement` turns
`comp(ε)` into `(re.+ re.allchar)`, so `re.allchar` appears in
derivatives of terms that never mentioned it. `re.allchar`,
`re.full_seq`, `ε`, `∅` are therefore excluded from the
under-approximation.

The check runs **before the nullability bail**, so a state that cannot
reach its goal no longer aborts the entire search with `l_undef` merely
because its nullability is undecidable. That is where the newly decided
benchmarks come from.

## Results

Full regex corpus, 1545 files, two repetitions, same binary with the
filter on and off:

| mode | decided | solve time |
|---|---|---|
| brz | 1472 → 1472 | 26.1s → 15.4s (**−41%**) |
| light-ant | 1469 → **1473** | 13.6s → 8.6s (**−37%**) |

Newly decided (all four agree with their expected status):
`split_membership_easy_unsat_0006` undef→unsat,
`split_membership_medium_sat_0003` undef→sat,
`split_membership_medium_sat_0053` timeout→sat,
`split_membership_medium_unsat_0058` undef→unsat.

**Soundness checks:** across all runs, 0 benchmarks changed sat↔unsat, 0
lost a verdict, and 0 disagreed with their expected status. Baseline brz
variance also drops sharply (31.6s/20.6s across reps → 15.7s/15.2s).

So the honest summary is: on this corpus the check converts mostly into
**speed**, and only marginally into **completeness** (+4 files,
light-ant only).

## What did not work

I also evaluated the "relevant alphabet" `A_R` — a `range_predicate` per
node with `A_{R|S} = A_R ∪ A_S`, `A_{R&S} = A_R ∩ A_S`, `A_{RS} = A_R ∪
A_S`, `A_{R*} = A_R`, `A_{~R} = ⊤` plus the `~(.*p.*) = (^p)*` rewrite
for a single character `p`. It is sound (0 false positives once the `∩`
rule and the directional discipline are in place) but its unique
contribution over the atom check is **0.6% of dead states in brz and
2.8% in light-ant**, because the atom check already carries one atom per
literal character. Its only extra power is interval-subset reasoning on
`re.range` leaves. Not worth the machinery, so it is not in this PR.

## Notes

- Stacked on #10384 → #10381. Please merge those first.
- 94/94 unit tests pass.
- The one residual soundness caveat worth recording: `mk_re_star`
rewrites `(b*|c)* → (b|c)*`, which synthesizes a *fresh* loop body. That
fires when a star is **constructed**, not during derivation (`δ(r*)`
reuses the existing node), so the lemma holds — but it is the place to
look first if a false prune ever shows up.

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Margus Veanes 2026-08-04 15:04:00 -07:00 • committed by Margus Veanes
parent 57ddf8e7bf
commit f96e37753d
2 changed files with 144 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

107
src/ast/rewriter/seq_monadic.cpp
View file

@ -189,6 +189,82 @@ seq_monadic::ivl_list const* seq_monadic::interval_cofactors(expr* r, expr* v0)
return res;
}
void seq_monadic::reset_atom_cache() {
m_atom_cache.reset();
m_atom_pin.reset();
}
// See atom_sig in the header for what the abstraction computes and why it is sound.
void seq_monadic::compute_atoms(expr* t, atom_sigs& out, unsigned depth) {
auto const& re = u().re;
// An unmodelled construct may hide anything, so it saturates the over-approximation
// and leaves the under-approximation empty.
auto unknown = [&]() { out.over.saturate(); };
if (depth > 200) { unknown(); return; }
expr* a = nullptr, *b = nullptr, *c = nullptr;
unsigned lo = 0, hi = 0;
auto rec = [&](expr* e) {
atom_sigs s;
compute_atoms(e, s, depth + 1);
out.under |= s.under;
out.over |= s.over;
};
auto chr = [&](unsigned ch) { out.under.add(ch); out.over.add(ch); };
// Some nodes are synthesized by normalization rather than inherited: the rewriter
// turns comp(eps) into (re.+ re.allchar), so re.allchar can appear in a derivative of
// a term that never mentioned it. Such nodes must not gate the under-approximation.
auto is_free = [&](expr* e) {
return re.is_full_char(e) || re.is_full_seq(e) || re.is_epsilon(e) || re.is_empty(e);
};
auto node = [&](expr* e) {
uint64_t h = 0x9E3779B9ull ^ e->get_id();
out.over.add(h);
if (!is_free(e))
out.under.add(h);
};
if (m.is_ite(t, c, a, b)) { rec(a); rec(b); return; } // guards are freshly built predicates
if (re.is_concat(t, a, b) || re.is_union(t, a, b) ||
re.is_intersection(t, a, b) || re.is_diff(t, a, b)) { rec(a); rec(b); return; }
if (re.is_complement(t, a) || re.is_opt(t, a) || re.is_reverse(t, a)) { rec(a); return; }
if (re.is_star(t, a) || re.is_plus(t, a) ||
re.is_loop(t, a, lo, hi) || re.is_loop(t, a, lo)) {
node(a); // the body survives derivation
rec(a);
return;
}
if (re.is_empty(t) || re.is_epsilon(t) || re.is_full_seq(t))
return;
if (re.is_full_char(t)) { node(t); return; }
if (re.is_range(t, a, b)) {
unsigned cl = 0, ch = 0;
if (!u().is_const_char(a, cl) || !u().is_const_char(b, ch)) { unknown(); return; }
node(t);
return;
}
// A string literal is not itself an atom: d(to_re("bc")) = to_re("c") is a fresh node.
// Its characters are, and they can only be dropped by a derivative, never added.
if (re.is_to_re(t, a)) {
zstring s;
if (!u().str.is_string(a, s)) { unknown(); return; }
for (unsigned i = 0; i < s.length(); ++i)
chr(s[i]);
return;
}
if (re.is_of_pred(t, a)) { node(t); return; }
unknown();
}
seq_monadic::atom_sigs seq_monadic::atoms_of(expr* t) {
atom_sigs s;
if (m_atom_cache.find(t, s))
return s;
compute_atoms(t, s, 0);
m_atom_pin.push_back(t); // keep the key alive for the cache's lifetime
m_atom_cache.insert(t, s);
return s;
}
lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* witness_word) {
unsigned n = comps.size();
if (n == 0) {
@ -228,6 +304,29 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
};
bool undecided = false;
// Goal signatures are fixed for the whole search, so they are computed once here.
// A component without a goal accepts by nullability and cannot be filtered this way.
svector<atom_sig> goal_atoms;
bool has_goal = false;
goal_atoms.resize(n);
for (unsigned i = 0; i < n; ++i)
if (comps[i].target) {
goal_atoms[i] = atoms_of(comps[i].target).under;
has_goal = true;
}
// A state from which some component can no longer reach its goal is not on any path
// to acceptance. Filtering these is what keeps the search from expanding, on this
// corpus, roughly half of the product states it otherwise visits.
auto cannot_reach_goal = [&]() -> bool {
if (!has_goal)
return false;
for (unsigned i = 0; i < n; ++i)
if (comps[i].target && st[i] != comps[i].target &&
!goal_atoms[i].subset_of(atoms_of(st[i]).over))
return true;
return false;
};
auto is_accept = [&]() -> bool {
for (unsigned i = 0; i < n; ++i) {
if (comps[i].target) {
@ -421,6 +520,13 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
*witness_word = reconstruct(fill_key(st));
return l_true;
}
// Checked before the nullability bail on purpose: a state that cannot reach its
// goal is irrelevant, so an undecidable nullability in it must not abort the
// whole search. `undecided` is reset because it only concerned this state.
if (cannot_reach_goal()) {
undecided = false;
continue;
}
if (undecided) {
m_stats.inc_bail(bail_reason::nullability);
return l_undef;
@ -494,6 +600,7 @@ void seq_monadic::reset_search() {
m_nullable_cache.reset();
m_undef_vars = 0;
m_live_states.reset();
reset_atom_cache();
}
bool seq_monadic::prepare(membership_vec const& memberships) {

37
src/ast/rewriter/seq_monadic.h
View file

@ -128,6 +128,42 @@ class seq_monadic {
expr_ref_vector m_ivl_pin; // pins the states and targets the cache refers to
ivl_list const* interval_cofactors(expr* r, expr* v0);
void reset_ivl_cache();
// Goal-directed reachability filter. Certain syntactic features of a regex can be
// inherited by a derivative but never created by one: the characters of a string
// literal (d(to_re("bc")) = to_re("c")) and the body of a star or bounded loop
// (d(r*) = d(r)r* and d(r{k,l}) = d(r)r{k-1,l-1} both keep r verbatim). Hashing
// those features into a Bloom filter gives, for every regex t, a set atoms(t) with
// atoms(d_a(t)) subset-of atoms(t) for every character a,
// hence atoms(d_w(t)) subset-of atoms(t) for every word w. So if the atoms of a goal
// state are not contained in those of the current state, no sequence of derivatives
// can turn one into the other and the goal is unreachable.
//
// The abstraction must be directional, because constructs it does not model have to
// be approximated in opposite directions on the two sides: the test is
// under(goal) subset-of over(source), so an unmodelled construct contributes
// everything to `over` and nothing to `under`. Saturating both would make an
// unmodelled goal look unreachable and prune a live state.
struct atom_sig {
uint64_t w[4] = { 0, 0, 0, 0 };
void operator|=(atom_sig const& o) { for (unsigned i = 0; i < 4; ++i) w[i] |= o.w[i]; }
void add(uint64_t h) {
h *= 1099511628211ull;
w[(h >> 58) & 3] |= 1ull << ((h >> 6) & 63);
}
void saturate() { for (unsigned i = 0; i < 4; ++i) w[i] = ~0ull; }
bool subset_of(atom_sig const& o) const {
for (unsigned i = 0; i < 4; ++i)
if (w[i] & ~o.w[i]) return false;
return true;
}
};
struct atom_sigs { atom_sig under, over; };
obj_map<expr, atom_sigs> m_atom_cache;
expr_ref_vector m_atom_pin; // pins the keys of m_atom_cache
void compute_atoms(expr* t, atom_sigs& out, unsigned depth);
atom_sigs atoms_of(expr* t);
void reset_atom_cache();
obj_pair_map<expr, expr, expr*> m_der_cache; // memoizes der_elem per (regex, element)
obj_map<expr, char> m_nullable_cache; // memoizes nullability (0 false / 1 true / 2 unknown);
// seq_rewriter's own cache is capped and flushed whole
@ -251,6 +287,7 @@ public:
seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) :
m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail),
m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), m_ivl_pin(rw.m()),
m_atom_pin(rw.m()),
m_regexes(rw.m()), m_live_states(rw, mode, 1u << 12) {}
~seq_monadic() { reset_ivl_cache(); }