From 690c5a4c22ce9dd8adf4b8351852233def20b685 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sun, 2 Aug 2026 11:26:50 -0700 Subject: [PATCH] guard_set: cache guard -> range predicate translation (#10361) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- src/ast/rewriter/guard_set.cpp | 40 +++++++++++++++++++++++++------- src/ast/rewriter/guard_set.h | 12 +++++++++- src/ast/rewriter/seq_monadic.cpp | 3 ++- src/ast/rewriter/seq_monadic.h | 4 ++++ 4 files changed, 49 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/guard_set.cpp b/src/ast/rewriter/guard_set.cpp index 5bdbe40398..4cfe52e3da 100644 --- a/src/ast/rewriter/guard_set.cpp +++ b/src/ast/rewriter/guard_set.cpp @@ -19,14 +19,21 @@ Author: #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" -guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0) +guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, + rp_cache* cache) : m(_m), u(_u), m_sort(elem_sort), m_v0(v0), - m_is_char(_u.is_char(elem_sort)), + m_is_char(_u.is_char(elem_sort)), m_rp_cache(cache), m_rp(_u.max_char()), m_guard(_m) { if (m_is_char) m_rp = seq::range_predicate::top(u.max_char()); else m_guard = m.mk_true(); } +void guard_set::dealloc_cache(rp_cache& c) { + for (auto const& [k, v] : c) + dealloc(v); + c.reset(); +} + void guard_set::collect_consts(expr* g, ptr_vector& out) const { expr* a = nullptr, * b = nullptr; if (m.is_and(g) || m.is_or(g)) { @@ -132,13 +139,30 @@ lbool guard_set::generic_eval(expr_ref* witness) const { void guard_set::conjoin(expr* g) { if (!m_ok) return; - if (m_is_char) { - seq::range_predicate s(u.max_char()); - if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; } - m_rp = m_rp & s; - } - else + if (!m_is_char) { m_guard = m.mk_and(m_guard, g); + return; + } + if (m_rp_cache) { + // Translating a guard expression into a range predicate is the inner loop of the + // product-transition enumeration; the same handful of guards recurs on every + // branch, so translate each one once. + seq::range_predicate* s = nullptr; + if (!m_rp_cache->find(g, s)) { + s = alloc(seq::range_predicate, u.max_char()); + if (!seq::guard_to_range_predicate(u, m_v0, g, *s)) { + dealloc(s); + s = nullptr; + } + m_rp_cache->insert(g, s); + } + if (!s) { m_ok = false; return; } + m_rp = m_rp & *s; + return; + } + seq::range_predicate s(u.max_char()); + if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; } + m_rp = m_rp & s; } lbool guard_set::eval(expr_ref* witness) const { diff --git a/src/ast/rewriter/guard_set.h b/src/ast/rewriter/guard_set.h index f15f582ac7..18bb71b998 100644 --- a/src/ast/rewriter/guard_set.h +++ b/src/ast/rewriter/guard_set.h @@ -31,12 +31,21 @@ Author: #include "ast/rewriter/seq_range_collapse.h" class guard_set { +public: + // Cache of guard expression -> its range predicate (null value: unsupported guard). + // Only meaningful for the character sort, and only valid while every guard_set sharing + // it uses the same element variable v0 (v0 is hash-consed per element sort). + typedef obj_map rp_cache; + static void dealloc_cache(rp_cache& c); + +private: ast_manager& m; seq_util& u; sort* m_sort; expr* m_v0; bool m_is_char; bool m_ok = true; // false: an unsupported guard was conjoined + rp_cache* m_rp_cache = nullptr; seq::range_predicate m_rp; // char representation expr_ref m_guard; // generic representation (conjunction over v0) @@ -54,7 +63,8 @@ class guard_set { lbool generic_eval(expr_ref* witness) const; public: - guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0); + guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, + rp_cache* cache = nullptr); bool ok() const { return m_ok; } diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 72332cf2de..0abf3f0135 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -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 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; diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 87b3a09a26..ed5cdefe48 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -54,6 +54,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_range_predicate.h" +#include "ast/rewriter/guard_set.h" #include "ast/rewriter/th_rewriter.h" #include "util/lbool.h" #include "util/obj_hashtable.h" @@ -85,6 +86,9 @@ private: bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) obj_map m_model; // last extracted model (var -> witness); see get_model() obj_map m_cofactor_cache; // memoizes derivative_cofactors per regex + guard_set::rp_cache m_rp_cache; // cofactor guard -> range predicate; the guards + // are owned by m_cofactor_cache, so both are + // reset together using membership_vec = vector>; membership_vec m_memberships; // asserted (term in regex, dep) for check() ptr_vector m_core; // dependencies of an unsat subset, filled by check() on l_false