| 620 | } |
| 621 | |
| 622 | bool expr::isIsFPZero() const { |
| 623 | if (isBV()) { |
| 624 | // extract(bits()-2, 0) == 0 |
| 625 | expr lhs, rhs, v; |
| 626 | unsigned high, low; |
| 627 | return isEq(lhs, rhs) && |
| 628 | lhs.isExtract(v, high, low) && |
| 629 | high == bits()-2 && low == 0 && |
| 630 | rhs.isZero(); |
| 631 | } |
| 632 | return isAppOf(Z3_OP_FPA_IS_ZERO); |
| 633 | } |
| 634 | |
| 635 | bool expr::isNaNCheck(expr &fp) const { |
| 636 | if (auto app = isAppOf(Z3_OP_FPA_IS_NAN)) { |
no test coverage detected