mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Corrected unspecified behavior of corner cases in fp.min/fp.max.

Browse source 
Partially addresses #68.
This commit is contained in:
Christoph M. Wintersteiger 2015-10-06 19:45:05 +01:00
parent 6e852762ba
commit 8a026c355f
10 changed files with 211 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1088,16 +1088,55 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
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;);
result = y;
mk_ite(lt, x, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
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);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref res(m);
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
if (m_hi_fp_unspecified)
// The hardware interpretation is -0.0.
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());
expr_ref pn(m), np(m);
mk_fp(pn_nondet,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(np_nondet,
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);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res);
}
return res;
}
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
@ -1121,17 +1160,55 @@ 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), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
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);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref res(m);
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
if (m_hi_fp_unspecified)
// 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());
expr_ref pn(m), np(m);
mk_fp(pn_nondet,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(np_nondet,
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);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res);
}
return res;
}
void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 4);

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

@ -55,7 +55,8 @@ protected:
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
public:
fpa2bv_converter(ast_manager & m);
@ -136,13 +137,16 @@ 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);
expr_ref mk_to_ubv_unspecified(unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned width);
expr_ref mk_to_real_unspecified();
obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
obj_hashtable<func_decl> const & decls_to_hide() const { return m_decls_to_hide; }
void reset(void);

2
src/ast/fpa/fpa2bv_rewriter_params.pyg
View file

@ -1,5 +1,5 @@
def_module_params(module_name='rewriter',
class_name='fpa2bv_rewriter_params',
export=True,
params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"),
params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.min, fp.max, fp.to_ubv, fp.to_sbv, and fp.to_real"),
))

34
src/ast/fpa_decl_plugin.cpp
View file

@ -689,6 +689,28 @@ 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 != 0)
m_manager->raise_exception("invalid number of arguments to fp.min_unspecified");
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"), 0, (sort*)0, 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)
m_manager->raise_exception("invalid number of arguments to fp.max_unspecified");
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));
}
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) {
@ -796,6 +818,10 @@ 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_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);
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:
@ -1001,6 +1027,14 @@ 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_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_to_ubv_unspecified(unsigned width) {
parameter ps[] = { parameter(width) };
sort * range = m_bv_util.mk_sort(width);

8
src/ast/fpa_decl_plugin.h
View file

@ -87,6 +87,8 @@ enum fpa_op_kind {
/* Internal use only */
OP_FPA_INTERNAL_BVWRAP,
OP_FPA_INTERNAL_BVUNWRAP,
OP_FPA_INTERNAL_MIN_UNSPECIFIED,
OP_FPA_INTERNAL_MAX_UNSPECIFIED,
OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED,
@ -160,6 +162,10 @@ 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,
@ -332,6 +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_to_ubv_unspecified(unsigned width);
app * mk_internal_to_sbv_unspecified(unsigned width);
app * mk_internal_to_ieee_bv_unspecified(unsigned width);

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

@ -93,6 +93,10 @@ 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_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
SASSERT(num_args == 0); st = BR_FAILED; break;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
@ -422,29 +426,24 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
result = arg2;
return BR_DONE;
}
if (m_util.is_nan(arg2)) {
else if (m_util.is_nan(arg2)) {
result = arg1;
return BR_DONE;
}
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = arg2;
return BR_DONE;
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.
else {
scoped_mpf r(m_fm);
m_fm.minimum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
}
}
result = m().mk_ite(mk_eq_nan(arg1),
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
// min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2,
m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1,
arg2)))));
return BR_REWRITE_FULL;
return BR_FAILED;
}
br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
@ -452,29 +451,24 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
result = arg2;
return BR_DONE;
}
if (m_util.is_nan(arg2)) {
else if (m_util.is_nan(arg2)) {
result = arg1;
return BR_DONE;
}
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = arg2;
return BR_DONE;
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.
else {
scoped_mpf r(m_fm);
m_fm.maximum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
}
}
result = m().mk_ite(mk_eq_nan(arg1),
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
// max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2,
m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1,
arg2)))));
return BR_REWRITE_FULL;
return BR_FAILED;
}
br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {

33
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -44,7 +44,12 @@ void fpa2bv_model_converter::display(std::ostream & out) {
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
}
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++) {
out << "\n to hide: " << mk_ismt2_pp(*it, m);
}
out << ")" << std::endl;
}
@ -70,6 +75,22 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
func_decl * k = translator(it->m_key);
func_decl * v = translator(it->m_value);
res->m_uf2bvuf.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++) {
func_decl * k = translator(*it);
res->m_decls_to_hide.insert(k);
translator.to().inc_ref(k);
}
return res;
}
@ -188,6 +209,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
obj_hashtable<func_decl> seen;
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++)
seen.insert(*it);
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
@ -329,6 +355,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf);
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide);
}

14
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -27,11 +27,13 @@ class fpa2bv_model_converter : public model_converter {
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf) :
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) :
m(m) {
// Just create a copy?
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
@ -58,12 +60,19 @@ public:
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_hashtable<func_decl>::iterator it = decls_to_hide.begin();
it != decls_to_hide.end();
it++) {
m_decls_to_hide.insert(*it);
m.inc_ref(*it);
}
}
virtual ~fpa2bv_model_converter() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
dec_ref_collection_values(m, m_decls_to_hide);
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
@ -96,6 +105,7 @@ protected:
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf);
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & m_decls_to_hide);
#endif

2
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -107,7 +107,7 @@ class fpa2bv_tactic : public tactic {
}
if (g->models_enabled())
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf());
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide());
g->inc_depth();
result.push_back(g.get());

18
src/util/mpf.cpp
View file

@ -1248,12 +1248,13 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) {
UNREACHABLE(); // max(+0, -0) and max(-0, +0) are unspecified.
}
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (gt(x, y))
set(o, x);
else
@ -1263,12 +1264,13 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) {
UNREACHABLE(); // min(+0, -0) and min(-0, +0) are unspecified.
}
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (lt(x, y))
set(o, x);
else