mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Added int to float conversion.
This commit is contained in:
parent
a792790882
commit
9cbf45f689
|
@ -1878,6 +1878,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
else if (num == 2 &&
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_bv_util.get_bv_size(args[0]) == 3 &&
|
||||
m_arith_util.is_int(args[1]) ||
|
||||
m_arith_util.is_real(args[1])) {
|
||||
// rm + real -> float
|
||||
mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
|
||||
|
@ -2066,7 +2067,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl <<
|
||||
"x: " << mk_ismt2_pp(x, m) << std::endl;);
|
||||
SASSERT(m_util.is_float(s));
|
||||
SASSERT(au().is_real(x));
|
||||
SASSERT(au().is_real(x) || au().is_int(x));
|
||||
|
||||
unsigned ebits = m_util.get_ebits(s);
|
||||
unsigned sbits = m_util.get_sbits(s);
|
||||
|
@ -2089,7 +2090,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
}
|
||||
|
||||
rational q;
|
||||
m_util.au().is_numeral(x, q);
|
||||
bool is_int;
|
||||
m_util.au().is_numeral(x, q, is_int);
|
||||
|
||||
scoped_mpf v(m_mpf_manager);
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
|
||||
|
|
|
@ -521,14 +521,26 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
|
|||
symbol name("to_fp");
|
||||
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
else if (arity == 2 &&
|
||||
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
|
||||
is_sort_of(domain[1], m_arith_fid, INT_SORT)) {
|
||||
// Rounding + 1 Int -> 1 FP
|
||||
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
|
||||
m_manager->raise_exception("expecting two integer parameters to to_fp");
|
||||
|
||||
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
|
||||
symbol name("to_fp");
|
||||
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
else {
|
||||
m_manager->raise_exception("Unexpected argument combination for (_ to_fp eb sb). Supported argument combinations are: "
|
||||
"((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)),"
|
||||
"(_ BitVec (eb+sb)),"
|
||||
"(Real),"
|
||||
"(RoundingMode (_ BitVec (eb+sb))),"
|
||||
"(RoundingMode (_ FloatingPoint eb' sb')),"
|
||||
"(RoundingMode Real Int), and"
|
||||
"((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)), "
|
||||
"(_ BitVec (eb+sb)), "
|
||||
"(Real), "
|
||||
"(RoundingMode (_ BitVec (eb+sb))), "
|
||||
"(RoundingMode (_ FloatingPoint eb' sb')), "
|
||||
"(RoundingMode Real Int), "
|
||||
"(RoundingMode Int), and "
|
||||
"(RoundingMode Real)."
|
||||
);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue