z3-src 503.2.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
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

/*++
Copyright (c) 2026 Microsoft Corporation

Tests for the sequence power operator s^n:
rewrite rules and the axioms used by the sequence solver.

--*/

#include "ast/arith_decl_plugin.h"
#include "ast/reg_decl_plugins.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/seq_decl_plugin.h"
#include "smt/smt_context.h"

static void tst_power_rewriter() {
    ast_manager m;
    reg_decl_plugins(m);
    th_rewriter rw(m);
    seq_util seq(m);
    arith_util a(m);

    sort* str_sort = seq.str.mk_string_sort();
    app_ref x(m.mk_const("x", str_sort), m);
    app_ref n(m.mk_const("n", a.mk_int()), m);
    app_ref k(m.mk_const("k", a.mk_int()), m);
    expr_ref emp(seq.str.mk_empty(str_sort), m);

    auto power = [&](expr* s, expr* k) { return expr_ref(seq.str.mk_power(s, k), m); };
    auto powi = [&](expr* s, int k) { return power(s, a.mk_int(k)); };
    auto simp = [&](expr_ref e) { rw(e); return e; };

    ENSURE(simp(powi(x, 0)) == emp);
    ENSURE(simp(powi(x, -2)) == emp);
    ENSURE(simp(powi(x, 1)) == x);
    ENSURE(simp(power(emp, n)) == emp);

    // a constant base folds into a string
    ENSURE(simp(powi(seq.str.mk_string(zstring("ab")), 2)) == seq.str.mk_string(zstring("abab")));

    // a small exponent unfolds into a concatenation
    ENSURE(simp(powi(x, 2)) == seq.str.mk_concat(x, x));

    // exponents beyond rewriter.max_power_expansion are left alone
    ENSURE(seq.str.is_power(simp(powi(x, 3))));
    ENSURE(seq.str.is_power(simp(powi(seq.str.mk_string(zstring("ab")), 3))));
    params_ref p;
    p.set_uint("max_power_expansion", 4);
    th_rewriter rw4(m, p);
    expr_ref x3(powi(x, 3));
    rw4(x3);
    ENSURE(x3 == seq.str.mk_concat(x, seq.str.mk_concat(x, x)));

    // (x^k)^l = x^(k*l)
    {
        expr_ref x100 = powi(x, 100);
        expr_ref three(a.mk_int(3), m);
        expr_ref lhs = simp(power(x100, three));
        expr_ref rhs = simp(powi(x, 300));
        ENSURE(lhs == rhs);
    }
    {
        expr_ref xn = power(x, n);
        expr_ref three(a.mk_int(3), m);
        expr_ref lhs = simp(power(xn, three));
        expr_ref rhs = simp(power(x, a.mk_mul(three, n)));
        ENSURE(lhs == rhs);
    }

    // the length of an unexpanded power is still known
    expr_ref big = simp(powi(x, 1000));
    {
        expr_ref lhs = simp(expr_ref(seq.str.mk_length(big), m));
        expr_ref thousand(a.mk_int(1000), m);
        expr_ref len_x(seq.str.mk_length(x), m);
        expr_ref rhs = simp(expr_ref(a.mk_mul(thousand, len_x), m));
        ENSURE(lhs == rhs);
    }

    // symbolic exponents are not touched
    ENSURE(seq.str.is_power(simp(power(x, n))));

    // equality rewrites for powers
    {
        expr_ref lhs = simp(expr_ref(m.mk_eq(power(x, n), emp), m));
        expr_ref nonpositive(a.mk_le(n, a.mk_int(0)), m);
        expr_ref empty(m.mk_eq(x, emp), m);
        expr_ref rhs = simp(expr_ref(m.mk_or(nonpositive, empty), m));
        ENSURE(lhs == rhs);
    }
    {
        expr_ref xn = power(x, n);
        expr_ref xk = power(x, k);
        expr_ref lhs = simp(expr_ref(m.mk_eq(xn, xk), m));
        expr_ref empty(m.mk_eq(x, emp), m);
        expr_ref zero(a.mk_int(0), m);
        expr_ref n_nonpositive(a.mk_le(n, zero), m);
        expr_ref k_nonpositive(a.mk_le(k, zero), m);
        expr_ref both_nonpositive(m.mk_and(n_nonpositive, k_nonpositive), m);
        expr_ref n_positive(a.mk_lt(zero, n), m);
        expr_ref k_positive(a.mk_lt(zero, k), m);
        expr_ref equal(m.mk_eq(n, k), m);
        expr_ref positive_equal(m.mk_and(n_positive, k_positive, equal), m);
        expr_ref rhs = simp(expr_ref(m.mk_or(empty, both_nonpositive, positive_equal), m));
        ENSURE(lhs == rhs);
    }
}

static lbool check(ast_manager& m, expr_ref_vector const& fmls) {
    smt_params sp;
    smt::context ctx(m, sp);
    for (expr* f : fmls)
        ctx.assert_expr(f);
    return ctx.check();
}

static void tst_power_solver() {
    ast_manager m;
    reg_decl_plugins(m);
    seq_util seq(m);
    arith_util a(m);

    sort* str_sort = seq.str.mk_string_sort();
    app_ref x(m.mk_const("x", str_sort), m);
    app_ref n(m.mk_const("n", a.mk_int()), m);
    expr_ref ab(seq.str.mk_string(zstring("ab")), m);
    expr_ref_vector fmls(m);

    // "ab"^n = "abab" has the solution n = 2
    {
        expr_ref lhs(seq.str.mk_power(ab, n), m);
        expr_ref rhs(seq.str.mk_string(zstring("abab")), m);
        fmls.push_back(m.mk_eq(lhs, rhs));
    }
    ENSURE(check(m, fmls) == l_true);

    // the length of "ab"^n is even
    fmls.reset();
    {
        expr_ref lhs(seq.str.mk_power(ab, n), m);
        expr_ref rhs(seq.str.mk_string(zstring("aba")), m);
        fmls.push_back(m.mk_eq(lhs, rhs));
    }
    ENSURE(check(m, fmls) == l_false);

    // x^n is empty for n <= 0
    fmls.reset();
    fmls.push_back(a.mk_le(n, a.mk_int(0)));
    {
        expr_ref lhs(seq.str.mk_power(x, n), m);
        expr_ref rhs(seq.str.mk_string(zstring("a")), m);
        fmls.push_back(m.mk_eq(lhs, rhs));
    }
    ENSURE(check(m, fmls) == l_false);

    // x^n = "aaaa" with |x| = 2 has the solution x = "aa", n = 2
    fmls.reset();
    {
        expr_ref lhs(seq.str.mk_power(x, n), m);
        expr_ref rhs(seq.str.mk_string(zstring("aaaa")), m);
        fmls.push_back(m.mk_eq(lhs, rhs));
    }
    {
        expr_ref lhs(seq.str.mk_length(x), m);
        expr_ref rhs(a.mk_int(2), m);
        fmls.push_back(m.mk_eq(lhs, rhs));
    }
    ENSURE(check(m, fmls) == l_true);

    // the unfolding is exact for a fixed exponent
    fmls.reset();
    fmls.push_back(a.mk_eq(n, a.mk_int(3)));
    {
        expr_ref lhs(seq.str.mk_power(x, n), m);
        expr_ref rhs(seq.str.mk_concat(x, seq.str.mk_concat(x, x)), m);
        fmls.push_back(m.mk_not(m.mk_eq(lhs, rhs)));
    }
    ENSURE(check(m, fmls) == l_false);
}

void tst_seq_power() {
    tst_power_rewriter();
    tst_power_solver();
}