mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
Eliminated the remaining operator kinds for partially unspecified FP operators.
This commit is contained in:
Christoph M. Wintersteiger
parent
cb15473d5b
commit
cc9f67267d
|
|
@ -993,18 +993,6 @@ typedef enum
|
|||
3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
|
||||
4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO.
|
||||
|
||||
- Z3_OP_FPA_MIN_I: The same as Z3_OP_FPA_MIN, but the arguments are
|
||||
expected not to be zeroes with different signs.
|
||||
|
||||
- Z3_OP_FPA_MAX_I: The same as Z3_OP_FPA_MAX, but the arguments are
|
||||
expected not to be zeroes with different signs.
|
||||
|
||||
- Z3_OP_FPA_MIN_UNSPECIFIED: The same as Z3_OP_FPA_MIN, but the
|
||||
arguments are expected to be zeroes with different signs.
|
||||
|
||||
- Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the
|
||||
arguments are expected to be zeroes with different signs.
|
||||
|
||||
- Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
|
||||
information is exposed. Tools may use the string representation of the
|
||||
function declaration to obtain more information.
|
||||
|
|
@ -1291,13 +1279,8 @@ typedef enum {
|
|||
|
||||
Z3_OP_FPA_TO_IEEE_BV,
|
||||
|
||||
Z3_OP_FPA_MIN_I,
|
||||
Z3_OP_FPA_MAX_I,
|
||||
|
||||
Z3_OP_FPA_BVWRAP,
|
||||
Z3_OP_FPA_BV2RM,
|
||||
Z3_OP_FPA_MIN_UNSPECIFIED,
|
||||
Z3_OP_FPA_MAX_UNSPECIFIED,
|
||||
|
||||
Z3_OP_INTERNAL,
|
||||
|
||||
|
|
|
|||
|
|
@ -62,8 +62,8 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
|
|||
m.inc_ref(it->m_key);
|
||||
m.inc_ref(it->m_value);
|
||||
}
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_min_max_specials.begin();
|
||||
it != conv.m_min_max_specials.end();
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_min_max_ufs.begin();
|
||||
it != conv.m_min_max_ufs.end();
|
||||
it++) {
|
||||
m_specials.insert(it->m_key, it->m_value);
|
||||
m.inc_ref(it->m_key);
|
||||
|
|
|
|||
|
|
@ -230,39 +230,7 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
|
|||
result = m_util.mk_fp(sgn, e, s);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result) {
|
||||
if (m_util.is_float(rng)) {
|
||||
unsigned ebits = m_util.get_ebits(rng);
|
||||
unsigned sbits = m_util.get_sbits(rng);
|
||||
unsigned bv_sz = ebits + sbits;
|
||||
|
||||
app_ref na(m);
|
||||
na = m.mk_app(fbv, fbv->get_arity(), new_args);
|
||||
result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
|
||||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, na));
|
||||
}
|
||||
else if (m_util.is_rm(rng)) {
|
||||
app_ref na(m);
|
||||
na = m.mk_app(fbv, fbv->get_arity(), new_args);
|
||||
result = m_util.mk_bv2rm(na);
|
||||
}
|
||||
else
|
||||
result = m.mk_app(fbv, fbv->get_arity(), new_args);
|
||||
}
|
||||
|
||||
func_decl * fpa2bv_converter::get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity) {
|
||||
func_decl * res;
|
||||
if (!m_uf2bvuf.find(f, res)) {
|
||||
res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), arity, f->get_domain(), bv_rng);
|
||||
m_uf2bvuf.insert(f, res);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(res);
|
||||
TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
|
||||
void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
|
||||
{
|
||||
TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
|
||||
|
||||
|
|
@ -278,7 +246,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
|
|||
unsigned sbits = m_util.get_sbits(rng);
|
||||
unsigned bv_sz = ebits+sbits;
|
||||
bv_rng = m_bv_util.mk_sort(bv_sz);
|
||||
func_decl * bv_f = get_bv_uf(f, bv_rng, num);
|
||||
func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng);
|
||||
bv_app = m.mk_app(bv_f, num, args);
|
||||
flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app),
|
||||
m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app),
|
||||
|
|
@ -291,7 +259,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
|
|||
sort_ref bv_rng(m);
|
||||
expr_ref new_eq(m);
|
||||
bv_rng = m_bv_util.mk_sort(3);
|
||||
func_decl * bv_f = get_bv_uf(f, bv_rng, num);
|
||||
func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng);
|
||||
bv_app = m.mk_app(bv_f, num, args);
|
||||
flt_app = m_util.mk_bv2rm(bv_app);
|
||||
new_eq = m.mk_eq(fapp, flt_app);
|
||||
|
|
@ -1211,61 +1179,89 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
expr_ref x(m), y(m);
|
||||
x = args[0];
|
||||
y = args[1];
|
||||
|
||||
expr_ref x_is_zero(m), y_is_zero(m), both_are_zero(m);
|
||||
x_is_zero = m_util.mk_is_zero(x);
|
||||
y_is_zero = m_util.mk_is_zero(y);
|
||||
both_are_zero = m.mk_and(x_is_zero, y_is_zero);
|
||||
|
||||
expr_ref x_is_positive(m), x_is_negative(m), y_is_positive(m), y_is_negative(m), pn(m), np(m), pn_or_np(m);
|
||||
x_is_positive = m_util.mk_is_positive(x);
|
||||
x_is_negative = m_util.mk_is_negative(x);
|
||||
y_is_positive = m_util.mk_is_positive(y);
|
||||
y_is_negative = m_util.mk_is_negative(y);
|
||||
pn = m.mk_and(x_is_positive, y_is_negative);
|
||||
np = m.mk_and(x_is_negative, y_is_positive);
|
||||
pn_or_np = m.mk_or(pn, np);
|
||||
|
||||
expr_ref c(m), v(m);
|
||||
c = m.mk_and(both_are_zero, pn_or_np);
|
||||
v = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_UNSPECIFIED, x, y);
|
||||
|
||||
// Note: This requires BR_REWRITE_FULL afterwards.
|
||||
expr_ref min_i(m);
|
||||
min_i = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_I, x, y);
|
||||
m_simp.mk_ite(c, v, min_i, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 2);
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
||||
expr * x = args[0], * y = args[1];
|
||||
|
||||
expr * x_sgn, * x_sig, * x_exp;
|
||||
expr * y_sgn, * y_sig, * y_exp;
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
|
||||
mk_is_zero(x, x_is_zero);
|
||||
mk_is_zero(y, y_is_zero);
|
||||
m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
|
||||
expr_ref bv0(m), bv1(m);
|
||||
bv0 = m_bv_util.mk_numeral(0, 1);
|
||||
bv1 = m_bv_util.mk_numeral(1, 1);
|
||||
|
||||
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
mk_is_nan(y, y_is_nan);
|
||||
mk_pzero(f, pzero);
|
||||
mk_is_zero(x, x_is_zero);
|
||||
mk_is_zero(y, y_is_zero);
|
||||
xy_are_zero = m.mk_and(x_is_zero, y_is_zero);
|
||||
|
||||
expr_ref sgn_eq(m), sgn_diff(m);
|
||||
sgn_eq = m.mk_eq(x_sgn, y_sgn);
|
||||
sgn_diff = m.mk_not(sgn_eq);
|
||||
expr_ref x_is_pos(m), x_is_neg(m);
|
||||
expr_ref y_is_pos(m), y_is_neg(m);
|
||||
expr_ref pn(m), np(m), pn_or_np_zeros(m);
|
||||
mk_is_pos(x, x_is_pos);
|
||||
mk_is_pos(y, y_is_pos);
|
||||
mk_is_neg(x, x_is_neg);
|
||||
mk_is_neg(y, y_is_neg);
|
||||
pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn)));
|
||||
|
||||
expr_ref lt(m);
|
||||
mk_float_lt(f, num, args, lt);
|
||||
expr_ref unspec(m);
|
||||
unspec = mk_min_max_unspecified(f, x, y);
|
||||
|
||||
mk_ite(lt, x, y, result);
|
||||
mk_ite(both_zero, y, result, result);
|
||||
expr_ref x_lt_y(m);
|
||||
mk_float_lt(f, num, args, x_lt_y);
|
||||
|
||||
mk_ite(x_lt_y, x, y, result);
|
||||
mk_ite(xy_are_zero, y, result, result);
|
||||
mk_ite(pn_or_np_zeros, unspec, result, result);
|
||||
mk_ite(y_is_nan, x, result, result);
|
||||
mk_ite(x_is_nan, y, result, result);
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 2);
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
||||
expr * x = args[0], *y = args[1];
|
||||
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
mk_is_nan(y, y_is_nan);
|
||||
mk_is_zero(x, x_is_zero);
|
||||
mk_is_zero(y, y_is_zero);
|
||||
xy_are_zero = m.mk_and(x_is_zero, y_is_zero);
|
||||
|
||||
expr_ref x_is_pos(m), x_is_neg(m);
|
||||
expr_ref y_is_pos(m), y_is_neg(m);
|
||||
expr_ref pn(m), np(m), pn_or_np_zeros(m);
|
||||
mk_is_pos(x, x_is_pos);
|
||||
mk_is_pos(y, y_is_pos);
|
||||
mk_is_neg(x, x_is_neg);
|
||||
mk_is_neg(y, y_is_neg);
|
||||
pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn)));
|
||||
|
||||
expr_ref unspec(m);
|
||||
unspec = mk_min_max_unspecified(f, x, y);
|
||||
|
||||
expr_ref x_gt_y(m);
|
||||
mk_float_gt(f, num, args, x_gt_y);
|
||||
|
||||
mk_ite(x_gt_y, x, y, result);
|
||||
mk_ite(xy_are_zero, y, result, result);
|
||||
mk_ite(pn_or_np_zeros, unspec, result, result);
|
||||
mk_ite(y_is_nan, x, result, result);
|
||||
mk_ite(x_is_nan, y, result, result);
|
||||
|
||||
|
|
@ -1281,10 +1277,10 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr
|
|||
// There is no "hardware interpretation" for fp.min/fp.max.
|
||||
|
||||
std::pair<app*, app*> decls(0, 0);
|
||||
if (!m_min_max_specials.find(f, decls)) {
|
||||
if (!m_min_max_ufs.find(f, decls)) {
|
||||
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_min_max_specials.insert(f, decls);
|
||||
m_min_max_ufs.insert(f, decls);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(decls.first);
|
||||
m.inc_ref(decls.second);
|
||||
|
|
@ -1303,68 +1299,6 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr
|
|||
return res;
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
expr_ref x(m), y(m);
|
||||
x = args[0];
|
||||
y = args[1];
|
||||
|
||||
expr_ref x_is_zero(m), y_is_zero(m), both_are_zero(m);
|
||||
x_is_zero = m_util.mk_is_zero(x);
|
||||
y_is_zero = m_util.mk_is_zero(y);
|
||||
both_are_zero = m.mk_and(x_is_zero, y_is_zero);
|
||||
|
||||
expr_ref x_is_positive(m), x_is_negative(m), y_is_positive(m), y_is_negative(m), pn(m), np(m), pn_or_np(m);
|
||||
x_is_positive = m_util.mk_is_positive(x);
|
||||
x_is_negative = m_util.mk_is_negative(x);
|
||||
y_is_positive = m_util.mk_is_positive(y);
|
||||
y_is_negative = m_util.mk_is_negative(y);
|
||||
pn = m.mk_and(x_is_positive, y_is_negative);
|
||||
np = m.mk_and(x_is_negative, y_is_positive);
|
||||
pn_or_np = m.mk_or(pn, np);
|
||||
|
||||
expr_ref c(m), v(m);
|
||||
c = m.mk_and(both_are_zero, pn_or_np);
|
||||
v = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_UNSPECIFIED, x, y);
|
||||
|
||||
// Note: This requires BR_REWRITE_FULL afterwards.
|
||||
expr_ref max_i(m);
|
||||
max_i = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_I, x, y);
|
||||
m_simp.mk_ite(c, v, max_i, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 2);
|
||||
|
||||
expr * x = args[0], *y = args[1];
|
||||
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
|
||||
mk_is_zero(x, x_is_zero);
|
||||
mk_is_zero(y, y_is_zero);
|
||||
m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
mk_is_nan(y, y_is_nan);
|
||||
mk_pzero(f, pzero);
|
||||
|
||||
expr_ref sgn_diff(m), sgn_eq(m);
|
||||
sgn_eq = m.mk_eq(x_sgn, y_sgn);
|
||||
sgn_diff = m.mk_not(sgn_eq);
|
||||
|
||||
expr_ref gt(m);
|
||||
mk_float_gt(f, num, args, gt);
|
||||
|
||||
mk_ite(gt, x, y, result);
|
||||
mk_ite(both_zero, y, result, result);
|
||||
mk_ite(y_is_nan, x, result, result);
|
||||
mk_ite(x_is_nan, y, result, result);
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 4);
|
||||
SASSERT(m_util.is_bv2rm(args[0]));
|
||||
|
|
@ -3150,19 +3084,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
unsigned ebits = m_util.get_ebits(fp_srt);
|
||||
unsigned sbits = m_util.get_sbits(fp_srt);
|
||||
|
||||
expr_ref nanv(m);
|
||||
if (m_hi_fp_unspecified)
|
||||
// The "hardware interpretation" is 01...10...01.
|
||||
nanv = 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))));
|
||||
else
|
||||
mk_to_ieee_bv_unspecified(f, num, args, nanv);
|
||||
expr_ref unspec(m);
|
||||
mk_to_ieee_bv_unspecified(f, num, args, unspec);
|
||||
|
||||
expr_ref sgn_e_s(m);
|
||||
join_fp(x, sgn_e_s);
|
||||
m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
|
||||
m_simp.mk_ite(x_is_nan, unspec, sgn_e_s, result);
|
||||
|
||||
TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
|
|
@ -3174,26 +3101,15 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
|
|||
unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int();
|
||||
unsigned sbits = f->get_domain()[0]->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));
|
||||
}
|
||||
if (m_hi_fp_unspecified)
|
||||
mk_nan(f->get_range(), result);
|
||||
else {
|
||||
expr * n = args[0];
|
||||
expr_ref n_bv(m);
|
||||
join_fp(n, n_bv);
|
||||
|
||||
func_decl * f_bv;
|
||||
if (!m_uf2bvuf.find(f, f_bv)) {
|
||||
sort * domain[2] = { m.get_sort(n_bv) };
|
||||
f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
|
||||
m_uf2bvuf.insert(f, f_bv);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(f_bv);
|
||||
}
|
||||
|
||||
sort * domain[1] = { m.get_sort(n_bv) };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, n_bv);
|
||||
|
||||
expr_ref exp_bv(m), exp_all_ones(m);
|
||||
|
|
@ -3382,14 +3298,8 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr *
|
|||
expr_ref n_bv(m);
|
||||
join_fp(n, n_bv);
|
||||
|
||||
func_decl * f_bv;
|
||||
if (!m_uf2bvuf.find(f, f_bv)) {
|
||||
sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) };
|
||||
f_bv = m.mk_fresh_func_decl(0, 2, domain, f->get_range());
|
||||
m_uf2bvuf.insert(f, f_bv);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(f_bv);
|
||||
}
|
||||
sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, rm_bv, n_bv);
|
||||
}
|
||||
|
||||
|
|
@ -3407,14 +3317,8 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
|
|||
expr_ref n_bv(m);
|
||||
join_fp(n, n_bv);
|
||||
|
||||
func_decl * f_bv;
|
||||
if (!m_uf2bvuf.find(f, f_bv)) {
|
||||
sort * domain[2] = { m.get_sort(n_bv) };
|
||||
f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
|
||||
m_uf2bvuf.insert(f, f_bv);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(f_bv);
|
||||
}
|
||||
sort * domain[1] = { m.get_sort(n_bv) };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, n_bv);
|
||||
}
|
||||
}
|
||||
|
|
@ -4190,13 +4094,25 @@ void fpa2bv_converter::reset(void) {
|
|||
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);
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_min_max_specials.begin();
|
||||
it != m_min_max_specials.end();
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_min_max_ufs.begin();
|
||||
it != m_min_max_ufs.end();
|
||||
it++) {
|
||||
m.dec_ref(it->m_key);
|
||||
m.dec_ref(it->m_value.first);
|
||||
m.dec_ref(it->m_value.second);
|
||||
}
|
||||
m_min_max_specials.reset();
|
||||
m_min_max_ufs.reset();
|
||||
m_extra_assertions.reset();
|
||||
}
|
||||
|
||||
func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
|
||||
func_decl * res;
|
||||
if (!m_uf2bvuf.find(f, res)) {
|
||||
res = m.mk_fresh_func_decl(0, f->get_arity(), domain, range);
|
||||
m_uf2bvuf.insert(f, res);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(res);
|
||||
TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@ protected:
|
|||
const2bv_t m_const2bv;
|
||||
const2bv_t m_rm_const2bv;
|
||||
uf2bvuf_t m_uf2bvuf;
|
||||
special_t m_min_max_specials;
|
||||
special_t m_min_max_ufs;
|
||||
|
||||
friend class fpa2bv_model_converter;
|
||||
friend class bv2fpa_converter;
|
||||
|
|
@ -87,7 +87,7 @@ public:
|
|||
void mk_numeral(sort * s, mpf const & v, expr_ref & result);
|
||||
virtual void mk_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_rm_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
virtual void mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_var(unsigned base_inx, sort * srt, expr_ref & result);
|
||||
|
||||
void mk_pinf(func_decl * f, expr_ref & result);
|
||||
|
|
@ -147,18 +147,15 @@ public:
|
|||
void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
|
||||
|
||||
void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
virtual expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
void reset(void);
|
||||
|
||||
void dbg_decouple(const char * prefix, expr_ref & e);
|
||||
expr_ref_vector m_extra_assertions;
|
||||
|
||||
special_t const & get_min_max_specials() const { return m_min_max_specials; };
|
||||
special_t const & get_min_max_specials() const { return m_min_max_ufs; };
|
||||
const2bv_t const & get_const2bv() const { return m_const2bv; };
|
||||
const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; };
|
||||
uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; };
|
||||
|
|
@ -202,12 +199,6 @@ protected:
|
|||
|
||||
void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result);
|
||||
|
||||
sort_ref replace_float_sorts(sort * s);
|
||||
func_decl_ref replace_function(func_decl * f);
|
||||
expr_ref replace_float_arg(expr * a);
|
||||
void mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result);
|
||||
func_decl * get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity);
|
||||
|
||||
private:
|
||||
void mk_nan(sort * s, expr_ref & result);
|
||||
void mk_nzero(sort * s, expr_ref & result);
|
||||
|
|
@ -226,6 +217,8 @@ private:
|
|||
void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
|
||||
|
||||
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
|
||||
func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -124,6 +124,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
|
||||
|
|
@ -147,14 +149,6 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
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_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_MIN_UNSPECIFIED:
|
||||
case OP_FPA_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE;
|
||||
case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
|
||||
|
||||
case OP_FPA_BVWRAP:
|
||||
case OP_FPA_BV2RM:
|
||||
return BR_FAILED;
|
||||
|
|
@ -169,7 +163,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
{
|
||||
SASSERT(!m_conv.is_float_family(f));
|
||||
if (m_conv.fu().contains_floats(f)) {
|
||||
m_conv.mk_function(f, num, args, result);
|
||||
m_conv.mk_uf(f, num, args, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -361,10 +361,6 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters
|
|||
case OP_FPA_REM: name = "fp.rem"; break;
|
||||
case OP_FPA_MIN: name = "fp.min"; break;
|
||||
case OP_FPA_MAX: name = "fp.max"; break;
|
||||
case OP_FPA_MIN_I: name = "fp.min_i"; break;
|
||||
case OP_FPA_MAX_I: name = "fp.max_i"; break;
|
||||
case OP_FPA_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break;
|
||||
case OP_FPA_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
|
|
@ -781,12 +777,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
case OP_FPA_BV2RM:
|
||||
return mk_bv2rm(k, num_parameters, parameters, arity, domain, range);
|
||||
|
||||
case OP_FPA_MIN_I:
|
||||
case OP_FPA_MAX_I:
|
||||
case OP_FPA_MIN_UNSPECIFIED:
|
||||
case OP_FPA_MAX_UNSPECIFIED:
|
||||
return mk_binary_decl(k, num_parameters, parameters, arity, domain, range);
|
||||
|
||||
default:
|
||||
m_manager->raise_exception("unsupported floating point operator");
|
||||
return 0;
|
||||
|
|
|
|||
|
|
@ -89,11 +89,6 @@ enum fpa_op_kind {
|
|||
OP_FPA_BVWRAP,
|
||||
OP_FPA_BV2RM,
|
||||
|
||||
OP_FPA_MIN_I,
|
||||
OP_FPA_MAX_I,
|
||||
OP_FPA_MIN_UNSPECIFIED,
|
||||
OP_FPA_MAX_UNSPECIFIED,
|
||||
|
||||
LAST_FLOAT_OP
|
||||
};
|
||||
|
||||
|
|
@ -351,21 +346,12 @@ public:
|
|||
}
|
||||
|
||||
bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); }
|
||||
bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; }
|
||||
bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BV2RM); }
|
||||
bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; }
|
||||
|
||||
bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_I); }
|
||||
bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); }
|
||||
bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); }
|
||||
bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); }
|
||||
bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); }
|
||||
bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); }
|
||||
|
||||
bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_I; }
|
||||
bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_UNSPECIFIED; }
|
||||
bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_I; }
|
||||
bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_UNSPECIFIED; }
|
||||
bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; }
|
||||
bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; }
|
||||
bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; }
|
||||
bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; }
|
||||
|
||||
|
|
|
|||
|
|
@ -94,12 +94,6 @@ 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_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break;
|
||||
case OP_FPA_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break;
|
||||
case OP_FPA_MIN_UNSPECIFIED:
|
||||
case OP_FPA_MAX_UNSPECIFIED:
|
||||
SASSERT(num_args == 2); st = BR_FAILED; break;
|
||||
|
||||
case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
|
||||
case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
|
||||
|
||||
|
|
@ -385,38 +379,13 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
}
|
||||
|
||||
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)) {
|
||||
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.minimum(v1, v2, r);
|
||||
result = m_util.mk_value(r);
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
expr_ref c(m()), v(m());
|
||||
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
|
||||
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
|
||||
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
|
||||
v = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
|
||||
|
||||
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MIN_I, arg1, arg2));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
|
||||
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))
|
||||
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
|
||||
else
|
||||
result = m_util.mk_min(arg1, arg2);
|
||||
return BR_FAILED;
|
||||
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.minimum(v1, v2, r);
|
||||
result = m_util.mk_value(r);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
@ -434,38 +403,13 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
}
|
||||
|
||||
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)) {
|
||||
result = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.maximum(v1, v2, r);
|
||||
result = m_util.mk_value(r);
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
expr_ref c(m()), v(m());
|
||||
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
|
||||
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
|
||||
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
|
||||
v = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2);
|
||||
|
||||
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MAX_I, arg1, arg2));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
|
||||
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))
|
||||
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
|
||||
else
|
||||
result = m_util.mk_max(arg1, arg2);
|
||||
return BR_FAILED;
|
||||
|
||||
scoped_mpf r(m_fm);
|
||||
m_fm.maximum(v1, v2, r);
|
||||
result = m_util.mk_value(r);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -884,22 +884,4 @@ namespace smt {
|
|||
out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
bool theory_fpa::include_func_interp(func_decl * f) {
|
||||
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
|
||||
|
||||
if (f->get_family_id() == get_family_id()) {
|
||||
bool include =
|
||||
m_fpa_util.is_min_unspecified(f) ||
|
||||
m_fpa_util.is_max_unspecified(f) ;
|
||||
if (include && !m_is_added_to_model.contains(f)) {
|
||||
//m_is_added_to_model.insert(f);
|
||||
//get_manager().inc_ref(f);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
else
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -158,7 +158,6 @@ namespace smt {
|
|||
virtual char const * get_name() const { return "fpa"; }
|
||||
|
||||
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
|
||||
virtual bool include_func_interp(func_decl * f);
|
||||
|
||||
void assign_eh(bool_var v, bool is_true);
|
||||
virtual void relevant_eh(app * n);
|
||||
|
|
@ -180,8 +179,6 @@ namespace smt {
|
|||
expr_ref convert_term(expr * e);
|
||||
expr_ref convert_conversion_term(expr * e);
|
||||
|
||||
void add_trail(ast * a);
|
||||
|
||||
void attach_new_th_var(enode * n);
|
||||
void assert_cnstr(expr * e);
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue