mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Bugfix for fp.to_ieee_bv for unspecified input/output.
This commit is contained in:
parent
5463167a84
commit
176782d62b
|
@ -2925,11 +2925,22 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
mk_ite(c1, v1, v2, result);
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned width) {
|
||||
if (m_hi_fp_unspecified)
|
||||
return expr_ref(m_bv_util.mk_numeral(0, width), m);
|
||||
else
|
||||
return expr_ref(m_util.mk_internal_to_ieee_bv_unspecified(width), m);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 1);
|
||||
expr_ref x(m), x_is_nan(m);
|
||||
expr * sgn, * s, * e;
|
||||
split_fp(args[0], sgn, e, s);
|
||||
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
|
||||
x = args[0];
|
||||
split_fp(x, sgn, e, s);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
result = m.mk_ite(x_is_nan, mk_to_ieee_bv_unspecified(m_bv_util.get_bv_size(x)),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
|
||||
|
|
|
@ -136,6 +136,7 @@ public:
|
|||
|
||||
expr_ref mk_to_ubv_unspecified(unsigned width);
|
||||
expr_ref mk_to_sbv_unspecified(unsigned width);
|
||||
expr_ref mk_to_ieee_bv_unspecified(unsigned width);
|
||||
expr_ref mk_to_real_unspecified();
|
||||
|
||||
void reset(void);
|
||||
|
|
|
@ -157,7 +157,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
case OP_FPA_INTERNAL_BVUNWRAP:
|
||||
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
|
||||
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
|
||||
return BR_FAILED;
|
||||
default:
|
||||
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
|
||||
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
|
||||
|
|
|
@ -1060,7 +1060,7 @@ app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) {
|
|||
app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) {
|
||||
parameter ps[] = { parameter(width) };
|
||||
sort * range = m_bv_util.mk_sort(width);
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range);
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range);
|
||||
}
|
||||
|
||||
app * fpa_util::mk_internal_to_real_unspecified() {
|
||||
|
|
|
@ -107,6 +107,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break;
|
||||
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break;
|
||||
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
|
||||
SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break;
|
||||
|
||||
case OP_FPA_INTERNAL_BVWRAP:
|
||||
case OP_FPA_INTERNAL_BVUNWRAP:
|
||||
|
|
Loading…
Reference in a new issue