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

Add seq::derive class for symbolic regex derivatives

Browse source 
Implement a new seq::derive class (seq_derive.h/cpp) that computes
symbolic derivatives of regular expressions using ITE-trees, based on
the RE# approach (Varatalu, Veanes, Ernits - POPL 2025).

Key features:
- Two-argument operator()(ele, r): computes derivative of regex r w.r.t.
  element ele (concrete character or de Bruijn variable for symbolic mode)
- ACI canonicalization (flatten, stable_sort, dedup) for union/intersection
- ITE-tree combinators for binary/unary operations
- Info-based nullability with recursive fallback
- Complement absorption rules
- Depth-bounded recursion to prevent stack overflow

Integration with seq_rewriter:
- mk_derivative(ele, r) and mk_derivative(r) now delegate to m_derive
- Removed dead mk_derivative_rec function
- Added ITE hoisting in mk_re_star, mk_re_concat, mk_re_union0,
  mk_re_inter0, mk_re_complement
- Added depth limiting in Antimirov derivative helpers

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-03 10:36:19 -07:00
parent ab259b6830
commit 1f28fd0e6b
6 changed files with 921 additions and 234 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/seq_rewriter.h
View file

@ -19,6 +19,7 @@ Notes:
#pragma once
#include "ast/seq_decl_plugin.h"
#include "ast/seq_derive.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h"
@ -130,10 +131,13 @@ class seq_rewriter {
seq_util m_util;
arith_util m_autil;
bool_rewriter m_br;
seq::derive m_derive;
// re2automaton m_re2aut;
op_cache m_op_cache;
expr_ref_vector m_es, m_lhs, m_rhs;
bool m_coalesce_chars;
unsigned m_re_deriv_depth { 0 };
static const unsigned m_max_re_deriv_depth = 512;
enum length_comparison {
shorter_c,
@ -172,7 +176,6 @@ class seq_rewriter {
// Calculate derivative, memoized and enforcing a normal form
expr_ref is_nullable_rec(expr* r);
expr_ref mk_derivative_rec(expr* ele, expr* r);
expr_ref mk_der_op(decl_kind k, expr* a, expr* b);
expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b);
expr_ref mk_der_concat(expr* a, expr* b);
@ -340,7 +343,7 @@ class seq_rewriter {
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m),
m_util(m), m_autil(m), m_br(m, p), m_derive(m), // m_re2aut(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
}