From f96e37753d6e3064d81b68ddee9e3ec4001f58ab Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Tue, 4 Aug 2026 15:04:00 -0700 Subject: [PATCH] Prune seq_monadic product states that can no longer reach their goal (#10386) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2 --- src/ast/rewriter/seq_monadic.cpp | 107 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_monadic.h | 37 +++++++++++ 2 files changed, 144 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 1843aa66b6..9af4e1ea85 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -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 const& comps, expr_ref* witness_word) { unsigned n = comps.size(); if (n == 0) { @@ -228,6 +304,29 @@ lbool seq_monadic::product_nonempty(svector 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 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 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) { diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 93b743301f..f30adda3db 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -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 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 m_der_cache; // memoizes der_elem per (regex, element) obj_map 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(); }