1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_derive.h
Abstract:
Symbolic derivative computation for regular expressions.
Produces an ITE-tree (transition regex) representation where
the free variable is de Bruijn index 0 representing the input character.
Based on the theory of symbolic derivatives and transition regexes:
- Veanes et al., "On Symbolic Derivatives and Transition Regexes" (LPAR 2024)
- Varatalu, Veanes, Ernits, "RE#" (POPL 2025)
- Stanford, Veanes, Bjørner, "Symbolic Boolean Derivatives" (PLDI 2021)
Authors:
Nikolaj Bjorner (nbjorner) 2025-06-03
--*/
#pragma once
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
#include "util/obj_pair_hashtable.h"
#include "util/obj_triple_hashtable.h"
#include <functional>
class seq_rewriter;
namespace seq {
enum class derivative_kind { antimirov_t, brzozowski_t };
enum class transition_mode { brzozowski_tm, light_antimirov_tm };
const char* transition_mode_name(transition_mode mode);
/**
* Symbolic derivative engine for regular expressions.
*
* Given a regex r, operator()(r) computes a symbolic derivative δ(r)
* represented as an ITE-tree over character predicates (using de Bruijn
* variable 0 for the character). Evaluating the ITE-tree for a concrete
* character 'a' yields the classical Brzozowski derivative δ_a(r).
*
* The ITE-tree structure implicitly defines minterms (equivalence classes
* of characters indistinguishable by the regex).
*
* Key properties:
* - Results are memoized for termination on cyclic derivative graphs
* - Union/intersection operands are sorted for ACI canonicalization
* - Regex construction uses the shared seq_rewriter smart constructors;
* only canonical constants and opaque, stuck derivatives are built raw
* - Depth-bounded to prevent stack overflow
*/
class derive {
class cofactor_cache {
obj_map<expr, expr_ref_pair_vector *> m_cache;
expr_ref_vector m_pin; // trail of pinned keys
public:
cofactor_cache(ast_manager &m) : m_pin(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();
}
void reset() {
for (auto const &[k, v] : m_cache)
dealloc(v);
m_cache.reset();
m_pin.reset();
}
void maybe_reset(unsigned cap) {
if (m_cache.size() > cap)
reset();
}
};
ast_manager& m;
seq_util m_util;
arith_util m_autil;
bool_rewriter m_br;
seq_rewriter& m_re;
// Cache: maps (ele, regex) pair to its derivative
obj_pair_map<expr, expr, expr*> m_acache, m_bcache;
obj_pair_map<expr, expr, expr*> m_atop_cache, m_btop_cache; // post-simplify cache
expr_ref_vector m_trail; // pin cached results
cofactor_cache m_brz_cofactor_cache;
cofactor_cache m_ant_cofactor_cache;
// Op cache for ITE-hoisting operations (union, inter, concat, complement)
// Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement
obj_triple_map<expr, expr, expr, expr *> m_aunion_cache, m_bunion_cache, m_ainter_cache, m_binter_cache, m_axor_cache, m_bxor_cache;
obj_pair_map<expr, expr, expr*> m_aconcat_cache, m_bconcat_cache;
obj_pair_map<expr, expr, expr*> m_acomplement_cache, m_bcomplement_cache;
// Depth limiting
unsigned m_depth { 0 };
static const unsigned m_max_depth = 512;
seq_util::rex& re() { return m_util.re; }
seq_util& u() { return m_util; }
derivative_kind m_derivative_kind = derivative_kind::antimirov_t;
// The element (character) for the current derivative computation
expr_ref m_ele;
// Path state for inline pruning during mk_inter/mk_union/mk_complement
using intervals_t = svector<std::pair<unsigned, unsigned>>;
// Path: vector of signed atoms
svector<std::pair<expr*, bool>> m_path;
// Intervals: feasible character ranges under current path (append-only)
intervals_t m_intervals;
unsigned m_intervals_start { 0 };
// Stack of saved states for push/pop
struct path_save { unsigned path_sz; unsigned intervals_sz; unsigned intervals_start; expr* path_expr; };
svector<path_save> m_path_stack;
// Boolean expression encoding of current path (for cache keys)
expr_ref m_path_expr;
// Path interface
lbool push(expr* c, bool sign); // l_true: implied, l_undef: pushed (must pop), l_false: contradicts
void pop(); // restore state to matching push
expr* get_path_expr() { return m_path_expr; }
obj_pair_map<expr, expr, expr *> &cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_acache : m_bcache;
}
obj_pair_map<expr, expr, expr *> &top_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_atop_cache : m_btop_cache;
}
obj_triple_map<expr, expr, expr, expr *> &union_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_aunion_cache : m_bunion_cache;
}
obj_triple_map<expr, expr, expr, expr *> &inter_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_ainter_cache : m_binter_cache;
}
obj_triple_map<expr, expr, expr, expr *> &xor_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_axor_cache : m_bxor_cache;
}
obj_pair_map<expr, expr, expr *> &concat_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_aconcat_cache : m_bconcat_cache;
}
obj_pair_map<expr, expr, expr *> &complement_cache() {
return m_derivative_kind == derivative_kind::antimirov_t ? m_acomplement_cache : m_bcomplement_cache;
}
// Hoist ITE: apply_op through ite(c, t, e) with path pruning
expr_ref apply_ite(expr* c, expr* t, expr* e, expr* r, std::function<expr_ref(expr*, expr*)> apply_op);
expr_ref apply_ite(expr* c, expr* t1, expr* e1, expr* t2, expr* e2, std::function<expr_ref(expr*, expr*)> apply_op);
expr_ref apply_ite(expr* c, expr* t, expr* e, std::function<expr_ref(expr*)> apply_op);
// Common ITE dispatch for binary ops (union/inter)
expr_ref hoist_ite(expr* a, expr* b, std::function<expr_ref(expr*, expr*)> apply_op);
// Evaluate a condition against the current path/intervals
lbool eval_path_cond(expr* c);
// Internal helpers for push
lbool push_path_atoms(expr* c, bool sign);
lbool push_intervals_impl(expr* c, bool sign);
// Core derivative computation
expr_ref derive_rec(expr* r);
expr_ref derive_core(expr* r);
expr_ref mk_stuck_derivative(expr* r) {
// Rewriting this node would re-enter the depth-limited computation.
return expr_ref(re().mk_derivative(m_ele, r), m);
}
// Helpers for specific regex constructs
expr_ref derive_to_re(expr* s, sort* seq_sort);
expr_ref derive_range(expr* lo, expr* hi, sort* seq_sort);
expr_ref derive_of_pred(expr* pred, sort* seq_sort);
// Nullable check: returns a Boolean expression
expr_ref is_nullable(expr* r);
expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort);
// Smart constructors with path-aware simplification and ACI canonicalization
expr_ref mk_union(expr* a, expr* b);
bool are_complements(expr* a, expr* b);
unsigned union_id(expr* e); // complement-aware ID for sorting
bool is_subset(expr* a, expr* b);
expr_ref mk_union_core(expr* a, expr* b);
void add_union_elem(expr_ref_vector& set, expr* e);
expr_ref mk_inter(expr* a, expr* b);
expr_ref mk_inter_core(expr* a, expr* b);
expr_ref mk_concat(expr* a, expr* b);
expr_ref mk_complement(expr* a);
expr_ref mk_complement_core(expr* a);
expr_ref mk_xor(expr *a, expr *b);
expr_ref mk_xor_core(expr *a, expr *b);
expr_ref mk_core(decl_kind k, expr* a, expr* b);
expr_ref mk_ite(expr* c, expr* t, expr* e);
// Distribute concatenation through ITE/union in derivative
expr_ref mk_deriv_concat(expr* d, expr* tail);
expr_ref mk_deriv_concat_core(expr* d, expr* tail);
// Extract head character and tail from a sequence expression
bool get_head_tail(expr* s1, expr* s2, expr_ref& hd, expr_ref& tl);
// Predicate implication for character range conditions.
bool pred_implies(bool sign_a, expr* a, bool sign_b, expr* b);
bool pred_implies(expr* a, expr* b);
// Condition evaluation helpers
lbool eval_cond(expr* cond);
lbool eval_range_cond(expr* c);
void intersect_intervals(unsigned lo, unsigned hi);
void exclude_interval(unsigned lo, unsigned hi);
// Cofactor enumeration over a transition regex (ITE-tree).
void get_cofactors_rec(expr* r, expr_ref_pair_vector& result);
// Rebuild cofactor leaves bottom-up through smart constructors.
// decompose_ite substitutes branches without simplifying any of the
// surrounding operators. Shared subterms are visited only once.
expr_ref clean_leaf(expr* r);
sort* re_sort(expr* r) { return r->get_sort(); }
sort* seq_sort(expr* r) { sort* s = nullptr; m_util.is_re(r, s); return s; }
sort* ele_sort(expr* r) { sort* s = seq_sort(r); sort* e = nullptr; m_util.is_seq(s, e); return e; }
void reset();
void reset_op_caches();
public:
derive(ast_manager& m, seq_rewriter& re);
/**
* Compute the derivative of regex r with respect to element ele.
* When ele is a de Bruijn variable, produces a symbolic ITE-tree.
* When ele is a concrete character, produces the concrete derivative.
*/
expr_ref operator()(derivative_kind k, expr* ele, expr* r);
/**
* Convenience: symbolic derivative using de Bruijn var 0.
*/
expr_ref operator()(derivative_kind k, expr* r);
/**
* Nullable check: returns a Boolean expression that is true iff r accepts the empty string.
*/
expr_ref nullable(expr* r) { return is_nullable(r); }
/**
* Enumerate the cofactors (min-terms) of a transition regex r taken with
* respect to element ele. r is an ITE-tree over character predicates on
* ele; for every feasible path through the tree this produces a pair
* (path_condition, leaf_regex). Infeasible character-interval
* combinations are pruned using the same path/interval context that the
* derivative engine uses while hoisting ITEs.
*/
void get_cofactors(expr* ele, expr* r, expr_ref_pair_vector& result);
expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r);
void maybe_reset_cached_cofactors(unsigned cap) {
m_brz_cofactor_cache.maybe_reset(cap);
m_ant_cofactor_cache.maybe_reset(cap);
}
/**
* Compute the symbolic derivative of r and enumerate its reachable
* leaves in fully ITE-hoisted normal form.
*
* Concretely this returns, for every feasible minterm (character
* class) of δ(r), a pair (path_condition, target_regex). Every
* if-then-else over the input character (including ones that would
* otherwise be buried under a concat/union) is hoisted to the top
* via the same path/interval pruning used by the derivative engine,
* so each target_regex is free of (:var 0) and its nullability is
* always decidable. Unions are kept intact as single leaves (a
* union leaf denotes a single bisimulation state). Infeasible
* minterms are pruned, so all returned leaves are reachable.
*
* This is the entry point the regex_bisim equivalence procedure
* uses: it consumes the target_regex of each pair and ignores the
* (redundant) path condition.
*/
void derivative_cofactors(expr* r, expr_ref_pair_vector& result);
/**
* Compute the Brzozowski cofactors of r (derivative_cofactors above),
* then expose the nondeterminism that a union leaf hides: a target of
* the form (s1 | ... | sn), or (s1 | ... | sn) . tail, is split into
* one cofactor per alternative si (resp. si . tail). Splitting is
* applied recursively, so nested unions are flattened as well.
*
* Splitting can make two originally distinct cofactors reach the same
* target; such cofactors are merged back into a single pair whose
* guard is the disjunction of the original guards. The result is
* therefore still a list of distinct targets, but each one is a
* single Antimirov-style alternative rather than a union state.
*
* The guards are not required to be mutually exclusive after merging,
* and the transition relation is genuinely nondeterministic: a
* character may be accepted by several of the returned guards.
*/
void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result);
};
}