1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 api_algebraic.cpp
7
8 Abstract:
9
10 Additional APIs for handling Z3 algebraic numbers encoded as
11 Z3_ASTs
12
13 Author:
14
15 Leonardo de Moura (leonardo) 2012-12-07
16
17 Notes:
18
19 --*/
20 #include "api/z3.h"
21 #include "api/api_log_macros.h"
22 #include "api/api_context.h"
23 #include "api/api_ast_vector.h"
24 #include "math/polynomial/algebraic_numbers.h"
25 #include "ast/expr2polynomial.h"
26 #include "util/cancel_eh.h"
27 #include "util/scoped_timer.h"
28
29
30 #define CHECK_IS_ALGEBRAIC(ARG, RET) { \
31 if (!Z3_algebraic_is_value_core(c, ARG)) { \
32 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); \
33 return RET; \
34 } \
35 }
36
37 #define CHECK_IS_ALGEBRAIC_X(ARG, RET) { \
38 if (!Z3_algebraic_is_value_core(c, ARG)) { \
39 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); \
40 RETURN_Z3(RET); \
41 } \
42 }
43
au(Z3_context c)44 static arith_util & au(Z3_context c) {
45 return mk_c(c)->autil();
46 }
47
am(Z3_context c)48 static algebraic_numbers::manager & am(Z3_context c) {
49 return au(c).am();
50 }
51
is_rational(Z3_context c,Z3_ast a)52 static bool is_rational(Z3_context c, Z3_ast a) {
53 return au(c).is_numeral(to_expr(a));
54 }
55
is_irrational(Z3_context c,Z3_ast a)56 static bool is_irrational(Z3_context c, Z3_ast a) {
57 return au(c).is_irrational_algebraic_numeral(to_expr(a));
58 }
59
get_rational(Z3_context c,Z3_ast a)60 static rational get_rational(Z3_context c, Z3_ast a) {
61 SASSERT(is_rational(c, a));
62 rational r;
63 VERIFY(au(c).is_numeral(to_expr(a), r));
64 return r;
65 }
66
get_irrational(Z3_context c,Z3_ast a)67 static algebraic_numbers::anum const & get_irrational(Z3_context c, Z3_ast a) {
68 SASSERT(is_irrational(c, a));
69 return au(c).to_irrational_algebraic_numeral(to_expr(a));
70 }
71
72 extern "C" {
73
Z3_algebraic_is_value_core(Z3_context c,Z3_ast a)74 bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) {
75 api::context * _c = mk_c(c);
76 return
77 is_expr(a) &&
78 (_c->autil().is_numeral(to_expr(a)) ||
79 _c->autil().is_irrational_algebraic_numeral(to_expr(a)));
80 }
81
Z3_algebraic_is_value(Z3_context c,Z3_ast a)82 bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
83 Z3_TRY;
84 LOG_Z3_algebraic_is_value(c, a);
85 RESET_ERROR_CODE();
86 return Z3_algebraic_is_value_core(c, a);
87 Z3_CATCH_RETURN(false);
88 }
89
Z3_algebraic_is_pos(Z3_context c,Z3_ast a)90 bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
91 return Z3_algebraic_sign(c, a) > 0;
92 }
93
Z3_algebraic_is_neg(Z3_context c,Z3_ast a)94 bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
95 return Z3_algebraic_sign(c, a) < 0;
96 }
97
Z3_algebraic_is_zero(Z3_context c,Z3_ast a)98 bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
99 return Z3_algebraic_sign(c, a) == 0;
100 }
101
Z3_algebraic_sign(Z3_context c,Z3_ast a)102 int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a) {
103 Z3_TRY;
104 LOG_Z3_algebraic_sign(c, a);
105 RESET_ERROR_CODE();
106 CHECK_IS_ALGEBRAIC(a, 0);
107 if (is_rational(c, a)) {
108 rational v = get_rational(c, a);
109 if (v.is_pos()) return 1;
110 else if (v.is_neg()) return -1;
111 else return 0;
112 }
113 else {
114 algebraic_numbers::anum const & v = get_irrational(c, a);
115 if (am(c).is_pos(v)) return 1;
116 else if (am(c).is_neg(v)) return -1;
117 else return 0;
118 }
119 Z3_CATCH_RETURN(0);
120 }
121
122 #define BIN_OP(RAT_OP, IRAT_OP) \
123 algebraic_numbers::manager & _am = am(c); \
124 ast * r = 0; \
125 if (is_rational(c, a)) { \
126 rational av = get_rational(c, a); \
127 if (is_rational(c, b)) { \
128 rational bv = get_rational(c, b); \
129 r = au(c).mk_numeral(av RAT_OP bv, false); \
130 } \
131 else { \
132 algebraic_numbers::anum const & bv = get_irrational(c, b); \
133 scoped_anum _av(_am); \
134 _am.set(_av, av.to_mpq()); \
135 scoped_anum _r(_am); \
136 _am.IRAT_OP(_av, bv, _r); \
137 r = au(c).mk_numeral(_am, _r, false); \
138 } \
139 } \
140 else { \
141 algebraic_numbers::anum const & av = get_irrational(c, a); \
142 if (is_rational(c, b)) { \
143 rational bv = get_rational(c, b); \
144 scoped_anum _bv(_am); \
145 _am.set(_bv, bv.to_mpq()); \
146 scoped_anum _r(_am); \
147 _am.IRAT_OP(av, _bv, _r); \
148 r = au(c).mk_numeral(_am, _r, false); \
149 } \
150 else { \
151 algebraic_numbers::anum const & bv = get_irrational(c, b); \
152 scoped_anum _r(_am); \
153 _am.IRAT_OP(av, bv, _r); \
154 r = au(c).mk_numeral(_am, _r, false); \
155 } \
156 } \
157 mk_c(c)->save_ast_trail(r); \
158 RETURN_Z3(of_ast(r));
159
160
Z3_algebraic_add(Z3_context c,Z3_ast a,Z3_ast b)161 Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) {
162 Z3_TRY;
163 LOG_Z3_algebraic_add(c, a, b);
164 RESET_ERROR_CODE();
165 CHECK_IS_ALGEBRAIC_X(a, nullptr);
166 CHECK_IS_ALGEBRAIC_X(b, nullptr);
167 BIN_OP(+,add);
168 Z3_CATCH_RETURN(nullptr);
169 }
170
Z3_algebraic_sub(Z3_context c,Z3_ast a,Z3_ast b)171 Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) {
172 Z3_TRY;
173 LOG_Z3_algebraic_sub(c, a, b);
174 RESET_ERROR_CODE();
175 CHECK_IS_ALGEBRAIC_X(a, nullptr);
176 CHECK_IS_ALGEBRAIC_X(b, nullptr);
177 BIN_OP(-,sub);
178 Z3_CATCH_RETURN(nullptr);
179 }
180
Z3_algebraic_mul(Z3_context c,Z3_ast a,Z3_ast b)181 Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) {
182 Z3_TRY;
183 LOG_Z3_algebraic_mul(c, a, b);
184 RESET_ERROR_CODE();
185 CHECK_IS_ALGEBRAIC_X(a, nullptr);
186 CHECK_IS_ALGEBRAIC_X(b, nullptr);
187 BIN_OP(*,mul);
188 Z3_CATCH_RETURN(nullptr);
189 }
190
Z3_algebraic_div(Z3_context c,Z3_ast a,Z3_ast b)191 Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b) {
192 Z3_TRY;
193 LOG_Z3_algebraic_div(c, a, b);
194 RESET_ERROR_CODE();
195 CHECK_IS_ALGEBRAIC_X(a, nullptr);
196 CHECK_IS_ALGEBRAIC_X(b, nullptr);
197 if ((is_rational(c, b) && get_rational(c, b).is_zero()) ||
198 (!is_rational(c, b) && am(c).is_zero(get_irrational(c, b)))) {
199 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
200 RETURN_Z3(nullptr);
201 }
202 BIN_OP(/,div);
203 Z3_CATCH_RETURN(nullptr);
204 }
205
Z3_algebraic_root(Z3_context c,Z3_ast a,unsigned k)206 Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k) {
207 Z3_TRY;
208 LOG_Z3_algebraic_root(c, a, k);
209 RESET_ERROR_CODE();
210 CHECK_IS_ALGEBRAIC_X(a, nullptr);
211 if (k % 2 == 0) {
212 if ((is_rational(c, a) && get_rational(c, a).is_neg()) ||
213 (!is_rational(c, a) && am(c).is_neg(get_irrational(c, a)))) {
214 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
215 RETURN_Z3(nullptr);
216 }
217 }
218 algebraic_numbers::manager & _am = am(c);
219 scoped_anum _r(_am);
220 if (is_rational(c, a)) {
221 scoped_anum av(_am);
222 _am.set(av, get_rational(c, a).to_mpq());
223 _am.root(av, k, _r);
224 }
225 else {
226 algebraic_numbers::anum const & av = get_irrational(c, a);
227 _am.root(av, k, _r);
228 }
229 expr * r = au(c).mk_numeral(_am, _r, false);
230 mk_c(c)->save_ast_trail(r);
231 RETURN_Z3(of_ast(r));
232 Z3_CATCH_RETURN(nullptr);
233 }
234
Z3_algebraic_power(Z3_context c,Z3_ast a,unsigned k)235 Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k) {
236 Z3_TRY;
237 LOG_Z3_algebraic_power(c, a, k);
238 RESET_ERROR_CODE();
239 CHECK_IS_ALGEBRAIC_X(a, nullptr);
240 algebraic_numbers::manager & _am = am(c);
241 scoped_anum _r(_am);
242 if (is_rational(c, a)) {
243 scoped_anum av(_am);
244 _am.set(av, get_rational(c, a).to_mpq());
245 _am.power(av, k, _r);
246 }
247 else {
248 algebraic_numbers::anum const & av = get_irrational(c, a);
249 _am.power(av, k, _r);
250 }
251 expr * r = au(c).mk_numeral(_am, _r, false);
252 mk_c(c)->save_ast_trail(r);
253 RETURN_Z3(of_ast(r));
254 Z3_CATCH_RETURN(nullptr);
255 }
256
257 #define BIN_PRED(RAT_PRED, IRAT_PRED) \
258 algebraic_numbers::manager & _am = am(c); \
259 bool r; \
260 if (is_rational(c, a)) { \
261 rational av = get_rational(c, a); \
262 if (is_rational(c, b)) { \
263 rational bv = get_rational(c, b); \
264 r = av RAT_PRED bv; \
265 } \
266 else { \
267 algebraic_numbers::anum const & bv = get_irrational(c, b); \
268 scoped_anum _av(_am); \
269 _am.set(_av, av.to_mpq()); \
270 r = _am.IRAT_PRED(_av, bv); \
271 } \
272 } \
273 else { \
274 algebraic_numbers::anum const & av = get_irrational(c, a); \
275 if (is_rational(c, b)) { \
276 rational bv = get_rational(c, b); \
277 scoped_anum _bv(_am); \
278 _am.set(_bv, bv.to_mpq()); \
279 r = _am.IRAT_PRED(av, _bv); \
280 } \
281 else { \
282 algebraic_numbers::anum const & bv = get_irrational(c, b); \
283 r = _am.IRAT_PRED(av, bv); \
284 } \
285 } \
286 return r;
287
288
Z3_algebraic_lt(Z3_context c,Z3_ast a,Z3_ast b)289 bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
290 Z3_TRY;
291 LOG_Z3_algebraic_lt(c, a, b);
292 RESET_ERROR_CODE();
293 CHECK_IS_ALGEBRAIC(a, 0);
294 CHECK_IS_ALGEBRAIC(b, 0);
295 BIN_PRED(<,lt);
296 Z3_CATCH_RETURN(false);
297 }
298
Z3_algebraic_gt(Z3_context c,Z3_ast a,Z3_ast b)299 bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
300 return Z3_algebraic_lt(c, b, a);
301 }
302
Z3_algebraic_le(Z3_context c,Z3_ast a,Z3_ast b)303 bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
304 return !Z3_algebraic_lt(c, b, a);
305 }
306
Z3_algebraic_ge(Z3_context c,Z3_ast a,Z3_ast b)307 bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
308 return !Z3_algebraic_lt(c, a, b);
309 }
310
Z3_algebraic_eq(Z3_context c,Z3_ast a,Z3_ast b)311 bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
312 Z3_TRY;
313 LOG_Z3_algebraic_eq(c, a, b);
314 RESET_ERROR_CODE();
315 CHECK_IS_ALGEBRAIC(a, 0);
316 CHECK_IS_ALGEBRAIC(b, 0);
317 BIN_PRED(==,eq);
318 Z3_CATCH_RETURN(0);
319 }
320
Z3_algebraic_neq(Z3_context c,Z3_ast a,Z3_ast b)321 bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
322 return !Z3_algebraic_eq(c, a, b);
323 }
324
to_anum_vector(Z3_context c,unsigned n,Z3_ast a[],scoped_anum_vector & as)325 static bool to_anum_vector(Z3_context c, unsigned n, Z3_ast a[], scoped_anum_vector & as) {
326 algebraic_numbers::manager & _am = am(c);
327 scoped_anum tmp(_am);
328 for (unsigned i = 0; i < n; i++) {
329 if (is_rational(c, a[i])) {
330 _am.set(tmp, get_rational(c, a[i]).to_mpq());
331 as.push_back(tmp);
332 }
333 else if (is_irrational(c, a[i])) {
334 as.push_back(get_irrational(c, a[i]));
335 }
336 else {
337 return false;
338 }
339 }
340 return true;
341 }
342
343 class vector_var2anum : public polynomial::var2anum {
344 scoped_anum_vector const & m_as;
345 public:
vector_var2anum(scoped_anum_vector & as)346 vector_var2anum(scoped_anum_vector & as):m_as(as) {}
~vector_var2anum()347 virtual ~vector_var2anum() {}
m() const348 algebraic_numbers::manager & m() const override { return m_as.m(); }
contains(polynomial::var x) const349 bool contains(polynomial::var x) const override { return static_cast<unsigned>(x) < m_as.size(); }
operator ()(polynomial::var x) const350 algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); }
351 };
352
Z3_algebraic_roots(Z3_context c,Z3_ast p,unsigned n,Z3_ast a[])353 Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
354 Z3_TRY;
355 LOG_Z3_algebraic_roots(c, p, n, a);
356 RESET_ERROR_CODE();
357 polynomial::manager & pm = mk_c(c)->pm();
358 polynomial_ref _p(pm);
359 polynomial::scoped_numeral d(pm.m());
360 expr2polynomial converter(mk_c(c)->m(), pm, nullptr, true);
361 if (!converter.to_polynomial(to_expr(p), _p, d) ||
362 static_cast<unsigned>(max_var(_p)) >= n + 1) {
363 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
364 return nullptr;
365 }
366 algebraic_numbers::manager & _am = am(c);
367 scoped_anum_vector as(_am);
368 if (!to_anum_vector(c, n, a, as)) {
369 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
370 return nullptr;
371 }
372 scoped_anum_vector roots(_am);
373 {
374 cancel_eh<reslimit> eh(mk_c(c)->m().limit());
375 api::context::set_interruptable si(*(mk_c(c)), eh);
376 scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
377 vector_var2anum v2a(as);
378 _am.isolate_roots(_p, v2a, roots);
379 }
380 Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
381 mk_c(c)->save_object(result);
382 for (unsigned i = 0; i < roots.size(); i++) {
383 result->m_ast_vector.push_back(au(c).mk_numeral(_am, roots.get(i), false));
384 }
385 RETURN_Z3(of_ast_vector(result));
386 Z3_CATCH_RETURN(nullptr);
387 }
388
Z3_algebraic_eval(Z3_context c,Z3_ast p,unsigned n,Z3_ast a[])389 int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
390 Z3_TRY;
391 LOG_Z3_algebraic_eval(c, p, n, a);
392 RESET_ERROR_CODE();
393 polynomial::manager & pm = mk_c(c)->pm();
394 polynomial_ref _p(pm);
395 polynomial::scoped_numeral d(pm.m());
396 expr2polynomial converter(mk_c(c)->m(), pm, nullptr, true);
397 if (!converter.to_polynomial(to_expr(p), _p, d) ||
398 static_cast<unsigned>(max_var(_p)) >= n) {
399 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
400 return 0;
401 }
402 algebraic_numbers::manager & _am = am(c);
403 scoped_anum_vector as(_am);
404 if (!to_anum_vector(c, n, a, as)) {
405 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
406 return 0;
407 }
408 {
409 cancel_eh<reslimit> eh(mk_c(c)->m().limit());
410 api::context::set_interruptable si(*(mk_c(c)), eh);
411 scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
412 vector_var2anum v2a(as);
413 int r = _am.eval_sign_at(_p, v2a);
414 if (r > 0) return 1;
415 else if (r < 0) return -1;
416 else return 0;
417 }
418 Z3_CATCH_RETURN(0);
419 }
420
Z3_algebraic_get_poly(Z3_context c,Z3_ast a)421 Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a) {
422 Z3_TRY;
423 LOG_Z3_algebraic_get_poly(c, a);
424 RESET_ERROR_CODE();
425 CHECK_IS_ALGEBRAIC(a, 0);
426 algebraic_numbers::manager & _am = am(c);
427 algebraic_numbers::anum const & av = get_irrational(c, a);
428 scoped_mpz_vector coeffs(_am.qm());
429 _am.get_polynomial(av, coeffs);
430 api::context& _c = *mk_c(c);
431 sort * s = _c.m().mk_sort(_c.get_arith_fid(), REAL_SORT);
432 Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, _c, _c.m());
433 _c.save_object(result);
434 for (auto const& c : coeffs) {
435 result->m_ast_vector.push_back(_c.mk_numeral_core(c, s));
436 }
437 RETURN_Z3(of_ast_vector(result));
438 Z3_CATCH_RETURN(nullptr);
439 }
440
Z3_algebraic_get_i(Z3_context c,Z3_ast a)441 unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a) {
442 Z3_TRY;
443 LOG_Z3_algebraic_get_i(c, a);
444 RESET_ERROR_CODE();
445 CHECK_IS_ALGEBRAIC(a, 0);
446 algebraic_numbers::manager & _am = am(c);
447 algebraic_numbers::anum const & av = get_irrational(c, a);
448 return _am.get_i(av);
449 Z3_CATCH_RETURN(0);
450 }
451 };
452