From 6b91929df9708dfa7e1ebcad2f3fcc036665c6a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 12:13:42 -0700 Subject: [PATCH] separate out guard_set_cache Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/guard_set.h | 4 ++++ src/ast/rewriter/seq_monadic.cpp | 4 +++- src/ast/rewriter/seq_monadic.h | 10 +++------- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/guard_set.h b/src/ast/rewriter/guard_set.h index 3c3040c351..3b68cd6af9 100644 --- a/src/ast/rewriter/guard_set.h +++ b/src/ast/rewriter/guard_set.h @@ -46,6 +46,10 @@ public: guard_set_cache(ast_manager& m): m(m), m_trail(m) {} ~guard_set_cache() { reset(); } void reset(); + void maybe_reset(unsigned cap) { + if (m_cache.size() > cap) + 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); } diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index b2b75d8881..e2283a11d8 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -245,7 +245,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w if (bail) return; } }; - guard_set top(m, u(), m_elem_sort, var0, &m_cofactors.rp_cache()); + guard_set top(m, u(), m_elem_sort, var0, &m_rp_cache); rec(0, top); if (bail) return l_undef; @@ -349,6 +349,7 @@ void seq_monadic::simplify_dnf(vector& dnf) { lbool seq_monadic::solve(expr* term, expr* R) { m_pin.reset(); m_cofactors.maybe_reset(1u << 16); + m_rp_cache.maybe_reset(1u << 16); m_budget = 200000; // global work budget: bail fast on DNF explosion m_giveup = false; vector dnf; @@ -446,6 +447,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) { return l_true; // empty conjunction is vacuously true m_pin.reset(); m_cofactors.maybe_reset(1u << 16); + m_rp_cache.maybe_reset(1u << 16); m_budget = 200000; m_giveup = false; // Multiply the per-membership DNFs: combined = { d ++ e : d in combined, e in dnf_i }. diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 196cfc7c33..48abdfe15d 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -79,22 +79,17 @@ private: class cofactor_cache { obj_map m_cache; expr_ref_vector m_pin; // trail of pinned keys - guard_set_cache m_rp_cache; // cofactor guard -> range predicate; the - // guards are owned by the cofactor vectors, - // so it is reset together with the cache public: - cofactor_cache(ast_manager& m) : m_pin(m), m_rp_cache(m) {} + cofactor_cache(ast_manager& m) : m_pin(m) {} ~cofactor_cache() { reset(); } bool find(expr* r, expr_ref_pair_vector*& v) const { return m_cache.find(r, v); } void insert(expr* r, expr_ref_pair_vector* v) { m_pin.push_back(r); m_cache.insert(r, v); } unsigned size() const { return m_cache.size(); } - guard_set_cache& rp_cache() { return m_rp_cache; } void reset() { for (auto const& [k, v] : m_cache) dealloc(v); m_cache.reset(); m_pin.reset(); - m_rp_cache.reset(); } void maybe_reset(unsigned cap) { if (m_cache.size() > cap) reset(); } }; @@ -114,6 +109,7 @@ 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() cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above) + guard_set_cache m_rp_cache; // cofactor guard -> range predicate 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 @@ -197,7 +193,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_cofactors(rw.m()) {} + m_mode(mode), m_pin(rw.m()), m_cofactors(rw.m()), m_rp_cache(rw.m()) {} ~seq_monadic() = default;