Method getFloat

ir/type.cpp:433–449

}

expr FloatType::getFloat(const expr &v) const {
  expr ty = getDummyFloat();

  if (isNaNInt(v))
    return expr::mkNaN(ty);

  expr cond, then, els, n, n2;
  // match (ite (isNaN x) int_nan (fp.to_ieee_bv x))
  if (v.isIf(cond, then, els) &&
      cond.isNaNCheck(n) &&
      isNaNInt(then) &&
      els.isfloat2BV(n2) &&
      n.eq(n2))
    return n;

  return v.BV2float(ty);
}

expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0,
                          unsigned nary, const expr &a, const expr &b,