mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Partial fix for fp,min/fp.max models

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-13 14:29:08 +01:00
parent e3ed0159a8
commit 099775947e
9 changed files with 115 additions and 148 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,7 +35,11 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_arith_util(m),
m_mpf_manager(m_util.fm()),
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_hi_fp_unspecified(true),
m_hi_fp_unspecified(true),
m_min_pn_zeros(0, m),
m_min_np_zeros(0, m),
m_max_pn_zeros(0, m),
m_max_np_zeros(0, m),
m_extra_assertions(m) {
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m.mk_family_id("fpa")));
}
@ -1064,7 +1068,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
mk_fp(m_bv_util.mk_numeral(0, 1), e, s, result);
}
void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
expr * x = args[0], * y = args[1];
@ -1086,16 +1090,11 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
expr_ref lt(m);
mk_float_lt(f, num, args, lt);
expr_ref zz(m);
zz = mk_min_unspecified(f, x, y);
TRACE("fpa2bv", tout << "min = " << mk_ismt2_pp(zz, m) << std::endl;);
mk_float_lt(f, num, args, lt);
result = y;
mk_ite(lt, x, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);
@ -1111,33 +1110,40 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
if (m_hi_fp_unspecified)
// The hardware interpretation is -0.0.
mk_nzero(f, res);
mk_nzero(f, res);
else {
app_ref pn_nondet(m), np_nondet(m);
pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert(pn_nondet->get_decl());
m_decls_to_hide.insert(np_nondet->get_decl());
if (m_min_pn_zeros.get() == 0) m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
if (m_min_np_zeros.get() == 0) m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
expr_ref pn(m), np(m);
mk_fp(pn_nondet,
mk_fp(m_min_pn_zeros,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(np_nondet,
mk_fp(m_min_np_zeros,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m);
expr_ref x_is_pzero(m), x_is_nzero(m), ite(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, ite);
expr * args[] = { x, y };
mk_uninterpreted_function(f, 2, args, res);
expr_ref pzero(m), nzero(m), extra(m);
mk_pzero(f, pzero);
mk_nzero(f, nzero);
extra = m.mk_or(m.mk_eq(ite, pzero), m.mk_eq(ite, nzero));
m_extra_assertions.push_back(extra);
}
return res;
}
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
expr * x = args[0], *y = args[1];
@ -1160,14 +1166,10 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
expr_ref gt(m);
mk_float_gt(f, num, args, gt);
expr_ref zz(m);
zz = mk_max_unspecified(f, x, y);
result = y;
mk_ite(gt, x, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);
@ -1185,21 +1187,19 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
// The hardware interpretation is +0.0.
mk_pzero(f, res);
else {
app_ref pn_nondet(m), np_nondet(m);
pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert(pn_nondet->get_decl());
m_decls_to_hide.insert(np_nondet->get_decl());
if (m_max_pn_zeros.get() == 0) m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
if (m_max_np_zeros.get() == 0) m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
expr_ref pn(m), np(m);
mk_fp(pn_nondet,
mk_fp(m_max_pn_zeros,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(np_nondet,
mk_fp(m_max_np_zeros,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);

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

@ -57,6 +57,11 @@ protected:
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
app_ref m_min_pn_zeros;
app_ref m_min_np_zeros;
app_ref m_max_pn_zeros;
app_ref m_max_np_zeros;
public:
fpa2bv_converter(ast_manager & m);
@ -102,8 +107,8 @@ public:
void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

12
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -141,9 +141,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
@ -166,8 +164,16 @@ 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_MIN:
case OP_FPA_MAX:
throw rewriter_exception("operator is not supported, you must simplify the goal before applying fpa2bv");
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_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:

49
src/ast/fpa_decl_plugin.cpp
View file

@ -359,6 +359,10 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters
case OP_FPA_REM: name = "fp.rem"; break;
case OP_FPA_MIN: name = "fp.min"; break;
case OP_FPA_MAX: name = "fp.max"; break;
case OP_FPA_INTERNAL_MIN_I: name = "fp.min_i"; break;
case OP_FPA_INTERNAL_MAX_I: name = "fp.max_i"; break;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break;
default:
UNREACHABLE();
break;
@ -689,32 +693,6 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par
return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
}
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 != 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");
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 != 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"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
@ -822,10 +800,13 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_BVUNWRAP:
return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
return mk_internal_min_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
return mk_internal_max_unspecified(k, num_parameters, parameters, arity, domain, range);
return mk_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
@ -1031,18 +1012,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
return mk_value(v);
}
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(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) {
parameter ps[] = { parameter(width) };
sort * range = m_bv_util.mk_sort(width);

11
src/ast/fpa_decl_plugin.h
View file

@ -86,7 +86,10 @@ enum fpa_op_kind {
/* Internal use only */
OP_FPA_INTERNAL_BVWRAP,
OP_FPA_INTERNAL_BVUNWRAP,
OP_FPA_INTERNAL_BVUNWRAP,
OP_FPA_INTERNAL_MIN_I,
OP_FPA_INTERNAL_MAX_I,
OP_FPA_INTERNAL_MIN_UNSPECIFIED,
OP_FPA_INTERNAL_MAX_UNSPECIFIED,
OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED,
@ -162,10 +165,6 @@ class fpa_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_min_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_max_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -338,8 +337,6 @@ 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(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);

58
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -93,6 +93,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
SASSERT(num_args == 2); st = BR_FAILED; break;
@ -432,21 +434,23 @@ 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)) {
// 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);
result = m_util.mk_value(r);
return BR_DONE;
}
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2) &&
!(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) {
scoped_mpf r(m_fm);
m_fm.minimum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
}
else {
expr_ref c(m()), v(m());
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
return BR_FAILED;
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_I, arg1, arg2));
return BR_REWRITE_FULL;
}
}
br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
@ -460,21 +464,23 @@ 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)) {
// 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);
result = m_util.mk_value(r);
return BR_DONE;
}
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2) &&
!(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) {
scoped_mpf r(m_fm);
m_fm.maximum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
}
else {
expr_ref c(m()), v(m());
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
return BR_FAILED;
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_I, arg1, arg2));
return BR_REWRITE_FULL;
}
}
br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {