diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index df0dd232a..12d32c04a 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -88,6 +88,7 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) { Z3_TRY; LOG_Z3_mk_fpa_sort(c, ebits, sbits); @@ -105,18 +106,34 @@ extern "C" { return Z3_mk_fpa_sort(c, 5, 11); } + Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 5, 11); + } + Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c) { return Z3_mk_fpa_sort(c, 8, 24); } + Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 8, 24); + } + Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c) { return Z3_mk_fpa_sort(c, 11, 53); } + Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 11, 53); + } + Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c) { return Z3_mk_fpa_sort(c, 15, 113); } + Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 15, 113); + } + Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) { Z3_TRY; LOG_Z3_mk_fpa_nan(c, s); @@ -373,22 +390,12 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_convert(c, s, rm, t); RESET_ERROR_CODE(); - api::context * ctx = mk_c(c); + api::context * ctx = mk_c(c); expr * args [2] = { to_expr(rm), to_expr(t) }; - Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_TO_FLOAT, + Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_FLOAT_TO_FP, to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(), 2, args)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - - Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t) { - Z3_TRY; - LOG_Z3_mk_fpa_to_ieee_bv(c, t); - RESET_ERROR_CODE(); - api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_float_to_ieee_bv(to_expr(t))); - RETURN_Z3(r); - Z3_CATCH_RETURN(0); - } }; diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 63b489c83..f04b87ea3 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -117,6 +117,19 @@ extern "C" { */ Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c); + /** + \brief Create the half-precision (16-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c); + /** \brief Create the single-precision (32-bit) floating point sort. @@ -130,6 +143,19 @@ extern "C" { */ Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c); + /** + \brief Create the single-precision (32-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c); + /** \brief Create the double-precision (64-bit) floating point sort. @@ -143,6 +169,19 @@ extern "C" { */ Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c); + /** + \brief Create the double-precision (64-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort__64(__in Z3_context c); + /** \brief Create the quadruple-precision (128-bit) floating point sort. @@ -156,6 +195,18 @@ extern "C" { */ Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c); + /** + \brief Create the quadruple-precision (128-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c); /** \brief Create a NaN of sort s. @@ -504,18 +555,6 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t); - /** - \brief Conversion of a floating point term to a bit-vector term in IEEE754 format. - - \param c logical context. - \param t floating-point term. - - t must have floating point sort. The size of the resulting bit-vector is automatically determined. - - def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST))) - */ - Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t); - /*@}*/ /*@}*/ diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 20078f73f..4f8650610 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -118,23 +118,23 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { } bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) { - if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) { + if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_AWAY)) { val = MPF_ROUND_NEAREST_TAWAY; return true; } - else if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_EVEN)) { + else if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_EVEN)) { val = MPF_ROUND_NEAREST_TEVEN; return true; } - else if (is_app_of(n, m_family_id, OP_RM_TOWARD_NEGATIVE)) { + else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_NEGATIVE)) { val = MPF_ROUND_TOWARD_NEGATIVE; return true; } - else if (is_app_of(n, m_family_id, OP_RM_TOWARD_POSITIVE)) { + else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_POSITIVE)) { val = MPF_ROUND_TOWARD_POSITIVE; return true; } - else if (is_app_of(n, m_family_id, OP_RM_TOWARD_ZERO)) { + else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_ZERO)) { val = MPF_ROUND_TOWARD_ZERO; return true; } @@ -210,15 +210,15 @@ func_decl * float_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_parame sort * s = mk_rm_sort(); func_decl_info finfo(m_family_id, k); switch (k) { - case OP_RM_NEAREST_TIES_TO_EVEN: + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: return m_manager->mk_const_decl(symbol("roundNearestTiesToEven"), s, finfo); - case OP_RM_NEAREST_TIES_TO_AWAY: + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: return m_manager->mk_const_decl(symbol("roundNearestTiesToAway"), s, finfo); - case OP_RM_TOWARD_POSITIVE: + case OP_FLOAT_RM_TOWARD_POSITIVE: return m_manager->mk_const_decl(symbol("roundTowardPositive"), s, finfo); - case OP_RM_TOWARD_NEGATIVE: + case OP_FLOAT_RM_TOWARD_NEGATIVE: return m_manager->mk_const_decl(symbol("roundTowardNegative"), s, finfo); - case OP_RM_TOWARD_ZERO: + case OP_FLOAT_RM_TOWARD_ZERO: return m_manager->mk_const_decl(symbol("roundTowardZero"), s, finfo); default: UNREACHABLE(); @@ -471,20 +471,6 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_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 (arity != 1) - m_manager->raise_exception("invalid number of arguments to asIEEEBV"); - if (!is_float_sort(domain[0])) - 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); - symbol name("asIEEEBV"); - 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 (arity != 3) @@ -528,17 +514,19 @@ func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, 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) { - case OP_TO_FLOAT: + case OP_FLOAT_TO_FP: return mk_to_float(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_MINUS_INF: case OP_FLOAT_PLUS_INF: case OP_FLOAT_NAN: + case OP_FLOAT_MINUS_ZERO: + case OP_FLOAT_PLUS_ZERO: return mk_float_const_decl(k, num_parameters, parameters, arity, domain, range); - case OP_RM_NEAREST_TIES_TO_EVEN: - case OP_RM_NEAREST_TIES_TO_AWAY: - case OP_RM_TOWARD_POSITIVE: - case OP_RM_TOWARD_NEGATIVE: - case OP_RM_TOWARD_ZERO: + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: + case OP_FLOAT_RM_TOWARD_POSITIVE: + case OP_FLOAT_RM_TOWARD_NEGATIVE: + case OP_FLOAT_RM_TOWARD_ZERO: return mk_rm_const_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_EQ: case OP_FLOAT_LT: @@ -577,8 +565,6 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_rm_unary_decl(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_UBV: @@ -601,17 +587,17 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co 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)); - op_names.push_back(builtin_name("roundNearestTiesToAway", OP_RM_NEAREST_TIES_TO_AWAY)); - op_names.push_back(builtin_name("roundTowardPositive", OP_RM_TOWARD_POSITIVE)); - 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("roundNearestTiesToEven", OP_FLOAT_RM_NEAREST_TIES_TO_EVEN)); + op_names.push_back(builtin_name("roundNearestTiesToAway", OP_FLOAT_RM_NEAREST_TIES_TO_AWAY)); + op_names.push_back(builtin_name("roundTowardPositive", OP_FLOAT_RM_TOWARD_POSITIVE)); + op_names.push_back(builtin_name("roundTowardNegative", OP_FLOAT_RM_TOWARD_NEGATIVE)); + op_names.push_back(builtin_name("roundTowardZero", OP_FLOAT_RM_TOWARD_ZERO)); - 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)); - op_names.push_back(builtin_name("RTN", OP_RM_TOWARD_NEGATIVE)); - op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO)); + op_names.push_back(builtin_name("RNE", OP_FLOAT_RM_NEAREST_TIES_TO_EVEN)); + op_names.push_back(builtin_name("RNA", OP_FLOAT_RM_NEAREST_TIES_TO_AWAY)); + op_names.push_back(builtin_name("RTP", OP_FLOAT_RM_TOWARD_POSITIVE)); + op_names.push_back(builtin_name("RTN", OP_FLOAT_RM_TOWARD_NEGATIVE)); + op_names.push_back(builtin_name("RTZ", OP_FLOAT_RM_TOWARD_ZERO)); op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS)); op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG)); @@ -643,7 +629,8 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co 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("to_fp", OP_TO_FLOAT)); + op_names.push_back(builtin_name("to_fp", OP_FLOAT_TO_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { @@ -670,11 +657,11 @@ bool float_decl_plugin::is_value(app * e) const { if (e->get_family_id() != m_family_id) return false; switch (e->get_decl_kind()) { - case OP_RM_NEAREST_TIES_TO_EVEN: - case OP_RM_NEAREST_TIES_TO_AWAY: - case OP_RM_TOWARD_POSITIVE: - case OP_RM_TOWARD_NEGATIVE: - case OP_RM_TOWARD_ZERO: + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: + case OP_FLOAT_RM_TOWARD_POSITIVE: + case OP_FLOAT_RM_TOWARD_NEGATIVE: + case OP_FLOAT_RM_TOWARD_ZERO: case OP_FLOAT_VALUE: case OP_FLOAT_PLUS_INF: case OP_FLOAT_MINUS_INF: @@ -682,7 +669,7 @@ bool float_decl_plugin::is_value(app * e) const { case OP_FLOAT_MINUS_ZERO: case OP_FLOAT_NAN: return true; - case OP_TO_FLOAT: + case OP_FLOAT_TO_FP: return m_manager->is_value(e->get_arg(0)); default: return false; diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 93ff2e664..98b87f6c9 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -35,11 +35,11 @@ enum float_sort_kind { }; enum float_op_kind { - OP_RM_NEAREST_TIES_TO_EVEN, - OP_RM_NEAREST_TIES_TO_AWAY, - OP_RM_TOWARD_POSITIVE, - OP_RM_TOWARD_NEGATIVE, - OP_RM_TOWARD_ZERO, + OP_FLOAT_RM_NEAREST_TIES_TO_EVEN, + OP_FLOAT_RM_NEAREST_TIES_TO_AWAY, + OP_FLOAT_RM_TOWARD_POSITIVE, + OP_FLOAT_RM_TOWARD_NEGATIVE, + OP_FLOAT_RM_TOWARD_ZERO, OP_FLOAT_VALUE, OP_FLOAT_PLUS_INF, @@ -76,11 +76,9 @@ enum float_op_kind { OP_FLOAT_IS_NEGATIVE, OP_FLOAT_IS_POSITIVE, - OP_TO_FLOAT, - OP_FLOAT_TO_IEEE_BV, - OP_FLOAT_FP, - OP_FLOAT_TO_FP, + OP_FLOAT_TO_FP, + OP_FLOAT_TO_FP_UNSIGNED, OP_FLOAT_TO_UBV, OP_FLOAT_TO_SBV, OP_FLOAT_TO_REAL, @@ -134,9 +132,7 @@ class float_decl_plugin : public decl_plugin { 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_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + 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_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -210,11 +206,11 @@ public: unsigned get_ebits(sort * s); unsigned get_sbits(sort * s); - app * mk_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_RM_NEAREST_TIES_TO_EVEN); } - app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_RM_NEAREST_TIES_TO_AWAY); } - app * mk_round_toward_positive() { return m().mk_const(m_fid, OP_RM_TOWARD_POSITIVE); } - app * mk_round_toward_negative() { return m().mk_const(m_fid, OP_RM_TOWARD_NEGATIVE); } - app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_RM_TOWARD_ZERO); } + app * mk_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_FLOAT_RM_NEAREST_TIES_TO_EVEN); } + app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_FLOAT_RM_NEAREST_TIES_TO_AWAY); } + app * mk_round_toward_positive() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_POSITIVE); } + app * mk_round_toward_negative() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_NEGATIVE); } + app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_ZERO); } app * mk_nan(unsigned ebits, unsigned sbits); app * mk_plus_inf(unsigned ebits, unsigned sbits); @@ -240,9 +236,9 @@ public: bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); } - bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); } + bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_FLOAT_TO_FP); } - app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); } + app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_TO_FP, arg1, arg2); } app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); } 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); } @@ -277,8 +273,6 @@ public: app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); } bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); } - - 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 de4797f80..3fbb7ccf8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -53,8 +53,8 @@ fpa2bv_converter::~fpa2bv_converter() { } void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_TO_FLOAT)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); expr_ref sgn(m), s(m), e(m); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn); @@ -73,8 +73,8 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { } void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { - SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_TO_FLOAT)); - SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); expr_ref sgn(m), s(m), e(m); m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), sgn); @@ -2203,7 +2203,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar } 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(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); sgn = to_app(e)->get_arg(0); @@ -2252,7 +2252,7 @@ void fpa2bv_converter::mk_is_ninf(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref zero(m); @@ -2261,7 +2261,7 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref one(m); @@ -2424,7 +2424,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { } void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); sort * srt = to_app(e)->get_decl()->get_range(); @@ -2519,11 +2519,11 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) { switch(f->get_decl_kind()) { - case OP_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; - case OP_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break; - case OP_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; - case OP_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break; - case OP_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break; + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break; + case OP_FLOAT_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; + case OP_FLOAT_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break; + case OP_FLOAT_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break; default: UNREACHABLE(); } } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index eb539d8ae..d033890be 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -73,7 +73,7 @@ public: SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); SASSERT(m_bv_util.is_bv(significand)); SASSERT(m_bv_util.is_bv(exponent)); - result = m.mk_app(m_util.get_family_id(), OP_TO_FLOAT, sign, significand, exponent); + result = m.mk_app(m_util.get_family_id(), OP_FLOAT_FP, sign, significand, exponent); } void mk_eq(expr * a, expr * b, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 7a245b71a..62554e06e 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -107,11 +107,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { - case OP_RM_NEAREST_TIES_TO_AWAY: - case OP_RM_NEAREST_TIES_TO_EVEN: - case OP_RM_TOWARD_NEGATIVE: - case OP_RM_TOWARD_POSITIVE: - case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: + case OP_FLOAT_RM_TOWARD_NEGATIVE: + case OP_FLOAT_RM_TOWARD_POSITIVE: + case OP_FLOAT_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; 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; @@ -144,8 +144,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(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_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP: m_conv.mk_to_float(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_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; diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 04546bb4b..436194844 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -36,7 +36,7 @@ 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_fp(f, num_args, args, result); break; + case OP_FLOAT_TO_FP: 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_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; @@ -63,8 +63,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c 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_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_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(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_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; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index a7e1c7bf1..b1947ceb5 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -135,13 +135,7 @@ namespace smt { simp(a->get_arg(2), exp, pr_exp); m_converter.mk_triple(sgn, sig, exp, bv_term); - } - else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) { - SASSERT(is_app(t)); - expr_ref bv_e(m); - proof_ref bv_pr(m); - simp(t, bv_term, bv_pr); - } + } else NOT_IMPLEMENTED_YET(); @@ -420,17 +414,6 @@ namespace smt { ctx.mark_as_relevant(bv_sig); ctx.mark_as_relevant(bv_exp); } - else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) { - expr_ref eq(m); - app * ex_a = to_app(ex); - if (n->get_id() > ex_a->get_id()) - std::swap(n, ex_a); - eq = m.mk_eq(n, ex_a); - ctx.internalize(eq, false); - literal l = ctx.get_literal(eq); - ctx.mk_th_axiom(get_id(), 1, &l); - ctx.mark_as_relevant(l); - } else NOT_IMPLEMENTED_YET(); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 5c0d2acca..c833f2be3 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -81,7 +81,7 @@ namespace smt { protected: void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { - SASSERT(is_app_of(e, get_family_id(), OP_TO_FLOAT)); + SASSERT(is_app_of(e, get_family_id(), OP_FLOAT_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); sgn = to_app(e)->get_arg(0); sig = to_app(e)->get_arg(1); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 3de869e15..23809d265 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -116,7 +116,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { bv_mdl->eval(a->get_arg(1), sig, true); bv_mdl->eval(a->get_arg(2), exp, true); - SASSERT(a->is_app_of(fu.get_family_id(), OP_TO_FLOAT)); + SASSERT(a->is_app_of(fu.get_family_id(), OP_FLOAT_TO_FP)); #ifdef Z3DEBUG SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0);