1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_numeral.cpp
7 
8 Abstract:
9     API for handling numerals in Z3
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-02-29.
14 
15 Revision History:
16 
17 --*/
18 #include<cmath>
19 #include<iostream>
20 #include "api/z3.h"
21 #include "api/api_log_macros.h"
22 #include "api/api_context.h"
23 #include "api/api_util.h"
24 #include "ast/arith_decl_plugin.h"
25 #include "ast/bv_decl_plugin.h"
26 #include "math/polynomial/algebraic_numbers.h"
27 #include "ast/fpa_decl_plugin.h"
28 
is_numeral_sort(Z3_context c,Z3_sort ty)29 bool is_numeral_sort(Z3_context c, Z3_sort ty) {
30     if (!ty) return false;
31     sort * _ty = to_sort(ty);
32     family_id fid  = _ty->get_family_id();
33     if (fid != mk_c(c)->get_arith_fid() &&
34         fid != mk_c(c)->get_bv_fid() &&
35         fid != mk_c(c)->get_datalog_fid() &&
36         fid != mk_c(c)->get_fpa_fid()) {
37         return false;
38     }
39     return true;
40 }
41 
check_numeral_sort(Z3_context c,Z3_sort ty)42 static bool check_numeral_sort(Z3_context c, Z3_sort ty) {
43     bool is_num = is_numeral_sort(c, ty);
44     if (!is_num) {
45         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
46     }
47     return is_num;
48 }
49 
50 extern "C" {
51 
Z3_mk_numeral(Z3_context c,const char * n,Z3_sort ty)52     Z3_ast Z3_API Z3_mk_numeral(Z3_context c, const char* n, Z3_sort ty) {
53         Z3_TRY;
54         LOG_Z3_mk_numeral(c, n, ty);
55         RESET_ERROR_CODE();
56         if (!check_numeral_sort(c, ty)) {
57             RETURN_Z3(nullptr);
58         }
59         if (!n) {
60             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
61             RETURN_Z3(nullptr);
62         }
63         sort * _ty = to_sort(ty);
64         bool is_float = mk_c(c)->fpautil().is_float(_ty);
65         char const* m = n;
66         while (*m) {
67             if (!(('0' <= *m && *m <= '9') ||
68                 ('/' == *m) || ('-' == *m) ||
69                 (' ' == *m) || ('\n' == *m) ||
70                 ('.' == *m) || ('e' == *m) ||
71                 ('E' == *m) || ('+' == *m) ||
72                 (is_float &&
73                     (('p' == *m) ||
74                      ('P' == *m))))) {
75                 SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr);
76                 RETURN_Z3(nullptr);
77             }
78             ++m;
79         }
80         ast * a = nullptr;
81         if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) {
82             // avoid expanding floats into huge rationals.
83             fpa_util & fu = mk_c(c)->fpautil();
84             scoped_mpf t(fu.fm());
85             fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_NEAREST_TEVEN, n);
86             a = fu.mk_value(t);
87             mk_c(c)->save_ast_trail(a);
88         }
89         else
90             a = mk_c(c)->mk_numeral_core(rational(n), _ty);
91         RETURN_Z3(of_ast(a));
92         Z3_CATCH_RETURN(nullptr);
93     }
94 
Z3_mk_int(Z3_context c,int value,Z3_sort ty)95     Z3_ast Z3_API Z3_mk_int(Z3_context c, int value, Z3_sort ty) {
96         Z3_TRY;
97         LOG_Z3_mk_int(c, value, ty);
98         RESET_ERROR_CODE();
99         if (!check_numeral_sort(c, ty)) {
100             RETURN_Z3(nullptr);
101         }
102         ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
103         RETURN_Z3(of_ast(a));
104         Z3_CATCH_RETURN(nullptr);
105     }
106 
Z3_mk_unsigned_int(Z3_context c,unsigned value,Z3_sort ty)107     Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned value, Z3_sort ty) {
108         Z3_TRY;
109         LOG_Z3_mk_unsigned_int(c, value, ty);
110         RESET_ERROR_CODE();
111         if (!check_numeral_sort(c, ty)) {
112             RETURN_Z3(nullptr);
113         }
114         ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
115         RETURN_Z3(of_ast(a));
116         Z3_CATCH_RETURN(nullptr);
117     }
118 
Z3_mk_int64(Z3_context c,int64_t value,Z3_sort ty)119     Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t value, Z3_sort ty) {
120         Z3_TRY;
121         LOG_Z3_mk_int64(c, value, ty);
122         RESET_ERROR_CODE();
123         if (!check_numeral_sort(c, ty)) {
124             RETURN_Z3(nullptr);
125         }
126         rational n(value, rational::i64());
127         ast* a = mk_c(c)->mk_numeral_core(n, to_sort(ty));
128         RETURN_Z3(of_ast(a));
129         Z3_CATCH_RETURN(nullptr);
130     }
131 
Z3_mk_unsigned_int64(Z3_context c,uint64_t value,Z3_sort ty)132     Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t value, Z3_sort ty) {
133         Z3_TRY;
134         LOG_Z3_mk_unsigned_int64(c, value, ty);
135         RESET_ERROR_CODE();
136         if (!check_numeral_sort(c, ty)) {
137             RETURN_Z3(nullptr);
138         }
139         rational n(value, rational::ui64());
140         ast * a = mk_c(c)->mk_numeral_core(n, to_sort(ty));
141         RETURN_Z3(of_ast(a));
142         Z3_CATCH_RETURN(nullptr);
143     }
144 
Z3_is_numeral_ast(Z3_context c,Z3_ast a)145     bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
146         Z3_TRY;
147         LOG_Z3_is_numeral_ast(c, a);
148         RESET_ERROR_CODE();
149         CHECK_IS_EXPR(a, false);
150         expr* e = to_expr(a);
151         return
152             mk_c(c)->autil().is_numeral(e) ||
153             mk_c(c)->bvutil().is_numeral(e) ||
154             mk_c(c)->fpautil().is_numeral(e) ||
155             mk_c(c)->fpautil().is_rm_numeral(e) ||
156             mk_c(c)->datalog_util().is_numeral_ext(e);
157         Z3_CATCH_RETURN(false);
158     }
159 
Z3_get_numeral_rational(Z3_context c,Z3_ast a,rational & r)160     bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r) {
161         Z3_TRY;
162         // This function is not part of the public API
163         RESET_ERROR_CODE();
164         CHECK_IS_EXPR(a, false);
165         expr* e = to_expr(a);
166         if (mk_c(c)->autil().is_numeral(e, r)) {
167             return true;
168         }
169         unsigned bv_size;
170         if (mk_c(c)->bvutil().is_numeral(e, r, bv_size)) {
171             return true;
172         }
173         uint64_t v;
174         if (mk_c(c)->datalog_util().is_numeral(e, v)) {
175             r = rational(v, rational::ui64());
176             return true;
177         }
178         return false;
179         Z3_CATCH_RETURN(false);
180     }
181 
182 
Z3_get_numeral_binary_string(Z3_context c,Z3_ast a)183     Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a) {
184         Z3_TRY;
185         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
186         LOG_Z3_get_numeral_binary_string(c, a);
187         RESET_ERROR_CODE();
188         CHECK_IS_EXPR(a, "");
189         rational r;
190         bool ok = Z3_get_numeral_rational(c, a, r);
191         if (ok && r.is_int() && !r.is_neg()) {
192             std::stringstream strm;
193             r.display_bin(strm, r.get_num_bits());
194             return mk_c(c)->mk_external_string(strm.str());
195         }
196         else {
197             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
198             return "";
199         }
200         Z3_CATCH_RETURN("");
201 
202     }
203 
Z3_get_numeral_string(Z3_context c,Z3_ast a)204     Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a) {
205         Z3_TRY;
206         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
207         LOG_Z3_get_numeral_string(c, a);
208         RESET_ERROR_CODE();
209         CHECK_IS_EXPR(a, "");
210         rational r;
211         bool ok = Z3_get_numeral_rational(c, a, r);
212         if (ok) {
213             return mk_c(c)->mk_external_string(r.to_string());
214         }
215         else {
216             fpa_util & fu = mk_c(c)->fpautil();
217             scoped_mpf tmp(fu.fm());
218             mpf_rounding_mode rm;
219             if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
220                 switch (rm) {
221                 case MPF_ROUND_NEAREST_TEVEN:
222                     return mk_c(c)->mk_external_string("roundNearestTiesToEven");
223                     break;
224                 case MPF_ROUND_NEAREST_TAWAY:
225                     return mk_c(c)->mk_external_string("roundNearestTiesToAway");
226                     break;
227                 case MPF_ROUND_TOWARD_POSITIVE:
228                     return mk_c(c)->mk_external_string("roundTowardPositive");
229                     break;
230                 case MPF_ROUND_TOWARD_NEGATIVE:
231                     return mk_c(c)->mk_external_string("roundTowardNegative");
232                     break;
233                 case MPF_ROUND_TOWARD_ZERO:
234                 default:
235                     return mk_c(c)->mk_external_string("roundTowardZero");
236                     break;
237                 }
238             }
239             else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
240                 std::ostringstream buffer;
241                 fu.fm().display_smt2(buffer, tmp, false);
242                 return mk_c(c)->mk_external_string(buffer.str());
243             }
244             else {
245                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
246                 return "";
247             }
248         }
249         Z3_CATCH_RETURN("");
250     }
251 
Z3_get_numeral_double(Z3_context c,Z3_ast a)252     double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a) {
253         LOG_Z3_get_numeral_double(c, a);
254         RESET_ERROR_CODE();
255         if (!is_expr(a)) {
256             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
257             return NAN;
258         }
259         expr* e = to_expr(a);
260         fpa_util & fu = mk_c(c)->fpautil();
261         scoped_mpf tmp(fu.fm());
262         if (mk_c(c)->fpautil().is_numeral(e, tmp)) {
263             if (tmp.get().get_ebits() > 11 ||
264                 tmp.get().get_sbits() > 53) {
265                 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
266                 return NAN;
267             }
268             return fu.fm().to_double(tmp);
269         }
270         rational r;
271         arith_util & u = mk_c(c)->autil();
272         if (u.is_numeral(e, r)) {
273             return r.get_double();
274         }
275         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
276         return 0.0;
277     }
278 
Z3_get_numeral_decimal_string(Z3_context c,Z3_ast a,unsigned precision)279     Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision) {
280         Z3_TRY;
281         LOG_Z3_get_numeral_decimal_string(c, a, precision);
282         RESET_ERROR_CODE();
283         CHECK_IS_EXPR(a, "");
284         expr* e = to_expr(a);
285         rational r;
286         arith_util & u = mk_c(c)->autil();
287         fpa_util & fu = mk_c(c)->fpautil();
288         scoped_mpf ftmp(fu.fm());
289         mpf_rounding_mode rm;
290         if (u.is_numeral(e, r) && !r.is_int()) {
291             std::ostringstream buffer;
292             r.display_decimal(buffer, precision);
293             return mk_c(c)->mk_external_string(buffer.str());
294         }
295         if (u.is_irrational_algebraic_numeral(e)) {
296             algebraic_numbers::anum const & n = u.to_irrational_algebraic_numeral(e);
297             algebraic_numbers::manager & am   = u.am();
298             std::ostringstream buffer;
299             am.display_decimal(buffer, n, precision);
300             return mk_c(c)->mk_external_string(buffer.str());
301         }
302         else if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm))
303             return Z3_get_numeral_string(c, a);
304         else if (mk_c(c)->fpautil().is_numeral(to_expr(a), ftmp)) {
305             std::ostringstream buffer;
306             fu.fm().display_decimal(buffer, ftmp, 12);
307             return mk_c(c)->mk_external_string(buffer.str());
308         }
309         else if (Z3_get_numeral_rational(c, a, r)) {
310             return mk_c(c)->mk_external_string(r.to_string());
311         }
312         else {
313             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
314             return "";
315         }
316         Z3_CATCH_RETURN("");
317     }
318 
Z3_get_numeral_small(Z3_context c,Z3_ast a,int64_t * num,int64_t * den)319     bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den) {
320         Z3_TRY;
321         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
322         LOG_Z3_get_numeral_small(c, a, num, den);
323         RESET_ERROR_CODE();
324         CHECK_IS_EXPR(a, false);
325         rational r;
326         bool ok = Z3_get_numeral_rational(c, a, r);
327         if (ok) {
328             rational n = numerator(r);
329             rational d = denominator(r);
330             if (n.is_int64() && d.is_int64()) {
331                 *num = n.get_int64();
332                 *den = d.get_int64();
333                 return true;
334             }
335             else {
336                 return false;
337             }
338         }
339         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
340         return false;
341         Z3_CATCH_RETURN(false);
342     }
343 
344 
Z3_get_numeral_int(Z3_context c,Z3_ast v,int * i)345     bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i) {
346         Z3_TRY;
347         // This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
348         LOG_Z3_get_numeral_int(c, v, i);
349         RESET_ERROR_CODE();
350         CHECK_IS_EXPR(v, false);
351         if (!i) {
352             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
353             return false;
354         }
355         int64_t l;
356         if (Z3_get_numeral_int64(c, v, &l) && l >= INT_MIN && l <= INT_MAX) {
357             *i = static_cast<int>(l);
358             return true;
359         }
360         return false;
361         Z3_CATCH_RETURN(false);
362     }
363 
Z3_get_numeral_uint(Z3_context c,Z3_ast v,unsigned * u)364     bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u) {
365         Z3_TRY;
366         // This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
367         LOG_Z3_get_numeral_uint(c, v, u);
368         RESET_ERROR_CODE();
369         CHECK_IS_EXPR(v, false);
370         if (!u) {
371             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
372             return false;
373         }
374         uint64_t l;
375         if (Z3_get_numeral_uint64(c, v, &l) && (l <= 0xFFFFFFFF)) {
376             *u = static_cast<unsigned>(l);
377             return true;
378         }
379         return false;
380         Z3_CATCH_RETURN(false);
381     }
382 
Z3_get_numeral_uint64(Z3_context c,Z3_ast v,uint64_t * u)383     bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u) {
384         Z3_TRY;
385         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
386         LOG_Z3_get_numeral_uint64(c, v, u);
387         RESET_ERROR_CODE();
388         CHECK_IS_EXPR(v, false);
389         if (!u) {
390             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
391             return false;
392         }
393         rational r;
394         bool ok = Z3_get_numeral_rational(c, v, r);
395         SASSERT(u);
396         if (ok && r.is_uint64()) {
397             *u = r.get_uint64();
398             return ok;
399         }
400         return false;
401         Z3_CATCH_RETURN(false);
402     }
403 
Z3_get_numeral_int64(Z3_context c,Z3_ast v,int64_t * i)404     bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i) {
405         Z3_TRY;
406         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
407         LOG_Z3_get_numeral_int64(c, v, i);
408         RESET_ERROR_CODE();
409         CHECK_IS_EXPR(v, false);
410         if (!i) {
411             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
412             return false;
413         }
414         rational r;
415         bool ok = Z3_get_numeral_rational(c, v, r);
416         if (ok && r.is_int64()) {
417             *i = r.get_int64();
418             return ok;
419         }
420         return false;
421         Z3_CATCH_RETURN(false);
422     }
423 
Z3_get_numeral_rational_int64(Z3_context c,Z3_ast v,int64_t * num,int64_t * den)424     bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den) {
425         Z3_TRY;
426         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
427         LOG_Z3_get_numeral_rational_int64(c, v, num, den);
428         RESET_ERROR_CODE();
429         CHECK_IS_EXPR(v, false);
430         if (!num || !den) {
431             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
432             return false;
433         }
434         rational r;
435         bool ok = Z3_get_numeral_rational(c, v, r);
436         if (ok != true) {
437             return ok;
438         }
439         rational n = numerator(r);
440         rational d = denominator(r);
441         if (n.is_int64() && d.is_int64()) {
442             *num = n.get_int64();
443             *den = d.get_int64();
444             return ok;
445         }
446         return false;
447         Z3_CATCH_RETURN(false);
448     }
449 
Z3_mk_bv_numeral(Z3_context c,unsigned sz,bool const * bits)450     Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits) {
451         Z3_TRY;
452         LOG_Z3_mk_bv_numeral(c, sz, bits);
453         RESET_ERROR_CODE();
454         rational r(0);
455         for (unsigned i = 0; i < sz; ++i) {
456             if (bits[i]) r += rational::power_of_two(i);
457         }
458         ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
459         RETURN_Z3(of_ast(a));
460         Z3_CATCH_RETURN(nullptr);
461     }
462 
463 };
464