Method BV2float

smt/expr.cpp:2016–2025

}

expr expr::BV2float(const expr &type) const {
  C(type);
  if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) {
    expr arg = Z3_get_app_arg(ctx(), app, 0);
    if (arg.sort() == type.sort())
      return arg;
  }

  return simplify_const(Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort()), *this);
}

expr expr::float2Float(const expr &type, const expr &rm) const {
  C(type, rm);