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
// Tests for the Parikh abstraction over word equations, seq_parikh.
//
// Each case builds the constraint system for one equation and decides it on its own,
// without asserting the equation itself. So the verdict is about the observers, not about
// the equation: `refuted` means they contradict each other, `allowed` means they do not -
// the equation may still be unsatisfiable.
//
// In the specifications below 'a'..'e' are constant characters and 'x', 'y', 'z' are
// variables.
#include "ast/ast_pp.h"
#include "ast/reg_decl_plugins.h"
#include "ast/seq/seq_parikh.h"
#include "smt/smt_kernel.h"
#include "params/smt_params.h"
#include "util/rlimit.h"
#include "util/util.h"
#include <iostream>
#include <string>
namespace {
enum class verdict { refuted, allowed, skipped };
std::ostream& operator<<(std::ostream& out, verdict v) {
switch (v) {
case verdict::refuted: return out << "refuted";
case verdict::allowed: return out << "allowed";
default: return out << "skipped";
}
}
struct fixture {
ast_manager m;
seq_util u;
sort_ref str_sort;
fixture(): u((reg_decl_plugins(m), m)), str_sort(u.str.mk_string_sort(), m) {}
void side(std::string const& s, expr_ref_vector& out) {
for (char c : s) {
if (c >= 'x')
out.push_back(m.mk_const(symbol(c), str_sort));
else
out.push_back(u.str.mk_unit(u.mk_char(c)));
}
}
};
unsigned g_checks = 0;
unsigned g_failures = 0;
unsigned g_bounded = 0;
// decide the observation system of l = r for the grid bounded by (k, n)
verdict observe(std::string const& l, std::string const& r, unsigned k, unsigned n) {
fixture f;
expr_ref_vector ls(f.m), rs(f.m), defs(f.m), eqs(f.m);
f.side(l, ls);
f.side(r, rs);
seq::parikh::config cfg;
cfg.m_k = k;
cfg.m_n = n;
seq::parikh parikh(f.m, cfg);
if (!parikh(ls, rs, defs, eqs))
return verdict::skipped;
smt_params fp;
// A single hard system must not stall the suite. Running out of resources reads as
// `allowed`, which is the safe direction: the test only complains about refutations.
// A larger grid is strictly stronger, so any drop in the refutation count between
// grids is this bound and nothing else - g_bounded says how often it was hit.
scoped_rlimit rl(f.m.limit(), 2000000);
smt::kernel solver(f.m, fp);
for (expr* e : defs) {
solver.assert_expr(e);
}
for (expr* e : eqs) {
solver.assert_expr(e);
}
lbool res = solver.check();
if (res == l_undef)
++g_bounded;
return res == l_false ? verdict::refuted : verdict::allowed;
}
void check(std::string const& l, std::string const& r, unsigned k, unsigned n, verdict expected) {
verdict actual = observe(l, r, k, n);
++g_checks;
if (actual == expected)
return;
++g_failures;
std::cout << "seq_parikh: " << l << " = " << r << " at (" << k << "," << n
<< ") expected " << expected << " got " << actual << std::endl;
}
std::string subst(std::string const& s, std::string const& x, std::string const& y) {
std::string out;
for (char c : s) {
if (c == 'x')
out += x;
else if (c == 'y')
out += y;
else
out += c;
}
return out;
}
// does some assignment of words up to max_len solve l = r?
bool has_solution(std::string const& l, std::string const& r, unsigned max_len) {
vector<std::string> words;
words.push_back(std::string());
for (unsigned i = 0; i < words.size() && words[i].size() < max_len; ++i) {
words.push_back(words[i] + "a");
words.push_back(words[i] + "b");
}
for (auto const& x : words) {
for (auto const& y : words) {
if (subst(l, x, y) == subst(r, x, y))
return true;
}
}
return false;
}
// The abstraction is only allowed to refute. Generate random equations, search for a
// solution by hand, and insist that a refuted equation really has none.
void test_random(unsigned num_equations, unsigned k, unsigned n) {
random_gen rnd(17);
char const* alphabet = "abxy";
unsigned refuted = 0, skipped = 0;
g_bounded = 0;
for (unsigned i = 0; i < num_equations; ++i) {
std::string l, r;
for (unsigned j = 2 + rnd(5); j-- > 0; ) {
l += alphabet[rnd(4)];
}
for (unsigned j = 2 + rnd(5); j-- > 0; ) {
r += alphabet[rnd(4)];
}
verdict v = observe(l, r, k, n);
if (v == verdict::skipped)
++skipped;
if (v != verdict::refuted)
continue;
++refuted;
if (!has_solution(l, r, 6))
continue;
++g_failures;
std::cout << "seq_parikh: (" << k << "," << n << ") refuted the satisfiable equation "
<< l << " = " << r << std::endl;
}
std::cout << "seq_parikh: (" << k << "," << n << ") " << num_equations
<< " random equations, " << refuted << " refuted, " << skipped
<< " out of scope, " << g_bounded << " over the resource bound" << std::endl;
}
// theory_seq feeds many equations to one seq_parikh instance and asserts every
// definition it gets back. The counters are shared, so definitions coming from
// equations over different alphabets have to stay consistent with each other.
void test_shared_alphabet() {
char const* equations[][2] = {
{ "xa", "ax" }, { "xb", "bx" }, { "xc", "cx" },
{ "xx", "abab" }, { "bx", "xb" }, { "xcx", "cc" },
{ "xaby", "abxy" }, { "yx", "xy" }, { "xdx", "dd" }
};
fixture f;
seq::parikh::config cfg;
seq::parikh parikh(f.m, cfg);
expr_ref_vector defs(f.m), eqs(f.m);
for (auto const& e : equations) {
expr_ref_vector ls(f.m), rs(f.m);
f.side(e[0], ls);
f.side(e[1], rs);
parikh(ls, rs, defs, eqs);
}
// x = "" solves every one of them, so the definitions alone must be satisfiable
smt_params fp;
smt::kernel solver(f.m, fp);
for (expr* d : defs) {
solver.assert_expr(d);
}
lbool r = solver.check();
if (r != l_true) {
std::cout << "seq_parikh: shared definitions are inconsistent, got " << r << std::endl;
ENSURE(false);
}
std::cout << "seq_parikh: shared alphabet ok, " << defs.size()
<< " definitions over " << (sizeof(equations) / sizeof(*equations))
<< " equations" << std::endl;
}
}
void tst_seq_parikh() {
// 3|x| = 2 + |x| is solvable, but counting the characters gives 2|x|_a = 1
check("xxx", "abx", 1, 1, verdict::refuted);
// Parikh is satisfied, the pairs are not: x has one a and one b, but no arrangement
// gives both sides the same pairs
check("xx", "axb", 1, 1, verdict::allowed);
check("xx", "axb", 2, 1, verdict::refuted);
// yy = abba, the standard witness that adjacent pairs see more than single characters
check("yy", "abba", 1, 1, verdict::allowed);
check("yy", "abba", 2, 1, verdict::refuted);
// the same equation with a common prefix left in place. The residue observer refutes it
// on its own: the a's on the right sit at two even positions and one odd one, which the
// two copies of y cannot reproduce
check("ayy", "aabba", 1, 1, verdict::allowed);
check("ayy", "aabba", 1, 2, verdict::refuted);
check("ayy", "aabba", 2, 1, verdict::refuted);
check("ayy", "aabba", 2, 2, verdict::refuted);
// the abstraction is blind to order. a x x y = x b x x is unsatisfiable but has almost
// solutions for every observer, so the abstraction must not refute it
check("axxy", "xbxx", 1, 1, verdict::allowed);
check("axxy", "xbxx", 2, 1, verdict::allowed);
check("axxy", "xbxx", 2, 2, verdict::allowed);
// satisfiable equations must stay satisfiable under every observer
check("xax", "axa", 2, 2, verdict::allowed);
check("xay", "xya", 2, 2, verdict::allowed);
check("axb", "axb", 2, 2, verdict::allowed);
check("xaay", "xaay", 2, 2, verdict::allowed);
check("ax", "xa", 2, 2, verdict::allowed);
check("xxa", "axx", 2, 2, verdict::allowed);
check("abxy", "abxy", 2, 2, verdict::allowed);
check("xyab", "xyab", 2, 2, verdict::allowed);
// empty blocks: x = "" and y = "ab" solves it, so no observer may refute it
check("xyx", "ab", 2, 2, verdict::allowed);
check("xaybz", "aybz", 2, 2, verdict::allowed);
// an equation without constants collapses to the length equation and is skipped
check("xy", "yx", 2, 2, verdict::skipped);
// the abstraction can be turned off
check("yy", "abba", 0, 1, verdict::skipped);
// Including the catch-all class, the default bound admits p = 5 (25 pairs)
// and rejects p = 6 (36 pairs).
check("abcd", "abcd", 2, 1, verdict::allowed);
check("abcde", "abcde", 2, 1, verdict::skipped);
// Regression for the rotation being shared across observers. The clock is an argument
// of the rotation, so clocks of different moduli that happen to agree used to make
// congruence identify rotations that mean different things. n >= 3 puts two observers
// in the same system, which is what it takes to see this. n = 4..6 repeat the
// same check with more observers and take tens of seconds each in Debug, so
// they run in seq_parikh_long.
for (unsigned n = 1; n <= 3; ++n) {
check("ayyx", "aba", 1, n, verdict::allowed); // y empty, x = "ba"
check("aba", "ax", 1, n, verdict::allowed); // x = "ba"
check("xax", "axa", 2, n, verdict::allowed); // x in a*
}
test_shared_alphabet();
// Only the random grids that finish in a few seconds (n = 1) run here. The
// larger grids spend most of their time on systems that exhaust the
// resource bound and read as `allowed`, which no assertion consumes;
// they run in seq_parikh_long, only when named (see FOR_EACH_EXTRA_TEST
// in main.cpp).
test_random(80, 1, 1);
test_random(25, 2, 1);
std::cout << "seq_parikh: " << g_checks << " directed cases, " << g_failures << " failures" << std::endl;
ENSURE(g_failures == 0);
}
// The directed cases with many observers and the random grids dominated by
// the resource bound (about 20 minutes in Debug).
// Not part of `test-z3 -a`; run as `test-z3 seq_parikh_long`.
void tst_seq_parikh_long() {
g_failures = 0;
for (unsigned n = 4; n <= 6; ++n) {
check("ayyx", "aba", 1, n, verdict::allowed);
check("aba", "ax", 1, n, verdict::allowed);
check("xax", "axa", 2, n, verdict::allowed);
}
for (unsigned n = 2; n <= 4; ++n) {
test_random(80, 1, n);
}
for (unsigned n = 2; n <= 3; ++n) {
test_random(25, 2, n);
}
std::cout << "seq_parikh_long: " << g_failures << " failures" << std::endl;
ENSURE(g_failures == 0);
}