mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00
Code Activity

separate out guard_set_cache

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-02 12:17:24 -07:00
parent 867f45496d
commit ee319167ad
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/guard_set.cpp
View file

@ -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);

2
src/ast/rewriter/seq_monadic.h
View file

@ -109,7 +109,7 @@ private:
bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps)
obj_map<expr, expr*> 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<std::tuple<expr_ref, expr_ref, void*>>;
membership_vec m_memberships; // asserted (term in regex, dep) for check()
ptr_vector<void> m_core; // dependencies of an unsat subset, filled by check() on l_false