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

Bug fixes for underspecified FP operations.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-12 18:37:41 +01:00
parent bc257211d6
commit 7e705a2d32
7 changed files with 139 additions and 107 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3072,13 +3072,57 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
m_bv_util.mk_numeral(1, 1)))); m_bv_util.mk_numeral(1, 1))));
else else {
nanv = mk_to_ieee_bv_unspecified(ebits, sbits); expr_ref unspec_bits(m);
unspec_bits = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
nanv = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-1, unspec_bits),
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
m_bv_util.mk_extract(sbits-2, 0, unspec_bits)));
}
expr_ref sgn_e_s(m); expr_ref sgn_e_s(m);
sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result); m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
if (m_hi_fp_unspecified) {
result = m_bv_util.mk_concat(m_bv_util.mk_concat(
m_bv_util.mk_numeral(0, 1),
m_bv_util.mk_numeral(-1, ebits)),
m_bv_util.mk_numeral(1, sbits-1));
}
else {
func_decl * fd;
if (m_uf2bvuf.find(f, fd))
result = m.mk_const(fd);
else {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
result = m.mk_const(fd);
expr_ref exp_bv(m), exp_all_ones(m);
exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
m_extra_assertions.push_back(exp_all_ones);
expr_ref sig_bv(m), sig_is_non_zero(m);
sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
m_extra_assertions.push_back(sig_is_non_zero);
}
}
TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result)); SASSERT(is_well_sorted(m, result));
} }
@ -3308,41 +3352,10 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits
m.inc_ref(fd); m.inc_ref(fd);
} }
result = m.mk_const(fd); result = m.mk_const(fd);
result = unspec;
} }
return result; return result;
} }
expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
expr_ref result(m);
app_ref unspec(m);
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
func_decl * unspec_fd = unspec->get_decl();
func_decl * fd;
if (!m_uf2bvuf.find(unspec_fd, fd)) {
app_ref bvc(m);
bvc = m.mk_fresh_const(0, unspec_fd->get_range());
fd = bvc->get_decl();
m_uf2bvuf.insert(unspec_fd, fd);
m.inc_ref(unspec_fd);
m.inc_ref(fd);
}
result = m.mk_const(fd);
app_ref mask(m), extra(m), result_and_mask(m);
mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
m_bv_util.mk_numeral(1, 1))));
expr * args[2] = { result, mask };
result_and_mask = m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args);
extra = m.mk_eq(result_and_mask, mask);
m_extra_assertions.push_back(extra);
return result;
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3); SASSERT(num == 3);
SASSERT(m_bv_util.get_bv_size(args[0]) == 1); SASSERT(m_bv_util.get_bv_size(args[0]) == 1);

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

@ -133,6 +133,7 @@ public:
void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -152,7 +153,6 @@ public:
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
void reset(void); void reset(void);

4
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -145,7 +145,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; 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_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_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
@ -161,7 +162,6 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
return BR_FAILED; return BR_FAILED;
default: default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";

40
src/ast/fpa_decl_plugin.h
View file

@ -377,28 +377,28 @@ public:
app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits); app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits);
bool is_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
bool is_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; } bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
bool is_bv2rm(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); } bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
bool is_bv2rm(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; } bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; }
bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); } bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); } bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
bool is_max_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); } bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
bool is_max_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); } bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
bool is_to_ubv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); } bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
bool is_to_sbv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); } bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
bool is_to_ieee_bv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); } bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
bool is_to_real_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); } bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
bool is_min_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; } bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
bool is_min_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; } bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
bool is_max_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; } bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
bool is_max_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; } bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
bool is_to_ubv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; } bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
bool is_to_sbv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; } bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
bool is_to_ieee_bv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; } bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
bool is_to_real_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; } bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
bool contains_floats(ast * a); bool contains_floats(ast * a);
}; };

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

@ -18,11 +18,12 @@ Notes:
--*/ --*/
#include"fpa_rewriter.h" #include"fpa_rewriter.h"
#include"fpa_rewriter_params.hpp" #include"fpa_rewriter_params.hpp"
#include"ast_smt2_pp.h"
fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) :
m_util(m), m_util(m),
m_fm(m_util.fm()), m_fm(m_util.fm()),
m_hi_fp_unspecified(true) { m_hi_fp_unspecified(false) {
updt_params(p); updt_params(p);
} }
@ -117,34 +118,40 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m()); bv_util bu(m());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = bu.mk_numeral(0, width); result = bu.mk_numeral(0, width);
else return BR_DONE;
}
else {
result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
return BR_REWRITE1;
return BR_DONE; }
} }
br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m()); bv_util bu(m());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = bu.mk_numeral(0, width); result = bu.mk_numeral(0, width);
else return BR_DONE;
}
else {
result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
return BR_REWRITE1;
return BR_DONE; }
} }
br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) { br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = m_util.au().mk_numeral(rational(0), false); result = m_util.au().mk_numeral(rational(0), false);
else return BR_DONE;
}
else {
result = m_util.mk_internal_to_real_unspecified(ebits, sbits); result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
return BR_REWRITE1;
return BR_DONE; }
} }
br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -776,10 +783,8 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
const mpf & x = v.get(); const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v))
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_REWRITE_FULL;
}
bv_util bu(m()); bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager()); scoped_mpq q(m_fm.mpq_manager());
@ -789,11 +794,13 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
rational ul, ll; rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz); ul = m_fm.m_powers2.m1(bv_sz);
ll = rational(0); ll = rational(0);
if (r >= ll && r <= ul) if (r >= ll && r <= ul) {
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
return BR_DONE;
}
else else
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
@ -810,10 +817,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
const mpf & x = v.get(); const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v))
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_REWRITE_FULL;
}
bv_util bu(m()); bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager()); scoped_mpq q(m_fm.mpq_manager());
@ -823,46 +828,42 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
rational ul, ll; rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz - 1); ul = m_fm.m_powers2.m1(bv_sz - 1);
ll = - m_fm.m_powers2(bv_sz - 1); ll = - m_fm.m_powers2(bv_sz - 1);
if (r >= ll && r <= ul) if (r >= ll && r <= ul) {
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
return BR_DONE;
}
else else
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;);
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg, v)) { if (m_util.is_numeral(arg, v)) {
TRACE("fp_rewriter", tout << "to_ieee_bv numeral: " << m_fm.to_string(v) << std::endl;);
bv_util bu(m()); bv_util bu(m());
const mpf & x = v.get(); const mpf & x = v.get();
if (m_fm.is_nan(v)) { if (m_fm.is_nan(v)) {
if (m_hi_fp_unspecified) { if (m_hi_fp_unspecified) {
result = bu.mk_concat(bu.mk_numeral(0, 1), expr * args[4] = { bu.mk_numeral(0, 1),
bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()), bu.mk_numeral(-1, x.get_ebits()),
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2), bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1)))); bu.mk_numeral(1, 1) };
result = bu.mk_concat(4, args);
} }
else { else
app_ref unspec(m()), mask(m()), extra(m()); result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
mask = bu.mk_concat(bu.mk_numeral(0, 1), return BR_REWRITE1;
bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1))));
expr * args[2] = { unspec, mask };
result = m().mk_app(bu.get_fid(), OP_BOR, 2, args);
}
return BR_REWRITE_FULL;
} }
else { else {
scoped_mpz rz(m_fm.mpq_manager()); scoped_mpz rz(m_fm.mpq_manager());
m_fm.to_ieee_bv_mpz(v, rz); m_fm.to_ieee_bv_mpz(v, rz);
result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits()); result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
return BR_DONE; return BR_DONE;
} }

2
src/ast/rewriter/fpa_rewriter_params.pyg
View file

@ -1,5 +1,5 @@
def_module_params(module_name='rewriter', def_module_params(module_name='rewriter',
class_name='fpa_rewriter_params', class_name='fpa_rewriter_params',
export=True, 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.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"),
)) ))

30
src/smt/theory_fpa.cpp
View file

@ -715,14 +715,14 @@ namespace smt {
fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf(); fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf();
for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin(); for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin();
it != uf2bvuf.end(); it != uf2bvuf.end();
it++) { it++) {
mg.hide(it->m_value); //mg.hide(it->m_value);
} }
fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials(); fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials();
for (fpa2bv_converter::special_t::iterator it = specials.begin(); for (fpa2bv_converter::special_t::iterator it = specials.begin();
it != specials.end(); it != specials.end();
it++) { it++) {
mg.hide(it->m_value.first->get_decl()); mg.hide(it->m_value.first->get_decl());
mg.hide(it->m_value.second->get_decl()); mg.hide(it->m_value.second->get_decl());
} }
@ -811,7 +811,25 @@ namespace smt {
return res; return res;
} }
void theory_fpa::finalize_model(model_generator & mg) {} void theory_fpa::finalize_model(model_generator & mg) {
ast_manager & m = get_manager();
proto_model & mdl = mg.get_model();
fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf();
for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin();
it != uf2bvuf.end();
it++) {
func_decl * bv_fd = it->m_value;
if (bv_fd->get_arity() == 0) {
expr_ref bve(m), v(m);
bve = m.mk_const(bv_fd);
mdl.eval(bve, v, true);
mdl.register_decl(it->m_key, v);
}
else
NOT_IMPLEMENTED_YET();
}
}
void theory_fpa::display(std::ostream & out) const void theory_fpa::display(std::ostream & out) const
{ {