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

Add interpreted versions of unspecified cases of fp.to_ieee_bv and fp.to_real (#6077)

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2022-06-04 17:53:23 +01:00 • committed by GitHub
parent d722c73d4c
commit f77608ed88
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 57 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -312,17 +312,29 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
}
}
auto fid = m_fpa_util.get_family_id();
expr_ref_vector dom(m);
for (unsigned i = 0; i < f->get_arity(); ++i)
dom.push_back(m.mk_var(i, f->get_domain(i)));
if (m_fpa_util.is_to_sbv(f) || m_fpa_util.is_to_ubv(f)) {
auto fid = m_fpa_util.get_family_id();
auto k = m_fpa_util.is_to_sbv(f) ? OP_FPA_TO_SBV_I : OP_FPA_TO_UBV_I;
expr_ref_vector dom(m);
for (unsigned i = 0; i < f->get_arity(); ++i)
dom.push_back(m.mk_var(i, f->get_domain(i)));
parameter param = f->get_parameter(0);
func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, &param, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m);
result->set_else(else_value);
}
else if (m_fpa_util.is_to_real(f)) {
expr_ref_vector dom(m);
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, NULL, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m);
result->set_else(else_value);
}
else if (m_fpa_util.is_to_ieee_bv(f)) {
func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, NULL, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_ieee_bv_i, dom.size(), dom.data()), m);
result->set_else(else_value);
}
else if (bv_fi->get_else()) {
expr_ref ft_els = rebuild_floats(mc, rng, bv_fi->get_else());
m_th_rw(ft_els);

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

@ -52,7 +52,6 @@ fpa2bv_converter::~fpa2bv_converter() {
void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
if (is_float(a) && is_float(b)) {
TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
@ -98,12 +97,12 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
expr* c2 = nullptr, *t2 = nullptr, *f2 = nullptr;
if (m.is_ite(t, c2, t2, f2)) {
mk_ite(c2, t2, f2, result);
mk_ite(c, result, f, result);
mk_ite(c, result, f, result);
}
else if (m.is_ite(f, c2, t2, f2)) {
mk_ite(c2, t2, f2, result);
mk_ite(c, t, result, result);
}
mk_ite(c, t, result, result);
}
else if (m_util.is_fp(t) && m_util.is_fp(f)) {
expr_ref t_sgn(m), t_sig(m), t_exp(m);
expr_ref f_sgn(m), f_sig(m), f_exp(m);
@ -3261,6 +3260,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
SASSERT(is_well_sorted(m, result));
}
void fpa2bv_converter::mk_to_ieee_bv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
{
func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_IEEE_BV, 0, nullptr, num, args), m);
mk_to_bv(f, num, args, true, result);
}
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
@ -3491,6 +3496,11 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
}
}
void fpa2bv_converter::mk_to_real_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_REAL, 0, nullptr, num, args), m);
mk_to_real(f, num, args, result);
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
@ -3500,7 +3510,6 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
}
void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const {
expr* e_sgn = nullptr, *e_exp = nullptr, *e_sig = nullptr;
VERIFY(m_util.is_fp(e, e_sgn, e_exp, e_sig));

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

@ -136,6 +136,7 @@ public:
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_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv_i(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_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -145,6 +146,7 @@ public:
void mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
@ -245,6 +247,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter {
expr* bv2rm_value(expr* b);
expr* bv2fpa_value(sort* s, expr* a, expr* b = nullptr, expr* c = nullptr);
};

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

@ -149,7 +149,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_UBV_I: m_conv.mk_to_ubv_i(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV_I: m_conv.mk_to_sbv_i(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_I: m_conv.mk_to_real_i(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_I: m_conv.mk_to_ieee_bv_i(f, num, args, result); return BR_DONE;
case OP_FPA_BVWRAP:
case OP_FPA_BV2RM:
@ -290,15 +292,15 @@ expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) {
expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
SASSERT(fu().is_rm(e) || fu().is_float(e));
ast_manager& m = m_cfg.m();
expr_ref e_conv(m), res(m);
proof_ref pr(m);
(*this)(e, e_conv);
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
if (fu().is_rm(e)) {
SASSERT(fu().is_bv2rm(e_conv));
expr_ref bv_rm(m);
@ -316,7 +318,7 @@ expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
}
else
UNREACHABLE();
return res;
}
@ -333,7 +335,7 @@ expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
ast_manager& m = m_cfg.m();
expr_ref res(m);
TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
if (fu().is_fp(e))
res = e;
else if (m.is_bool(e))
@ -342,10 +344,10 @@ expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
res = convert_term(rw, e);
else
res = convert_conversion_term(rw, e);
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}