mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 12:13:25 +00:00
Code Activity

Cache derivative_cofactors calls in seq_monadic

Browse source 
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
This commit is contained in:
Nikolaj Bjorner 2026-07-31 19:20:52 -07:00
parent 168b51d332
commit 6212042e80
2 changed files with 30 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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<expr>& out, bool& ok) {
@ -89,8 +101,7 @@ void seq_monadic::live_states(expr* R, ptr_vector<expr>& 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<component> const& comps, expr_ref* w
// per-component cofactor branches (target, guard); pin both, they outlive `cof`.
std::vector<std::vector<std::pair<expr*, expr*>>> 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<disjunct> const& dnf, obj_map<expr, expr*>*
lbool seq_monadic::solve(expr* term, expr* R, obj_map<expr, expr*>* model) {
m_pin.reset();
reset_cofactor_cache();
m_budget = 200000; // global work budget: bail fast on DNF explosion
m_giveup = false;
vector<disjunct> dnf;
@ -428,6 +439,7 @@ lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> 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 }.

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

@ -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<expr, expr_ref_pair_vector*> 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