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

Persist derivative cofactor cache across decide() calls

Browse source 
The cofactor cache is a pure function of the regex (and the fixed transition
mode), independent of the membership set, so tearing it down on every solve()/
decide() call forced it to be recomputed n+1 times during minimize_core()'s n
deletion trials. Keep it instead, resetting only when it grows past a size cap.

Encapsulate the cofactor memo, its pinned-key trail, and the coupled range-
predicate (guard_set_cache) into a self-contained cofactor_cache class with
find/insert/reset/maybe_reset, so the three reset in lockstep (the range
predicates' guards are owned by the cofactor vectors).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-08-02 11:43:52 -07:00
parent ddfd403013
commit c9a480cb37
2 changed files with 39 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,8 +29,6 @@ TODOs:
- take into account shape of terms to prune the search space (e.g., if the term is xax, then retain the effect of
intersecting with .*a.*).
- use expr_ref in component and replace svector<component> by vector<component>, save on m_pin.
- don't tear down cofactor cache between calls, but use a self-contained set of pinned regexes that don't get reset
between calls. This will allow for a more efficient caching of cofactor computations. Reset the cache upon bloat.
- support units of non-values (element variables).
Model construction would assign values to the elements.
- make unsat core tracking less naive by tracking dependencies at a finer grain.
@ -64,25 +62,17 @@ expr_ref seq_monadic::der_elem(expr* r, expr* elem) {
expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) {
expr_ref_pair_vector* v = nullptr;
if (m_cofactor_cache.find(r, v))
if (m_cofactors.find(r, v))
return *v;
v = alloc(expr_ref_pair_vector, m);
if (m_mode == transition_mode::light_antimirov)
m_rw.light_ant_derivative_cofactors(r, *v);
else
m_rw.brz_derivative_cofactors(r, *v);
m_pin.push_back(r); // keep the key alive for the cache's lifetime
m_cofactor_cache.insert(r, v);
m_cofactors.insert(r, v); // takes ownership of v and pins the key r
return *v;
}
void seq_monadic::reset_cofactor_cache() {
for (auto const& [k, v] : m_cofactor_cache)
dealloc(v);
m_cofactor_cache.reset();
m_rp_cache.reset(); // the guards live in the cofactor vectors
}
bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
obj_map<expr, unsigned> id;
expr_ref_vector states(m);
@ -253,7 +243,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_rp_cache);
guard_set top(m, u(), m_elem_sort, var0, &m_cofactors.rp_cache());
rec(0, top);
if (bail)
return l_undef;
@ -356,7 +346,7 @@ void seq_monadic::simplify_dnf(vector<disjunct>& dnf) {
lbool seq_monadic::solve(expr* term, expr* R) {
m_pin.reset();
reset_cofactor_cache();
m_cofactors.maybe_reset(1u << 16);
m_budget = 200000; // global work budget: bail fast on DNF explosion
m_giveup = false;
vector<disjunct> dnf;
@ -453,7 +443,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
if (memberships.empty())
return l_true; // empty conjunction is vacuously true
m_pin.reset();
reset_cofactor_cache();
m_cofactors.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 }.

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

@ -71,6 +71,34 @@ public:
};
private:
// Self-contained memo for derivative_cofactors: maps a regex to its (owned) cofactor
// vector and keeps a trail of pinned keys so they stay live for the cache's lifetime.
// The memoized cofactors depend only on the regex (and the fixed transition mode), so
// the cache is valid across solve()/decide()/check() calls; callers reset it only when
// it grows past a size cap (maybe_reset).
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() { 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(); }
};
ast_manager& m;
seq_rewriter& m_rw;
th_rewriter m_thrw; // normalizes constant-element derivatives (folds
@ -85,10 +113,7 @@ private:
bool m_gen_model = true; // whether solve()/check() extract a feasible model
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()
obj_map<expr, expr_ref_pair_vector*> m_cofactor_cache; // memoizes derivative_cofactors per regex
guard_set_cache m_rp_cache; // cofactor guard -> range predicate; the guards
// are owned by m_cofactor_cache, so both are
// reset together
cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above)
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
@ -118,14 +143,11 @@ private:
// Brzozowski derivative of regex `r` by the concrete element `elem`.
expr_ref der_elem(expr* r, expr* elem);
// Symbolic transition cofactors in the selected mode. Memoized per regex `r`: the
// returned vector is owned by the cofactor cache and stays valid until the next
// top-level solve()/check() (which resets the cache).
// Symbolic transition cofactors in the selected mode. Memoized per regex `r` in
// m_cofactors: the returned vector is owned by that cache (see the cofactor_cache
// class above for the persistence/reset policy).
expr_ref_pair_vector const& derivative_cofactors(expr* r);
// Drop all memoized cofactors and free their owned vectors.
void reset_cofactor_cache();
// Live reachable derivative states of R (BFS over cofactor targets + liveness
// least-fixpoint). These are the split states q. Returns false on a cap overrun.
bool live_states(expr* R, expr_ref_vector& out);
@ -175,9 +197,9 @@ 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_rp_cache(m) {}
m_mode(mode), m_pin(rw.m()), m_cofactors(rw.m()) {}
~seq_monadic() { reset_cofactor_cache(); }
~seq_monadic() = default;
transition_mode mode() const { return m_mode; }