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
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_regex_bisim.cpp
Abstract:
See seq_regex_bisim.h.
Author:
Margus Veanes (veanes)
Nikolaj Bjorner (nbjorner)
--*/
#include "ast/rewriter/seq_regex_bisim.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
namespace seq {
regex_bisim::regex_bisim(seq_rewriter& rw):
m(rw.m()),
m_rw(rw),
m_util(rw.u()),
m_pinned(m),
m_worklist(m) {
}
void regex_bisim::reset() {
m_uf.reset();
m_node_of.reset();
m_pinned.reset();
m_worklist.reset();
m_steps = 0;
}
/*
Map an expression to a union-find node, allocating a fresh node on
first encounter.
*/
unsigned regex_bisim::node_of(expr* r) {
unsigned id = 0;
if (m_node_of.find(r, id))
return id;
id = m_uf.mk_var();
m_node_of.insert(r, id);
m_pinned.push_back(r);
return id;
}
/*
Compute a definite nullability answer for r.
If the seq_rewriter is unable to produce a literal true/false (for
example because r contains an uninterpreted symbol), return l_undef.
*/
lbool regex_bisim::nullability(expr* r) {
expr_ref n = m_rw.is_nullable(r);
if (m.is_true(n))
return l_true;
if (m.is_false(n))
return l_false;
return l_undef;
}
/*
Test whether a regex expression is a kind that the bisimulation
procedure can reason about. We require it to be a syntactic ground
term (no free variables) and that its info reports min_length info
(which implies that it parses cleanly as a regex constructor).
*/
bool regex_bisim::is_supported(expr* r) {
if (!m_util.is_re(r))
return false;
if (!m_util.re.get_info(r).is_known())
return false;
// Reject regexes mentioning free variables; the symbolic
// derivative engine introduces (:var 0) only after we call it
// ourselves, so any pre-existing variable would be a free var.
return is_ground(r);
}
/*
Fast inequivalence check based on the get_info().classical flag.
Invariant: if r is well-formed and get_info(r).classical is true,
then L(r) is non-empty. The flag is set for regexes built only
from str.to_re, re.all, union, concat, star, plus, opt, loop;
it excludes complement, intersection, diff, xor, and the empty
regex.
A bare regex leaf l (i.e. not a XOR pair) represents the implicit
pair (empty XOR l). If l is classical, L(l) is non-empty so the
pair is non-empty: the original two regexes have a distinguishing
prefix and are inequivalent.
For an XOR leaf xor(a, b): if both a and b are classical and have
different min_length, then the shortest word of one is not in the
other, so the pair is non-empty and we can short-circuit. (The
case a == b syntactically is already handled by mk_re_xor0.)
Returns true if the leaf proves inequivalence; false if no
conclusion can be drawn.
*/
bool regex_bisim::classical_distinguishing(expr* l) {
expr* a = nullptr, * b = nullptr;
if (m_util.re.is_xor(l, a, b)) {
auto ia = m_util.re.get_info(a);
auto ib = m_util.re.get_info(b);
if (ia.is_known() && ib.is_known() &&
ia.classical && ib.classical &&
ia.min_length != ib.min_length)
return true;
return false;
}
if (m_util.re.is_empty(l))
return false;
auto info = m_util.re.get_info(l);
return info.is_known() && info.classical;
}
/*
Merge the two sides of the XOR pair, returning true if a fresh
merge happened (i.e. the pair must still be processed) and false
if the two sides were already in the same union-find class.
For non-XOR leaves we treat the leaf l as the pair (empty XOR l).
*/
bool regex_bisim::merge_leaf(expr* leaf) {
expr* a = nullptr, * b = nullptr;
if (!m_util.re.is_xor(leaf, a, b)) {
a = m_util.re.mk_empty(leaf->get_sort());
b = leaf;
m_pinned.push_back(a);
}
unsigned ia = node_of(a);
unsigned ib = node_of(b);
if (m_uf.find(ia) == m_uf.find(ib))
return false;
m_uf.merge(ia, ib);
return true;
}
/*
Decide equivalence by bisimulation on D(p XOR q).
*/
lbool regex_bisim::are_equivalent(expr* p, expr* q) {
return are_equivalent_core(p, q);
}
lbool regex_bisim::are_equivalent_core(expr* p, expr* q) {
if (!is_supported(p) || !is_supported(q))
return l_undef;
if (p == q)
return l_true;
reset();
// Build the initial pair r0 = p XOR q applying the structural
// XOR rewrites (r XOR r = empty, AC normalisation, etc.).
expr_ref r0 = m_rw.mk_re_xor_simplified(p, q);
// If r0 simplified to empty, the two regexes are equivalent.
if (m_util.re.is_empty(r0))
return l_true;
lbool n0 = nullability(r0);
if (n0 == l_true)
return l_false; // distinguishing empty word
if (n0 == l_undef)
return l_undef;
// Classical-leaf shortcut applied to r0 (covers the case where
// mk_re_xor_simplified collapsed p XOR q to a bare classical
// residual, e.g. when one side reduced to empty).
if (classical_distinguishing(r0))
return l_false;
if (!merge_leaf(r0))
return l_true; // already merged: trivially equivalent
m_worklist.push_back(r0);
while (!m_worklist.empty()) {
if (++m_steps > m_step_bound)
return l_undef;
expr_ref r(m_worklist.back(), m);
m_worklist.pop_back();
// Compute the symbolic derivative wrt the canonical variable
// (:var 0) and enumerate its reachable leaves in fully
// ITE-hoisted normal form. Every if-then-else over the input
// character — even one that would otherwise be buried under a
// concat or union — is hoisted to the top and infeasible
// minterms are pruned, so each leaf is a ground regex free of
// (:var 0) whose nullability is always decidable. Unions are
// kept intact as single leaves (a union leaf denotes a single
// bisimulation state, never a split into separate states).
expr_ref_pair_vector cofs(m);
m_rw.brz_derivative_cofactors(r, cofs);
expr_ref_vector leaves(m);
for (auto const& p : cofs)
leaves.push_back(p.second);
// First pass: check for any nullable leaf (definitive
// distinguishing empty-continuation word) or any classically
// non-empty leaf (definitive distinguishing non-empty prefix).
for (expr* l : leaves) {
lbool nl = nullability(l);
if (nl == l_true)
return l_false;
if (nl == l_undef)
return l_undef;
if (classical_distinguishing(l))
return l_false;
}
// Second pass: merge each leaf into the union-find; new
// merges go onto the worklist.
for (expr* l : leaves) {
if (merge_leaf(l)) {
m_pinned.push_back(l);
m_worklist.push_back(l);
}
}
}
return l_true;
}
}