Method fromFloat

ir/type.cpp:451–518

}

expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0,
                          unsigned nary, const expr &a, const expr &b,
                          const expr &c) const {
  expr isnan = fp.isNaN();
  expr val = fp.float2BV();

  if (isnan.isFalse())
    return val;

  unsigned fraction_bits = fractionBits();

  // sign bit, exponent (-1), qnan bit (1) or snan (0), rest of fraction
  expr var = s.getFreshNondetVar("#NaN", expr::mkUInt(0, 2));

  ChoiceExpr<expr> exprs;

  // 1) preferred QNaN (1000..00)
  exprs.add(expr::mkUInt(1, 1).concat_zeros(fraction_bits-1), expr(true));

  // 2) input NaN
  // 3) quieted input NaN
  const FloatType *from_type = from_type0.getAsFloatType();

  auto add_maybe_quiet = [&](const expr &e) {
    // account for fpext/fptruc
    auto orig_bw = from_type->fractionBits();
    expr fraction = e.trunc(orig_bw);
    expr truncated_is_nan = true;

    if (orig_bw > fraction_bits) {
      fraction = fraction.extract(orig_bw-1, orig_bw - fraction_bits);
      truncated_is_nan = fraction != 0;
    } else if (orig_bw < fraction_bits) {
      fraction = fraction.concat_zeros(fraction_bits - fraction.bits());
    }
    assert(!fraction.isValid() || fraction.bits() == fraction_bits);

    expr qnan = fraction.sign();
    expr quieted = var.extract(0, 0);
    qnan = expr::mkIf(truncated_is_nan, qnan | quieted, expr::mkUInt(1, 1));
    exprs.add(qnan.concat(fraction.trunc(fraction_bits - 1)),
              from_type->getFloat(e).isNaN());
  };
  if (nary >= 1) {
    add_maybe_quiet(a);
    if (nary >= 2) {
      add_maybe_quiet(b);
      if (nary >= 3)
        add_maybe_quiet(c);
    }
  }

  // 4) target specific preferred QNaN (a set, possibly empty)
  // approximated by adding just one more value
  auto preferred_qnan_fraction
    = expr::mkVar("#preferred_qnan", expr::mkUInt(0, fraction_bits - 1));
  exprs.add(expr::mkUInt(1, 1).concat(preferred_qnan_fraction), expr(true));