diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index eb8aba9ae..1adedb2d7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) { s = to_sort(parameters[0].get_ast()); } + else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) { + s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + } else if (range != 0 && is_float_sort(range)) { s = range; } @@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } + else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) { + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_fp"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameter type to to_fp"); + int ebits = parameters[0].get_int(); + int sbits = parameters[1].get_int(); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) @@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("fp unsupported; use a logic with BV support"); + if (arity != 3) + m_manager->raise_exception("invalid number of arguments to fp"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || + !is_sort_of(domain[1], m_bv_fid, BV_SORT) || + !is_sort_of(domain[2], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1); + symbol name("fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support"); + if (arity != 2) + m_manager->raise_exception("invalid number of arguments to to_fp_unsigned"); + if (is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismtach"); + if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp_unsigned"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); case OP_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_FP: + return mk_from3bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_FP_UNSIGNED: + return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_UBV: + return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_SBV: + return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_REAL: + return mk_to_real(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co if (m_bv_plugin) op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - // We also support draft version 3 - op_names.push_back(builtin_name("fp", OP_TO_FLOAT)); + // These are the operators from the final draft of the SMT FloatingPoints standard + op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF)); + op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF)); op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN)); op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY)); @@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN)); op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); if (m_bv_plugin) { - // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV)); - // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV)); + op_names.push_back(builtin_name("fp", OP_FLOAT_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); + op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV)); + op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV)); } - - op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toReal", ?)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { sort_names.push_back(builtin_name("FP", FLOAT_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); + + // In the SMT FPA final draft, FP is called FloatingPoint + sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index f1b60a91b..3786b76ee 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -72,6 +72,12 @@ enum float_op_kind { OP_TO_FLOAT, OP_TO_IEEE_BV, + + OP_FLOAT_FP, + OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_UBV, + OP_FLOAT_TO_SBV, + OP_FLOAT_TO_REAL, LAST_FLOAT_OP }; @@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - + func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 6ef147f1c..ecd06ff38 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break; + case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; + case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; } return st; } @@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { return BR_FAILED; } + +br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { + bv_util bu(m()); + rational r1, r2, r3; + 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, + 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;); + result = m_util.mk_value(v); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 4a0879d4b..0f44d227c 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -73,6 +73,12 @@ public: br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, 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); }; #endif diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index ebccf4d52..144925164 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1836,6 +1836,21 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 1 && m_bv_util.is_bv(args[0])) { + sort * s = f->get_range(); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + expr * bv = args[0]; + int sz = m_bv_util.get_bv_size(bv); + SASSERT((unsigned)sz == to_sbits + to_ebits); + + m_bv_util.mk_extract(sz - 1, sz - 1, bv); + mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), + m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), + m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), + result); + } else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { // We also support float to float conversion sort * s = f->get_range(); @@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } +void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 3); + mk_triple(args[0], args[2], args[1], result); +} + +void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 821618bae..79c8039ef 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -122,7 +122,13 @@ public: void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d737683a8..b2e3da939 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index f3c913ccc..90cfc8c92 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -36,3 +36,77 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m, p), mk_fail_if_undecided_tactic()); } + +struct is_non_qffpa_predicate { + struct found {}; + ast_manager & m; + float_util u; + + is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == u.get_family_id()) + return; + + throw found(); + } +}; + +struct is_non_qffpabv_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + float_util fu; + + is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s))) + throw found(); + family_id fid = s->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == fu.get_family_id() || fid == bu.get_family_id()) + return; + + throw found(); + } +}; + +class is_qffpa_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +class is_qffpabv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qffpa_probe() { + return alloc(is_qffpa_probe); +} + +probe * mk_is_qffpabv_probe() { + return alloc(is_qffpabv_probe); +} + \ No newline at end of file diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 8ca2183c1..cd16c5817 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ +probe * mk_is_qffpa_probe(); +probe * mk_is_qffpabv_probe(); +/* + ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()") + ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()") +*/ + #endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index d65ba8d35..9ecc16ecf 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include"nra_tactic.h" #include"probe_arith.h" #include"quant_tactics.h" +#include"qffpa_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - mk_smt_tactic())))))))), + cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p), + mk_smt_tactic()))))))))), p); return st; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5910f55c9..8cb6ed4fc 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) { return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false)); } +mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) { + return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); +} + void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) { o.sbits = sbits; o.ebits = ebits; diff --git a/src/util/mpf.h b/src/util/mpf.h index 284b0ba7f..83646f9f3 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -182,6 +182,8 @@ public: mpf_exp_t mk_max_exp(unsigned ebits); mpf_exp_t mk_min_exp(unsigned ebits); + mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent); + /** \brief Return the biggest k s.t. 2^k <= a.