| 455 | } |
| 456 | |
| 457 | bool expr::isInt(int64_t &n) const { |
| 458 | C(); |
| 459 | auto bw = bits(); |
| 460 | if (bw > 64 || !Z3_get_numeral_int64(ctx(), ast(), &n)) |
| 461 | return false; |
| 462 | |
| 463 | if (bw < 64) |
| 464 | n = (int64_t)((uint64_t)n << (64 - bw)) >> (64 - bw); |
| 465 | return true; |
| 466 | } |
| 467 | |
| 468 | bool expr::isSameTypeOf(const expr &other) const { |
| 469 | C(other); |