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