From c9a480cb37b581623576201da850623ab44ce645 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 11:43:52 -0700 Subject: [PATCH] Persist derivative cofactor cache across decide() calls 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 --- src/ast/rewriter/seq_monadic.cpp | 20 ++++---------- src/ast/rewriter/seq_monadic.h | 46 +++++++++++++++++++++++--------- 2 files changed, 39 insertions(+), 27 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 5623c89c4a..17a71ec4cc 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -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 by vector, 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 id; expr_ref_vector states(m); @@ -253,7 +243,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_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& 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 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 }. diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 733dac1212..196cfc7c33 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -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 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 m_model; // last extracted model (var -> witness); see get_model() - obj_map 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>; 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 @@ -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; }