From 31a017e99e1569b3913bd260816a3b9a45d44b3f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 22 Oct 2014 19:47:50 +0100 Subject: [PATCH] FPA: standard function names consistency, improved error messages, bugfixes. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 308 +++++++++++++++------------- src/ast/float_decl_plugin.h | 45 ++-- src/ast/fpa/fpa2bv_converter.cpp | 88 ++++++-- src/ast/fpa/fpa2bv_converter.h | 9 +- src/ast/fpa/fpa2bv_rewriter.h | 18 +- src/ast/rewriter/float_rewriter.cpp | 41 ++-- src/ast/rewriter/float_rewriter.h | 9 +- 7 files changed, 303 insertions(+), 215 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 5466df069..f51101d79 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -40,11 +40,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) { SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin. m_manager->inc_ref(m_int_sort); - if (m_manager->has_plugin(symbol("bv"))) { - // bv plugin is optional, so m_bv_plugin may be 0 + // BV is not optional anymore. + SASSERT(m_manager->has_plugin(symbol("bv"))); m_bv_fid = m_manager->mk_family_id("bv"); m_bv_plugin = static_cast(m_manager->get_plugin(m_bv_fid)); - } } float_decl_plugin::~float_decl_plugin() { @@ -103,6 +102,18 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { m_fm.mk_nan(ebits, sbits, val); return true; } + else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_pzero(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_ZERO)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_nzero(ebits, sbits, val); + return true; + } return false; } @@ -156,7 +167,7 @@ sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { parameter ps[2] = { p1, p2 }; sort_size sz; sz = sort_size::mk_very_big(); // TODO: refine - return m_manager->mk_sort(symbol("FP"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps)); + return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps)); } sort * float_decl_plugin::mk_rm_sort() { @@ -176,6 +187,14 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); case ROUNDING_MODE_SORT: return mk_rm_sort(); + case FLOAT16_SORT: + return mk_float_sort(5, 11); + case FLOAT32_SORT: + return mk_float_sort(8, 24); + case FLOAT64_SORT: + return mk_float_sort(11, 53); + case FLOAT128_SORT: + return mk_float_sort(15, 133); default: m_manager->raise_exception("unknown floating point theory sort"); return 0; @@ -229,17 +248,18 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par unsigned ebits = s->get_parameter(0).get_int(); unsigned sbits = s->get_parameter(1).get_int(); scoped_mpf val(m_fm); - if (k == OP_FLOAT_NAN) { - m_fm.mk_nan(ebits, sbits, val); + + switch (k) + { + case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val); SASSERT(m_fm.is_nan(val)); + break; + case OP_FLOAT_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break; + case OP_FLOAT_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break; + case OP_FLOAT_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break; + case OP_FLOAT_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break; } - else if (k == OP_FLOAT_MINUS_INF) { - m_fm.mk_ninf(ebits, sbits, val); - } - else { - SASSERT(k == OP_FLOAT_PLUS_INF); - m_fm.mk_pinf(ebits, sbits, val); - } + return mk_value_decl(val); } @@ -248,14 +268,14 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point relation"); if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments"); symbol name; switch (k) { - case OP_FLOAT_EQ: name = "=="; break; - case OP_FLOAT_LT: name = "<"; break; - case OP_FLOAT_GT: name = ">"; break; - case OP_FLOAT_LE: name = "<="; break; - case OP_FLOAT_GE: name = ">="; break; + case OP_FLOAT_EQ: name = "fp.eq"; break; + case OP_FLOAT_LT: name = "fp.lt"; break; + case OP_FLOAT_GT: name = "fp.gt"; break; + case OP_FLOAT_LE: name = "fp.lte"; break; + case OP_FLOAT_GE: name = "fp.gte"; break; default: UNREACHABLE(); break; @@ -270,17 +290,18 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param if (arity != 1) m_manager->raise_exception("invalid number of arguments to floating point relation"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - case OP_FLOAT_IS_ZERO: name = "isZero"; break; - case OP_FLOAT_IS_NZERO: name = "isNZero"; break; - case OP_FLOAT_IS_PZERO: name = "isPZero"; break; - case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break; - case OP_FLOAT_IS_NAN: name = "isNaN"; break; - case OP_FLOAT_IS_INF: name = "isInfinite"; break; - case OP_FLOAT_IS_NORMAL: name = "isNormal"; break; - case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break; + case OP_FLOAT_IS_ZERO: name = "fp.isZero"; break; + case OP_FLOAT_IS_NZERO: name = "fp.isNZero"; break; + case OP_FLOAT_IS_PZERO: name = "fp.isPZero"; break; + case OP_FLOAT_IS_NEGATIVE: name = "fp.isNegative"; break; + case OP_FLOAT_IS_POSITIVE: name = "fp.isPositive"; break; + case OP_FLOAT_IS_NAN: name = "fp.isNaN"; break; + case OP_FLOAT_IS_INF: name = "fp.isInfinite"; break; + case OP_FLOAT_IS_NORMAL: name = "fp.isNormal"; break; + case OP_FLOAT_IS_SUBNORMAL: name = "fp.isSubnormal"; break; default: UNREACHABLE(); break; @@ -293,11 +314,11 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter if (arity != 1) m_manager->raise_exception("invalid number of arguments to floating point operator"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - case OP_FLOAT_ABS: name = "abs"; break; - case OP_FLOAT_UMINUS: name = "-"; break; + case OP_FLOAT_ABS: name = "fp.abs"; break; + case OP_FLOAT_NEG: name = "fp.neg"; break; default: UNREACHABLE(); break; @@ -310,12 +331,12 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); symbol name; switch (k) { - case OP_FLOAT_REM: name = "remainder"; break; - case OP_FLOAT_MIN: name = "fp.min"; break; - case OP_FLOAT_MAX: name = "fp.max"; break; + case OP_FLOAT_REM: name = "fp.rem"; break; + case OP_FLOAT_MIN: name = "fp.min"; break; + case OP_FLOAT_MAX: name = "fp.max"; break; default: UNREACHABLE(); break; @@ -327,14 +348,16 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param unsigned arity, sort * const * domain, sort * range) { if (arity != 3) m_manager->raise_exception("invalid number of arguments to floating point operator"); - if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); + if (domain[1] != domain[2] || !is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts"); symbol name; switch (k) { - case OP_FLOAT_ADD: name = "+"; break; - case OP_FLOAT_SUB: name = "-"; break; - case OP_FLOAT_MUL: name = "*"; break; - case OP_FLOAT_DIV: name = "/"; break; + case OP_FLOAT_ADD: name = "fp.add"; break; + case OP_FLOAT_SUB: name = "fp.sub"; break; + case OP_FLOAT_MUL: name = "fp.mul"; break; + case OP_FLOAT_DIV: name = "fp.div"; break; default: UNREACHABLE(); break; @@ -346,12 +369,14 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame unsigned arity, sort * const * domain, sort * range) { if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); - if (!is_rm_sort(domain[0]) || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument"); + if (!is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument"); symbol name; switch (k) { - case OP_FLOAT_SQRT: name = "squareRoot"; break; - case OP_FLOAT_ROUND_TO_INTEGRAL: name = "roundToIntegral"; break; + case OP_FLOAT_SQRT: name = "fp.sqrt"; break; + case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break; default: UNREACHABLE(); break; @@ -359,13 +384,15 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 4) m_manager->raise_exception("invalid number of arguments to fused_ma operator"); - if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1])) - m_manager->raise_exception("sort mismatch"); - symbol name("fusedMA"); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument"); + if (domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1])) + m_manager->raise_exception("sort mismatch, expected arguments 1,2,3 of equal FloatingPoint sort"); + symbol name("fp.fma"); return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } @@ -375,12 +402,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, 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)) { - // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float! + // 3 BVs -> 1 FP sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); - symbol name("asFloat"); + symbol name("fp"); 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)) { + // 1 BV -> 1 FP if (num_parameters != 2) m_manager->raise_exception("invalid number of parameters to to_fp"); if (!parameters[0].is_int() || !parameters[1].is_int()) @@ -389,37 +417,67 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, int sbits = parameters[1].get_int(); sort * fp = mk_float_sort(ebits, sbits); - symbol name("asFloat"); + symbol name("to_fp"); + 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 == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_bv_fid, BV_SORT)) { + // Rounding + 1 BV -> 1 FP + 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("to_fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } + else if (arity == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_family_id, FLOAT_SORT)) { + // Rounding + 1 FP -> 1 FP + 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(); + if (!is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); + if (!is_sort_of(domain[1], m_family_id, FLOAT_SORT)) + m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort"); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("to_fp"); 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. + // 1 Real -> 1 FP if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) - m_manager->raise_exception("expecting two integer parameters to asFloat"); + m_manager->raise_exception("expecting two integer parameters to to_fp"); if (arity != 2 && arity != 3) - m_manager->raise_exception("invalid number of arguments to asFloat operator"); + m_manager->raise_exception("invalid number of arguments to to_fp operator"); if (arity == 3 && domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch"); - if (!is_rm_sort(domain[0]) || - !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT))) - m_manager->raise_exception("sort mismatch"); + m_manager->raise_exception("sort mismatch, expected second argument of Int sort"); + if (domain[1] != m_real_sort) + m_manager->raise_exception("sort mismatch, expected second argument of Real sort"); sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); + symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } } -func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (!m_bv_plugin) - m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support"); if (arity != 1) m_manager->raise_exception("invalid number of arguments to asIEEEBV"); if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch"); - - // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector. + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); + unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); parameter ps[] = { parameter(float_sz) }; sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); @@ -429,41 +487,34 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter 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"); + m_manager->raise_exception("sort mismatch"); 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, +func_decl * float_decl_plugin::mk_to_ubv(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"); + m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort"); if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) - m_manager->raise_exception("sort mismtach"); + m_manager->raise_exception("sort mismatch, expected second argument of BV sort"); sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("to_fp_unsigned"); + symbol name("fp.t_ubv"); 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(); @@ -498,14 +549,15 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_FLOAT_IS_ZERO: case OP_FLOAT_IS_NZERO: case OP_FLOAT_IS_PZERO: - case OP_FLOAT_IS_SIGN_MINUS: + case OP_FLOAT_IS_NEGATIVE: + case OP_FLOAT_IS_POSITIVE: case OP_FLOAT_IS_NAN: case OP_FLOAT_IS_INF: case OP_FLOAT_IS_NORMAL: case OP_FLOAT_IS_SUBNORMAL: return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_ABS: - case OP_FLOAT_UMINUS: + case OP_FLOAT_NEG: return mk_unary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_REM: case OP_FLOAT_MIN: @@ -517,20 +569,18 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_SUB: if (arity == 1) - return mk_unary_decl(OP_FLOAT_UMINUS, num_parameters, parameters, arity, domain, range); + return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range); else return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_SQRT: case OP_FLOAT_ROUND_TO_INTEGRAL: return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_FUSED_MA: - 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_FMA: + return mk_fma(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_IEEE_BV: + return mk_float_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: @@ -544,8 +594,11 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } void float_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF)); - op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF)); + // These are the operators from the final draft of the SMT FloatingPoint 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("+zero", OP_FLOAT_PLUS_ZERO)); + op_names.push_back(builtin_name("-zero", OP_FLOAT_MINUS_ZERO)); op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN)); op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN)); @@ -554,46 +607,6 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("roundTowardNegative", OP_RM_TOWARD_NEGATIVE)); op_names.push_back(builtin_name("roundTowardZero", OP_RM_TOWARD_ZERO)); - op_names.push_back(builtin_name("+", OP_FLOAT_ADD)); - op_names.push_back(builtin_name("-", OP_FLOAT_SUB)); - op_names.push_back(builtin_name("/", OP_FLOAT_DIV)); - op_names.push_back(builtin_name("*", OP_FLOAT_MUL)); - - op_names.push_back(builtin_name("abs", OP_FLOAT_ABS)); - op_names.push_back(builtin_name("remainder", OP_FLOAT_REM)); - op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA)); - op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT)); - op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL)); - - op_names.push_back(builtin_name("==", OP_FLOAT_EQ)); - - op_names.push_back(builtin_name("<", OP_FLOAT_LT)); - op_names.push_back(builtin_name(">", OP_FLOAT_GT)); - op_names.push_back(builtin_name("<=", OP_FLOAT_LE)); - op_names.push_back(builtin_name(">=", OP_FLOAT_GE)); - - op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN)); - op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF)); - op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO)); - op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO)); - op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO)); - op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL)); - op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); - op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); - - // Disabled min/max, clashes with user-defined min/max functions - // op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); - // op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); - - op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); - - if (m_bv_plugin) - op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - - // 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)); op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE)); @@ -601,44 +614,47 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO)); op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS)); - op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS)); + op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG)); op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD)); op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB)); op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL)); op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV)); - op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA)); + op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FMA)); op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT)); op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM)); - op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ)); + op_names.push_back(builtin_name("fp.roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL)); + 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.leq", OP_FLOAT_LE)); op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT)); op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE)); op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT)); + op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ)); + op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL)); op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO)); op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF)); 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("to_fp", OP_TO_FLOAT)); + op_names.push_back(builtin_name("fp.isNegative", OP_FLOAT_IS_NEGATIVE)); + op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE)); - if (m_bv_plugin) { - 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", OP_FLOAT_FP)); + 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.toReal", ?)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); } 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("FloatingPoint", 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)); + // The final theory supports three common FloatingPoint sorts + sort_names.push_back(builtin_name("Float16", FLOAT16_SORT)); + sort_names.push_back(builtin_name("Float32", FLOAT32_SORT)); + sort_names.push_back(builtin_name("Float64", FLOAT64_SORT)); + sort_names.push_back(builtin_name("Float128", FLOAT128_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { @@ -662,6 +678,8 @@ bool float_decl_plugin::is_value(app * e) const { case OP_FLOAT_VALUE: case OP_FLOAT_PLUS_INF: case OP_FLOAT_MINUS_INF: + case OP_FLOAT_PLUS_ZERO: + case OP_FLOAT_MINUS_ZERO: case OP_FLOAT_NAN: return true; case OP_TO_FLOAT: diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 58c37080d..c7ec04932 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -27,7 +27,11 @@ Revision History: enum float_sort_kind { FLOAT_SORT, - ROUNDING_MODE_SORT + ROUNDING_MODE_SORT, + FLOAT16_SORT, + FLOAT32_SORT, + FLOAT64_SORT, + FLOAT128_SORT }; enum float_op_kind { @@ -37,22 +41,23 @@ enum float_op_kind { OP_RM_TOWARD_NEGATIVE, OP_RM_TOWARD_ZERO, - OP_FLOAT_VALUE, OP_FLOAT_PLUS_INF, OP_FLOAT_MINUS_INF, OP_FLOAT_NAN, + OP_FLOAT_PLUS_ZERO, + OP_FLOAT_MINUS_ZERO, OP_FLOAT_ADD, OP_FLOAT_SUB, - OP_FLOAT_UMINUS, + OP_FLOAT_NEG, OP_FLOAT_MUL, OP_FLOAT_DIV, OP_FLOAT_REM, OP_FLOAT_ABS, OP_FLOAT_MIN, OP_FLOAT_MAX, - OP_FLOAT_FUSED_MA, // x*y + z + OP_FLOAT_FMA, // x*y + z OP_FLOAT_SQRT, OP_FLOAT_ROUND_TO_INTEGRAL, @@ -68,13 +73,14 @@ enum float_op_kind { OP_FLOAT_IS_SUBNORMAL, OP_FLOAT_IS_PZERO, OP_FLOAT_IS_NZERO, - OP_FLOAT_IS_SIGN_MINUS, + OP_FLOAT_IS_NEGATIVE, + OP_FLOAT_IS_POSITIVE, OP_TO_FLOAT, - OP_TO_IEEE_BV, + OP_FLOAT_TO_IEEE_BV, OP_FLOAT_FP, - OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_FP, OP_FLOAT_TO_UBV, OP_FLOAT_TO_SBV, OP_FLOAT_TO_REAL, @@ -125,16 +131,14 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters, 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_float_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, @@ -195,6 +199,7 @@ public: family_id get_fid() const { return m_fid; } family_id get_family_id() const { return m_fid; } arith_util & au() { return m_a_util; } + float_decl_plugin & plugin() { return *m_plugin; } sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); } @@ -242,16 +247,16 @@ public: app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); } app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); } app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); } - app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_UMINUS, arg1); } + app * mk_neg(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_NEG, arg1); } app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); } app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); } app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); } app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); } app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); } app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } - app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { + app * mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { expr * args[4] = { arg1, arg2, arg3, arg4 }; - return m().mk_app(m_fid, OP_FLOAT_FUSED_MA, 4, args); + return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args); } app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); } @@ -267,11 +272,13 @@ public: app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); } app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); } app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); } - app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } + app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); } + app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_POSITIVE, arg1); } + app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); } - bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); } + bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); } - app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); } + app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); } }; #endif diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d6f362902..5f92b4d94 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { unsigned sbits = m_util.get_sbits(srt); expr_ref sgn(m), s(m), e(m); - sort_ref s_sgn(m), s_sig(m), s_exp(m); - s_sgn = m_bv_util.mk_sort(1); - s_sig = m_bv_util.mk_sort(sbits-1); - s_exp = m_bv_util.mk_sort(ebits); #ifdef Z3DEBUG + sort_ref s_sgn(m), s_sig(m), s_exp(m); + s_sgn = m_bv_util.mk_sort(1); + s_sig = m_bv_util.mk_sort(sbits - 1); + s_exp = m_bv_util.mk_sort(ebits); + std::string p("fpa2bv"); std::string name = f->get_name().str(); @@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig); e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp); #else - sgn = m.mk_fresh_const(0, s_sgn); - s = m.mk_fresh_const(0, s_sig); - e = m.mk_fresh_const(0, s_exp); + expr_ref bv(m); + unsigned bv_sz = 1 + ebits + (sbits - 1); + bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz)); + + sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv); + e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv); + s = m_bv_util.mk_extract(sbits - 2, 0, bv); + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(s) == sbits-1); + SASSERT(m_bv_util.get_bv_size(e) == ebits); #endif mk_triple(sgn, s, e, result); @@ -595,12 +604,12 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); expr_ref t(m); - mk_uminus(f, 1, &args[2], t); + mk_neg(f, 1, &args[2], t); expr * nargs[3] = { args[0], args[1], t }; mk_add(f, 3, nargs, result); } -void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; split(args[0], sgn, s, e); @@ -906,7 +915,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; ); } -void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); // Remainder is always exact, so there is no rounding mode. @@ -1114,7 +1123,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, mk_triple(r_sgn, r_sig, r_exp, result); } -void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); // fusedma means (x * y) + z @@ -1835,9 +1844,18 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const mk_is_denormal(args[0], result); } -void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_neg(args[0], result); + TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;); +} + +void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + expr_ref t1(m), t2(m); + mk_is_nan(args[0], t1); + mk_is_pos(args[0], t2); + result = m.mk_and(m.mk_not(t1), t2); } void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2123,7 +2141,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; - split(args[0], sgn, s, e); + split(args[0], sgn, s, e); result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } @@ -2132,19 +2150,55 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e 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) { + SASSERT(num == 2); + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_int()); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + int width = f->get_parameter(0).get_int(); + + expr * rm = args[0]; + expr * x = args[1]; + + expr * sgn, *s, *e; + split(x, sgn, s, e); + NOT_IMPLEMENTED_YET(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index dcb508ffd..eb539d8ae 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -94,14 +94,14 @@ public: void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result); 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_remainder(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(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_fusedma(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); @@ -114,7 +114,8 @@ public: void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 225aad668..7a245b71a 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -65,8 +65,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("fpa2bv"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps > m_max_steps; } @@ -117,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE; case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE; case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE; + case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; + case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE; case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE; case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE; - case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE; + case OP_FLOAT_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE; case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; - case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE; + case OP_FLOAT_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; - case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE; + case OP_FLOAT_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; @@ -142,18 +142,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(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_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;); - throw tactic_exception("NYI"); + NOT_IMPLEMENTED_YET(); } } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index a4212d579..7dc34dd11 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -36,17 +36,17 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c br_status st = BR_FAILED; SASSERT(f->get_family_id() == get_fid()); switch (f->get_decl_kind()) { - case OP_TO_FLOAT: st = mk_to_float(f, num_args, args, result); break; + case OP_TO_FLOAT: st = mk_to_fp(f, num_args, args, result); break; case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break; case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break; - case OP_FLOAT_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; + case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; case OP_FLOAT_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break; case OP_FLOAT_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break; case OP_FLOAT_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break; case OP_FLOAT_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break; case OP_FLOAT_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break; case OP_FLOAT_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; - case OP_FLOAT_FUSED_MA: SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break; + case OP_FLOAT_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break; case OP_FLOAT_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break; @@ -62,10 +62,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; 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_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; + case OP_FLOAT_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; + case OP_FLOAT_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; @@ -73,7 +73,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c return st; } -br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status float_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()); @@ -154,7 +154,7 @@ br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { // a - b = a + (-b) - result = m_util.mk_add(arg1, arg2, m_util.mk_uminus(arg3)); + result = m_util.mk_add(arg1, arg2, m_util.mk_neg(arg3)); return BR_REWRITE2; } @@ -188,7 +188,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) { +br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) { if (m_util.is_nan(arg1)) { // -nan --> nan result = arg1; @@ -204,7 +204,7 @@ br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) { result = m_util.mk_plus_inf(m().get_sort(arg1)); return BR_DONE; } - if (m_util.is_uminus(arg1)) { + if (m_util.is_neg(arg1)) { // - - a --> a result = to_app(arg1)->get_arg(0); return BR_DONE; @@ -239,7 +239,7 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) { return BR_DONE; } result = m().mk_ite(m_util.mk_is_sign_minus(arg1), - m_util.mk_uminus(arg1), + m_util.mk_neg(arg1), arg1); return BR_REWRITE2; } @@ -284,7 +284,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE_FULL; } -br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { +br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); @@ -480,7 +480,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { +br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false(); @@ -490,6 +490,17 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { return BR_FAILED; } +br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true(); + return BR_DONE; + } + + return BR_FAILED; +} + + // This the SMT = br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); @@ -532,10 +543,6 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref 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; } diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 0f44d227c..4d8cec856 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -45,17 +45,16 @@ 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_to_float(func_decl * f, unsigned num_args, expr * const * args, 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); br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); - br_status mk_uminus(expr * arg1, expr_ref & result); + br_status mk_neg(expr * arg1, expr_ref & result); br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result); br_status mk_abs(expr * arg1, expr_ref & result); br_status mk_min(expr * arg1, expr * arg2, expr_ref & result); br_status mk_max(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result); + br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result); br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result); br_status mk_round(expr * arg1, expr * arg2, expr_ref & result); br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result); @@ -70,10 +69,12 @@ public: br_status mk_is_inf(expr * arg1, expr_ref & result); br_status mk_is_normal(expr * arg1, expr_ref & result); br_status mk_is_subnormal(expr * arg1, expr_ref & result); - br_status mk_is_sign_minus(expr * arg1, expr_ref & result); + br_status mk_is_negative(expr * arg1, expr_ref & result); + br_status mk_is_positive(expr * arg1, expr_ref & result); 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_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);