diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index bdaf2017e..8e2dd326a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1872,7 +1872,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args m_bv_util.is_bv(args[0]) && m_bv_util.get_bv_size(args[0]) == 3 && m_util.is_float(m.get_sort(args[1]))) { - // float -> float conversion + // rm + float -> float mk_to_fp_float(f, f->get_range(), args[0], args[1], result); } else if (num == 2 && @@ -1886,12 +1886,14 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args m_bv_util.is_bv(args[0]) && m_bv_util.get_bv_size(args[0]) == 3 && m_bv_util.is_bv(args[1])) { + // rm + signed bv -> float mk_to_fp_signed(f, num, args, result); } else if (num == 3 && m_bv_util.is_bv(args[0]) && m_bv_util.is_bv(args[1]) && - m_bv_util.is_bv(args[2])) { + m_bv_util.is_bv(args[2])) { + // 3 BV -> float SASSERT(m_bv_util.get_bv_size(args[0]) == 1); SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); @@ -1899,9 +1901,11 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args } else if (num == 3 && m_bv_util.is_bv(args[0]) && + m_bv_util.get_bv_size(args[0]) == 3 && m_arith_util.is_numeral(args[1]) && m_arith_util.is_numeral(args[2])) { + // rm + real + int -> float mk_to_fp_real_int(f, num, args, result); } else @@ -3206,7 +3210,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m); inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nround_lors)); expr *taway_args[2] = { m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nl_r)), - m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(3, nl_nr_sn)) }; + m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(3, nl_nr_sn)) }; inc_taway = m_bv_util.mk_bv_or(2, taway_args); inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args)); inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); diff --git a/src/ast/fpa/fpa2bv_rewriter_params.pyg b/src/ast/fpa/fpa2bv_rewriter_params.pyg index 42df0fa0e..91304f143 100644 --- a/src/ast/fpa/fpa2bv_rewriter_params.pyg +++ b/src/ast/fpa/fpa2bv_rewriter_params.pyg @@ -1,5 +1,5 @@ def_module_params(module_name='rewriter', class_name='fpa2bv_rewriter_params', export=True, - params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real)"), - )) + params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"), +)) diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index fc1521456..0e7901aca 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -206,11 +206,12 @@ public: }; class fpa_util { - ast_manager & m_manager; + ast_manager & m_manager; fpa_decl_plugin * m_plugin; - family_id m_fid; - arith_util m_a_util; - bv_util m_bv_util; + family_id m_fid; + arith_util m_a_util; + bv_util m_bv_util; + public: fpa_util(ast_manager & m); ~fpa_util(); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 9a8ab7da0..394c2f117 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -17,16 +17,21 @@ Notes: --*/ #include"fpa_rewriter.h" +#include"fpa_rewriter_params.hpp" -fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p): - m_util(m) { +fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : + m_util(m), + m_fm(m_util.fm()), + m_hi_fp_unspecified(true) { updt_params(p); } fpa_rewriter::~fpa_rewriter() { } -void fpa_rewriter::updt_params(params_ref const & p) { +void fpa_rewriter::updt_params(params_ref const & _p) { + fpa_rewriter_params p(_p); + m_hi_fp_unspecified = p.hi_fp_unspecified(); } void fpa_rewriter::get_param_descrs(param_descrs & r) { @@ -35,9 +40,25 @@ void fpa_rewriter::get_param_descrs(param_descrs & r) { br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status st = BR_FAILED; SASSERT(f->get_family_id() == get_fid()); - switch (f->get_decl_kind()) { - case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; - case OP_FPA_TO_FP_UNSIGNED: st = mk_to_fp_unsigned(f, num_args, args, result); break; + fpa_op_kind k = (fpa_op_kind)f->get_decl_kind(); + switch (k) { + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_ZERO: + SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break; + + case OP_FPA_PLUS_INF: + case OP_FPA_MINUS_INF: + case OP_FPA_NAN: + case OP_FPA_PLUS_ZERO: + case OP_FPA_MINUS_ZERO: + SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break; + + case OP_FPA_NUM: + SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break; + case OP_FPA_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break; case OP_FPA_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break; case OP_FPA_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; @@ -63,115 +84,208 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; + case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; - case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; - case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; + case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break; + case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; + case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; - case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: + SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; + + default: + NOT_IMPLEMENTED_YET(); } return st; } +br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + unsigned bv_sz = f->get_parameter(0).get_int(); + + bv_util bu(m()); + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 0. + result = bu.mk_numeral(0, bv_sz); + else + result = m_util.mk_internal_to_real_unspecified(); + + return BR_DONE; +} + +br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + unsigned bv_sz = f->get_parameter(0).get_int(); + + bv_util bu(m()); + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 0. + result = bu.mk_numeral(0, bv_sz); + else + result = m_util.mk_internal_to_real_unspecified(); + + return BR_DONE; +} + +br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { + if (m_hi_fp_unspecified) + result = m_util.au().mk_numeral(0, false); + else + // The "hardware interpretation" is 0. + result = m_util.mk_internal_to_real_unspecified(); + + return BR_DONE; +} + br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); + bv_util bu(m()); + scoped_mpf v(m_fm); + mpf_rounding_mode rmv; + rational r1, r2, r3; + unsigned bvs1, bvs2, bvs3; unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); - if (num_args == 2) { - mpf_rounding_mode rm; - if (!m_util.is_rm_numeral(args[0], rm)) + if (num_args == 1) { + if (bu.is_numeral(args[0], r1, bvs1)) { + // BV -> float + SASSERT(bvs1 == sbits + ebits); + unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); + unsynch_mpq_manager & mpqm = m_fm.mpq_manager(); + scoped_mpz sig(mpzm), exp(mpzm); + + const mpz & sm1 = m_fm.m_powers2(sbits - 1); + const mpz & em1 = m_fm.m_powers2(ebits); + + scoped_mpq q(mpqm); + mpqm.set(q, r1.to_mpq()); + SASSERT(mpzm.is_one(q.get().denominator())); + scoped_mpz z(mpzm); + z = q.get().numerator(); + + mpzm.rem(z, sm1, sig); + mpzm.div(z, sm1, z); + + mpzm.rem(z, em1, exp); + mpzm.div(z, em1, z); + + SASSERT(mpzm.is_int64(exp)); + mpf_exp_t mpf_exp = mpzm.get_int64(exp); + + m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp); + result = m_util.mk_value(v); + return BR_DONE; + } + } + else if (num_args == 2) { + if (!m_util.is_rm_numeral(args[0], rmv)) return BR_FAILED; - rational q; - scoped_mpf q_mpf(m_util.fm()); - if (m_util.au().is_numeral(args[1], q)) { - TRACE("fp_rewriter", tout << "q: " << q << std::endl; ); - scoped_mpf v(m_util.fm()); - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); - result = m_util.mk_value(v); - m_util.fm().del(v); + if (m_util.au().is_numeral(args[1], r1)) { + // rm + real -> float + TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); + scoped_mpf v(m_fm); + m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); + result = m_util.mk_value(v); // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (m_util.is_numeral(args[1], q_mpf)) { - TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); - scoped_mpf v(m_util.fm()); - m_util.fm().set(v, ebits, sbits, rm, q_mpf); + else if (m_util.is_numeral(args[1], v)) { + // rm + float -> float + TRACE("fp_rewriter", tout << "v: " << m_fm.to_string(v) << std::endl; ); + scoped_mpf v(m_fm); + m_fm.set(v, ebits, sbits, rmv, v); result = m_util.mk_value(v); - m_util.fm().del(v); // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else - return BR_FAILED; + else if (bu.is_numeral(args[1], r1, bvs1)) { + // rm + signed bv -> float + scoped_mpf v(m_fm); + m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); + result = m_util.mk_value(v); + return BR_DONE; + } } - else if (num_args == 3) { - bv_util bu(m()); - rational r1, r2, r3; - unsigned bvs1, bvs2, bvs3; - - if (m_util.is_rm(args[0]) && + else if (num_args == 3) { + if (m_util.is_rm_numeral(args[0], rmv) && m_util.au().is_real(args[1]) && m_util.au().is_int(args[2])) { - mpf_rounding_mode rm; - if (!m_util.is_rm_numeral(args[0], rm)) + // rm + real + int -> float + if (!m_util.is_rm_numeral(args[0], rmv) || + !m_util.au().is_numeral(args[1], r1) || + !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; - rational q; - if (!m_util.au().is_numeral(args[1], q)) - return BR_FAILED; - - rational e; - if (!m_util.au().is_numeral(args[2], e)) - return BR_FAILED; - - TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";); - scoped_mpf v(m_util.fm()); - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); + TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); + scoped_mpf v(m_fm); + m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); result = m_util.mk_value(v); - m_util.fm().del(v); return BR_DONE; } else if (bu.is_numeral(args[0], r1, bvs1) && bu.is_numeral(args[1], r2, bvs2) && bu.is_numeral(args[2], r3, bvs3)) { - SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator())); - SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator())); - SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator())); - scoped_mpf v(m_util.fm()); - mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator()); - m_util.fm().set(v, bvs2, bvs3 + 1, + // 3 BV -> float + SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); + SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator())); + SASSERT(m_fm.mpz_manager().is_int64(r3.to_mpq().numerator())); + scoped_mpf v(m_fm); + mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator()); + m_fm.set(v, bvs2, bvs3 + 1, r1.is_one(), r3.to_mpq().numerator(), - m_util.fm().unbias_exp(bvs2, biased_exp)); - TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;); + m_fm.unbias_exp(bvs2, biased_exp)); + TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;); result = m_util.mk_value(v); return BR_DONE; - } - else - return BR_FAILED; + } } - else - return BR_FAILED; + + return BR_FAILED; } -br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); + SASSERT(f->get_parameter(1).is_int()); + bv_util bu(m()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + mpf_rounding_mode rmv; + rational r; + unsigned bvs; + if (m_util.is_rm_numeral(arg1, rmv) && + bu.is_numeral(arg2, r, bvs)) { + scoped_mpf v(m_fm); + m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); + result = m_util.mk_value(v); + return BR_DONE; + } + return BR_FAILED; } br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()), v3(m_util.fm()); + scoped_mpf v2(m_fm), v3(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { - scoped_mpf t(m_util.fm()); - m_util.fm().add(rm, v2, v3, t); + scoped_mpf t(m_fm); + m_fm.add(rm, v2, v3, t); result = m_util.mk_value(t); return BR_DONE; } @@ -189,10 +303,10 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()), v3(m_util.fm()); + scoped_mpf v2(m_fm), v3(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { - scoped_mpf t(m_util.fm()); - m_util.fm().mul(rm, v2, v3, t); + scoped_mpf t(m_fm); + m_fm.mul(rm, v2, v3, t); result = m_util.mk_value(t); return BR_DONE; } @@ -204,10 +318,10 @@ br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()), v3(m_util.fm()); + scoped_mpf v2(m_fm), v3(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { - scoped_mpf t(m_util.fm()); - m_util.fm().div(rm, v2, v3, t); + scoped_mpf t(m_fm); + m_fm.div(rm, v2, v3, t); result = m_util.mk_value(t); return BR_DONE; } @@ -238,22 +352,21 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { return BR_DONE; } - scoped_mpf v1(m_util.fm()); + scoped_mpf v1(m_fm); if (m_util.is_numeral(arg1, v1)) { - m_util.fm().neg(v1); + m_fm.neg(v1); result = m_util.mk_value(v1); return BR_DONE; } - // TODO: more simplifications return BR_FAILED; } br_status fpa_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { - scoped_mpf v1(m_util.fm()), v2(m_util.fm()); + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - scoped_mpf t(m_util.fm()); - m_util.fm().rem(v1, v2, t); + scoped_mpf t(m_fm); + m_fm.rem(v1, v2, t); result = m_util.mk_value(t); return BR_DONE; } @@ -267,6 +380,13 @@ br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) { return BR_DONE; } + scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { + if (m_fm.is_neg(v)) m_fm.neg(v); + result = m_util.mk_value(v); + return BR_DONE; + } + return BR_FAILED; } @@ -313,10 +433,10 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); + scoped_mpf v2(m_fm), v3(m_fm), v4(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) { - scoped_mpf t(m_util.fm()); - m_util.fm().fused_mul_add(rm, v2, v3, v4, t); + scoped_mpf t(m_fm); + m_fm.fused_mul_add(rm, v2, v3, v4, t); result = m_util.mk_value(t); return BR_DONE; } @@ -328,10 +448,10 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()); + scoped_mpf v2(m_fm); if (m_util.is_numeral(arg2, v2)) { - scoped_mpf t(m_util.fm()); - m_util.fm().sqrt(rm, v2, t); + scoped_mpf t(m_fm); + m_fm.sqrt(rm, v2, t); result = m_util.mk_value(t); return BR_DONE; } @@ -343,10 +463,10 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { - scoped_mpf v2(m_util.fm()); + scoped_mpf v2(m_fm); if (m_util.is_numeral(arg2, v2)) { - scoped_mpf t(m_util.fm()); - m_util.fm().round_to_integral(rm, v2, t); + scoped_mpf t(m_fm); + m_fm.round_to_integral(rm, v2, t); result = m_util.mk_value(t); return BR_DONE; } @@ -357,9 +477,9 @@ br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { // This the floating point theory == br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { - scoped_mpf v1(m_util.fm()), v2(m_util.fm()); + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - result = (m_util.fm().eq(v1, v2)) ? m().mk_true() : m().mk_false(); + result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -402,9 +522,9 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE3; } - scoped_mpf v1(m_util.fm()), v2(m_util.fm()); + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - result = (m_util.fm().lt(v1, v2)) ? m().mk_true() : m().mk_false(); + result = (m_fm.lt(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -422,9 +542,10 @@ br_status fpa_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) { result = m().mk_false(); return BR_DONE; } - scoped_mpf v1(m_util.fm()), v2(m_util.fm()); + + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - result = (m_util.fm().le(v1, v2)) ? m().mk_true() : m().mk_false(); + result = (m_fm.le(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -437,9 +558,9 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { } br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_zero(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -447,9 +568,9 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_nzero(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -457,9 +578,9 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_pzero(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -467,9 +588,9 @@ br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_nan(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -477,9 +598,9 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_inf(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -487,9 +608,9 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_normal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -497,9 +618,9 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_denormal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -507,9 +628,9 @@ br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false(); + result = (m_fm.is_neg(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -517,9 +638,9 @@ br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { - scoped_mpf v(m_util.fm()); + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { - result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true(); + result = (m_fm.is_neg(v) || m_fm.is_nan(v)) ? m().mk_false() : m().mk_true(); return BR_DONE; } @@ -529,7 +650,7 @@ br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { // This the SMT = br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { - scoped_mpf v1(m_util.fm()), v2(m_util.fm()); + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { // Note: == is the floats-equality, here we need normal equality. result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() : @@ -547,21 +668,24 @@ br_status fpa_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { } br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { + unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); bv_util bu(m()); rational r1, r2, r3; - unsigned bvs1, bvs2, bvs3; + unsigned bvs1, bvs2, bvs3; - if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) { - SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator())); - SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator())); - SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator())); - scoped_mpf v(m_util.fm()); - mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator()); - m_util.fm().set(v, bvs2, bvs3 + 1, + if (bu.is_numeral(arg1, r1, bvs1) && + bu.is_numeral(arg2, r2, bvs2) && + bu.is_numeral(arg3, r3, bvs3)) { + SASSERT(mpzm.is_one(r2.to_mpq().denominator())); + SASSERT(mpzm.is_one(r3.to_mpq().denominator())); + SASSERT(mpzm.is_int64(r3.to_mpq().numerator())); + scoped_mpf v(m_fm); + mpf_exp_t biased_exp = mpzm.get_int64(r2.to_mpq().numerator()); + m_fm.set(v, bvs2, bvs3 + 1, r1.is_one(), r3.to_mpq().numerator(), - m_util.fm().unbias_exp(bvs2, biased_exp)); - TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_util.fm().to_string(v) << std::endl;); + m_fm.unbias_exp(bvs2, biased_exp)); + TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;); result = m_util.mk_value(v); return BR_DONE; } @@ -569,24 +693,68 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & return BR_FAILED; } -br_status fpa_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + int bv_sz = f->get_parameter(0).get_int(); + mpf_rounding_mode rmv; + scoped_mpf v(m_fm); + + if (m_util.is_rm_numeral(arg1, rmv) && + m_util.is_numeral(arg2, v)) { + + if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { + result = m_util.mk_internal_to_ubv_unspecified(bv_sz); + return BR_REWRITE_FULL; + } + + bv_util bu(m()); + scoped_mpq q(m_fm.mpq_manager()); + m_fm.to_sbv_mpq(rmv, v, q); + rational r(q); + result = bu.mk_numeral(r, bv_sz); + return BR_DONE; + } + return BR_FAILED; } -br_status fpa_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + int bv_sz = f->get_parameter(0).get_int(); + mpf_rounding_mode rmv; + scoped_mpf v(m_fm); + + if (m_util.is_rm_numeral(arg1, rmv) && + m_util.is_numeral(arg2, v)) { + + if (m_fm.is_nan(v) || m_fm.is_inf(v)) { + result = m_util.mk_internal_to_sbv_unspecified(bv_sz); + return BR_REWRITE_FULL; + } + + bv_util bu(m()); + scoped_mpq q(m_fm.mpq_manager()); + m_fm.to_sbv_mpq(rmv, v, q); + rational r(q); + result = bu.mk_numeral(r, bv_sz); + return BR_DONE; + } + return BR_FAILED; } -br_status fpa_rewriter::mk_to_real(expr * arg1, expr_ref & result) { - scoped_mpf fv(m_util.fm()); +br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { + scoped_mpf v(m_fm); - if (m_util.is_numeral(arg1, fv)) { - if (m_fm.is_nan(fv) || m_fm.is_inf(fv)) { + if (m_util.is_numeral(arg, v)) { + if (m_fm.is_nan(v) || m_fm.is_inf(v)) { result = m_util.mk_internal_to_real_unspecified(); } else { scoped_mpq r(m_fm.mpq_manager()); - m_fm.to_rational(fv, r); + m_fm.to_rational(v, r); result = m_util.au().mk_numeral(r.get(), false); } return BR_DONE; diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index a10df95ca..2c76fad6a 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -27,7 +27,8 @@ Notes: class fpa_rewriter { fpa_util m_util; - mpf_manager m_fm; + mpf_manager & m_fm; + bool m_hi_fp_unspecified; app * mk_eq_nan(expr * arg); app * mk_neq_nan(expr * arg); @@ -44,7 +45,7 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); - + br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); @@ -75,12 +76,16 @@ public: br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_real(expr * arg1, expr_ref & result); + br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_real(expr * arg, expr_ref & result); + + br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result); + br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result); + br_status mk_to_real_unspecified(expr_ref & result); }; #endif diff --git a/src/ast/rewriter/fpa_rewriter_params.pyg b/src/ast/rewriter/fpa_rewriter_params.pyg new file mode 100644 index 000000000..85973e744 --- /dev/null +++ b/src/ast/rewriter/fpa_rewriter_params.pyg @@ -0,0 +1,5 @@ +def_module_params(module_name='rewriter', + class_name='fpa_rewriter_params', + export=True, + params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"), +)) diff --git a/src/ast/simplifier/fpa_simplifier_plugin.h b/src/ast/simplifier/fpa_simplifier_plugin.h index 13a235091..08fa6c49b 100644 --- a/src/ast/simplifier/fpa_simplifier_plugin.h +++ b/src/ast/simplifier/fpa_simplifier_plugin.h @@ -22,8 +22,8 @@ Author: #include"fpa_rewriter.h" class fpa_simplifier_plugin : public simplifier_plugin { - fpa_util m_util; - fpa_rewriter m_rw; + fpa_util m_util; + fpa_rewriter m_rw; public: fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 6b081f0a5..c45898cc7 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -89,6 +89,8 @@ public: virtual result operator()(goal const & g) { return !test(g); } + + virtual ~is_qffp_probe() {} }; probe * mk_is_qffp_probe() { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index de4107746..323ffa3af 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1098,6 +1098,46 @@ void mpf_manager::to_mpz(mpf const & x, unsynch_mpz_manager & zm, mpz & o) { zm.mul2k(o, e); } +void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o) { + SASSERT(!is_nan(x) && !is_inf(x)); + + scoped_mpf t(*this); + scoped_mpz z(m_mpz_manager); + + set(t, x); + unpack(t, true); + + SASSERT(t.exponent() < INT_MAX); + + m_mpz_manager.set(z, t.significand()); + if (t.sign()) m_mpz_manager.neg(z); + mpf_exp_t e = (mpf_exp_t)t.exponent() - t.sbits() + 1; + if (e < 0) { + bool last = false, round = false, guard = false, sticky = m_mpz_manager.is_odd(z); + for (; e != 0; e++) { + m_mpz_manager.machine_div2k(z, 1); + sticky |= guard; + guard = round; + round = last; + last = m_mpz_manager.is_odd(z); + } + bool inc = false; + switch (rm) { + case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break; + case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Check! + case MPF_ROUND_TOWARD_POSITIVE: inc = (!m_mpz_manager.is_neg(z) && (round || sticky)); break; + case MPF_ROUND_TOWARD_NEGATIVE: inc = (m_mpz_manager.is_neg(z) && (round || sticky)); break; + case MPF_ROUND_TOWARD_ZERO: inc = false; break; + default: UNREACHABLE(); + } + if (inc) m_mpz_manager.inc(z); + } + else + m_mpz_manager.mul2k(z, (unsigned) e); + + m_mpq_manager.set(o, z); +} + void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { SASSERT(x.sbits == y.sbits && x.ebits == y.ebits); @@ -1662,7 +1702,8 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) { bool inc = false; switch (rm) { case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break; - case MPF_ROUND_NEAREST_TAWAY: inc = round; break; // CMW: Check this. + // case MPF_ROUND_NEAREST_TAWAY: inc = round; break; // CMW: Check + case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Fix ok? case MPF_ROUND_TOWARD_POSITIVE: inc = (!o.sign && (round || sticky)); break; case MPF_ROUND_TOWARD_NEGATIVE: inc = (o.sign && (round || sticky)); break; case MPF_ROUND_TOWARD_ZERO: inc = false; break; diff --git a/src/util/mpf.h b/src/util/mpf.h index 39eb7330e..bac502c58 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -206,6 +206,8 @@ public: */ unsigned prev_power_of_two(mpf const & a); + void to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o); + protected: bool has_bot_exp(mpf const & x); bool has_top_exp(mpf const & x); @@ -218,8 +220,8 @@ protected: void mk_round_inf(mpf_rounding_mode rm, mpf & o); // Convert x into a mpz numeral. zm is the manager that owns o. - void to_mpz(mpf const & x, unsynch_mpz_manager & zm, mpz & o); - void to_mpz(mpf const & x, scoped_mpz & o) { to_mpz(x, o.m(), o); } + void to_mpz(mpf const & x, unsynch_mpz_manager & zm, mpz & o); + void to_mpz(mpf const & x, scoped_mpz & o) { to_mpz(x, o.m(), o); } class powers2 { unsynch_mpz_manager & m;