From ee319167ad67c115e7e74fee40f6ae5cc249fb24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 12:17:24 -0700 Subject: [PATCH] separate out guard_set_cache Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/guard_set.cpp | 8 ++++---- src/ast/rewriter/seq_monadic.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/guard_set.cpp b/src/ast/rewriter/guard_set.cpp index 834bcf9b85..42c04abe31 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, - guard_set_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,7 +28,7 @@ guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0, else m_guard = m.mk_true(); } -void guard_set_cache::reset() { +void guard_set::cache::reset() { for (auto const& [k, v] : m_cache) dealloc(v); m_cache.reset(); dealloc(m_fresh); @@ -36,12 +36,12 @@ void guard_set_cache::reset() { m_fresh = nullptr; } -seq::range_predicate* guard_set_cache::fresh(unsigned max_char) { +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) { +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); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 48abdfe15d..ee8904d00c 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -109,7 +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 + 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