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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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