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
330
331
332
333
334
335
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
test/seq_profile_abs.cpp
Abstract:
Unit tests for seq::profile_abs, the per-letter Parikh abstraction
refined by length.
The abstraction has two directions, and the tests check both against a
brute-force oracle rather than against hand-computed masks alone:
* profiles(R) OVER-approximates: w in L(R) implies profile(w) is in
the mask. Verified by enumerating every word up to a small length
over a small alphabet and matching it against R with an independent
reference matcher.
* forced(R) UNDER-approximates: if profile p is in forced(R) then
EVERY word with profile p lies in L(R). Verified by searching the
same word set for a counterexample.
Both properties are what the consumer relies on for refutation, so a
regression in either direction is a soundness bug, not a precision loss.
Author:
Margus Veanes (veanes) 2026
--*/
#include "ast/seq/seq_profile_abs.h"
#include "ast/reg_decl_plugins.h"
#include "ast/ast_pp.h"
#include "util/util.h"
#include <iostream>
#include <set>
#include <string>
#include <vector>
namespace {
using seq::profile_abs;
static unsigned const LCAP = 2;
static void check(bool ok, char const* what) {
if (!ok) {
std::cerr << "seq_profile_abs FAILED: " << what << "\n";
ENSURE(false);
}
}
static inline unsigned pbit(unsigned c, unsigned l) { return 1u << (c * 3 + l); }
// ---- reference matcher -------------------------------------------
//
// match_set(r, w, i) = { j : w[i..j) in L(r) }. Computing the set of
// end positions rather than a yes/no answer makes concat, star and
// intersection straightforward and keeps complement exact.
class matcher {
seq_util& u;
std::string const& w;
public:
matcher(seq_util& u, std::string const& w) : u(u), w(w) {}
std::set<unsigned> ends(expr* r, unsigned i) {
std::set<unsigned> res;
unsigned const n = (unsigned)w.size();
expr *a = nullptr, *b = nullptr, *s = nullptr;
unsigned lo = 0, hi = 0;
zstring str;
if (u.re.is_empty(r))
return res;
if (u.re.is_full_seq(r)) {
for (unsigned j = i; j <= n; ++j)
res.insert(j);
return res;
}
if (u.re.is_full_char(r)) {
if (i < n)
res.insert(i + 1);
return res;
}
if (u.re.is_to_re(r, s) && u.str.is_string(s, str)) {
unsigned const L = str.length();
if (i + L <= n) {
bool ok = true;
for (unsigned k = 0; k < L && ok; ++k)
ok = (unsigned)(unsigned char)w[i + k] == str[k];
if (ok)
res.insert(i + L);
}
return res;
}
if (u.re.is_range(r, lo, hi)) {
if (i < n) {
unsigned c = (unsigned)(unsigned char)w[i];
if (lo <= c && c <= hi)
res.insert(i + 1);
}
return res;
}
if (u.re.is_concat(r, a, b)) {
for (unsigned mid : ends(a, i))
for (unsigned j : ends(b, mid))
res.insert(j);
return res;
}
if (u.re.is_union(r, a, b)) {
for (unsigned j : ends(a, i)) res.insert(j);
for (unsigned j : ends(b, i)) res.insert(j);
return res;
}
if (u.re.is_intersection(r, a, b)) {
std::set<unsigned> ra = ends(a, i), rb = ends(b, i);
for (unsigned j : ra)
if (rb.count(j))
res.insert(j);
return res;
}
if (u.re.is_diff(r, a, b)) {
std::set<unsigned> rb = ends(b, i);
for (unsigned j : ends(a, i))
if (!rb.count(j))
res.insert(j);
return res;
}
if (u.re.is_complement(r, a)) {
// w[i..j) not in L(a), for every j
std::set<unsigned> ra = ends(a, i);
for (unsigned j = i; j <= n; ++j)
if (!ra.count(j))
res.insert(j);
return res;
}
if (u.re.is_star(r, a)) {
res.insert(i);
bool grew = true;
while (grew) {
grew = false;
std::vector<unsigned> cur(res.begin(), res.end());
for (unsigned p : cur)
for (unsigned j : ends(a, p))
if (j > p && res.insert(j).second)
grew = true;
}
return res;
}
if (u.re.is_plus(r, a)) {
for (unsigned mid : ends(a, i)) {
expr_ref st(u.re.mk_star(a), u.get_manager());
for (unsigned j : ends(st, mid))
res.insert(j);
}
return res;
}
if (u.re.is_opt(r, a)) {
res.insert(i);
for (unsigned j : ends(a, i)) res.insert(j);
return res;
}
std::cerr << "seq_profile_abs: reference matcher has no case for "
<< mk_pp(r, u.get_manager()) << "\n";
ENSURE(false);
return res;
}
bool matches(expr* r) {
return ends(r, 0).count((unsigned)w.size()) > 0;
}
};
// Every word of length <= max_len over `alphabet`.
static void all_words(std::string const& alphabet, unsigned max_len,
std::vector<std::string>& out) {
out.push_back("");
size_t start = 0;
for (unsigned len = 1; len <= max_len; ++len) {
size_t end = out.size();
for (size_t k = start; k < end; ++k)
for (char c : alphabet)
out.push_back(out[k] + c);
start = end;
}
}
static unsigned word_profile(std::string const& w, unsigned sigma, unsigned mod) {
unsigned cnt = 0;
for (char c : w)
if ((unsigned)(unsigned char)c == sigma)
++cnt;
return pbit(cnt % mod, std::min((unsigned)w.size(), LCAP));
}
static expr_ref chr(seq_util& u, char c) {
return expr_ref(u.re.mk_to_re(u.str.mk_string(zstring((unsigned)(unsigned char)c))),
u.get_manager());
}
static void run() {
ast_manager m;
reg_decl_plugins(m);
seq_util u(m);
profile_abs abs(m);
sort* str_sort = u.str.mk_string_sort();
sort* re_sort = u.re.mk_re(str_sort);
expr_ref a(chr(u, 'a')), b(chr(u, 'b'));
expr_ref dot(u.re.mk_full_char(re_sort), m);
expr_ref all(u.re.mk_full_seq(re_sort), m);
// The battery deliberately includes the extended idioms that the
// length refinement exists for.
expr_ref_vector battery(m);
battery.push_back(a); // "a"
battery.push_back(u.re.mk_concat(a, a)); // "aa"
battery.push_back(u.re.mk_union(a, b)); // a | b
battery.push_back(u.re.mk_star(a)); // a*
battery.push_back(u.re.mk_plus(a)); // a+
battery.push_back(u.re.mk_opt(a)); // a?
battery.push_back(u.re.mk_star(u.re.mk_concat(a, a))); // (aa)*
{
expr_ref lhs(u.re.mk_star(u.re.mk_concat(a, a)), m);
expr_ref rhs(u.re.mk_star(u.re.mk_concat(a, u.re.mk_concat(a, a))), m);
battery.push_back(u.re.mk_union(lhs, rhs));
}
battery.push_back(u.re.mk_inter(dot, u.re.mk_complement(a))); // . & ~a
battery.push_back(u.re.mk_complement(a)); // ~a
battery.push_back(u.re.mk_complement(u.re.mk_star(a))); // ~(a*)
battery.push_back(u.re.mk_diff(dot, a)); // . \ a
battery.push_back(u.re.mk_concat(u.re.mk_star(a), b)); // a* b
{
expr_ref lhs(u.re.mk_star(a), m);
expr_ref rhs(u.re.mk_complement(u.re.mk_concat(a, a)), m);
battery.push_back(u.re.mk_inter(lhs, rhs));
}
battery.push_back(dot);
battery.push_back(all);
battery.push_back(u.re.mk_empty(re_sort));
std::vector<std::string> words;
all_words("abc", 4, words);
unsigned checked = 0;
for (unsigned mod = 2; mod <= 4; ++mod) {
for (char sig : std::string("ab")) {
unsigned sigma = (unsigned)(unsigned char)sig;
for (expr* r : battery) {
abs.begin_pass(mod, sigma);
unsigned const prof = abs.profiles(r);
unsigned const forc = abs.forced(r);
for (std::string const& w : words) {
matcher mt(u, w);
bool const in = mt.matches(r);
unsigned const p = word_profile(w, sigma, mod);
// over-approximation: membership implies the bit is set
if (in && !(prof & p)) {
std::cerr << "profiles() unsound for "
<< mk_pp(r, m) << " on \"" << w << "\""
<< " (mod " << mod << ", sigma " << sig << ")\n";
check(false, "profiles over-approximation");
}
// under-approximation: a forced bit admits no non-member
if (!in && (forc & p)) {
std::cerr << "forced() unsound for "
<< mk_pp(r, m) << " on \"" << w << "\""
<< " (mod " << mod << ", sigma " << sig << ")\n";
check(false, "forced under-approximation");
}
++checked;
}
}
}
}
// Note: forced() is NOT contained in profiles(). A profile that no
// word realizes -- e.g. length 1 with two occurrences of sigma -- is
// vacuously forced, since every word realizing it (there are none)
// lies in L(R), yet it is absent from profiles(R). The two masks are
// deliberately independent approximations.
// ---- concrete residue expectations ----
// "aa" counting 'a' mod 2 -> only residue 0
{
unsigned res = abs.regex_residues(u.re.mk_concat(a, a), 2, 'a');
check(res == 0x1, "residues of \"aa\" mod 2 = {0}");
}
// "a" counting 'a' mod 2 -> only residue 1
{
unsigned res = abs.regex_residues(a, 2, 'a');
check(res == 0x2, "residues of \"a\" mod 2 = {1}");
}
// (aa)* counting 'a' mod 2 -> only residue 0
{
unsigned res = abs.regex_residues(u.re.mk_star(u.re.mk_concat(a, a)), 2, 'a');
check(res == 0x1, "residues of (aa)* mod 2 = {0}");
}
// . & ~a is exactly one non-'a' character: residue 0, and it must
// NOT degrade to "all residues" -- this is the case the length
// refinement exists for.
{
expr_ref e(u.re.mk_inter(dot, u.re.mk_complement(a)), m);
unsigned res = abs.regex_residues(e, 3, 'a');
check(res == 0x1, "residues of (. & ~a) mod 3 = {0}");
}
// re.all carries no information.
{
unsigned res = abs.regex_residues(all, 3, 'a');
check(res == 0x7, "residues of re.all mod 3 = all");
}
// out-of-range modulus is rejected
{
check(abs.regex_residues(a, 1, 'a') == UINT_MAX, "modulus 1 rejected");
check(abs.regex_residues(a, profile_abs::max_modulus + 1, 'a') == UINT_MAX,
"modulus above max rejected");
}
std::cerr << "seq_profile_abs tests passed (" << checked
<< " word/regex soundness checks)\n";
}
}
void tst_seq_profile_abs() {
run();
}