| 597 | } |
| 598 | |
| 599 | bool expr::isFPNeg(expr &val) const { |
| 600 | if (isBV()) { |
| 601 | // extract(signbit, signbit) ^ 1).concat(extract(signbit-1, 0)) |
| 602 | expr sign, rest, a, b, val, val2; |
| 603 | unsigned high, high2, low; |
| 604 | auto check_not = [&](const expr &a, const expr &b) { |
| 605 | unsigned l; |
| 606 | return a.isExtract(val, high, l) && b.isAllOnes() && b.bits() == 1; |
| 607 | }; |
| 608 | return isConcat(sign, rest) && |
| 609 | sign.isBinOp(a, b, Z3_OP_BXOR) && |
| 610 | (check_not(a, b) || check_not(b, a)) && |
| 611 | rest.isExtract(val2, high2, low) && |
| 612 | low == 0 && high2 == high - 1 && |
| 613 | val.eq(val2); |
| 614 | } |
| 615 | return isUnOp(val, Z3_OP_FPA_NEG); |
| 616 | } |
| 617 | |
| 618 | bool expr::isFAbs(expr &val) const { |
| 619 | return isUnOp(val, Z3_OP_FPA_ABS); |