1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #ifdef _WINDOWS
8 #include "api/z3.h"
9 #include "api/z3_private.h"
10 #include <iostream>
11 #include "util/util.h"
12 #include "util/trace.h"
13
14
ev_const(Z3_context ctx,Z3_ast e)15 static void ev_const(Z3_context ctx, Z3_ast e) {
16 Z3_ast r = Z3_simplify(ctx, e);
17 TRACE("simplifier",
18 tout << Z3_ast_to_string(ctx, e) << " -> ";
19 tout << Z3_ast_to_string(ctx, r) << "\n";);
20 Z3_ast_kind k = Z3_get_ast_kind(ctx, r);
21 ENSURE(k == Z3_NUMERAL_AST ||
22 (k == Z3_APP_AST &&
23 (Z3_OP_TRUE == Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx, Z3_to_app(ctx, r))) ||
24 Z3_OP_FALSE == Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx, Z3_to_app(ctx, r))))));
25 }
26
test_bv()27 static void test_bv() {
28 Z3_config cfg = Z3_mk_config();
29 Z3_context ctx = Z3_mk_context(cfg);
30 Z3_sort bv1 = Z3_mk_bv_sort(ctx,1);
31 Z3_sort bv2 = Z3_mk_bv_sort(ctx,2);
32 Z3_sort bv72 = Z3_mk_bv_sort(ctx,72);
33 Z3_ast bit1_1 = Z3_mk_numeral(ctx, "1", bv1);
34 Z3_ast bit3_2 = Z3_mk_numeral(ctx, "3", bv2);
35
36 Z3_ast e = Z3_mk_eq(ctx, bit3_2, Z3_mk_sign_ext(ctx, 1, bit1_1));
37 ENSURE(Z3_simplify(ctx, e) == Z3_mk_true(ctx));
38 TRACE("simplifier", tout << Z3_ast_to_string(ctx, e) << "\n";);
39
40 Z3_ast b12 = Z3_mk_numeral(ctx, "12", bv72);
41 Z3_ast b13 = Z3_mk_numeral(ctx, "13", bv72);
42
43 ev_const(ctx, Z3_mk_bvnot(ctx,b12));
44 ev_const(ctx, Z3_mk_bvnot(ctx,Z3_simplify(ctx, Z3_mk_bvnot(ctx, b12))));
45 ev_const(ctx, Z3_mk_bvand(ctx,b12,b13));
46 ev_const(ctx, Z3_mk_bvor(ctx,b12,b13));
47 ev_const(ctx, Z3_mk_bvxor(ctx,b12,b13));
48 ev_const(ctx, Z3_mk_bvnand(ctx,b12,b13));
49 ev_const(ctx, Z3_mk_bvnor(ctx,b12,b13));
50 ev_const(ctx, Z3_mk_bvxnor(ctx,b12,b13));
51 ev_const(ctx, Z3_mk_bvneg(ctx,b12));
52 ev_const(ctx, Z3_mk_bvadd(ctx,b12,b13));
53 ev_const(ctx, Z3_mk_bvsub(ctx,b12,b13));
54 ev_const(ctx, Z3_mk_bvmul(ctx,b12,b13));
55 ev_const(ctx, Z3_mk_bvudiv(ctx,b12,b13));
56 ev_const(ctx, Z3_mk_bvsdiv(ctx,b12,b13));
57 ev_const(ctx, Z3_mk_bvsrem(ctx,b12,b13));
58
59 ev_const(ctx, Z3_mk_bvuge(ctx,b12,b13));
60 ev_const(ctx, Z3_mk_bvsge(ctx,b12,b13));
61 ev_const(ctx, Z3_mk_bvugt(ctx,b12,b13));
62 ev_const(ctx, Z3_mk_bvsgt(ctx,b12,b13));
63 ev_const(ctx, Z3_mk_bvule(ctx,b12,b13));
64 ev_const(ctx, Z3_mk_bvult(ctx,b12,b13));
65 ev_const(ctx, Z3_mk_bvsle(ctx,b12,b13));
66 ev_const(ctx, Z3_mk_bvslt(ctx,b12,b13));
67
68 ev_const(ctx, Z3_mk_concat(ctx,b12,b13));
69 ev_const(ctx, Z3_mk_extract(ctx,43,1,b13));
70 ev_const(ctx, Z3_mk_sign_ext(ctx,33,b13));
71 ev_const(ctx, Z3_mk_zero_ext(ctx,33,b13));
72 ev_const(ctx, Z3_mk_bvshl(ctx,b12,b13));
73
74 ev_const(ctx, Z3_mk_bvshl(ctx,b12,b13));
75 ev_const(ctx, Z3_mk_bvlshr(ctx,b12,b13));
76 ev_const(ctx, Z3_mk_bvashr(ctx,b12,b13));
77
78 ev_const(ctx, Z3_mk_rotate_left(ctx,21,b13));
79 ev_const(ctx, Z3_mk_rotate_right(ctx,21,b13));
80
81 Z3_del_config(cfg);
82 Z3_del_context(ctx);
83 }
84
test_datatypes()85 static void test_datatypes() {
86 Z3_config cfg = Z3_mk_config();
87 Z3_context ctx = Z3_mk_context(cfg);
88 Z3_sort int_ty, int_list;
89 Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl;
90 Z3_ast nil, l1;
91
92 int_ty = Z3_mk_int_sort(ctx);
93
94 int_list = Z3_mk_list_sort(ctx, Z3_mk_string_symbol(ctx, "int_list"), int_ty,
95 &nil_decl, &is_nil_decl, &cons_decl, &is_cons_decl, &head_decl, &tail_decl);
96
97 nil = Z3_mk_app(ctx, nil_decl, 0, 0);
98
99 Z3_ast a = Z3_simplify(ctx, Z3_mk_app(ctx, is_nil_decl, 1, &nil));
100 ENSURE(a == Z3_mk_true(ctx));
101
102 a = Z3_simplify(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &nil));
103 ENSURE(a == Z3_mk_false(ctx));
104
105 Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
106 Z3_ast args[2] = { one, nil };
107 l1 = Z3_mk_app(ctx, cons_decl, 2, args);
108 ENSURE(nil == Z3_simplify(ctx, Z3_mk_app(ctx, tail_decl, 1, &l1)));
109 ENSURE(one == Z3_simplify(ctx, Z3_mk_app(ctx, head_decl, 1, &l1)));
110
111 ENSURE(Z3_mk_false(ctx) == Z3_simplify(ctx, Z3_mk_eq(ctx, nil, l1)));
112
113 Z3_del_config(cfg);
114 Z3_del_context(ctx);
115 }
116
117
test_skolemize_bug()118 static void test_skolemize_bug() {
119 Z3_config cfg = Z3_mk_config();
120 Z3_set_param_value(cfg, "MODEL", "true");
121 Z3_context ctx = Z3_mk_context(cfg);
122 Z3_del_config(cfg);
123
124 Z3_sort Real = Z3_mk_real_sort(ctx);
125 Z3_ast x = Z3_mk_bound(ctx, 0, Real);
126 Z3_symbol x_name = Z3_mk_string_symbol(ctx, "x");
127 Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), Real);
128 Z3_ast xp = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "xp"), Real);
129 Z3_ast n0 = Z3_mk_numeral(ctx, "0", Real);
130 Z3_ast n1 = Z3_mk_numeral(ctx, "1", Real);
131 Z3_ast args1[2] = { x, n1 };
132 Z3_ast args2[2] = { x, y };
133 Z3_ast args[2] = { Z3_mk_eq(ctx, Z3_mk_add(ctx, 2, args1), xp),
134 Z3_mk_ge(ctx, Z3_mk_add(ctx, 2, args2), n0) };
135 Z3_ast f = Z3_mk_and(ctx, 2, args);
136 Z3_ast f2 = Z3_mk_exists(ctx, 0, 0, 0, 1, &Real, &x_name, f);
137 std::cout << Z3_ast_to_string(ctx, f2) << "\n";
138 Z3_ast f3 = Z3_simplify(ctx, f2);
139 std::cout << Z3_ast_to_string(ctx, f3) << "\n";
140
141 }
142
143
test_bool()144 static void test_bool() {
145 Z3_config cfg = Z3_mk_config();
146 Z3_context ctx = Z3_mk_context(cfg);
147
148 Z3_ast a = Z3_simplify(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx))));
149 Z3_ast b = Z3_simplify(ctx, Z3_mk_not(ctx, Z3_mk_iff(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx))));
150 ENSURE(Z3_mk_true(ctx) == a);
151 ENSURE(Z3_mk_true(ctx) == b);
152 TRACE("simplifier", tout << Z3_ast_to_string(ctx, a) << "\n";);
153 TRACE("simplifier", tout << Z3_ast_to_string(ctx, b) << "\n";);
154
155 Z3_del_config(cfg);
156 Z3_del_context(ctx);
157 }
158
test_array()159 static void test_array() {
160
161 Z3_config cfg = Z3_mk_config();
162 Z3_context ctx = Z3_mk_context(cfg);
163 Z3_sort i = Z3_mk_int_sort(ctx);
164 Z3_ast n1 = Z3_mk_numeral(ctx, "1", i);
165 Z3_ast n2 = Z3_mk_numeral(ctx, "2", i);
166 Z3_ast n3 = Z3_mk_numeral(ctx, "3", i);
167 Z3_ast n4 = Z3_mk_numeral(ctx, "4", i);
168 Z3_ast s1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"s1"), i);
169 Z3_ast s2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"s2"), i);
170
171 Z3_ast c1 = Z3_mk_const_array(ctx, i, n1);
172 Z3_ast x1 = Z3_mk_store(ctx, Z3_mk_store(ctx, c1, n2, n3), n1, n4);
173 Z3_ast x2 = Z3_mk_store(ctx, Z3_mk_store(ctx, c1, n1, n4), n2, n3);
174 Z3_ast x3 = Z3_mk_store(ctx, Z3_mk_store(ctx, c1, s1, n1), n2, n3);
175 Z3_ast x4 = Z3_mk_store(ctx, Z3_mk_store(ctx, Z3_mk_store(ctx, c1, n2, n3), n1, n4), n2, n3);
176 Z3_ast xs[4] = { x1, x2, x3, x4};
177 Z3_ast exy = Z3_mk_eq(ctx, x2, x1);
178 Z3_ast rxy = Z3_simplify(ctx, exy);
179
180 TRACE("simplifier", tout << Z3_ast_to_string(ctx, rxy) << "\n";);
181 TRACE("simplifier", tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3))) << "\n";);
182 // ENSURE(rxy == Z3_mk_true(ctx));
183 // ENSURE(Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3)) == Z3_mk_false(ctx));
184
185 for (unsigned i = 0; i < 4; ++i) {
186 for (unsigned j = 0; j < 4; ++j) {
187 exy = Z3_mk_eq(ctx, xs[i], xs[j]);
188 rxy = Z3_simplify(ctx, exy);
189
190 TRACE("simplifier",
191 tout << Z3_ast_to_string(ctx, exy);
192 tout << " -> " << Z3_ast_to_string(ctx, rxy) << "\n";
193 );
194 }
195 }
196
197 Z3_ast sel1 = Z3_mk_select(ctx, x1, n1);
198 Z3_ast sel2 = Z3_mk_select(ctx, x1, n4);
199
200 TRACE("simplifier",
201 tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, sel1)) << "\n";
202 tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, sel2)) << "\n";
203 );
204
205 Z3_del_config(cfg);
206 Z3_del_context(ctx);
207 }
208
tst_simplifier()209 void tst_simplifier() {
210
211 test_array();
212 test_bv();
213 test_datatypes();
214 test_bool();
215 test_skolemize_bug();
216 }
217
218 #else
tst_simplifier()219 void tst_simplifier() {
220 }
221 #endif
222