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

fix perf

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-17 10:03:52 -06:00
parent 05c394aa6c
commit f261c7732b
2 changed files with 24 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/ast/rewriter/seq_derive.cpp
View file

@ -52,6 +52,7 @@ namespace seq {
m_concat_cache.reset();
m_complement_cache.reset();
m_trail.reset();
m_ele = nullptr;
}
// Reset only operation caches (union/inter/concat/complement)
@ -61,48 +62,44 @@ namespace seq {
m_inter_cache.reset();
m_concat_cache.reset();
m_complement_cache.reset();
m_ele = nullptr;
}
expr_ref derive::operator()(expr* ele, expr* r) {
SASSERT(m_util.is_re(r));
if (m_trail.size() > 500000)
reset();
else if (m_trail.size() > 100000)
else if (m_trail.size() > 100000 || ele != m_ele)
reset_op_caches();
sort *seq_sort = nullptr, *ele_sort = nullptr;
VERIFY(m_util.is_re(r, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort));
expr_ref v(m.mk_var(0, ele_sort), m);
// Check top-level cache (post-simplify result)
expr* cached = nullptr;
expr_ref result(m);
if (m_top_cache.find(r, cached)) {
if (m_top_cache.find(ele, r, cached)) {
result = cached;
}
else {
// Always compute the SYMBOLIC derivative wrt the canonical
// variable v (so the cached result is reusable for any
// concrete ele via substitution below). Using the concrete
// `ele` here would bake it into the cached ITE-tree and
// poison future lookups for the same r with a different ele.
m_ele = v;
m_depth = 0;
// Initialize path state for inline pruning
m_path.reset();
m_intervals.reset();
m_intervals.push_back({0u, u().max_char()});
m_intervals_start = 0;
m_path_expr = m.mk_true();
result = derive_rec(r);
m_top_cache.insert(r, result);
}
if (v != ele) {
var_subst subst(m);
result = subst(result, 1, &ele);
}
m_ele = nullptr;
return result;
}
// Cache and pin the final result
m_trail.push_back(ele);
// Always compute the SYMBOLIC derivative wrt the canonical
// variable v (so the cached result is reusable for any
// concrete ele via substitution below). Using the concrete
// `ele` here would bake it into the cached ITE-tree and
// poison future lookups for the same r with a different ele.
m_ele = ele;
m_depth = 0;
// Initialize path state for inline pruning
m_path.reset();
m_intervals.reset();
m_intervals.push_back({0u, u().max_char()});
m_intervals_start = 0;
m_path_expr = m.mk_true();
result = derive_rec(r);
m_top_cache.insert(ele, r, result);
m_trail.push_back(r);
m_trail.push_back(result);
return result;

2
src/ast/rewriter/seq_derive.h
View file

@ -61,7 +61,7 @@ namespace seq {
// Cache: maps (ele, regex) pair to its derivative
obj_pair_map<expr, expr, expr*> m_cache;
obj_map<expr, expr*> m_top_cache; // post-simplify cache
obj_pair_map<expr, expr, expr*> m_top_cache; // post-simplify cache
expr_ref_vector m_trail; // pin cached results
// Op cache for ITE-hoisting operations (union, inter, concat, complement)