diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index cba2b3a7f..c3feeb10a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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(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); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index ed59a32d1..95f2ca057 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -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); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index e2ecc388a..c3720421c 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -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: diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 4da3b3169..062703be0 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -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()); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 66af5c815..701efb2ba 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index eb6d724c9..6ead927e0 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -210,6 +210,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { obj_hashtable seen; + for (obj_hashtable::iterator it = m_decls_to_hide.begin(); + it != m_decls_to_hide.end(); + it++) + seen.insert(*it); + for (obj_map::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 const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf); + obj_map const & uf2bvuf, + obj_hashtable const & decls_to_hide) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 021538ac1..a864f753a 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -27,13 +27,14 @@ class fpa2bv_model_converter : public model_converter { obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_hashtable m_decls_to_hide; public: fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf) : + obj_map const & uf2bvuf, + obj_hashtable const & decls_to_hide) : m(m) { - // Just create a copy? for (obj_map::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::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 const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf); + obj_map const & uf2bvuf, + obj_hashtable const & decls_to_hide); #endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 07669f513..4418f0f9f 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -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() {