mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-22 20:32:05 +00:00
Code Activity

Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-02-03 16:48:05 +00:00
parent c3ed986031
commit 333374229d
2 changed files with 21 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -3098,13 +3098,11 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
join_fp(result, result); join_fp(result, result);
} }
else { else {
expr * n = args[0]; expr_ref nw = nan_wrap(args[0]);
expr_ref n_bv(m);
join_fp(n, n_bv);
sort * domain[1] = { m.get_sort(n_bv) }; sort * domain[1] = { m.get_sort(nw) };
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
result = m.mk_app(f_bv, n_bv); result = m.mk_app(f_bv, nw);
expr_ref exp_bv(m), exp_all_ones(m); expr_ref exp_bv(m), exp_all_ones(m);
exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
@ -3280,6 +3278,17 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
mk_to_bv(f, num, args, true, result); mk_to_bv(f, num, args, true, result);
} }
expr_ref fpa2bv_converter::nan_wrap(expr * n) {
expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m);
mk_is_nan(n, arg_is_nan);
mk_nan(m.get_sort(n), nan);
join_fp(nan, nan_bv);
join_fp(n, n_bv);
res = expr_ref(m.mk_ite(arg_is_nan, nan_bv, n_bv), m);
SASSERT(is_well_sorted(m, res));
return res;
}
void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2); SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0])); SASSERT(m_util.is_bv2rm(args[0]));
@ -3289,13 +3298,10 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr *
result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range())); result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range()));
else { else {
expr * rm_bv = to_app(args[0])->get_arg(0); expr * rm_bv = to_app(args[0])->get_arg(0);
expr * n = args[1]; expr_ref nw = nan_wrap(args[1]);
expr_ref n_bv(m); sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(nw) };
join_fp(n, n_bv);
sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) };
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
result = m.mk_app(f_bv, rm_bv, n_bv); result = m.mk_app(f_bv, rm_bv, nw);
} }
TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
@ -3309,12 +3315,10 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
result = m_arith_util.mk_numeral(rational(0), false); result = m_arith_util.mk_numeral(rational(0), false);
else { else {
expr * n = args[0]; expr * n = args[0];
expr_ref n_bv(m); expr_ref nw = nan_wrap(n);
join_fp(n, n_bv); sort * domain[1] = { m.get_sort(nw) };
sort * domain[1] = { m.get_sort(n_bv) };
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
result = m.mk_app(f_bv, n_bv); result = m.mk_app(f_bv, nw);
} }
} }

1
src/ast/fpa/fpa2bv_converter.h
View file

@ -219,6 +219,7 @@ private:
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range); func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
expr_ref nan_wrap(expr * n);
}; };
#endif #endif