mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa.
Fixes #68
This commit is contained in:
parent
8a026c355f
commit
de39173f6f
|
@ -137,8 +137,10 @@ public:
|
|||
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
|
||||
expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
|
||||
expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
|
||||
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
expr_ref mk_to_ubv_unspecified(unsigned width);
|
||||
expr_ref mk_to_sbv_unspecified(unsigned width);
|
||||
expr_ref mk_to_real_unspecified();
|
||||
|
|
|
@ -166,8 +166,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_BVWRAP:
|
||||
case OP_FPA_INTERNAL_BVUNWRAP:
|
||||
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;
|
||||
|
|
|
@ -692,23 +692,27 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par
|
|||
func_decl * fpa_decl_plugin::mk_internal_min_unspecified(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
if (arity != 2)
|
||||
m_manager->raise_exception("invalid number of arguments to fp.min_unspecified");
|
||||
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
|
||||
m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts");
|
||||
if (!is_float_sort(range))
|
||||
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
|
||||
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
|
||||
|
||||
return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * fpa_decl_plugin::mk_internal_max_unspecified(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
if (arity != 2)
|
||||
m_manager->raise_exception("invalid number of arguments to fp.max_unspecified");
|
||||
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
|
||||
m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts");
|
||||
if (!is_float_sort(range))
|
||||
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
|
||||
|
||||
return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
|
||||
|
@ -1027,12 +1031,16 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
|
|||
return mk_value(v);
|
||||
}
|
||||
|
||||
app * fpa_util::mk_internal_min_unspecified(unsigned ebits, unsigned sbits) {
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits));
|
||||
app * fpa_util::mk_internal_min_unspecified(expr * x, expr * y) {
|
||||
SASSERT(m().get_sort(x) == m().get_sort(y));
|
||||
expr * args[] = { x, y };
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x));
|
||||
}
|
||||
|
||||
app * fpa_util::mk_internal_max_unspecified(unsigned ebits, unsigned sbits) {
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits));
|
||||
app * fpa_util::mk_internal_max_unspecified(expr * x, expr * y) {
|
||||
SASSERT(m().get_sort(x) == m().get_sort(y));
|
||||
expr * args[] = { x, y };
|
||||
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x));
|
||||
}
|
||||
|
||||
app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) {
|
||||
|
|
|
@ -338,8 +338,8 @@ public:
|
|||
|
||||
app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); }
|
||||
|
||||
app * mk_internal_min_unspecified(unsigned ebits, unsigned sbits);
|
||||
app * mk_internal_max_unspecified(unsigned ebits, unsigned sbits);
|
||||
app * mk_internal_min_unspecified(expr * x, expr * y);
|
||||
app * mk_internal_max_unspecified(expr * x, expr * y);
|
||||
app * mk_internal_to_ubv_unspecified(unsigned width);
|
||||
app * mk_internal_to_sbv_unspecified(unsigned width);
|
||||
app * mk_internal_to_ieee_bv_unspecified(unsigned width);
|
||||
|
|
|
@ -95,7 +95,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
|
||||
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
|
||||
SASSERT(num_args == 0); st = BR_FAILED; break;
|
||||
SASSERT(num_args == 2); st = BR_FAILED; break;
|
||||
|
||||
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
|
||||
SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break;
|
||||
|
@ -433,8 +433,11 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
|
||||
scoped_mpf v1(m_fm), v2(m_fm);
|
||||
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
|
||||
return BR_FAILED; // Result could be +zero or -zero.
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
|
||||
// Result could be +zero or -zero.
|
||||
result = m_util.mk_internal_min_unspecified(arg1, arg2);
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.minimum(v1, v2, r);
|
||||
|
@ -458,8 +461,11 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
|
||||
scoped_mpf v1(m_fm), v2(m_fm);
|
||||
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
|
||||
return BR_FAILED; // Result could be +zero or -zero.
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
|
||||
// Result could be +zero or -zero.
|
||||
result = m_util.mk_internal_max_unspecified(arg1, arg2);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.maximum(v1, v2, r);
|
||||
|
|
|
@ -82,7 +82,56 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
|
||||
// TODO: This introduces temporary variables/func_decls that should be filtered in the end.
|
||||
return fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
|
||||
}
|
||||
|
||||
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
|
||||
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
unsigned bv_sz = ebits + sbits;
|
||||
expr_ref res(m);
|
||||
|
||||
expr * args[] = { x, y };
|
||||
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range());
|
||||
expr_ref a(m), wrapped(m);
|
||||
a = m.mk_app(w, x, y);
|
||||
wrapped = m_th.wrap(a);
|
||||
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
|
||||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, wrapped),
|
||||
res);
|
||||
|
||||
expr_ref sc(m);
|
||||
m_th.m_converter.mk_is_zero(res, sc);
|
||||
m_extra_assertions.push_back(sc);
|
||||
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
|
||||
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
unsigned bv_sz = ebits + sbits;
|
||||
expr_ref res(m);
|
||||
|
||||
expr * args[] = { x, y };
|
||||
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range());
|
||||
expr_ref a(m), wrapped(m);
|
||||
a = m.mk_app(w, x, y);
|
||||
wrapped = m_th.wrap(a);
|
||||
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
|
||||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, wrapped),
|
||||
res);
|
||||
|
||||
expr_ref sc(m);
|
||||
m_th.m_converter.mk_is_zero(res, sc);
|
||||
m_extra_assertions.push_back(sc);
|
||||
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
|
||||
return res;
|
||||
}
|
||||
|
||||
theory_fpa::theory_fpa(ast_manager & m) :
|
||||
|
|
|
@ -84,6 +84,9 @@ namespace smt {
|
|||
virtual void mk_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_rm_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
|
||||
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
};
|
||||
|
||||
class fpa_value_proc : public model_value_proc {
|
||||
|
|
Loading…
Reference in a new issue