mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fpa2bv refactoring

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-21 18:44:12 +00:00
parent d5fef38c00
commit a1b4ef9e1b
5 changed files with 169 additions and 81 deletions
Download patch file Download diff file Expand all files Collapse all files

69
src/ast/float_decl_plugin.cpp
View file

@ -163,10 +163,10 @@ decl_plugin * float_decl_plugin::mk_fresh() {
} }
sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
if (ebits > sbits) if (sbits < 2)
m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported"); m_manager->raise_exception("minimum number of significand bits is 1");
if (ebits <= 2) if (ebits < 2)
m_manager->raise_exception("floating point sorts with ebits <= 2 are currently not supported"); m_manager->raise_exception("minimum number of exponent bits is 2");
parameter p1(ebits), p2(sbits); parameter p1(ebits), p2(sbits);
parameter ps[2] = { p1, p2 }; parameter ps[2] = { p1, p2 };
@ -182,13 +182,8 @@ sort * float_decl_plugin::mk_rm_sort() {
sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
switch (k) { switch (k) {
case FLOAT_SORT: case FLOAT_SORT:
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) { if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to floating point sort"); m_manager->raise_exception("expecting two integer parameters to floating point sort (ebits, sbits)");
}
if (parameters[0].get_int() <= 1 || parameters[1].get_int() <= 1)
m_manager->raise_exception("floating point sorts need parameters > 1");
if (parameters[0].get_int() > parameters[1].get_int())
m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported");
return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
case ROUNDING_MODE_SORT: case ROUNDING_MODE_SORT:
return mk_rm_sort(); return mk_rm_sort();
@ -279,8 +274,8 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet
case OP_FLOAT_EQ: name = "fp.eq"; break; case OP_FLOAT_EQ: name = "fp.eq"; break;
case OP_FLOAT_LT: name = "fp.lt"; break; case OP_FLOAT_LT: name = "fp.lt"; break;
case OP_FLOAT_GT: name = "fp.gt"; break; case OP_FLOAT_GT: name = "fp.gt"; break;
case OP_FLOAT_LE: name = "fp.lte"; break; case OP_FLOAT_LE: name = "fp.leq"; break;
case OP_FLOAT_GE: name = "fp.gte"; break; case OP_FLOAT_GE: name = "fp.geq"; break;
default: default:
UNREACHABLE(); UNREACHABLE();
break; break;
@ -408,9 +403,12 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa
is_sort_of(domain[1], m_bv_fid, BV_SORT) && is_sort_of(domain[1], m_bv_fid, BV_SORT) &&
is_sort_of(domain[2], m_bv_fid, BV_SORT)) { is_sort_of(domain[2], m_bv_fid, BV_SORT)) {
// 3 BVs -> 1 FP // 3 BVs -> 1 FP
sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); unsigned ebits = domain[1]->get_parameter(0).get_int();
symbol name("fp"); unsigned sbits = domain[2]->get_parameter(0).get_int() + 1;
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); parameter ps[] = { parameter(ebits), parameter(sbits) };
sort * fp = mk_float_sort(ebits, sbits);
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, 2, ps));
} }
else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) { else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
// 1 BV -> 1 FP // 1 BV -> 1 FP
@ -423,7 +421,7 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa
int sbits = parameters[1].get_int(); int sbits = parameters[1].get_int();
if (domain[0]->get_parameter(0).get_int() != (ebits + sbits)) if (domain[0]->get_parameter(0).get_int() != (ebits + sbits))
m_manager->raise_exception("sort mismtach; invalid bit-vector size, expected bitvector of size (ebits+sbits)"); m_manager->raise_exception("sort mismatch; invalid bit-vector size, expected bitvector of size (ebits+sbits)");
sort * fp = mk_float_sort(ebits, sbits); sort * fp = mk_float_sort(ebits, sbits);
symbol name("to_fp"); symbol name("to_fp");
@ -613,6 +611,39 @@ func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_par
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
} }
func_decl * float_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to internal_bv_wrap");
if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0]))
m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint or RoundingMode sort");
if (is_float_sort(domain[0]))
{
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
parameter ps[] = { parameter(float_sz) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
return m_manager->mk_func_decl(symbol("bv_wrap"), 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else {
parameter ps[] = { parameter(3) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
return m_manager->mk_func_decl(symbol("bv_wrap"), 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
}
func_decl * float_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to internal_bv_unwrap");
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT))
m_manager->raise_exception("sort mismatch, expected argument of bitvector sort");
if (!is_float_sort(range) && !is_rm_sort(range))
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
@ -680,6 +711,10 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_IEEE_BV: case OP_FLOAT_TO_IEEE_BV:
return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_INTERNAL_BVWRAP:
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_INTERNAL_BVUNWRAP:
return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range);
default: default:
m_manager->raise_exception("unsupported floating point operator"); m_manager->raise_exception("unsupported floating point operator");
return 0; return 0;

9
src/ast/float_decl_plugin.h
View file

@ -86,6 +86,10 @@ enum float_op_kind {
/* Extensions */ /* Extensions */
OP_FLOAT_TO_IEEE_BV, OP_FLOAT_TO_IEEE_BV,
/* Internal use only */
OP_FLOAT_INTERNAL_BVWRAP,
OP_FLOAT_INTERNAL_BVUNWRAP,
LAST_FLOAT_OP LAST_FLOAT_OP
}; };
@ -150,6 +154,11 @@ class float_decl_plugin : public decl_plugin {
func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
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);
virtual void set_manager(ast_manager * m, family_id id); virtual void set_manager(ast_manager * m, family_id id);
unsigned mk_id(mpf const & v); unsigned mk_id(mpf const & v);
void recycled_id(unsigned id); void recycled_id(unsigned id);

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

@ -32,7 +32,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_arith_util(m), m_arith_util(m),
m_mpf_manager(m_util.fm()), m_mpf_manager(m_util.fm()),
m_mpz_manager(m_mpf_manager.mpz_manager()), m_mpz_manager(m_mpf_manager.mpz_manager()),
extra_assertions(m) { m_extra_assertions(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float"))); m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
} }
@ -76,10 +76,15 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
split_triple(t, t_sgn, t_sig, t_exp);
split_triple(f, f_sgn, f_sig, f_exp);
expr_ref sgn(m), s(m), e(m); expr_ref sgn(m), s(m), e(m);
m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), sgn); m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
m_simp.mk_ite(c, to_app(t)->get_arg(1), to_app(f)->get_arg(1), s); m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, to_app(t)->get_arg(2), to_app(f)->get_arg(2), e); m_simp.mk_ite(c, t_exp, f_exp, e);
mk_triple(sgn, s, e, result); mk_triple(sgn, s, e, result);
} }
@ -122,6 +127,10 @@ void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args
} }
} }
app * fpa2bv_converter::mk_fresh_const(char const * prefix, unsigned sz) {
return m.mk_fresh_const(prefix, m_bv_util.mk_sort(sz));
}
void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id); SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0); SASSERT(f->get_arity() == 0);
@ -135,24 +144,20 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
unsigned ebits = m_util.get_ebits(srt); unsigned ebits = m_util.get_ebits(srt);
unsigned sbits = m_util.get_sbits(srt); unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m); app_ref sgn(m), s(m), e(m);
#ifdef Z3DEBUG #ifdef Z3DEBUG
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits - 1);
s_exp = m_bv_util.mk_sort(ebits);
std::string p("fpa2bv"); std::string p("fpa2bv");
std::string name = f->get_name().str(); std::string name = f->get_name().str();
sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), s_sgn); sgn = mk_fresh_const((p + "_sgn_" + name).c_str(), 1);
s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig); s = mk_fresh_const((p + "_sig_" + name).c_str(), sbits - 1);
e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp); e = mk_fresh_const((p + "_exp_" + name).c_str(), ebits);
#else #else
expr_ref bv(m); app_ref bv(m);
unsigned bv_sz = 1 + ebits + (sbits - 1); unsigned bv_sz = 1 + ebits + (sbits - 1);
bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz)); bv = mk_fresh_const(0, bv_sz);
m_fresh_bv_variables.insert(bv);
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv); sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv); e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
@ -196,7 +201,7 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex
if (is_float(args[i])) if (is_float(args[i]))
{ {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(args[i], sgn, sig, exp); split_triple(args[i], sgn, sig, exp);
new_args.push_back(sgn); new_args.push_back(sgn);
new_args.push_back(sig); new_args.push_back(sig);
new_args.push_back(exp); new_args.push_back(exp);
@ -294,7 +299,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
expr_ref rcc(m); expr_ref rcc(m);
rcc = bu().mk_ule(result, bu().mk_numeral(4, 3)); rcc = bu().mk_ule(result, bu().mk_numeral(4, 3));
extra_assertions.push_back(rcc); m_extra_assertions.push_back(rcc);
} }
} }
@ -612,7 +617,7 @@ void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1); SASSERT(num == 1);
expr * sgn, * s, * e; expr * sgn, * s, * e;
split(args[0], sgn, s, e); split_triple(args[0], sgn, s, e);
expr_ref c(m), nsgn(m); expr_ref c(m), nsgn(m);
mk_is_nan(args[0], c); mk_is_nan(args[0], c);
nsgn = m_bv_util.mk_bv_not(sgn); nsgn = m_bv_util.mk_bv_not(sgn);
@ -696,7 +701,6 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
// else comes the actual multiplication. // else comes the actual multiplication.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
@ -1033,7 +1037,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1); SASSERT(num == 1);
expr * sgn, * s, * e; expr * sgn, * s, * e;
split(args[0], sgn, s, e); split_triple(args[0], sgn, s, e);
mk_triple(m_bv_util.mk_numeral(0, 1), s, e, result); mk_triple(m_bv_util.mk_numeral(0, 1), s, e, result);
} }
@ -1044,8 +1048,8 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
expr * x_sgn, * x_sig, * x_exp; expr * x_sgn, * x_sig, * x_exp;
expr * y_sgn, * y_sig, * y_exp; expr * y_sgn, * y_sig, * y_exp;
split(x, x_sgn, x_sig, x_exp); split_triple(x, x_sgn, x_sig, x_exp);
split(y, y_sgn, y_sig, y_exp); split_triple(y, y_sgn, y_sig, y_exp);
expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m);
mk_is_zero(x, x_is_zero); mk_is_zero(x, x_is_zero);
@ -1087,8 +1091,8 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
expr * x_sgn, * x_sig, * x_exp; expr * x_sgn, * x_sig, * x_exp;
expr * y_sgn, * y_sig, * y_exp; expr * y_sgn, * y_sig, * y_exp;
split(x, x_sgn, x_sig, x_exp); split_triple(x, x_sgn, x_sig, x_exp);
split(y, y_sgn, y_sig, y_exp); split_triple(y, y_sgn, y_sig, y_exp);
expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m);
mk_is_zero(y, y_is_zero); mk_is_zero(y, y_is_zero);
@ -1225,11 +1229,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c);
mk_ite(ite_c, pzero, z, v7); mk_ite(ite_c, pzero, z, v7);
// else comes the fused multiplication. // else comes the fused multiplication.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
@ -1482,7 +1484,6 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
// else comes the actual square root. // else comes the actual square root.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
@ -1698,8 +1699,8 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
expr * x_sgn, * x_sig, * x_exp; expr * x_sgn, * x_sig, * x_exp;
expr * y_sgn, * y_sig, * y_exp; expr * y_sgn, * y_sig, * y_exp;
split(x, x_sgn, x_sig, x_exp); split_triple(x, x_sgn, x_sig, x_exp);
split(y, y_sgn, y_sig, y_exp); split_triple(y, y_sgn, y_sig, y_exp);
expr_ref x_eq_y_sgn(m), x_eq_y_exp(m), x_eq_y_sig(m); expr_ref x_eq_y_sgn(m), x_eq_y_exp(m), x_eq_y_sig(m);
m_simp.mk_eq(x_sgn, y_sgn, x_eq_y_sgn); m_simp.mk_eq(x_sgn, y_sgn, x_eq_y_sgn);
@ -1734,8 +1735,8 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a
expr * x_sgn, * x_sig, * x_exp; expr * x_sgn, * x_sig, * x_exp;
expr * y_sgn, * y_sig, * y_exp; expr * y_sgn, * y_sig, * y_exp;
split(x, x_sgn, x_sig, x_exp); split_triple(x, x_sgn, x_sig, x_exp);
split(y, y_sgn, y_sig, y_exp); split_triple(y, y_sgn, y_sig, y_exp);
expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m); expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m);
one_1 = m_bv_util.mk_numeral(1, 1); one_1 = m_bv_util.mk_numeral(1, 1);
@ -1866,9 +1867,10 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
m_bv_util.is_bv(args[0]) && m_bv_util.is_bv(args[0]) &&
m_bv_util.is_bv(args[1]) && m_bv_util.is_bv(args[1]) &&
m_bv_util.is_bv(args[2])) { m_bv_util.is_bv(args[2])) {
// Theoretically, the user could have thrown in it's own triple of bit-vectors. SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
// Just keep it here, as there will be something else that uses it. SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
mk_triple(args[0], args[1], args[2], result); SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1);
mk_triple(args[0], args[2], args[1], result);
} }
else if (num == 2 && else if (num == 2 &&
m_bv_util.is_bv(args[0]) && m_bv_util.is_bv(args[0]) &&
@ -2306,13 +2308,40 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1); SASSERT(num == 1);
expr * sgn, * s, * e; expr * sgn, * s, * e;
split(args[0], sgn, s, e); split_triple(args[0], sgn, s, e);
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
} }
void fpa2bv_converter::mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_internal", tout << "wrap ";
for (unsigned i = 0; i < num; i++)
tout << " " << mk_ismt2_pp(args[i], m);
tout << std::endl;);
SASSERT(num == 1);
result = m.mk_app(f, num, args);
}
void fpa2bv_converter::mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_internal", tout << "unwrap ";
for (unsigned i = 0; i < num; i++)
tout << " " << mk_ismt2_pp(args[i], m);
tout << std::endl;);
SASSERT(num == 1);
app * a0 = to_app(args[0]);
SASSERT(a0->get_kind() == AST_APP);
SASSERT(is_float_family(a0->get_decl()));
decl_kind k = a0->get_decl_kind();
SASSERT(k == OP_FLOAT_INTERNAL_BVWRAP);
SASSERT(a0->get_num_args() == 1);
result = a0->get_arg(0);
}
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_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1);
SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
mk_triple(args[0], args[2], args[1], result); mk_triple(args[0], args[2], args[1], result);
TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
} }
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -2328,7 +2357,7 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
//expr * x = args[1]; //expr * x = args[1];
//expr * sgn, *s, *e; //expr * sgn, *s, *e;
//split(x, sgn, s, e); //split_triple(x, sgn, s, e);
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
@ -2346,7 +2375,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
//expr * x = args[1]; //expr * x = args[1];
//expr * sgn, *s, *e; //expr * sgn, *s, *e;
//split(x, sgn, s, e); //split_triple(x, sgn, s, e);
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
@ -2440,18 +2469,28 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
SASSERT(is_well_sorted(m, result)); SASSERT(is_well_sorted(m, result));
} }
void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
SASSERT(to_app(e)->get_num_args() == 3); SASSERT(to_app(e)->get_num_args() == 3);
sgn = to_app(e)->get_arg(0); sgn = to_app(e)->get_arg(0);
sig = to_app(e)->get_arg(1); sig = to_app(e)->get_arg(2);
exp = to_app(e)->get_arg(2); exp = to_app(e)->get_arg(1);
}
void fpa2bv_converter::split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const {
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
SASSERT(to_app(e)->get_num_args() == 3);
expr *e_sgn, *e_sig, *e_exp;
split_triple(e, e_sgn, e_sig, e_exp);
sgn = e_sgn;
sig = e_sig;
exp = e_exp;
} }
void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
// exp == 1^n , sig != 0 // exp == 1^n , sig != 0
expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m); expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m);
@ -2466,7 +2505,7 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref eq1(m), eq2(m), top_exp(m), zero(m); expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
@ -2509,7 +2548,7 @@ void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref eq1(m), eq2(m), bot_exp(m), zero(m); expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp); mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
@ -2520,7 +2559,7 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref e_is_zero(m), eq(m), one_1(m); expr_ref e_is_zero(m), eq(m), one_1(m);
mk_is_zero(e, e_is_zero); mk_is_zero(e, e_is_zero);
one_1 = m_bv_util.mk_numeral(1, 1); one_1 = m_bv_util.mk_numeral(1, 1);
@ -2530,7 +2569,7 @@ void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref e_is_zero(m), eq(m), nil_1(m); expr_ref e_is_zero(m), eq(m), nil_1(m);
mk_is_zero(e, e_is_zero); mk_is_zero(e, e_is_zero);
nil_1 = m_bv_util.mk_numeral(0, 1); nil_1 = m_bv_util.mk_numeral(0, 1);
@ -2540,7 +2579,7 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref zero(m); expr_ref zero(m);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
m_simp.mk_eq(exp, zero, result); m_simp.mk_eq(exp, zero, result);
@ -2548,7 +2587,7 @@ void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split_triple(e, sgn, sig, exp);
expr_ref is_special(m), is_denormal(m), p(m); expr_ref is_special(m), is_denormal(m), p(m);
mk_is_denormal(e, is_denormal); mk_is_denormal(e, is_denormal);
@ -2670,9 +2709,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
unsigned sbits = m_util.get_sbits(srt); unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt); unsigned ebits = m_util.get_ebits(srt);
sgn = to_app(e)->get_arg(0); split_triple(e, sgn, sig, exp);
sig = to_app(e)->get_arg(1);
exp = to_app(e)->get_arg(2);
expr_ref is_normal(m); expr_ref is_normal(m);
mk_is_normal(e, is_normal); mk_is_normal(e, is_normal);
@ -2684,7 +2721,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
expr_ref denormal_sig(m), denormal_exp(m); expr_ref denormal_sig(m), denormal_exp(m);
denormal_sig = m_bv_util.mk_zero_extend(1, sig); denormal_sig = m_bv_util.mk_zero_extend(1, sig);
SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0. // SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0.
denormal_exp = m_bv_util.mk_numeral(1, ebits); denormal_exp = m_bv_util.mk_numeral(1, ebits);
mk_unbias(denormal_exp, denormal_exp); mk_unbias(denormal_exp, denormal_exp);
dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
@ -2772,7 +2809,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
// CMW: This works only for quantifier-free formulas. // CMW: This works only for quantifier-free formulas.
expr_ref new_e(m); expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e)); new_e = m.mk_fresh_const(prefix, m.get_sort(e));
extra_assertions.push_back(m.mk_eq(new_e, e)); m_extra_assertions.push_back(m.mk_eq(new_e, e));
e = new_e; e = new_e;
#endif #endif
} }
@ -2802,7 +2839,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
// i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn. // i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn.
// Furthermore, note that sig is an unsigned bit-vector, while exp is signed. // Furthermore, note that sig is an unsigned bit-vector, while exp is signed.
SASSERT(ebits <= sbits);
SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3); SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3);
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5); SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5);

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

@ -42,6 +42,7 @@ struct func_decl_triple {
}; };
class fpa2bv_converter { class fpa2bv_converter {
protected:
ast_manager & m; ast_manager & m;
basic_simplifier_plugin m_simp; basic_simplifier_plugin m_simp;
float_util m_util; float_util m_util;
@ -73,16 +74,19 @@ public:
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
SASSERT(m_bv_util.is_bv(significand)); SASSERT(m_bv_util.is_bv(significand));
SASSERT(m_bv_util.is_bv(exponent)); SASSERT(m_bv_util.is_bv(exponent));
result = m.mk_app(m_util.get_family_id(), OP_FLOAT_TO_FP, sign, significand, exponent); result = m.mk_app(m_util.get_family_id(), OP_FLOAT_TO_FP, sign, exponent, significand);
} }
void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const;
void split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const;
void mk_eq(expr * a, expr * b, expr_ref & result); void mk_eq(expr * a, expr * b, expr_ref & result);
void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
void mk_rounding_mode(func_decl * f, expr_ref & result); void mk_rounding_mode(func_decl * f, expr_ref & result);
void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_const(func_decl * f, expr_ref & result); virtual void mk_const(func_decl * f, expr_ref & result);
void mk_rm_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result);
void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_var(unsigned base_inx, sort * srt, expr_ref & result); void mk_var(unsigned base_inx, sort * srt, expr_ref & result);
@ -138,11 +142,11 @@ public:
obj_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; } obj_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; }
void dbg_decouple(const char * prefix, expr_ref & e); void dbg_decouple(const char * prefix, expr_ref & e);
expr_ref_vector extra_assertions; expr_ref_vector m_extra_assertions;
void mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
protected: protected:
void split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const;
void mk_is_nan(expr * e, expr_ref & result); void mk_is_nan(expr * e, expr_ref & result);
void mk_is_inf(expr * e, expr_ref & result); void mk_is_inf(expr * e, expr_ref & result);
void mk_is_pinf(expr * e, expr_ref & result); void mk_is_pinf(expr * e, expr_ref & result);
@ -173,6 +177,8 @@ protected:
void add_core(unsigned sbits, unsigned ebits, expr_ref & rm, void add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp, expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp,
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp); expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
app * mk_fresh_const(char const * prefix, unsigned sz);
}; };
#endif #endif

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

@ -150,6 +150,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FLOAT_INTERNAL_BVWRAP: m_conv.mk_internal_bvwrap(f, num, args, result); return BR_DONE;
case OP_FLOAT_INTERNAL_BVUNWRAP: m_conv.mk_internal_bvunwrap(f, num, args, result); return BR_DONE;
default: default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);