mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Improved support for FPA unspecified min/max values, model validation, and proof generation.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-21 20:11:59 +01:00
parent ca496f20cb
commit 9b5abcd55a
8 changed files with 192 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -42,6 +42,16 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_max_np_zeros(0, m),
m_extra_assertions(m) {
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m.mk_family_id("fpa")));
m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl());
m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl());
m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl());
m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl());
}
fpa2bv_converter::~fpa2bv_converter() {
@ -49,35 +59,48 @@ fpa2bv_converter::~fpa2bv_converter() {
}
void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
if (is_float(a) && is_float(b)) {
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp);
m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig);
expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp);
m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig);
dbg_decouple("fpa2bv_eq_sgn", eq_sgn);
dbg_decouple("fpa2bv_eq_exp", eq_exp);
dbg_decouple("fpa2bv_eq_sig", eq_sig);
dbg_decouple("fpa2bv_eq_sgn", eq_sgn);
dbg_decouple("fpa2bv_eq_exp", eq_exp);
dbg_decouple("fpa2bv_eq_sig", eq_sig);
expr_ref both_the_same(m);
m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same);
dbg_decouple("fpa2bv_eq_both_the_same", both_the_same);
expr_ref both_the_same(m);
m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same);
dbg_decouple("fpa2bv_eq_both_the_same", both_the_same);
// The SMT FPA theory asks for _one_ NaN value, but the bit-blasting
// has many, like IEEE754. This encoding of equality makes it look like
// a single NaN again.
expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m);
mk_is_nan(a, a_is_nan);
mk_is_nan(b, b_is_nan);
m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan);
dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan);
// The SMT FPA theory asks for _one_ NaN value, but the bit-blasting
// has many, like IEEE754. This encoding of equality makes it look like
// a single NaN again.
expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m);
mk_is_nan(a, a_is_nan);
mk_is_nan(b, b_is_nan);
m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan);
dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan);
m_simp.mk_or(both_are_nan, both_the_same, result);
m_simp.mk_or(both_are_nan, both_the_same, result);
}
else if (is_rm(a) && is_rm(b)) {
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
}
else
UNREACHABLE();
}
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
@ -224,6 +247,11 @@ void fpa2bv_converter::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr
m_bv_util.mk_extract(sbits - 2, 0, na),
result);
}
else if (m_util.is_rm(rng)) {
app_ref na(m);
na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
mk_rm(na, result);
}
else
result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
}
@ -242,6 +270,10 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex
expr * args[3] = { sgn, exp, sig };
new_args.push_back(m_bv_util.mk_concat(3, args));
}
else if (is_rm(args[i])) {
SASSERT(is_app_of(args[i], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
new_args.push_back(to_app(args[i])->get_arg(0));
}
else
new_args.push_back(args[i]);
}
@ -1073,6 +1105,21 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
mk_fp(m_bv_util.mk_numeral(0, 1), e, s, 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 c(m), v(m);
c = m.mk_and(m.mk_and(m_util.mk_is_zero(x), m_util.mk_is_zero(y)),
m.mk_or(m.mk_and(m_util.mk_is_positive(x), m_util.mk_is_negative(y)),
m.mk_and(m_util.mk_is_negative(x), m_util.mk_is_positive(y))));
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, x, y);
// Note: This requires BR_REWRITE_FULL afterwards.
result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y));
}
void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
@ -1117,9 +1164,6 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
// The hardware interpretation is -0.0.
mk_nzero(f, res);
else {
if (m_min_pn_zeros.get() == 0) m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
if (m_min_np_zeros.get() == 0) m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
expr_ref pn(m), np(m);
mk_fp(m_min_pn_zeros,
m_bv_util.mk_numeral(0, ebits),
@ -1130,24 +1174,31 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), ite(m);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, ite);
expr * args[] = { x, y };
mk_uninterpreted_function(f, 2, args, res);
expr_ref pzero(m), nzero(m), extra(m);
mk_pzero(f, pzero);
mk_nzero(f, nzero);
extra = m.mk_or(m.mk_eq(ite, pzero), m.mk_eq(ite, nzero));
m_extra_assertions.push_back(extra);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
}
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 c(m), v(m);
c = m.mk_and(m.mk_and(m_util.mk_is_zero(x), m_util.mk_is_zero(y)),
m.mk_or(m.mk_and(m_util.mk_is_positive(x), m_util.mk_is_negative(y)),
m.mk_and(m_util.mk_is_negative(x), m_util.mk_is_positive(y))));
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, x, y);
// Note: This requires BR_REWRITE_FULL afterwards.
result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y));
}
void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
@ -1192,9 +1243,6 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
// The hardware interpretation is +0.0.
mk_pzero(f, res);
else {
if (m_max_pn_zeros.get() == 0) m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
if (m_max_np_zeros.get() == 0) m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
expr_ref pn(m), np(m);
mk_fp(m_max_pn_zeros,
m_bv_util.mk_numeral(0, ebits),
@ -1205,10 +1253,11 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
}
return res;
@ -2085,23 +2134,20 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
result);
}
else if (num == 2 &&
m_bv_util.is_bv(args[0]) &&
m_bv_util.get_bv_size(args[0]) == 3 &&
m_util.is_rm(args[0]) &&
m_util.is_float(m.get_sort(args[1]))) {
// rm + float -> float
mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
}
else if (num == 2 &&
m_bv_util.is_bv(args[0]) &&
m_bv_util.get_bv_size(args[0]) == 3 &&
m_util.is_rm(args[0]) &&
(m_arith_util.is_int(args[1]) ||
m_arith_util.is_real(args[1]))) {
// rm + real -> float
mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
}
else if (num == 2 &&
m_bv_util.is_bv(args[0]) &&
m_bv_util.get_bv_size(args[0]) == 3 &&
m_util.is_rm(args[0]) &&
m_bv_util.is_bv(args[1])) {
// rm + signed bv -> float
mk_to_fp_signed(f, num, args, result);
@ -2117,8 +2163,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
mk_fp(args[0], args[1], args[2], result);
}
else if (num == 3 &&
m_bv_util.is_bv(args[0]) &&
m_bv_util.get_bv_size(args[0]) == 3 &&
m_util.is_rm(args[0]) &&
m_arith_util.is_numeral(args[1]) &&
m_arith_util.is_numeral(args[2]))
{
@ -2137,6 +2182,9 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
unsigned to_sbits = m_util.get_sbits(s);
unsigned to_ebits = m_util.get_ebits(s);
SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr * bv_rm = to_app(rm)->get_arg(0);
if (from_sbits == to_sbits && from_ebits == to_ebits)
result = x;
else {
@ -2285,7 +2333,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
expr_ref rounded(m);
expr_ref rm_e(rm, m);
expr_ref rm_e(bv_rm, m);
round(s, rm_e, res_sgn, res_sig, res_exp, rounded);
expr_ref is_neg(m), sig_inf(m);
@ -2310,19 +2358,20 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
"x: " << mk_ismt2_pp(x, m) << std::endl;);
SASSERT(m_util.is_float(s));
SASSERT(au().is_real(x) || au().is_int(x));
SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr * bv_rm = to_app(rm)->get_arg(0);
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) {
if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) {
rational tmp_rat; unsigned sz;
m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz);
m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz);
SASSERT(tmp_rat.is_int32());
SASSERT(sz == 3);
BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
mpf_rounding_mode mrm;
switch (bv_rm) {
switch ((BV_RM_VAL)tmp_rat.get_unsigned()) {
case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break;
@ -2359,11 +2408,11 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_pzero(f, result);
else {
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn);
mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz);
mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_nta);
mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_nte);
mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_tp);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn);
mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz);
scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager);
scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager);
@ -2428,7 +2477,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
sig = mk_fresh_const("fpa2bv_to_fp_real_sig", sbits + 4);
exp = mk_fresh_const("fpa2bv_to_fp_real_exp", ebits + 2);
expr_ref rme(rm, m);
expr_ref rme(bv_rm, m);
round(s, rme, sgn, sig, exp, result);
expr * e = m.mk_eq(m_util.mk_to_real(result), x);
@ -2734,9 +2783,8 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
SASSERT(num == 2);
SASSERT(m_util.is_float(f->get_range()));
SASSERT(m_bv_util.is_bv(args[0]));
SASSERT(m_bv_util.is_bv(args[1]));
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
SASSERT(m_bv_util.is_bv(args[1]));
expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0);

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

@ -83,7 +83,7 @@ public:
void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) 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_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -106,9 +106,7 @@ public:
void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(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);
void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -143,7 +141,12 @@ 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_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);
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
expr_ref mk_to_ubv_unspecified(unsigned width);

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

@ -165,15 +165,15 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
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:
case OP_FPA_MAX:
throw rewriter_exception("operator is not supported, you must simplify the goal before applying fpa2bv");
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_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:

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

@ -94,9 +94,9 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
SASSERT(num_args == 2); st = BR_FAILED; break;
case OP_FPA_INTERNAL_RM:
@ -436,12 +436,17 @@ 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) &&
!(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) {
scoped_mpf r(m_fm);
m_fm.minimum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
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_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
return BR_DONE;
}
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());
@ -466,12 +471,17 @@ 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) &&
!(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) {
scoped_mpf r(m_fm);
m_fm.maximum(v1, v2, r);
result = m_util.mk_value(r);
return BR_DONE;
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_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
return BR_DONE;
}
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());

32
src/smt/theory_fpa.cpp
View file

@ -74,7 +74,9 @@ namespace smt {
}
else {
SASSERT(is_rm(f->get_range()));
result = m_th.wrap(m.mk_const(f));
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
mk_rm(bv, result);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -83,7 +85,7 @@ namespace smt {
void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
// TODO: This introduces temporary variables/func_decls that should be filtered in the end.
return fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
}
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@ -106,7 +108,6 @@ namespace smt {
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
m_extra_assertions.push_back(sc);
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
return res;
}
@ -130,7 +131,6 @@ namespace smt {
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
m_extra_assertions.push_back(sc);
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
return res;
}
@ -349,11 +349,14 @@ namespace smt {
}
}
else if (m_fpa_util.is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(e_conv) == 3);
m_th_rw(e_conv, res);
SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m);
bv_rm = to_app(e_conv)->get_arg(0);
m_th_rw(bv_rm);
m_converter.mk_rm(bv_rm, res);
}
else if (m_fpa_util.is_float(e)) {
else if (m_fpa_util.is_float(e)) {
SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_FP));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
@ -440,7 +443,7 @@ namespace smt {
sort * srt = m.get_sort(e);
expr_ref res(m);
if (m_fpa_util.is_rm(srt)) {
res = to_app(e)->get_arg(0);
m_converter.mk_rm(to_app(e)->get_arg(0), res);
}
else {
SASSERT(m_fpa_util.is_float(srt));
@ -468,7 +471,6 @@ namespace smt {
TRACE("t_fpa_detail", tout << "cached:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}
else {
if (m_fpa_util.is_unwrap(e))
@ -490,7 +492,7 @@ namespace smt {
m.inc_ref(res);
m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
}
return res;
}
@ -663,7 +665,8 @@ namespace smt {
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
if ((fu.is_float(xe) && fu.is_float(ye)) ||
(fu.is_rm(xe) && fu.is_rm(ye)))
m_converter.mk_eq(xc, yc, c);
else
c = m.mk_eq(xc, yc);
@ -682,7 +685,7 @@ namespace smt {
TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
fpa_util & fu = m_fpa_util;
@ -699,7 +702,8 @@ namespace smt {
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye)) {
if ((fu.is_float(xe) && fu.is_float(ye))||
(fu.is_rm(xe) && fu.is_rm(ye))) {
m_converter.mk_eq(xc, yc, c);
c = m.mk_not(c);
}

10
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -210,6 +210,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
obj_hashtable<func_decl> seen;
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++)
seen.insert(*it);
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
@ -353,6 +358,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf);
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide);
}

16
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -27,13 +27,14 @@ class fpa2bv_model_converter : public model_converter {
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf) :
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) :
m(m) {
// Just create a copy?
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
it != const2bv.end();
it++)
@ -58,12 +59,20 @@ public:
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_hashtable<func_decl>::iterator it = decls_to_hide.begin();
it != decls_to_hide.end();
it++)
{
m_decls_to_hide.insert(*it);
m.inc_ref(*it);
}
}
virtual ~fpa2bv_model_converter() {
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);
dec_ref_collection_values(m, m_decls_to_hide);
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
@ -96,6 +105,7 @@ protected:
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf);
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide);
#endif

9
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -107,7 +107,7 @@ class fpa2bv_tactic : public tactic {
}
if (g->models_enabled())
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf());
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide());
g->inc_depth();
result.push_back(g.get());
@ -151,7 +151,12 @@ public:
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
try {
(*m_imp)(in, result, mc, pc, core);
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());
}
}
virtual void cleanup() {