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

seq_monadic_bench: model negated memberships instead of dropping them (#10399)

Browse source 
The benchmark harness in `seq_monadic_bench` only recognized positive
`(str.in_re t R)` assertions. Everything else it could not model was
dropped, counted in `dropped`, and cleared the `complete` flag.

A negated membership `(not (str.in_re t R))` is just a membership in the
complement. `seq_monadic` handles `re.comp` natively, and
`seq_regex::unfold_complement` performs exactly this rewrite on the
production path, so dropping it made the benchmark measure a strictly
weaker problem than the solver actually sees. Length constraints already
handled negation through `collect_len`'s `sign` parameter; this closes
the same gap for memberships.

### Effect

Full regex corpus (1476 files, `light-ant` mode, 20s timeout):

| metric | before | after |
|---|---|---|
| decided | 1396 | 1396 |
| **complete (all assertions modelled)** | 1384 | **1411** |
| files with dropped assertions | 90 | 63 |
| dropped assertions | 134 | 107 |
| sum of solve times | 181.3s | 165.6s |

No verdict changes on any of the 1476 files, and no measurable cost.
27 files that previously reported an unfaithful, weakened problem are
now
modelled exactly.

### What is still dropped

For reference, the remaining 107 drops across 63 files are:

| category | drops | files | example |
|---|---|---|---|
| word equations | 86 | 52 | `(= (str.++ x y) (str.++ y x))` |
| integer-variable guards | 8 | 7 | `(>= k 0)` |
| relational length | 8 | 6 | `(= (str.len x) (+ (str.len y) 1))` |
| modular length | 7 | 6 | `(= (str.len x) (* 2 k))` |

Word equations are genuinely outside a monadic decomposition and are
expected to stay dropped. The modular-length group is monadic in
disguise -- `|x| = 2k ∧ k >= 0` is exactly `x in (..)*` -- and encoding
it
as a regex loop would make 5 further files complete. That is left for a
follow-up.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2

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-04 19:56:42 -07:00 • committed by GitHub
parent 0d1e935327
commit 227238cc0c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/test/seq_monadic_bench.cpp
View file

@ -188,7 +188,15 @@ lbool run_file(
collect(arg);
return;
}
if (!u.str.is_in_re(e, s, r)) {
// A negated membership is a membership in the complement. seq_monadic handles
// re.comp natively and seq_regex::unfold_complement performs the same rewrite on
// the production path, so modelling it here rather than dropping it keeps the
// benchmark faithful to what the solver actually sees.
bool negated = false;
expr* arg = nullptr;
if (m.is_not(e, arg) && u.str.is_in_re(arg, s, r))
negated = true;
else if (!u.str.is_in_re(e, s, r)) {
if (!collect_len(e, false))
complete = false, ++dropped;
return;
@ -202,7 +210,7 @@ lbool run_file(
// Normalize the regex the way asserted_formulas normalizes assertions
// before seq_regex hands them to seq_monadic. Without this the bench
// measures raw parsed regexes, which no production path ever sees.
expr_ref normalized(r, m);
expr_ref normalized(negated ? u.re.mk_complement(r) : r, m);
trw(normalized);
pin.push_back(normalized);
r = normalized;