From ddfd4030138d66b25e05eb8f139f83c5b7a351a0 Mon Sep 17 00:00:00 2001 From: Copilot Date: Sun, 2 Aug 2026 11:26:51 -0700 Subject: [PATCH] guard_set: wrap rp_cache into guard_set_cache class (#10362) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses code review feedback on PR #10361: the raw `obj_map` typedef + static `dealloc_cache` helper is replaced by a proper `guard_set_cache` class that owns its memory and adds a recycling optimization. ## Changes - **New `guard_set_cache` class** (`guard_set.h` / `.cpp`): - `m_cache` — `obj_map` (null value = unsupported guard, avoids retranslation) - `m_fresh` — pre-allocated `range_predicate*` recycled across failed translations; when `guard_to_range_predicate` rejects a guard, the heap object is retained in `m_fresh` instead of deallocated, so the next miss reuses it without an alloc/dealloc round-trip - Public API: `reset()`, `find(expr*, seq::range_predicate*&) → bool`, `fresh(unsigned max_char) → seq::range_predicate*`, `insert(expr*, seq::range_predicate*)` - **`guard_set`**: removed `rp_cache` typedef and `dealloc_cache` static; constructor parameter updated to `guard_set_cache*`; `conjoin` updated to use `fresh()` + `insert()` for the recycling path - **`seq_monadic`**: field type `guard_set::rp_cache` → `guard_set_cache`; reset call updated to `m_rp_cache.reset()` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/guard_set.cpp | 42 +++++++++++++++++++++----------- src/ast/rewriter/guard_set.h | 38 ++++++++++++++++++++++------- src/ast/rewriter/seq_monadic.cpp | 2 +- src/ast/rewriter/seq_monadic.h | 8 +++--- 4 files changed, 62 insertions(+), 28 deletions(-) diff --git a/src/ast/rewriter/guard_set.cpp b/src/ast/rewriter/guard_set.cpp index 4cfe52e3da..834bcf9b85 100644 --- a/src/ast/rewriter/guard_set.cpp +++ b/src/ast/rewriter/guard_set.cpp @@ -20,7 +20,7 @@ Author: #include "ast/bv_decl_plugin.h" guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, - rp_cache* cache) + guard_set_cache* cache) : m(_m), u(_u), m_sort(elem_sort), m_v0(v0), m_is_char(_u.is_char(elem_sort)), m_rp_cache(cache), m_rp(_u.max_char()), m_guard(_m) { @@ -28,10 +28,23 @@ guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, 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_cache::reset() { + for (auto const& [k, v] : m_cache) dealloc(v); + m_cache.reset(); + dealloc(m_fresh); + m_trail.reset(); + m_fresh = nullptr; +} + +seq::range_predicate* guard_set_cache::fresh(unsigned max_char) { + if (!m_fresh) m_fresh = alloc(seq::range_predicate, max_char); + return m_fresh; +} + +void guard_set_cache::insert(expr* g, seq::range_predicate* p) { + if (p) m_fresh = nullptr; // ownership transferred to map + m_trail.push_back(g); + m_cache.insert(g, p); } void guard_set::collect_consts(expr* g, ptr_vector& out) const { @@ -138,7 +151,8 @@ lbool guard_set::generic_eval(expr_ref* witness) const { } void guard_set::conjoin(expr* g) { - if (!m_ok) return; + if (!m_ok) + return; if (!m_is_char) { m_guard = m.mk_and(m_guard, g); return; @@ -149,20 +163,20 @@ void guard_set::conjoin(expr* g) { // 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); + s = m_rp_cache->fresh(u.max_char()); + if (!seq::guard_to_range_predicate(u, m_v0, g, *s)) + s = nullptr; // recycles s into m_fresh + 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; + if (seq::guard_to_range_predicate(u, m_v0, g, s)) + m_rp = m_rp & s; + else + m_ok = false; } 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 18bb71b998..3c3040c351 100644 --- a/src/ast/rewriter/guard_set.h +++ b/src/ast/rewriter/guard_set.h @@ -30,22 +30,42 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_range_collapse.h" -class guard_set { +// Cache mapping guard expressions to their range predicates. +// A null value in the map records that the guard is unsupported (avoiding retranslation). +// m_fresh recycles the last allocated range_predicate so failed translations do not +// incur an alloc/dealloc cycle on every miss. +// +// Lifetime contract: expr* keys are assumed to outlive the cache (their lifetime is +// managed by the caller -- e.g. by the cofactor_cache that owns the guard expressions). +class guard_set_cache { + ast_manager& m; + expr_ref_vector m_trail; + obj_map m_cache; + seq::range_predicate* m_fresh = nullptr; 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); + guard_set_cache(ast_manager& m): m(m), m_trail(m) {} + ~guard_set_cache() { reset(); } + void reset(); + // Returns true if g is in the cache; val is set to the cached entry + // (val may be null = unsupported guard). + bool find(expr* g, seq::range_predicate*& val) const { return m_cache.find(g, val); } + // Returns a range_predicate* ready for guard_to_range_predicate to write into. + // Reuses the previously recycled object when available; otherwise allocates one. + seq::range_predicate* fresh(unsigned max_char); + // Records g -> p. If p is non-null (translation succeeded), ownership is transferred + // to the cache and m_fresh is cleared. If p is null (unsupported), the object + // previously returned by fresh() is retained in m_fresh for the next translation. + void insert(expr* g, seq::range_predicate* p); +}; -private: +class guard_set { 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; + guard_set_cache* m_rp_cache = nullptr; seq::range_predicate m_rp; // char representation expr_ref m_guard; // generic representation (conjunction over v0) @@ -64,7 +84,7 @@ private: public: guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, - rp_cache* cache = nullptr); + guard_set_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 0abf3f0135..5623c89c4a 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -80,7 +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 + m_rp_cache.reset(); // the guards live in the cofactor vectors } bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index ed5cdefe48..733dac1212 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -86,9 +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 + guard_set_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 @@ -175,7 +175,7 @@ public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, transition_mode mode = transition_mode::light_antimirov) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), - m_mode(mode), m_pin(rw.m()) {} + m_mode(mode), m_pin(rw.m()), m_rp_cache(m) {} ~seq_monadic() { reset_cofactor_cache(); }