| 548 | } |
| 549 | |
| 550 | bool FloatType::isNaNInt(const expr &e) const { |
| 551 | if (!e.isValid()) |
| 552 | return false; |
| 553 | |
| 554 | // expr var = s.getFreshNondetVar("#NaN", expr::mkUInt(0, 2)); |
| 555 | // var.sign().concat(expr::mkInt(-1, exp_bits)).concat(fraction) |
| 556 | auto bw = bits(); |
| 557 | |
| 558 | expr exponent = e.extract(bw - 2, fractionBits()); |
| 559 | assert(exponent.bits() == expBits()); |
| 560 | |
| 561 | expr nan; |
| 562 | unsigned h, l; |
| 563 | return exponent.isAllOnes() && |
| 564 | e.sign().isExtract(nan, h, l) && |
| 565 | h == 1 && h == 1 && |
| 566 | nan.fn_name().starts_with("#NaN"); |
| 567 | } |
| 568 | |
| 569 | expr FloatType::sizeVar() const { |
| 570 | return defined ? expr::mkUInt(bits(), var_bw_bits) : Type::sizeVar(); |