From 6212042e80dffa6925828d4087b293abed48a72d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2026 19:20:52 -0700 Subject: [PATCH] Cache derivative_cofactors calls in seq_monadic Memoize derivative_cofactors per regex in an owning cache so each regex's cofactors are computed once per top-level solve. The cache is reset at the start of solve()/solve_and() and freed in the destructor. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/ast/rewriter/seq_monadic.cpp | 28 ++++++++++++++++++++-------- src/ast/rewriter/seq_monadic.h | 12 ++++++++++-- 2 files changed, 30 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 71640041f8..5d22dcf4d1 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -23,7 +23,6 @@ TODOs: - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) - create a validation harness: expose certificates for correctness that can be checked. - extend with lower and upper bound constraints -- cache calls to cofactors so they are only computed once per regex. - consider using expr_ref as alternative to pinned expressions - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership @@ -61,11 +60,24 @@ expr_ref seq_monadic::der_elem(expr* r, expr* elem) { return d2; } -void seq_monadic::derivative_cofactors(expr* r, expr_ref_pair_vector& result) { +expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { + expr_ref_pair_vector* v = nullptr; + if (m_cofactor_cache.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, result); + m_rw.light_ant_derivative_cofactors(r, *v); else - m_rw.brz_derivative_cofactors(r, result); + 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); + return *v; +} + +void seq_monadic::reset_cofactor_cache() { + for (auto& kv : m_cofactor_cache) + dealloc(kv.m_value); + m_cofactor_cache.reset(); } void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { @@ -89,8 +101,7 @@ void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { const unsigned STATE_CAP = 1u << 12; for (unsigned i = 0; i < states.size(); ++i) { if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } - expr_ref_pair_vector cof(m); - derivative_cofactors(states.get(i), cof); + expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i)); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; unsigned k = intern(t); // MUST precede succ[i] indexing: intern may @@ -195,8 +206,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w // per-component cofactor branches (target, guard); pin both, they outlive `cof`. std::vector>> branches(n); for (unsigned i = 0; i < n; ++i) { - expr_ref_pair_vector cof(m); - derivative_cofactors(st[i], cof); + expr_ref_pair_vector const& cof = derivative_cofactors(st[i]); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; m_pin.push_back(t); @@ -415,6 +425,7 @@ lbool seq_monadic::decide_dnf(vector const& dnf, obj_map* lbool seq_monadic::solve(expr* term, expr* R, obj_map* model) { m_pin.reset(); + reset_cofactor_cache(); m_budget = 200000; // global work budget: bail fast on DNF explosion m_giveup = false; vector dnf; @@ -428,6 +439,7 @@ lbool seq_monadic::solve_and(vector> const& mems, if (mems.empty()) return l_undef; m_pin.reset(); + reset_cofactor_cache(); 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 06d603d408..a40efacbf3 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -77,6 +77,7 @@ private: expr_ref_vector m_pin; // pins derivative states / witnesses referenced later unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops) bool m_giveup = false; // set when the budget is exhausted + obj_map m_cofactor_cache; // memoizes derivative_cofactors per regex seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } @@ -95,8 +96,13 @@ 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. - void derivative_cofactors(expr* r, expr_ref_pair_vector& result); + // 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()/solve_and() (which resets the cache). + 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. Sets `ok` false on a cap overrun. @@ -133,6 +139,8 @@ public: seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_mode(mode), m_pin(rw.m()) {} + ~seq_monadic() { reset_cofactor_cache(); } + transition_mode mode() const { return m_mode; } // Decide (str.in_re term R) for a term that is a concatenation of string variables