mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 22:42:20 +00:00
Code Activity

Harden the seq_monadic goal-atom prune against rewriter changes

Browse source 
The goal-directed prune added in #10386 discards a product state when the
`under` atoms of a component's goal are not contained in the `over` atoms of
the current state.  This is sound only because atoms are *inherited* by
derivatives and never *created* by them:

    under(d_a(t)) subset-of over(t)

for every character a, and hence under(goal) subset-of over(source) for any
reachable goal.  A rewrite that synthesizes a fresh non-free node inside a
derivative breaks the invariant, and the failure mode is a silent wrong
`unsat` -- no crash, no warning.

Two changes:

1. A range is no longer treated as an atom.  Intersection narrows [a,b] & [c,d]
   to a freshly built sub-range in mk_regex_inter_normalize, so a derivative can
   contain a range that no ancestor did:

       d(inter([a-f][a-f], [d-z][d-z])) = inter([a-f], [d-z]) = [d-f]

   The previous code hashed a range by node id whenever both endpoints were
   const chars.  That branch was in practice dead -- re.range endpoints are
   `seq.unit (Char c)` rather than raw Char, so is_const_char fails and the
   range already saturated -- which is why an audit over 2676 benchmarks is
   clean.  Making the endpoint test succeed reintroduces the bug: with the
   precise test forced on, the two fresh-range probes produce 2 and 12
   invariant violations respectively.  The branch is now unconditionally
   saturating, with a comment explaining why it must not be "optimized" back.

2. A debug-only assertion checks the invariant on every product transition, on
   both the interval-sweep and the cartesian paths, so a future rewriter change
   trips a debug test rather than a user's benchmark.

Behaviour is unchanged: over 1476 regex benchmarks both configurations decide
the same 1378 instances with no disagreements and no :status contradictions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Margus Veanes 2026-08-07 01:37:24 -07:00
parent f96e37753d
commit 754c4243e6
1 changed files with 34 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -236,12 +236,16 @@ void seq_monadic::compute_atoms(expr* t, atom_sigs& out, unsigned depth) {
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 range is NOT an atom. Intersection narrows [a,b] & [c,d] to a freshly built
// sub-range (mk_regex_inter_normalize, seq_rewriter.cpp), so a derivative can contain
// a range that no ancestor did:
// d(inter([a-f][a-f], [d-z][d-z])) = inter([a-f], [d-z]) = [d-f]
// Hashing it by node id would put a fresh id into `under` and break
// under(d_w(t)) subset-of over(t), whose failure mode is a silent wrong `unsat`.
// Saturating `over` and contributing nothing to `under` is the only sound treatment.
// Do not "optimize" this into node(t): an audit over 2676 benchmarks is clean only
// because this branch never treats a range as an atom.
if (re.is_range(t)) { unknown(); 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)) {
@ -327,6 +331,28 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
return false;
};
// Debug-only guard on the property `cannot_reach_goal` above depends on.
//
// The prune is sound because the atoms an `under` signature can contain are
// *inherited* by derivatives and never *created* by them, giving
// under(delta_a(t)) subset-of over(t)
// on every edge and hence under(goal) subset-of over(source) for any reachable
// goal. A rewrite that synthesizes a fresh non-free node in a derivative breaks
// this, and the failure mode is a silent wrong `unsat` -- no crash, no warning.
// Character classes are the live risk here: seq_range_collapse materializes a
// collapsed class as a *freshly built* node (see the range comment in
// compute_atoms), so it must keep materializing into a kind that compute_atoms
// does not treat as an atom. Switching it to emit re.of_pred, for instance,
// would put a fresh id into `under` and make this assertion fail.
//
// Checked on every transition, in both the sweep and the product paths, so that a
// future rewriter change trips a debug test rather than a user's benchmark.
[[maybe_unused]] auto check_atom_monotone = [&](ptr_vector<expr> const& succ) {
for (unsigned i = 0; i < n; ++i)
SASSERT(succ[i] == st[i] || re().is_empty(succ[i]) ||
atoms_of(succ[i]).under.subset_of(atoms_of(st[i]).over));
};
auto is_accept = [&]() -> bool {
for (unsigned i = 0; i < n; ++i) {
if (comps[i].target) {
@ -438,6 +464,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
cur[i] = sw_lists[i]->targets[r.first + sw_odo[i]];
}
key const& ck = fill_key(cur);
DEBUG_CODE(check_atom_monotone(cur););
if (visited.find(ck) == visited.end()) {
visited.insert(ck);
if (witness_word) {
@ -468,6 +495,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
if (bail) return;
if (i == n) {
key const& ck = fill_key(cur);
DEBUG_CODE(check_atom_monotone(cur););
if (visited.find(ck) == visited.end()) {
visited.insert(ck);
if (witness_word) {