mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-15 18:16:44 +02:00
parent ab4bb8194e
commit 009af4455d
9 changed files with 817 additions and 644 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -23,6 +23,7 @@ Notes:
#include"th_rewriter.h"
#include"fpa2bv_converter.h"
#include"fpa_rewriter.h"
#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
@ -32,7 +33,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_util(m),
m_bv_util(m),
m_arith_util(m),
m_array_util(m),
m_dt_util(m),
m_seq_util(m),
m_mpf_manager(m_util.fm()),
@ -2771,6 +2771,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
expr_ref unspec(m);
unspec = mk_to_real_unspecified(ebits, sbits);
result = m.mk_ite(x_is_zero, zero, res);
result = m.mk_ite(x_is_inf, unspec, result);
result = m.mk_ite(x_is_nan, unspec, result);
@ -3073,11 +3074,9 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
m_bv_util.mk_numeral(1, 1))));
else {
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)));
app_ref unspec(m);
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv);
}
expr_ref sgn_e_s(m);
@ -3127,39 +3126,42 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
}
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;);
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
expr * rm = to_app(args[0])->get_arg(0);
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
expr * rm = to_app(args[0])->get_arg(0);
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
expr_ref bv0(m), bv1(m);
bv1 = m_bv_util.mk_numeral(1, 1);
expr_ref bv0(m), bv1(m);
bv1 = m_bv_util.mk_numeral(1, 1);
expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
mk_is_nan(x, x_is_nan);
mk_is_inf(x, x_is_inf);
mk_is_zero(x, x_is_zero);
mk_is_neg(x, x_is_neg);
mk_is_nzero(x, x_is_nzero);
expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
mk_is_nan(x, x_is_nan);
mk_is_inf(x, x_is_inf);
mk_is_zero(x, x_is_zero);
mk_is_neg(x, x_is_neg);
mk_is_nzero(x, x_is_nzero);
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
if (!is_signed)
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
else
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
if (!is_signed) {
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
}
else {
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz);
}
dbg_decouple("fpa2bv_to_bv_c1", c1);
// +-Zero -> 0
@ -3269,7 +3271,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
dbg_decouple("fpa2bv_to_bv_rnd", rnd);
expr_ref unspec(m);
unspec = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) :
mk_to_ubv_unspecified(ebits, sbits, bv_sz);
result = m.mk_ite(rnd_has_overflown, unspec, rnd);
result = m.mk_ite(c_in_limits, result, unspec);
result = m.mk_ite(c2, v2, result);
@ -3290,70 +3293,89 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
mk_to_bv(f, num, args, true, result);
}
void fpa2bv_converter::mk_to_ubv_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();
unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
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);
}
TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref result(m);
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
app_ref unspec(m);
unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
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);
}
return result;
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_to_sbv_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();
unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
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);
}
TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref result(m);
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
app_ref unspec(m);
unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
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);
}
return result;
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
expr_ref result(m);
void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
if (m_hi_fp_unspecified)
result = m_arith_util.mk_numeral(rational(0), false);
else {
app_ref unspec(m);
unspec = m_util.mk_internal_to_real_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);
if (!m_uf2bvuf.find(f, fd)) {
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);
}
return result;
}
expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_real_unspecified(ebits, sbits);
mk_to_real_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {