mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

guard_set: cache guard -> range predicate translation (#10361)

Browse source 
`guard_set::conjoin` re-translated its guard expression into a
`seq::range_predicate` on every call. It sits in the innermost loop of
`seq_monadic::product_nonempty`'s product-transition enumeration, where
the same handful of cofactor guards recurs on every branch of the
product search — a single regex benchmark was measured at **4.4M
translations of a few dozen distinct guards**.

## Change

Add an optional `guard -> range_predicate` cache to `guard_set`. It is
owned by the caller so its lifetime can be tied to the lifetime of the
guard expressions themselves; `seq_monadic` keys it off
`m_cofactor_cache` (which owns the guards) and resets both together. A
null cache entry records an unsupported guard, preserving the `m_ok =
false` behaviour without retranslating.

The cache is used only on the character-sort path, and is valid only
while every `guard_set` sharing it uses the same element variable `v0`.
That holds in `seq_monadic`: `v0` is `m.mk_var(0, m_elem_sort)`, which
is hash-consed, and the element sort is fixed for the duration of a
solve. The parameter defaults to `nullptr`, so any other caller keeps
the previous behaviour unchanged.

No behavioural change.

## Validation

`test-z3 seq_monadic`: ALL PASS (0 fail) in both `brz` and `light-ant`
modes.

1545-file regex corpus (`light-ant`, 20s timeout per file):

| | master | this PR |
|---|---|---|
| sat / unsat / undef | 1166 / 255 / 121 | 1166 / 255 / 121 |
| timeouts | 3 | 2 |
| solve time, 1421 files decided by both | 74.7 s | **8.4 s (~9x)** |

Verdicts are identical to master on every file; one benchmark that
previously hit the 20s timeout now terminates.

Full QF_S corpus (22,172 files) on the follow-up branch that builds on
this one: 0 crashes, 0 timeouts, and on the 4,089 benchmarks where the
monadic solver is complete and the expected status is known, 0
mismatches against the declared status.

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-02 11:26:50 -07:00 • committed by GitHub
parent 05321fbe0f
commit 690c5a4c22
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 49 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -80,6 +80,7 @@ void seq_monadic::reset_cofactor_cache() {
for (auto const& [k, v] : m_cofactor_cache)
dealloc(v);
m_cofactor_cache.reset();
guard_set::dealloc_cache(m_rp_cache); // the guards live in the cofactor vectors
}
bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
@ -252,7 +253,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
if (bail) return;
}
};
guard_set top(m, u(), m_elem_sort, var0);
guard_set top(m, u(), m_elem_sort, var0, &m_rp_cache);
rec(0, top);
if (bail)
return l_undef;