mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +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:13:42 -07:00
parent da159a9569
commit 6b91929df9
3 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/guard_set.h
View file

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

4
src/ast/rewriter/seq_monadic.cpp
View file

@ -245,7 +245,7 @@ lbool seq_monadic::product_nonempty(svector<component> 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<disjunct>& 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<disjunct> 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 }.

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

@ -79,22 +79,17 @@ private:
class cofactor_cache {
obj_map<expr, expr_ref_pair_vector*> 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<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
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
@ -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;