From dd17f3c7d6802e5649a22d2ae7f93f2cf368d416 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 8 Jan 2015 13:18:56 +0000 Subject: [PATCH] Renaming floats, float, Floats, Float -> FPA, fpa Signed-off-by: Christoph M. Wintersteiger --- src/api/api_ast.cpp | 62 ++- src/api/api_context.cpp | 2 +- src/api/api_context.h | 2 +- src/api/api_fpa.cpp | 2 +- src/api/api_numeral.cpp | 2 +- src/api/dotnet/Expr.cs | 4 +- src/api/z3_api.h | 53 +- src/ast/ast_smt2_pp.h | 2 +- src/ast/fpa/fpa2bv_converter.cpp | 373 ++++++++------ src/ast/fpa/fpa2bv_converter.h | 15 +- src/ast/fpa/fpa2bv_rewriter.h | 98 ++-- ...at_decl_plugin.cpp => fpa_decl_plugin.cpp} | 460 +++++++++--------- ...{float_decl_plugin.h => fpa_decl_plugin.h} | 216 ++++---- src/ast/reg_decl_plugins.cpp | 6 +- .../{float_rewriter.cpp => fpa_rewriter.cpp} | 154 +++--- .../{float_rewriter.h => fpa_rewriter.h} | 8 +- src/ast/rewriter/mk_simplified_app.cpp | 4 +- src/ast/rewriter/th_rewriter.cpp | 4 +- src/cmd_context/cmd_context.cpp | 8 +- src/cmd_context/cmd_context.h | 2 +- src/model/model_evaluator.cpp | 4 +- src/smt/theory_fpa.cpp | 27 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- src/tactic/fpa/qffpa_tactic.cpp | 32 +- src/tactic/fpa/qffpa_tactic.h | 4 +- 25 files changed, 859 insertions(+), 687 deletions(-) rename src/ast/{float_decl_plugin.cpp => fpa_decl_plugin.cpp} (71%) rename src/ast/{float_decl_plugin.h => fpa_decl_plugin.h} (77%) rename src/ast/rewriter/{float_rewriter.cpp => fpa_rewriter.cpp} (69%) rename src/ast/rewriter/{float_rewriter.h => fpa_rewriter.h} (95%) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 67358726c..c6b413dd4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -648,11 +648,11 @@ extern "C" { else if (fid == mk_c(c)->get_datalog_fid() && k == datalog::DL_FINITE_SORT) { return Z3_FINITE_DOMAIN_SORT; } - else if (fid == mk_c(c)->get_fpa_fid() && k == FLOAT_SORT) { + else if (fid == mk_c(c)->get_fpa_fid() && k == FLOATING_POINT_SORT) { return Z3_FLOATING_POINT_SORT; } else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) { - return Z3_FLOATING_POINT_ROUNDING_MODE_SORT; + return Z3_ROUNDING_MODE_SORT; } else { return Z3_UNKNOWN_SORT; @@ -1119,6 +1119,64 @@ extern "C" { return Z3_OP_UNINTERPRETED; } } + + if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) { + switch (_d->get_decl_kind()) { + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; + case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE; + case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE; + case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO; + case OP_FPA_VALUE: return Z3_OP_FPA_VALUE; + case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF; + case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF; + case OP_FPA_NAN: return Z3_OP_FPA_NAN; + case OP_FPA_MINUS_ZERO: return Z3_OP_FPA_MINUS_ZERO; + case OP_FPA_PLUS_ZERO: return Z3_OP_FPA_PLUS_ZERO; + case OP_FPA_ADD: return Z3_OP_FPA_ADD; + case OP_FPA_SUB: return Z3_OP_FPA_SUB; + case OP_FPA_NEG: return Z3_OP_FPA_NEG; + case OP_FPA_MUL: return Z3_OP_FPA_MUL; + case OP_FPA_DIV: return Z3_OP_FPA_DIV; + case OP_FPA_REM: return Z3_OP_FPA_REM; + case OP_FPA_ABS: return Z3_OP_FPA_ABS; + case OP_FPA_MIN: return Z3_OP_FPA_MIN; + case OP_FPA_MAX: return Z3_OP_FPA_MAX; + case OP_FPA_FMA: return Z3_OP_FPA_FMA; + case OP_FPA_SQRT: return Z3_OP_FPA_SQRT; + case OP_FPA_EQ: return Z3_OP_FPA_EQ; + case OP_FPA_ROUND_TO_INTEGRAL: return Z3_OP_FPA_ROUND_TO_INTEGRAL; + case OP_FPA_LT: return Z3_OP_FPA_LT; + case OP_FPA_GT: return Z3_OP_FPA_GT; + case OP_FPA_LE: return Z3_OP_FPA_LE; + case OP_FPA_GE: return Z3_OP_FPA_GE; + case OP_FPA_IS_NAN: return Z3_OP_FPA_IS_NAN; + case OP_FPA_IS_INF: return Z3_OP_FPA_IS_INF; + case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO; + case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL; + case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL; + case OP_FPA_IS_PZERO: return Z3_OP_FPA_IS_PZERO; + case OP_FPA_IS_NZERO: return Z3_OP_FPA_IS_NZERO; + case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE; + case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE; + case OP_FPA_FP: return Z3_OP_FPA_FP; + case OP_FPA_TO_FP: return Z3_OP_FPA_TO_FP; + case OP_FPA_TO_FP_UNSIGNED: return Z3_OP_FPA_TO_FP_UNSIGNED; + case OP_FPA_TO_UBV: return Z3_OP_FPA_TO_UBV; + case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV; + case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL; + case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + return Z3_OP_UNINTERPRETED; + default: + UNREACHABLE(); + return Z3_OP_UNINTERPRETED; + } + } if (mk_c(c)->m().get_label_family_id() == _d->get_family_id()) { switch(_d->get_decl_kind()) { diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 5d11e5bce..b83b72e35 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -113,7 +113,7 @@ namespace api { m_array_fid = m().mk_family_id("array"); m_dt_fid = m().mk_family_id("datatype"); m_datalog_fid = m().mk_family_id("datalog_relation"); - m_fpa_fid = m().mk_family_id("float"); + m_fpa_fid = m().mk_family_id("fpa"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); if (!m_user_ref_count) { diff --git a/src/api/api_context.h b/src/api/api_context.h index f409a4ece..c71b88b61 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -27,7 +27,7 @@ Revision History: #include"bv_decl_plugin.h" #include"datatype_decl_plugin.h" #include"dl_decl_plugin.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"smt_kernel.h" #include"smt_params.h" #include"event_handler.h" diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 87568af09..0f0f68ae1 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -20,7 +20,7 @@ Notes: #include"z3.h" #include"api_log_macros.h" #include"api_context.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" extern "C" { diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index d2829e990..17a743880 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -23,7 +23,7 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"algebraic_numbers.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" bool is_numeral_sort(Z3_context c, Z3_sort ty) { sort * _ty = to_sort(ty); diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index ec8beeac0..826860eec 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1543,7 +1543,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj); case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj); - case Z3_sort_kind.Z3_FLOATING_POINT_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj); + case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj); } } @@ -1556,7 +1556,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj); case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj); - case Z3_sort_kind.Z3_FLOATING_POINT_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); + case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); } return new Expr(ctx, obj); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 776e4e9fe..3c3a5d1c2 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -195,7 +195,7 @@ typedef enum Z3_RELATION_SORT, Z3_FINITE_DOMAIN_SORT, Z3_FLOATING_POINT_SORT, - Z3_FLOATING_POINT_ROUNDING_MODE_SORT, + Z3_ROUNDING_MODE_SORT, Z3_UNKNOWN_SORT = 1000 } Z3_sort_kind; @@ -1058,6 +1058,57 @@ typedef enum { Z3_OP_DT_RECOGNISER, Z3_OP_DT_ACCESSOR, + // Floating-Point Arithmetic + Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN, + Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, + Z3_OP_FPA_RM_TOWARD_POSITIVE, + Z3_OP_FPA_RM_TOWARD_NEGATIVE, + Z3_OP_FPA_RM_TOWARD_ZERO, + + Z3_OP_FPA_VALUE, + Z3_OP_FPA_PLUS_INF, + Z3_OP_FPA_MINUS_INF, + Z3_OP_FPA_NAN, + Z3_OP_FPA_PLUS_ZERO, + Z3_OP_FPA_MINUS_ZERO, + + Z3_OP_FPA_ADD, + Z3_OP_FPA_SUB, + Z3_OP_FPA_NEG, + Z3_OP_FPA_MUL, + Z3_OP_FPA_DIV, + Z3_OP_FPA_REM, + Z3_OP_FPA_ABS, + Z3_OP_FPA_MIN, + Z3_OP_FPA_MAX, + Z3_OP_FPA_FMA, + Z3_OP_FPA_SQRT, + Z3_OP_FPA_ROUND_TO_INTEGRAL, + + Z3_OP_FPA_EQ, + Z3_OP_FPA_LT, + Z3_OP_FPA_GT, + Z3_OP_FPA_LE, + Z3_OP_FPA_GE, + Z3_OP_FPA_IS_NAN, + Z3_OP_FPA_IS_INF, + Z3_OP_FPA_IS_ZERO, + Z3_OP_FPA_IS_NORMAL, + Z3_OP_FPA_IS_SUBNORMAL, + Z3_OP_FPA_IS_PZERO, + Z3_OP_FPA_IS_NZERO, + Z3_OP_FPA_IS_NEGATIVE, + Z3_OP_FPA_IS_POSITIVE, + + Z3_OP_FPA_FP, + Z3_OP_FPA_TO_FP, + Z3_OP_FPA_TO_FP_UNSIGNED, + Z3_OP_FPA_TO_UBV, + Z3_OP_FPA_TO_SBV, + Z3_OP_FPA_TO_REAL, + + Z3_OP_FPA_TO_IEEE_BV, + Z3_OP_UNINTERPRETED } Z3_decl_kind; diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index 37d13e57a..bc62448c7 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -27,7 +27,7 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"array_decl_plugin.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"dl_decl_plugin.h" #include"smt2_util.h" diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 24e606cdc..dc1a255e8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -16,8 +16,10 @@ Author: Notes: --*/ +#include #include"ast_smt2_pp.h" #include"well_sorted.h" +#include"th_rewriter.h" #include"fpa2bv_converter.h" @@ -34,7 +36,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), m_extra_assertions(m) { - m_plugin = static_cast(m.get_plugin(m.mk_family_id("float"))); + m_plugin = static_cast(m.get_plugin(m.mk_family_id("fpa"))); } fpa2bv_converter::~fpa2bv_converter() { @@ -42,8 +44,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_FLOAT_TO_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_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); @@ -62,8 +64,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_FLOAT_TO_FP)); - SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_TO_FP)); expr *t_sgn, *t_sig, *t_exp; expr *f_sgn, *f_sig, *f_exp; @@ -1881,15 +1883,15 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args mk_to_fp_real(f, f->get_range(), args[0], args[1], result); } else if (num == 2 && - m_bv_util.is_bv(args[0]) && - m_bv_util.get_bv_size(args[0]) == 3 && - m_bv_util.is_bv(args[1])) { - mk_to_fp_signed(f, num, args, result); + m_bv_util.is_bv(args[0]) && + m_bv_util.get_bv_size(args[0]) == 3 && + m_bv_util.is_bv(args[1])) { + mk_to_fp_signed(f, num, args, result); } else if (num == 3 && - m_bv_util.is_bv(args[0]) && - m_bv_util.is_bv(args[1]) && - m_bv_util.is_bv(args[2])) { + m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[1]) && + m_bv_util.is_bv(args[2])) { SASSERT(m_bv_util.get_bv_size(args[0]) == 1); SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); @@ -1900,55 +1902,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args m_arith_util.is_numeral(args[1]) && m_arith_util.is_numeral(args[2])) { - // rm + real + int -> float - SASSERT(m_util.is_float(f->get_range())); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - - expr * rm = args[0]; - - rational q; - if (!m_arith_util.is_numeral(args[1], q)) - UNREACHABLE(); - - rational e; - if (!m_arith_util.is_numeral(args[2], e)) - UNREACHABLE(); - - SASSERT(e.is_int64()); - SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1)); - - scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); - m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); - - app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); - a_nte = m_plugin->mk_value(nte); - a_nta = m_plugin->mk_value(nta); - a_tp = m_plugin->mk_value(tp); - a_tn = m_plugin->mk_value(tn); - a_tz = m_plugin->mk_value(tz); - - expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m); - mk_value(a_nte->get_decl(), 0, 0, bv_nte); - mk_value(a_nta->get_decl(), 0, 0, bv_nta); - mk_value(a_tp->get_decl(), 0, 0, bv_tp); - mk_value(a_tn->get_decl(), 0, 0, bv_tn); - mk_value(a_tz->get_decl(), 0, 0, bv_tz); - - expr_ref c1(m), c2(m), c3(m), c4(m); - c1 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); - c2 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); - c3 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); - c4 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)); - - mk_ite(c1, bv_tn, bv_tz, result); - mk_ite(c2, bv_tp, result, result); - mk_ite(c3, bv_nta, result, result); - mk_ite(c4, bv_nte, result, result); + mk_to_fp_real_int(f, num, args, result); } else UNREACHABLE(); @@ -2104,11 +2058,13 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * } void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { + TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << + "x: " << mk_ismt2_pp(x, m) << std::endl;); SASSERT(m_util.is_float(s)); unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); - if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) { + if (false && m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) { rational tmp_rat; unsigned sz; m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz); SASSERT(tmp_rat.is_int32()); @@ -2140,19 +2096,201 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_triple(sgn, s, e, result); } else { - NOT_IMPLEMENTED_YET(); + mpf_manager & fm = fu().fm(); + bv_util & bu = m_bv_util; + arith_util & au = m_arith_util; + + expr_ref bv0(m), bv1(m), zero(m), two(m); + bv0 = bu.mk_numeral(0, 1); + bv1 = bu.mk_numeral(1, 1); + zero = au.mk_numeral(rational(0), false); + two = au.mk_numeral(rational(2), false); + + expr_ref sgn(m), sig(m), exp(m); + sgn = m.mk_ite(au.mk_lt(x, zero), bv1, bv0); + sig = bu.mk_numeral(0, sbits + 4); + mpz const & max_normal_exponent = fm.m_powers2.m1(ebits-1); + exp = bu.mk_numeral(max_normal_exponent, ebits); + + //expr_ref cur_s(m), cur_d(m), cur_r(m), cur_s2(m), bv1_s4(m); + //bv1_s4 = bu.mk_numeral(1, sbits + 4); + //cur_s = x; + //std::string trace_name; + //for (unsigned i = 0; i < sbits + 3; i++) { + // std::stringstream dbg_name; + // dbg_name << "fpa2bv_to_float_real_sig_" << i; + // dbg_decouple(dbg_name.str().c_str(), sig); + + // cur_s = au.mk_div(cur_s, two); + // // cur_r = au.mk_rem(cur_s, two); + // cur_r = au.mk_mod(cur_s, two); + // cur_s2 = bu.mk_bv_shl(sig, bv1_s4); + // sig = m.mk_ite(au.mk_eq(cur_r, zero), + // cur_s2, + // bu.mk_bv_add(cur_s2, bv1_s4)); + //} + //dbg_decouple("fpa2bv_to_float_real_last_cur_s", cur_s); + //expr_ref inc(m); + //inc = m.mk_not(m.mk_eq(cur_s, zero)); + //dbg_decouple("fpa2bv_to_float_real_inc", inc); + //sig = m.mk_ite(inc, bu.mk_bv_add(sig, bv1_s4), sig); + + SASSERT(bu.get_bv_size(sgn) == 1); + SASSERT(bu.get_bv_size(sig) == sbits + 4); + SASSERT(bu.get_bv_size(exp) == ebits + 2); + + dbg_decouple("fpa2bv_to_float_real_sgn", sgn); + dbg_decouple("fpa2bv_to_float_real_sig", sig); + dbg_decouple("fpa2bv_to_float_real_exp", exp); + + expr_ref rmr(rm, m); + round(s, rmr, sgn, sig, exp, result); } SASSERT(is_well_sorted(m, result)); } +void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + // rm + real + int -> float + SASSERT(m_util.is_float(f->get_range())); + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + + expr * rm = args[0]; + + rational q; + if (!m_arith_util.is_numeral(args[1], q)) + UNREACHABLE(); + + rational e; + if (!m_arith_util.is_numeral(args[2], e)) + UNREACHABLE(); + + SASSERT(e.is_int64()); + SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1)); + + scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); + m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); + + app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); + a_nte = m_plugin->mk_value(nte); + a_nta = m_plugin->mk_value(nta); + a_tp = m_plugin->mk_value(tp); + a_tn = m_plugin->mk_value(tn); + a_tz = m_plugin->mk_value(tz); + + expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m); + mk_value(a_nte->get_decl(), 0, 0, bv_nte); + mk_value(a_nta->get_decl(), 0, 0, bv_nta); + mk_value(a_tp->get_decl(), 0, 0, bv_tp); + mk_value(a_tn->get_decl(), 0, 0, bv_tn); + mk_value(a_tz->get_decl(), 0, 0, bv_tz); + + expr_ref c1(m), c2(m), c3(m), c4(m); + c1 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c2 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c3 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); + c4 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)); + + mk_ite(c1, bv_tn, bv_tz, result); + mk_ite(c2, bv_tp, result, result); + mk_ite(c3, bv_nta, result, result); + mk_ite(c4, bv_nte, result, result); +} +void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); + SASSERT(num == 1); + SASSERT(f->get_num_parameters() == 0); + SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FPA_TO_FP)); + + expr * x = args[0]; + sort * s = m.get_sort(x); + unsigned ebits = m_util.get_ebits(s); + unsigned sbits = m_util.get_sbits(s); + + sort * rs = m_arith_util.mk_real(); + expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m); + mk_is_nan(x, x_is_nan); + mk_is_inf(x, x_is_inf); + mk_is_zero(x, x_is_zero); + + expr_ref sgn(m), sig(m), exp(m), lz(m); + unpack(x, sgn, sig, exp, lz, true); + // sig is of the form [1].[sigbits] + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(sig) == sbits); + SASSERT(m_bv_util.get_bv_size(exp) == ebits); + + expr_ref rsig(m), bit(m), zero(m), one(m), two(m), bv0(m), bv1(m); + zero = m_arith_util.mk_numeral(rational(0), rs); + one = m_arith_util.mk_numeral(rational(1), rs); + two = m_arith_util.mk_numeral(rational(2), rs); + bv0 = m_bv_util.mk_numeral(0, 1); + bv1 = m_bv_util.mk_numeral(1, 1); + rsig = one; + for (unsigned i = sbits - 2; i != (unsigned)-1; i--) { + bit = m_bv_util.mk_extract(i, i, sig); + rsig = m_arith_util.mk_add(m_arith_util.mk_mul(rsig, two), + m.mk_ite(m.mk_eq(bit, bv1), one, zero)); + } + + const mpz & p2 = fu().fm().m_powers2(sbits - 1); + expr_ref ep2(m); + ep2 = m_arith_util.mk_numeral(rational(p2), false); + rsig = m_arith_util.mk_div(rsig, ep2); + dbg_decouple("fpa2bv_to_real_ep2", ep2); + dbg_decouple("fpa2bv_to_real_rsig", rsig); + + expr_ref exp_n(m), exp_p(m), exp_is_neg(m), exp_abs(m); + exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1); + dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg); + exp_p = m_bv_util.mk_sign_extend(1, exp); + exp_n = m_bv_util.mk_bv_neg(exp_p); + exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p); + dbg_decouple("fpa2bv_to_real_exp_abs", exp); + SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1); + + expr_ref exp2(m), prev_bit(m); + exp2 = zero; + for (unsigned i = ebits; i != (unsigned)-1; i--) { + bit = m_bv_util.mk_extract(i, i, exp_abs); + exp2 = m_arith_util.mk_add(m_arith_util.mk_mul(exp2, two), + m.mk_ite(m.mk_eq(bit, bv1), one, zero)); + prev_bit = bit; + } + + exp2 = m.mk_ite(exp_is_neg, m_arith_util.mk_div(one, exp2), exp2); + dbg_decouple("fpa2bv_to_real_exp2", exp2); + + expr_ref res(m), two_exp2(m); + two_exp2 = m_arith_util.mk_power(two, exp2); + res = m_arith_util.mk_mul(rsig, two_exp2); + res = m.mk_ite(m.mk_eq(sgn, bv1), m_arith_util.mk_uminus(res), res); + dbg_decouple("fpa2bv_to_real_sig_times_exp2", res); + + TRACE("fpa2bv_to_real", tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl; + tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); + + result = m.mk_ite(x_is_zero, zero, res); + result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result); + result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result); + + SASSERT(is_well_sorted(m, result)); +} + void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); // This is a conversion from signed bitvector to float: // ; from signed machine integer, represented as a 2's complement bit vector - // ((_ to_fp eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb)) + // ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)) // Semantics: // Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format). // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite @@ -2293,7 +2431,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); // This is a conversion from unsigned bitvector to float: - // ((_ to_fp_unsigned eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb)) + // ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)) // Semantics: // Let b in[[(_ BitVec m)]] and let n be the unsigned integer represented by b. // [[(_ to_fp_unsigned eb sb)]](r, x) = +infinity if n is too large to be @@ -2700,91 +2838,6 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg SASSERT(is_well_sorted(m, result)); } -void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++) - tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); - SASSERT(num == 1); - SASSERT(f->get_num_parameters() == 0); - SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FLOAT_TO_FP)); - - expr * x = args[0]; - sort * s = m.get_sort(x); - unsigned ebits = m_util.get_ebits(s); - unsigned sbits = m_util.get_sbits(s); - - sort * rs = m_arith_util.mk_real(); - expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m); - mk_is_nan(x, x_is_nan); - mk_is_inf(x, x_is_inf); - mk_is_zero(x, x_is_zero); - - expr_ref sgn(m), sig(m), exp(m), lz(m); - unpack(x, sgn, sig, exp, lz, true); - // sig is of the form [1].[sigbits] - - SASSERT(m_bv_util.get_bv_size(sgn) == 1); - SASSERT(m_bv_util.get_bv_size(sig) == sbits); - SASSERT(m_bv_util.get_bv_size(exp) == ebits); - - expr_ref rsig(m), bit(m), zero(m), one(m), two(m), bv0(m), bv1(m); - zero = m_arith_util.mk_numeral(rational(0), rs); - one = m_arith_util.mk_numeral(rational(1), rs); - two = m_arith_util.mk_numeral(rational(2), rs); - bv0 = m_bv_util.mk_numeral(0, 1); - bv1 = m_bv_util.mk_numeral(1, 1); - rsig = one; - for (unsigned i = sbits-2; i != (unsigned)-1; i--) - { - bit = m_bv_util.mk_extract(i, i, sig); - rsig = m_arith_util.mk_add(m_arith_util.mk_mul(rsig, two), - m.mk_ite(m.mk_eq(bit, bv1), one, zero)); - } - - const mpz & p2 = fu().fm().m_powers2(sbits-1); - expr_ref ep2(m); - ep2 = m_arith_util.mk_numeral(rational(p2), false); - rsig = m_arith_util.mk_div(rsig, ep2); - dbg_decouple("fpa2bv_to_real_ep2", ep2); - dbg_decouple("fpa2bv_to_real_rsig", rsig); - - expr_ref exp_n(m), exp_p(m), exp_is_neg(m), exp_abs(m); - exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1); - dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg); - exp_p = m_bv_util.mk_sign_extend(1, exp); - exp_n = m_bv_util.mk_bv_neg(exp_p); - exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p); - dbg_decouple("fpa2bv_to_real_exp_abs", exp); - SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1); - - expr_ref exp2(m), prev_bit(m); - exp2 = zero; - for (unsigned i = ebits; i != (unsigned)-1; i--) - { - bit = m_bv_util.mk_extract(i, i, exp_abs); - exp2 = m_arith_util.mk_add(m_arith_util.mk_mul(exp2, two), - m.mk_ite(m.mk_eq(bit, bv1), one, zero)); - prev_bit = bit; - } - - exp2 = m.mk_ite(exp_is_neg, m_arith_util.mk_div(one, exp2), exp2); - dbg_decouple("fpa2bv_to_real_exp2", exp2); - - expr_ref res(m), two_exp2(m); - two_exp2 = m_arith_util.mk_power(two, exp2); - res = m_arith_util.mk_mul(rsig, two_exp2); - res = m.mk_ite(m.mk_eq(sgn, bv1), m_arith_util.mk_uminus(res), res); - dbg_decouple("fpa2bv_to_real_sig_times_exp2", res); - - TRACE("fpa2bv_to_real", tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl; - tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); - - result = m.mk_ite(x_is_zero, zero, res); - result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result); - result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result); - - SASSERT(is_well_sorted(m, result)); -} - expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) { if (m_hi_fp_unspecified) return expr_ref(m_bv_util.mk_numeral(0, width), m); @@ -2807,7 +2860,7 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified() { } void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); sgn = to_app(e)->get_arg(0); @@ -2816,7 +2869,7 @@ void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr * } void fpa2bv_converter::split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr *e_sgn, *e_sig, *e_exp; split_triple(e, e_sgn, e_sig, e_exp); @@ -2866,7 +2919,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_FLOAT_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref zero(m); @@ -2875,7 +2928,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_FLOAT_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref one(m); @@ -3038,7 +3091,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_FLOAT_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); SASSERT(to_app(e)->get_num_args() == 3); sort * srt = to_app(e)->get_decl()->get_range(); @@ -3131,11 +3184,11 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) { switch(f->get_decl_kind()) { - 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; + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break; + case OP_FPA_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; + case OP_FPA_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break; + case OP_FPA_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 6a7b6e92f..f81edb653 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -22,7 +22,7 @@ Notes: #include"ast.h" #include"obj_hashtable.h" #include"ref_util.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"bv_decl_plugin.h" #include"basic_simplifier_plugin.h" @@ -50,7 +50,7 @@ protected: arith_util m_arith_util; mpf_manager & m_mpf_manager; unsynch_mpz_manager & m_mpz_manager; - float_decl_plugin * m_plugin; + fpa_decl_plugin * m_plugin; bool m_hi_fp_unspecified; obj_map m_const2bv; @@ -76,7 +76,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_FLOAT_TO_FP, sign, exponent, significand); + result = m.mk_app(m_util.get_family_id(), OP_FPA_TO_FP, sign, exponent, significand); } void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const; @@ -130,15 +130,16 @@ public: void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); - void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); + void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_signed(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_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - + void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); + void mk_to_fp_real_int(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); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } expr_ref mk_to_ubv_unspecified(unsigned width); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 797f681e7..cbbd9e8a7 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -115,55 +115,55 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { - 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_pinf(f, result); return BR_DONE; - case OP_FLOAT_MINUS_INF: m_conv.mk_ninf(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_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_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_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; - case OP_FLOAT_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; - case OP_FLOAT_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; - case OP_FLOAT_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; - case OP_FLOAT_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; - case OP_FLOAT_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; - 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_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_FLOAT_TO_FP: m_conv.mk_to_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_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; - case OP_FLOAT_TO_REAL: m_conv.mk_to_real(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_INTERNAL_BVWRAP: - case OP_FLOAT_INTERNAL_BVUNWRAP: - case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; + case OP_FPA_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE; + case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; + case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; + case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; + case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; + case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; + case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE; + case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE; + case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE; + case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; + case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; + case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; + case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; + case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; + case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; + case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; + case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; + case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; + case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; + case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; + case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; + case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; + case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; + case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; + case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; + case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; + case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; + case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; + case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; 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/ast/float_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp similarity index 71% rename from src/ast/float_decl_plugin.cpp rename to src/ast/fpa_decl_plugin.cpp index bdc0c6fb1..be3e5f3ec 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - float_decl_plugin.cpp + fpa_decl_plugin.cpp Abstract: @@ -16,11 +16,11 @@ Author: Revision History: --*/ -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" -float_decl_plugin::float_decl_plugin(): +fpa_decl_plugin::fpa_decl_plugin(): m_values(m_fm), m_value_table(mpf_hash_proc(m_values), mpf_eq_proc(m_values)) { m_real_sort = 0; @@ -28,16 +28,16 @@ float_decl_plugin::float_decl_plugin(): m_bv_plugin = 0; } -void float_decl_plugin::set_manager(ast_manager * m, family_id id) { +void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) { decl_plugin::set_manager(m, id); m_arith_fid = m_manager->mk_family_id("arith"); m_real_sort = m_manager->mk_sort(m_arith_fid, REAL_SORT); - SASSERT(m_real_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin. + SASSERT(m_real_sort != 0); // arith_decl_plugin must be installed before fpa_decl_plugin. m_manager->inc_ref(m_real_sort); m_int_sort = m_manager->mk_sort(m_arith_fid, INT_SORT); - SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin. + SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before fpa_decl_plugin. m_manager->inc_ref(m_int_sort); // BV is not optional anymore. @@ -46,10 +46,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) { m_bv_plugin = static_cast(m_manager->get_plugin(m_bv_fid)); } -float_decl_plugin::~float_decl_plugin() { +fpa_decl_plugin::~fpa_decl_plugin() { } -unsigned float_decl_plugin::mk_id(mpf const & v) { +unsigned fpa_decl_plugin::mk_id(mpf const & v) { unsigned new_id = m_id_gen.mk(); m_values.reserve(new_id+1); m_fm.set(m_values[new_id], v); @@ -61,54 +61,54 @@ unsigned float_decl_plugin::mk_id(mpf const & v) { return old_id; } -void float_decl_plugin::recycled_id(unsigned id) { +void fpa_decl_plugin::recycled_id(unsigned id) { SASSERT(m_value_table.contains(id)); m_value_table.erase(id); m_id_gen.recycle(id); m_fm.del(m_values[id]); } -func_decl * float_decl_plugin::mk_value_decl(mpf const & v) { +func_decl * fpa_decl_plugin::mk_value_decl(mpf const & v) { parameter p(mk_id(v), true); SASSERT(p.is_external()); sort * s = mk_float_sort(v.get_ebits(), v.get_sbits()); - return m_manager->mk_const_decl(symbol("float"), s, func_decl_info(m_family_id, OP_FLOAT_VALUE, 1, &p)); + return m_manager->mk_const_decl(symbol("fpa"), s, func_decl_info(m_family_id, OP_FPA_VALUE, 1, &p)); } -app * float_decl_plugin::mk_value(mpf const & v) { +app * fpa_decl_plugin::mk_value(mpf const & v) { return m_manager->mk_const(mk_value_decl(v)); } -bool float_decl_plugin::is_value(expr * n, mpf & val) { - if (is_app_of(n, m_family_id, OP_FLOAT_VALUE)) { +bool fpa_decl_plugin::is_value(expr * n, mpf & val) { + if (is_app_of(n, m_family_id, OP_FPA_VALUE)) { m_fm.set(val, m_values[to_app(n)->get_decl()->get_parameter(0).get_ext_id()]); return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_INF)) { + else if (is_app_of(n, m_family_id, OP_FPA_MINUS_INF)) { 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_ninf(ebits, sbits, val); return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_INF)) { + else if (is_app_of(n, m_family_id, OP_FPA_PLUS_INF)) { 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_pinf(ebits, sbits, val); return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_NAN)) { + else if (is_app_of(n, m_family_id, OP_FPA_NAN)) { 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_nan(ebits, sbits, val); return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) { + else if (is_app_of(n, m_family_id, OP_FPA_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)) { + else if (is_app_of(n, m_family_id, OP_FPA_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); @@ -117,24 +117,24 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { return false; } -bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) { - if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_AWAY)) { +bool fpa_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) { + if (is_app_of(n, m_family_id, OP_FPA_RM_NEAREST_TIES_TO_AWAY)) { val = MPF_ROUND_NEAREST_TAWAY; return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_EVEN)) { + else if (is_app_of(n, m_family_id, OP_FPA_RM_NEAREST_TIES_TO_EVEN)) { val = MPF_ROUND_NEAREST_TEVEN; return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_NEGATIVE)) { + else if (is_app_of(n, m_family_id, OP_FPA_RM_TOWARD_NEGATIVE)) { val = MPF_ROUND_TOWARD_NEGATIVE; return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_POSITIVE)) { + else if (is_app_of(n, m_family_id, OP_FPA_RM_TOWARD_POSITIVE)) { val = MPF_ROUND_TOWARD_POSITIVE; return true; } - else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_ZERO)) { + else if (is_app_of(n, m_family_id, OP_FPA_RM_TOWARD_ZERO)) { val = MPF_ROUND_TOWARD_ZERO; return true; } @@ -142,27 +142,27 @@ bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) { return 0; } -void float_decl_plugin::del(parameter const & p) { +void fpa_decl_plugin::del(parameter const & p) { SASSERT(p.is_external()); recycled_id(p.get_ext_id()); } -parameter float_decl_plugin::translate(parameter const & p, decl_plugin & target) { +parameter fpa_decl_plugin::translate(parameter const & p, decl_plugin & target) { SASSERT(p.is_external()); - float_decl_plugin & _target = static_cast(target); + fpa_decl_plugin & _target = static_cast(target); return parameter(_target.mk_id(m_values[p.get_ext_id()]), true); } -void float_decl_plugin::finalize() { +void fpa_decl_plugin::finalize() { if (m_real_sort) { m_manager->dec_ref(m_real_sort); } if (m_int_sort) { m_manager->dec_ref(m_int_sort); } } -decl_plugin * float_decl_plugin::mk_fresh() { - return alloc(float_decl_plugin); +decl_plugin * fpa_decl_plugin::mk_fresh() { + return alloc(fpa_decl_plugin); } -sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { +sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { if (sbits < 2) m_manager->raise_exception("minimum number of significand bits is 1"); if (ebits < 2) @@ -172,16 +172,16 @@ 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("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps)); + return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOATING_POINT_SORT, sz, 2, ps)); } -sort * float_decl_plugin::mk_rm_sort() { +sort * fpa_decl_plugin::mk_rm_sort() { return m_manager->mk_sort(symbol("RoundingMode"), sort_info(m_family_id, ROUNDING_MODE_SORT)); } -sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { +sort * fpa_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { switch (k) { - case FLOAT_SORT: + case FLOATING_POINT_SORT: if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to floating point sort (ebits, sbits)"); return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); @@ -201,7 +201,7 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete } } -func_decl * float_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (num_parameters != 0) m_manager->raise_exception("rounding mode constant does not have parameters"); @@ -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_FLOAT_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return m_manager->mk_const_decl(symbol("roundNearestTiesToEven"), s, finfo); - case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return m_manager->mk_const_decl(symbol("roundNearestTiesToAway"), s, finfo); - case OP_FLOAT_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_POSITIVE: return m_manager->mk_const_decl(symbol("roundTowardPositive"), s, finfo); - case OP_FLOAT_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_NEGATIVE: return m_manager->mk_const_decl(symbol("roundTowardNegative"), s, finfo); - case OP_FLOAT_RM_TOWARD_ZERO: + case OP_FPA_RM_TOWARD_ZERO: return m_manager->mk_const_decl(symbol("roundTowardZero"), s, finfo); default: UNREACHABLE(); @@ -226,7 +226,7 @@ func_decl * float_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_parame } } -func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { sort * s; if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) { @@ -243,7 +243,7 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par UNREACHABLE(); } - SASSERT(is_sort_of(s, m_family_id, FLOAT_SORT)); + SASSERT(is_sort_of(s, m_family_id, FLOATING_POINT_SORT)); unsigned ebits = s->get_parameter(0).get_int(); unsigned sbits = s->get_parameter(1).get_int(); @@ -251,19 +251,19 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par switch (k) { - case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val); + case OP_FPA_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; + case OP_FPA_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break; + case OP_FPA_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break; + case OP_FPA_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break; + case OP_FPA_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break; } return mk_value_decl(val); } -func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point relation"); @@ -271,11 +271,11 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments"); symbol name; switch (k) { - 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.leq"; break; - case OP_FLOAT_GE: name = "fp.geq"; break; + case OP_FPA_EQ: name = "fp.eq"; break; + case OP_FPA_LT: name = "fp.lt"; break; + case OP_FPA_GT: name = "fp.gt"; break; + case OP_FPA_LE: name = "fp.leq"; break; + case OP_FPA_GE: name = "fp.geq"; break; default: UNREACHABLE(); break; @@ -285,7 +285,7 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo); } -func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_unary_rel_decl(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 floating point relation"); @@ -293,15 +293,15 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - 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; + case OP_FPA_IS_ZERO: name = "fp.isZero"; break; + case OP_FPA_IS_NZERO: name = "fp.isNZero"; break; + case OP_FPA_IS_PZERO: name = "fp.isPZero"; break; + case OP_FPA_IS_NEGATIVE: name = "fp.isNegative"; break; + case OP_FPA_IS_POSITIVE: name = "fp.isPositive"; break; + case OP_FPA_IS_NAN: name = "fp.isNaN"; break; + case OP_FPA_IS_INF: name = "fp.isInfinite"; break; + case OP_FPA_IS_NORMAL: name = "fp.isNormal"; break; + case OP_FPA_IS_SUBNORMAL: name = "fp.isSubnormal"; break; default: UNREACHABLE(); break; @@ -309,7 +309,7 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_unary_decl(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 floating point operator"); @@ -317,8 +317,8 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); symbol name; switch (k) { - case OP_FLOAT_ABS: name = "fp.abs"; break; - case OP_FLOAT_NEG: name = "fp.neg"; break; + case OP_FPA_ABS: name = "fp.abs"; break; + case OP_FPA_NEG: name = "fp.neg"; break; default: UNREACHABLE(); break; @@ -326,7 +326,7 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter return m_manager->mk_func_decl(name, arity, domain, domain[0], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); @@ -334,9 +334,9 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); symbol name; switch (k) { - case OP_FLOAT_REM: name = "fp.rem"; break; - case OP_FLOAT_MIN: name = "fp.min"; break; - case OP_FLOAT_MAX: name = "fp.max"; break; + case OP_FPA_REM: name = "fp.rem"; break; + case OP_FPA_MIN: name = "fp.min"; break; + case OP_FPA_MAX: name = "fp.max"; break; default: UNREACHABLE(); break; @@ -344,7 +344,7 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete return m_manager->mk_func_decl(name, arity, domain, domain[0], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 3) m_manager->raise_exception("invalid number of arguments to floating point operator"); @@ -354,10 +354,10 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts"); symbol name; switch (k) { - 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; + case OP_FPA_ADD: name = "fp.add"; break; + case OP_FPA_SUB: name = "fp.sub"; break; + case OP_FPA_MUL: name = "fp.mul"; break; + case OP_FPA_DIV: name = "fp.div"; break; default: UNREACHABLE(); break; @@ -365,7 +365,7 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 2) m_manager->raise_exception("invalid number of arguments to floating point operator"); @@ -375,8 +375,8 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument"); symbol name; switch (k) { - case OP_FLOAT_SQRT: name = "fp.sqrt"; break; - case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break; + case OP_FPA_SQRT: name = "fp.sqrt"; break; + case OP_FPA_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break; default: UNREACHABLE(); break; @@ -384,7 +384,7 @@ 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_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_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"); @@ -396,7 +396,7 @@ func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, para return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (m_bv_plugin && arity == 3 && is_sort_of(domain[0], m_bv_fid, BV_SORT) && @@ -444,7 +444,7 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa } 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)) { + is_sort_of(domain[1], m_family_id, FLOATING_POINT_SORT)) { // Rounding + 1 FP -> 1 FP if (num_parameters != 2) m_manager->raise_exception("invalid number of parameters to to_fp"); @@ -454,7 +454,7 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa 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)) + if (!is_sort_of(domain[1], m_family_id, FLOATING_POINT_SORT)) m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort"); sort * fp = mk_float_sort(ebits, sbits); @@ -514,7 +514,7 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa return 0; } -func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { SASSERT(m_bv_plugin); if (arity != 2) @@ -538,7 +538,7 @@ func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_param 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_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 3) m_manager->raise_exception("invalid number of arguments to fp"); @@ -555,7 +555,7 @@ func_decl * float_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, param 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, +func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { SASSERT(m_bv_plugin); if (arity != 2) @@ -566,7 +566,7 @@ func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, p m_manager->raise_exception("invalid parameter type; fp.to_ubv expects an int parameter"); 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)) + if (!is_sort_of(domain[1], m_family_id, FLOATING_POINT_SORT)) m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort"); if (parameters[0].get_int() <= 0) m_manager->raise_exception("invalid parameter value; fp.to_ubv expects a parameter larger than 0"); @@ -576,7 +576,7 @@ func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, p return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { SASSERT(m_bv_plugin); if (arity != 2) @@ -587,7 +587,7 @@ func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, p m_manager->raise_exception("invalid parameter type; fp.to_sbv expects an int parameter"); 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)) + if (!is_sort_of(domain[1], m_family_id, FLOATING_POINT_SORT)) m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort"); if (parameters[0].get_int() <= 0) m_manager->raise_exception("invalid parameter value; fp.to_sbv expects a parameter larger than 0"); @@ -598,7 +598,7 @@ func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, p } -func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_to_real(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 fp.to_real"); @@ -609,7 +609,7 @@ func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, return m_manager->mk_func_decl(name, 1, domain, m_real_sort, func_decl_info(m_family_id, k)); } -func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_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"); @@ -623,7 +623,7 @@ func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_par 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_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_internal_bv_wrap(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 internal_bv_wrap"); @@ -644,7 +644,7 @@ func_decl * float_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_par } } -func_decl * float_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(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 internal_bv_unwrap"); @@ -656,7 +656,7 @@ func_decl * float_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_p return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * float_decl_plugin::mk_internal_to_ubv_unspecified( +func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -670,7 +670,7 @@ func_decl * float_decl_plugin::mk_internal_to_ubv_unspecified( return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * float_decl_plugin::mk_internal_to_sbv_unspecified( +func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -683,7 +683,7 @@ func_decl * float_decl_plugin::mk_internal_to_sbv_unspecified( return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * float_decl_plugin::mk_internal_to_real_unspecified( +func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -695,81 +695,81 @@ func_decl * float_decl_plugin::mk_internal_to_real_unspecified( } -func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_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_FLOAT_MINUS_INF: - case OP_FLOAT_PLUS_INF: - case OP_FLOAT_NAN: - case OP_FLOAT_MINUS_ZERO: - case OP_FLOAT_PLUS_ZERO: + case OP_FPA_MINUS_INF: + case OP_FPA_PLUS_INF: + case OP_FPA_NAN: + case OP_FPA_MINUS_ZERO: + case OP_FPA_PLUS_ZERO: return mk_float_const_decl(k, num_parameters, parameters, arity, domain, range); - 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_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_ZERO: return mk_rm_const_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_EQ: - case OP_FLOAT_LT: - case OP_FLOAT_GT: - case OP_FLOAT_LE: - case OP_FLOAT_GE: + case OP_FPA_EQ: + case OP_FPA_LT: + case OP_FPA_GT: + case OP_FPA_LE: + case OP_FPA_GE: return mk_bin_rel_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_IS_ZERO: - case OP_FLOAT_IS_NZERO: - case OP_FLOAT_IS_PZERO: - 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: + case OP_FPA_IS_ZERO: + case OP_FPA_IS_NZERO: + case OP_FPA_IS_PZERO: + case OP_FPA_IS_NEGATIVE: + case OP_FPA_IS_POSITIVE: + case OP_FPA_IS_NAN: + case OP_FPA_IS_INF: + case OP_FPA_IS_NORMAL: + case OP_FPA_IS_SUBNORMAL: return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_ABS: - case OP_FLOAT_NEG: + case OP_FPA_ABS: + case OP_FPA_NEG: return mk_unary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_REM: - case OP_FLOAT_MIN: - case OP_FLOAT_MAX: + case OP_FPA_REM: + case OP_FPA_MIN: + case OP_FPA_MAX: return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_ADD: - case OP_FLOAT_MUL: - case OP_FLOAT_DIV: + case OP_FPA_ADD: + case OP_FPA_MUL: + case OP_FPA_DIV: return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_SUB: + case OP_FPA_SUB: if (arity == 1) - return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range); + return mk_unary_decl(OP_FPA_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: + case OP_FPA_SQRT: + case OP_FPA_ROUND_TO_INTEGRAL: return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_FMA: + case OP_FPA_FMA: return mk_fma(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_FP: + case OP_FPA_FP: return mk_fp(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_UBV: + case OP_FPA_TO_UBV: return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_SBV: + case OP_FPA_TO_SBV: return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_REAL: + case OP_FPA_TO_REAL: return mk_to_real(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_FP: + case OP_FPA_TO_FP: return mk_to_fp(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_FP_UNSIGNED: + case OP_FPA_TO_FP_UNSIGNED: return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_TO_IEEE_BV: + case OP_FPA_TO_IEEE_BV: return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVWRAP: return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); @@ -777,66 +777,66 @@ 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) { +void fpa_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { // 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("+oo", OP_FPA_PLUS_INF)); + op_names.push_back(builtin_name("-oo", OP_FPA_MINUS_INF)); + op_names.push_back(builtin_name("+zero", OP_FPA_PLUS_ZERO)); + op_names.push_back(builtin_name("-zero", OP_FPA_MINUS_ZERO)); + op_names.push_back(builtin_name("NaN", OP_FPA_NAN)); - 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("roundNearestTiesToEven", OP_FPA_RM_NEAREST_TIES_TO_EVEN)); + op_names.push_back(builtin_name("roundNearestTiesToAway", OP_FPA_RM_NEAREST_TIES_TO_AWAY)); + op_names.push_back(builtin_name("roundTowardPositive", OP_FPA_RM_TOWARD_POSITIVE)); + op_names.push_back(builtin_name("roundTowardNegative", OP_FPA_RM_TOWARD_NEGATIVE)); + op_names.push_back(builtin_name("roundTowardZero", OP_FPA_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("RNE", OP_FPA_RM_NEAREST_TIES_TO_EVEN)); + op_names.push_back(builtin_name("RNA", OP_FPA_RM_NEAREST_TIES_TO_AWAY)); + op_names.push_back(builtin_name("RTP", OP_FPA_RM_TOWARD_POSITIVE)); + op_names.push_back(builtin_name("RTN", OP_FPA_RM_TOWARD_NEGATIVE)); + op_names.push_back(builtin_name("RTZ", OP_FPA_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)); - 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_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.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.abs", OP_FPA_ABS)); + op_names.push_back(builtin_name("fp.neg", OP_FPA_NEG)); + op_names.push_back(builtin_name("fp.add", OP_FPA_ADD)); + op_names.push_back(builtin_name("fp.sub", OP_FPA_SUB)); + op_names.push_back(builtin_name("fp.mul", OP_FPA_MUL)); + op_names.push_back(builtin_name("fp.div", OP_FPA_DIV)); + op_names.push_back(builtin_name("fp.fma", OP_FPA_FMA)); + op_names.push_back(builtin_name("fp.sqrt", OP_FPA_SQRT)); + op_names.push_back(builtin_name("fp.rem", OP_FPA_REM)); + op_names.push_back(builtin_name("fp.roundToIntegral", OP_FPA_ROUND_TO_INTEGRAL)); + op_names.push_back(builtin_name("fp.min", OP_FPA_MIN)); + op_names.push_back(builtin_name("fp.max", OP_FPA_MAX)); + op_names.push_back(builtin_name("fp.leq", OP_FPA_LE)); + op_names.push_back(builtin_name("fp.lt", OP_FPA_LT)); + op_names.push_back(builtin_name("fp.geq", OP_FPA_GE)); + op_names.push_back(builtin_name("fp.gt", OP_FPA_GT)); + op_names.push_back(builtin_name("fp.eq", OP_FPA_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.isNegative", OP_FLOAT_IS_NEGATIVE)); - op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE)); + op_names.push_back(builtin_name("fp.isNormal", OP_FPA_IS_NORMAL)); + op_names.push_back(builtin_name("fp.isSubnormal", OP_FPA_IS_SUBNORMAL)); + op_names.push_back(builtin_name("fp.isZero", OP_FPA_IS_ZERO)); + op_names.push_back(builtin_name("fp.isInfinite", OP_FPA_IS_INF)); + op_names.push_back(builtin_name("fp.isNaN", OP_FPA_IS_NAN)); + op_names.push_back(builtin_name("fp.isNegative", OP_FPA_IS_NEGATIVE)); + op_names.push_back(builtin_name("fp.isPositive", OP_FPA_IS_POSITIVE)); - 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.to_real", OP_FLOAT_TO_REAL)); + op_names.push_back(builtin_name("fp", OP_FPA_FP)); + op_names.push_back(builtin_name("fp.to_ubv", OP_FPA_TO_UBV)); + op_names.push_back(builtin_name("fp.to_sbv", OP_FPA_TO_SBV)); + op_names.push_back(builtin_name("fp.to_real", OP_FPA_TO_REAL)); - 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)); + op_names.push_back(builtin_name("to_fp", OP_FPA_TO_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED)); /* Extensions */ - op_names.push_back(builtin_name("to_ieee_bv", OP_FLOAT_TO_IEEE_BV)); + op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); } -void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { - sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT)); +void fpa_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { + sort_names.push_back(builtin_name("FloatingPoint", FLOATING_POINT_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); // The final theory supports three common FloatingPoint sorts @@ -846,8 +846,8 @@ void float_decl_plugin::get_sort_names(svector & sort_names, symbo sort_names.push_back(builtin_name("Float128", FLOAT128_SORT)); } -expr * float_decl_plugin::get_some_value(sort * s) { - SASSERT(s->is_sort_of(m_family_id, FLOAT_SORT)); +expr * fpa_decl_plugin::get_some_value(sort * s) { + SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT)); mpf tmp; m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp); expr * res = this->mk_value(tmp); @@ -855,23 +855,23 @@ expr * float_decl_plugin::get_some_value(sort * s) { return res; } -bool float_decl_plugin::is_value(app * e) const { +bool fpa_decl_plugin::is_value(app * e) const { if (e->get_family_id() != m_family_id) return false; switch (e->get_decl_kind()) { - 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: - case OP_FLOAT_PLUS_ZERO: - case OP_FLOAT_MINUS_ZERO: - case OP_FLOAT_NAN: + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_ZERO: + case OP_FPA_VALUE: + case OP_FPA_PLUS_INF: + case OP_FPA_MINUS_INF: + case OP_FPA_PLUS_ZERO: + case OP_FPA_MINUS_ZERO: + case OP_FPA_NAN: return true; - case OP_FLOAT_FP: + case OP_FPA_FP: return m_manager->is_value(e->get_arg(0)) && m_manager->is_value(e->get_arg(1)) && m_manager->is_value(e->get_arg(2)); @@ -880,24 +880,24 @@ bool float_decl_plugin::is_value(app * e) const { } } -bool float_decl_plugin::is_unique_value(app* e) const { +bool fpa_decl_plugin::is_unique_value(app* e) const { if (e->get_family_id() != m_family_id) return false; switch (e->get_decl_kind()) { - 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_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_ZERO: return true; - case OP_FLOAT_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */ - case OP_FLOAT_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */ - case OP_FLOAT_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ - case OP_FLOAT_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ - case OP_FLOAT_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ - case OP_FLOAT_VALUE: /* see NaN */ + case OP_FPA_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */ + case OP_FPA_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */ + case OP_FPA_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ + case OP_FPA_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ + case OP_FPA_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ + case OP_FPA_VALUE: /* see NaN */ return false; - case OP_FLOAT_FP: + case OP_FPA_FP: return m_manager->is_unique_value(e->get_arg(0)) && m_manager->is_unique_value(e->get_arg(1)) && m_manager->is_unique_value(e->get_arg(2)); @@ -908,10 +908,10 @@ bool float_decl_plugin::is_unique_value(app* e) const { float_util::float_util(ast_manager & m): m_manager(m), - m_fid(m.mk_family_id("float")), + m_fid(m.mk_family_id("fpa")), m_a_util(m), m_bv_util(m) { - m_plugin = static_cast(m.get_plugin(m_fid)); + m_plugin = static_cast(m.get_plugin(m_fid)); } float_util::~float_util() { @@ -919,7 +919,7 @@ float_util::~float_util() { sort * float_util::mk_float_sort(unsigned ebits, unsigned sbits) { parameter ps[2] = { parameter(ebits), parameter(sbits) }; - return m().mk_sort(m_fid, FLOAT_SORT, 2, ps); + return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps); } unsigned float_util::get_ebits(sort * s) { @@ -965,16 +965,16 @@ app * float_util::mk_nzero(unsigned ebits, unsigned sbits) { app * float_util::mk_internal_to_ubv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); } app * float_util::mk_internal_to_sbv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); } app * float_util::mk_internal_to_real_unspecified() { sort * range = m_a_util.mk_real(); - return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); } \ No newline at end of file diff --git a/src/ast/float_decl_plugin.h b/src/ast/fpa_decl_plugin.h similarity index 77% rename from src/ast/float_decl_plugin.h rename to src/ast/fpa_decl_plugin.h index cbcd706cd..b7d59a6af 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - float_decl_plugin.h + fpa_decl_plugin.h Abstract: @@ -16,8 +16,8 @@ Author: Revision History: --*/ -#ifndef _FLOAT_DECL_PLUGIN_H_ -#define _FLOAT_DECL_PLUGIN_H_ +#ifndef _fpa_decl_plugin_H_ +#define _fpa_decl_plugin_H_ #include"ast.h" #include"id_gen.h" @@ -25,8 +25,8 @@ Revision History: #include"bv_decl_plugin.h" #include"mpf.h" -enum float_sort_kind { - FLOAT_SORT, +enum fpa_sort_kind { + FLOATING_POINT_SORT, ROUNDING_MODE_SORT, FLOAT16_SORT, FLOAT32_SORT, @@ -34,69 +34,69 @@ enum float_sort_kind { FLOAT128_SORT }; -enum float_op_kind { - 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, +enum fpa_op_kind { + OP_FPA_RM_NEAREST_TIES_TO_EVEN, + OP_FPA_RM_NEAREST_TIES_TO_AWAY, + OP_FPA_RM_TOWARD_POSITIVE, + OP_FPA_RM_TOWARD_NEGATIVE, + OP_FPA_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_FPA_VALUE, + OP_FPA_PLUS_INF, + OP_FPA_MINUS_INF, + OP_FPA_NAN, + OP_FPA_PLUS_ZERO, + OP_FPA_MINUS_ZERO, - OP_FLOAT_ADD, - OP_FLOAT_SUB, - OP_FLOAT_NEG, - OP_FLOAT_MUL, - OP_FLOAT_DIV, - OP_FLOAT_REM, - OP_FLOAT_ABS, - OP_FLOAT_MIN, - OP_FLOAT_MAX, - OP_FLOAT_FMA, // x*y + z - OP_FLOAT_SQRT, - OP_FLOAT_ROUND_TO_INTEGRAL, + OP_FPA_ADD, + OP_FPA_SUB, + OP_FPA_NEG, + OP_FPA_MUL, + OP_FPA_DIV, + OP_FPA_REM, + OP_FPA_ABS, + OP_FPA_MIN, + OP_FPA_MAX, + OP_FPA_FMA, // x*y + z + OP_FPA_SQRT, + OP_FPA_ROUND_TO_INTEGRAL, - OP_FLOAT_EQ, - OP_FLOAT_LT, - OP_FLOAT_GT, - OP_FLOAT_LE, - OP_FLOAT_GE, - OP_FLOAT_IS_NAN, - OP_FLOAT_IS_INF, - OP_FLOAT_IS_ZERO, - OP_FLOAT_IS_NORMAL, - OP_FLOAT_IS_SUBNORMAL, - OP_FLOAT_IS_PZERO, - OP_FLOAT_IS_NZERO, - OP_FLOAT_IS_NEGATIVE, - OP_FLOAT_IS_POSITIVE, + OP_FPA_EQ, + OP_FPA_LT, + OP_FPA_GT, + OP_FPA_LE, + OP_FPA_GE, + OP_FPA_IS_NAN, + OP_FPA_IS_INF, + OP_FPA_IS_ZERO, + OP_FPA_IS_NORMAL, + OP_FPA_IS_SUBNORMAL, + OP_FPA_IS_PZERO, + OP_FPA_IS_NZERO, + OP_FPA_IS_NEGATIVE, + OP_FPA_IS_POSITIVE, - OP_FLOAT_FP, - OP_FLOAT_TO_FP, - OP_FLOAT_TO_FP_UNSIGNED, - OP_FLOAT_TO_UBV, - OP_FLOAT_TO_SBV, - OP_FLOAT_TO_REAL, + OP_FPA_FP, + OP_FPA_TO_FP, + OP_FPA_TO_FP_UNSIGNED, + OP_FPA_TO_UBV, + OP_FPA_TO_SBV, + OP_FPA_TO_REAL, /* Extensions */ - OP_FLOAT_TO_IEEE_BV, + OP_FPA_TO_IEEE_BV, /* Internal use only */ - OP_FLOAT_INTERNAL_BVWRAP, - OP_FLOAT_INTERNAL_BVUNWRAP, - OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED, - OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED, - OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED, + OP_FPA_INTERNAL_BVWRAP, + OP_FPA_INTERNAL_BVUNWRAP, + OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, + OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, + OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, LAST_FLOAT_OP }; -class float_decl_plugin : public decl_plugin { +class fpa_decl_plugin : public decl_plugin { struct mpf_hash_proc { scoped_mpf_vector const & m_values; mpf_hash_proc(scoped_mpf_vector const & values):m_values(values) {} @@ -172,12 +172,12 @@ class float_decl_plugin : public decl_plugin { unsigned mk_id(mpf const & v); void recycled_id(unsigned id); public: - float_decl_plugin(); + fpa_decl_plugin(); - bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOAT_SORT); } + bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); } bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); } - virtual ~float_decl_plugin(); + virtual ~fpa_decl_plugin(); virtual void finalize(); virtual decl_plugin * mk_fresh(); @@ -193,7 +193,7 @@ public: mpf_manager & fm() { return m_fm; } func_decl * mk_value_decl(mpf const & v); app * mk_value(mpf const & v); - bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); } + bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FPA_VALUE); } bool is_value(expr * n, mpf & val); bool is_rm_value(expr * n, mpf_rounding_mode & val); bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); } @@ -209,7 +209,7 @@ public: class float_util { ast_manager & m_manager; - float_decl_plugin * m_plugin; + fpa_decl_plugin * m_plugin; family_id m_fid; arith_util m_a_util; bv_util m_bv_util; @@ -222,22 +222,22 @@ 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; } + fpa_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); } - bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); } + bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOATING_POINT_SORT); } bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); } bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); } bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); } unsigned get_ebits(sort * s); unsigned get_sbits(sort * s); - 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_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_FPA_RM_NEAREST_TIES_TO_EVEN); } + app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_FPA_RM_NEAREST_TIES_TO_AWAY); } + app * mk_round_toward_positive() { return m().mk_const(m_fid, OP_FPA_RM_TOWARD_POSITIVE); } + app * mk_round_toward_negative() { return m().mk_const(m_fid, OP_FPA_RM_TOWARD_NEGATIVE); } + app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_FPA_RM_TOWARD_ZERO); } app * mk_nan(unsigned ebits, unsigned sbits); app * mk_pinf(unsigned ebits, unsigned sbits); @@ -264,83 +264,83 @@ 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); } - app * mk_fp(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_FP, arg1, arg2, arg3); } + app * mk_fp(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_FP, arg1, arg2, arg3); } app * mk_to_fp(sort * s, expr * bv_t) { SASSERT(is_float(s) && s->get_num_parameters() == 2); - return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 1, &bv_t); + return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t); } app * mk_to_fp(sort * s, expr * rm, expr * t) { SASSERT(is_float(s) && s->get_num_parameters() == 2); expr * args[] = { rm, t }; - return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 2, args); + return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 2, args); } app * mk_to_fp(sort * s, expr * rm, expr * sig, expr * exp) { SASSERT(is_float(s) && s->get_num_parameters() == 2); expr * args[] = { rm, sig, exp }; - return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 3, args); + return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 3, args); } app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) { SASSERT(is_float(s) && s->get_num_parameters() == 2); expr * args[] = { rm, t }; - return m().mk_app(m_fid, OP_FLOAT_TO_FP_UNSIGNED, 2, s->get_parameters(), 2, args); + return m().mk_app(m_fid, OP_FPA_TO_FP_UNSIGNED, 2, s->get_parameters(), 2, args); } - bool is_to_fp(expr * n) { return is_app_of(n, m_fid, OP_FLOAT_TO_FP); } + bool is_to_fp(expr * n) { return is_app_of(n, m_fid, OP_FPA_TO_FP); } app * mk_to_ubv(expr * rm, expr * t, unsigned sz) { parameter ps[] = { parameter(sz) }; expr * args[] = { rm, t }; - return m().mk_app(m_fid, OP_FLOAT_TO_UBV, 1, ps, 2, args); } + return m().mk_app(m_fid, OP_FPA_TO_UBV, 1, ps, 2, args); } app * mk_to_sbv(expr * rm, expr * t, unsigned sz) { parameter ps[] = { parameter(sz) }; expr * args[] = { rm, t }; - return m().mk_app(m_fid, OP_FLOAT_TO_SBV, 1, ps, 2, args); + return m().mk_app(m_fid, OP_FPA_TO_SBV, 1, ps, 2, args); } - app * mk_to_real(expr * t) { return m().mk_app(m_fid, OP_FLOAT_TO_REAL, t); } + app * mk_to_real(expr * t) { return m().mk_app(m_fid, OP_FPA_TO_REAL, t); } - 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); } - app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); } - 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_to_integral(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } + app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_ADD, arg1, arg2, arg3); } + app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_MUL, arg1, arg2, arg3); } + app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_SUB, arg1, arg2, arg3); } + app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_DIV, arg1, arg2, arg3); } + app * mk_neg(expr * arg1) { return m().mk_app(m_fid, OP_FPA_NEG, arg1); } + app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_REM, arg1, arg2); } + app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_MAX, arg1, arg2); } + app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_MIN, arg1, arg2); } + app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FPA_ABS, arg1); } + app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_SQRT, arg1, arg2); } + app * mk_round_to_integral(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_ROUND_TO_INTEGRAL, arg1, arg2); } 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_FMA, 4, args); + return m().mk_app(m_fid, OP_FPA_FMA, 4, args); } - app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); } - app * mk_lt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LT, arg1, arg2); } - app * mk_gt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GT, arg1, arg2); } - app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); } - app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); } + app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_EQ, arg1, arg2); } + app * mk_lt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_LT, arg1, arg2); } + app * mk_gt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_GT, arg1, arg2); } + app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_LE, arg1, arg2); } + app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FPA_GE, arg1, arg2); } - app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NAN, arg1); } - app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); } - app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); } - app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); } - 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_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); } + app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NAN, arg1); } + app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_INF, arg1); } + app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); } + app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); } + app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); } + app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NZERO, arg1); } + app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_PZERO, arg1); } + app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); } + app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); } + app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); } - bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); } + bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FPA_NEG); } - app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); } + app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } app * mk_internal_to_ubv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_real_unspecified(); - bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FLOAT_INTERNAL_BVWRAP); } - bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP); } + bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } + bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVUNWRAP); } }; #endif diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index ab1844e07..f46dd76d4 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -24,7 +24,7 @@ Revision History: #include"datatype_decl_plugin.h" #include"dl_decl_plugin.h" #include"seq_decl_plugin.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -45,7 +45,7 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("seq")))) { m.register_plugin(symbol("seq"), alloc(seq_decl_plugin)); } - if (!m.get_plugin(m.mk_family_id(symbol("float")))) { - m.register_plugin(symbol("float"), alloc(float_decl_plugin)); + if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) { + m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin)); } } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp similarity index 69% rename from src/ast/rewriter/float_rewriter.cpp rename to src/ast/rewriter/fpa_rewriter.cpp index 96561395e..2977b7ab2 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - float_rewriter.cpp + fpa_rewriter.cpp Abstract: @@ -16,65 +16,65 @@ Author: Notes: --*/ -#include"float_rewriter.h" +#include"fpa_rewriter.h" -float_rewriter::float_rewriter(ast_manager & m, params_ref const & p): +fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p): m_util(m) { updt_params(p); } -float_rewriter::~float_rewriter() { +fpa_rewriter::~fpa_rewriter() { } -void float_rewriter::updt_params(params_ref const & p) { +void fpa_rewriter::updt_params(params_ref const & p) { } -void float_rewriter::get_param_descrs(param_descrs & r) { +void fpa_rewriter::get_param_descrs(param_descrs & r) { } -br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status st = BR_FAILED; SASSERT(f->get_family_id() == get_fid()); switch (f->get_decl_kind()) { - case OP_FLOAT_TO_FP: st = mk_to_fp(f, num_args, args, result); break; - case OP_FLOAT_TO_FP_UNSIGNED: st = mk_to_fp_unsigned(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; - 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_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; + case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; + case OP_FPA_TO_FP_UNSIGNED: st = mk_to_fp_unsigned(f, num_args, args, result); break; + case OP_FPA_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break; + case OP_FPA_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break; + case OP_FPA_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; + case OP_FPA_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break; + case OP_FPA_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break; + case OP_FPA_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break; + case OP_FPA_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break; + case OP_FPA_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break; + case OP_FPA_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; + case OP_FPA_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break; + case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; + case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break; - case OP_FLOAT_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; - case OP_FLOAT_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break; - case OP_FLOAT_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break; - case OP_FLOAT_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break; - case OP_FLOAT_GE: SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break; - case OP_FLOAT_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break; - case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; - case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; - case OP_FLOAT_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break; - 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_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_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; - case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(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_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; + case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break; + case OP_FPA_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break; + case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break; + case OP_FPA_GE: SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break; + case OP_FPA_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break; + case OP_FPA_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; + case OP_FPA_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; + case OP_FPA_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break; + case OP_FPA_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; + case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; + case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; + case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; + case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; + case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; + case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; + case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } return st; } -br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); @@ -159,7 +159,7 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons return BR_FAILED; } -br_status float_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { +br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, 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()); @@ -169,7 +169,7 @@ br_status float_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, ex return BR_FAILED; } -br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, 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()); @@ -184,13 +184,13 @@ br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_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_neg(arg3)); return BR_REWRITE2; } -br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, 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()); @@ -205,7 +205,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, 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()); @@ -220,7 +220,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { if (m_util.is_nan(arg1)) { // -nan --> nan result = arg1; @@ -253,7 +253,7 @@ br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { scoped_mpf t(m_util.fm()); @@ -265,7 +265,7 @@ br_status float_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) { if (m_util.is_nan(arg1)) { result = arg1; return BR_DONE; @@ -276,7 +276,7 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) { return BR_REWRITE2; } -br_status float_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_nan(arg1)) { result = arg2; return BR_DONE; @@ -296,7 +296,7 @@ br_status float_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE_FULL; } -br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_nan(arg1)) { result = arg2; return BR_DONE; @@ -316,7 +316,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE_FULL; } -br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { +br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); @@ -331,7 +331,7 @@ br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * a return BR_FAILED; } -br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { scoped_mpf v2(m_util.fm()); @@ -346,7 +346,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { scoped_mpf v2(m_util.fm()); @@ -362,7 +362,7 @@ br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) } // This the floating point theory == -br_status float_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { result = (m_util.fm().eq(v1, v2)) ? m().mk_true() : m().mk_false(); @@ -373,16 +373,16 @@ br_status float_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & resul } // Return (= arg NaN) -app * float_rewriter::mk_eq_nan(expr * arg) { +app * fpa_rewriter::mk_eq_nan(expr * arg) { return m().mk_eq(arg, m_util.mk_nan(m().get_sort(arg))); } // Return (not (= arg NaN)) -app * float_rewriter::mk_neq_nan(expr * arg) { +app * fpa_rewriter::mk_neq_nan(expr * arg) { return m().mk_not(mk_eq_nan(arg)); } -br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) { result = m().mk_false(); return BR_DONE; @@ -418,12 +418,12 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) { result = m_util.mk_lt(arg2, arg1); return BR_REWRITE1; } -br_status float_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) { result = m().mk_false(); return BR_DONE; @@ -437,12 +437,12 @@ br_status float_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { result = m_util.mk_le(arg2, arg1); return BR_REWRITE1; } -br_status float_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_zero(v)) ? m().mk_true() : m().mk_false(); @@ -452,7 +452,7 @@ br_status float_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_nzero(v)) ? m().mk_true() : m().mk_false(); @@ -462,7 +462,7 @@ br_status float_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_pzero(v)) ? m().mk_true() : m().mk_false(); @@ -472,7 +472,7 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false(); @@ -482,7 +482,7 @@ br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); @@ -492,7 +492,7 @@ br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); @@ -502,7 +502,7 @@ br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { +br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); @@ -512,7 +512,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { +br_status fpa_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(); @@ -522,7 +522,7 @@ br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { return BR_FAILED; } -br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { +br_status fpa_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(); @@ -534,7 +534,7 @@ br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { // This the SMT = -br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { // Note: == is the floats-equality, here we need normal equality. @@ -548,11 +548,11 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result return BR_FAILED; } -br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { +br_status fpa_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) { +br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { bv_util bu(m()); rational r1, r2, r3; unsigned bvs1, bvs2, bvs3; @@ -575,15 +575,15 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref return BR_FAILED; } -br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_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) { +br_status fpa_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) { +br_status fpa_rewriter::mk_to_real(expr * arg1, expr_ref & result) { scoped_mpf fv(m_util.fm()); if (m_util.is_value(arg1, fv)) { @@ -599,4 +599,4 @@ 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/fpa_rewriter.h similarity index 95% rename from src/ast/rewriter/float_rewriter.h rename to src/ast/rewriter/fpa_rewriter.h index 31c571f32..34a34b293 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -22,10 +22,10 @@ Notes: #include"ast.h" #include"rewriter.h" #include"params.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"mpf.h" -class float_rewriter { +class fpa_rewriter { float_util m_util; mpf_manager m_fm; @@ -33,8 +33,8 @@ class float_rewriter { app * mk_neq_nan(expr * arg); public: - float_rewriter(ast_manager & m, params_ref const & p = params_ref()); - ~float_rewriter(); + fpa_rewriter(ast_manager & m, params_ref const & p = params_ref()); + ~fpa_rewriter(); ast_manager & m() const { return m_util.m(); } family_id get_fid() const { return m_util.get_fid(); } diff --git a/src/ast/rewriter/mk_simplified_app.cpp b/src/ast/rewriter/mk_simplified_app.cpp index a46e71582..45245ce1b 100644 --- a/src/ast/rewriter/mk_simplified_app.cpp +++ b/src/ast/rewriter/mk_simplified_app.cpp @@ -22,7 +22,7 @@ Notes: #include"bv_rewriter.h" #include"datatype_rewriter.h" #include"array_rewriter.h" -#include"float_rewriter.h" +#include"fpa_rewriter.h" struct mk_simplified_app::imp { ast_manager & m; @@ -31,7 +31,7 @@ struct mk_simplified_app::imp { bv_rewriter m_bv_rw; array_rewriter m_ar_rw; datatype_rewriter m_dt_rw; - float_rewriter m_f_rw; + fpa_rewriter m_f_rw; imp(ast_manager & _m, params_ref const & p): m(_m), diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 0e2c8e781..f35c3b134 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -23,7 +23,7 @@ Notes: #include"bv_rewriter.h" #include"datatype_rewriter.h" #include"array_rewriter.h" -#include"float_rewriter.h" +#include"fpa_rewriter.h" #include"dl_rewriter.h" #include"rewriter_def.h" #include"expr_substitution.h" @@ -39,7 +39,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { bv_rewriter m_bv_rw; array_rewriter m_ar_rw; datatype_rewriter m_dt_rw; - float_rewriter m_f_rw; + fpa_rewriter m_f_rw; dl_rewriter m_dl_rw; arith_util m_a_util; bv_util m_bv_util; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4dd0cc614..d5ee9ff88 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -24,7 +24,7 @@ Notes: #include"array_decl_plugin.h" #include"datatype_decl_plugin.h" #include"seq_decl_plugin.h" -#include"float_decl_plugin.h" +#include"fpa_decl_plugin.h" #include"ast_pp.h" #include"var_subst.h" #include"pp.h" @@ -556,7 +556,7 @@ bool cmd_context::logic_has_seq() const { return !has_logic() || logic_has_seq_core(m_logic); } -bool cmd_context::logic_has_floats() const { +bool cmd_context::logic_has_fpa() const { return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV"; } @@ -601,7 +601,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); - register_plugin(symbol("float"), alloc(float_decl_plugin), logic_has_floats()); + register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); } else { // the manager was created by an external module @@ -614,7 +614,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("array"), logic_has_array(), fids); load_plugin(symbol("datatype"), logic_has_datatype(), fids); load_plugin(symbol("seq"), logic_has_seq(), fids); - load_plugin(symbol("float"), logic_has_floats(), fids); + load_plugin(symbol("fpa"), logic_has_fpa(), fids); svector::iterator it = fids.begin(); svector::iterator end = fids.end(); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 1c8dba21a..f9e50e611 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -241,7 +241,7 @@ protected: bool logic_has_seq() const; bool logic_has_array() const; bool logic_has_datatype() const; - bool logic_has_floats() const; + bool logic_has_fpa() const; bool supported_logic(symbol const & s) const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 41bca940d..02c43eaad 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -25,7 +25,7 @@ Revision History: #include"bv_rewriter.h" #include"datatype_rewriter.h" #include"array_rewriter.h" -#include"float_rewriter.h" +#include"fpa_rewriter.h" #include"rewriter_def.h" #include"cooperate.h" @@ -36,7 +36,7 @@ struct evaluator_cfg : public default_rewriter_cfg { bv_rewriter m_bv_rw; array_rewriter m_ar_rw; datatype_rewriter m_dt_rw; - float_rewriter m_f_rw; + fpa_rewriter m_f_rw; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index bec9cf235..7c4fce5cd 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -82,7 +82,7 @@ namespace smt { } theory_fpa::theory_fpa(ast_manager & m) : - theory(m.mk_family_id("float")), + theory(m.mk_family_id("fpa")), m_converter(m, this), m_rw(m, m_converter, params_ref()), m_th_rw(m), @@ -91,6 +91,9 @@ namespace smt { m_bv_util(m_converter.bu()), m_arith_util(m_converter.au()) { + params_ref p; + p.set_bool("arith_lhs", true); + m_th_rw.updt_params(p); } theory_fpa::~theory_fpa() @@ -207,7 +210,7 @@ namespace smt { bv_srt = m_bv_util.mk_sort(ebits + sbits); } - w = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); + w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); m_wraps.insert(e_srt, w); m.inc_ref(w); } @@ -226,7 +229,7 @@ namespace smt { if (!m_unwraps.find(e_srt, u)) { SASSERT(!m_unwraps.contains(e_srt)); sort * bv_srt = m.get_sort(e); - u = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s); + u = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s); m_unwraps.insert(s, u); m.inc_ref(u); } @@ -268,10 +271,10 @@ namespace smt { } else if (m_float_util.is_float(e)) { SASSERT(eca->get_family_id() == get_family_id()); - float_op_kind k = (float_op_kind)(eca->get_decl_kind()); - SASSERT(k == OP_FLOAT_TO_FP || k == OP_FLOAT_INTERNAL_BVUNWRAP); + fpa_op_kind k = (fpa_op_kind)(eca->get_decl_kind()); + SASSERT(k == OP_FPA_TO_FP || k == OP_FPA_INTERNAL_BVUNWRAP); switch (k) { - case OP_FLOAT_TO_FP: { + case OP_FPA_TO_FP: { SASSERT(eca->get_num_args() == 3); SASSERT(is_sort_of(m.get_sort(eca->get_arg(0)), m_bv_util.get_family_id(), BV_SORT)); SASSERT(is_sort_of(m.get_sort(eca->get_arg(1)), m_bv_util.get_family_id(), BV_SORT)); @@ -388,6 +391,8 @@ namespace smt { res = m.mk_and(res, t); } m_converter.m_extra_assertions.reset(); + + m_th_rw(res); CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";); return res; @@ -460,11 +465,11 @@ namespace smt { // The corresponding constraints will not be translated and added // via convert(...) and assert_cnstr(...) in initialize_atom(...). // Therefore, we translate and assert them here. - float_op_kind k = (float_op_kind)term->get_decl_kind(); + fpa_op_kind k = (fpa_op_kind)term->get_decl_kind(); switch (k) { - case OP_FLOAT_TO_UBV: - case OP_FLOAT_TO_SBV: - case OP_FLOAT_TO_REAL: { + case OP_FPA_TO_UBV: + case OP_FPA_TO_SBV: + case OP_FPA_TO_REAL: { expr_ref conv(m); conv = convert(term); assert_cnstr(m.mk_eq(term, conv)); @@ -546,7 +551,7 @@ namespace smt { c = m.mk_and(m.mk_eq(x_sgn, y_sgn), m.mk_eq(x_sig, y_sig), - m.mk_eq(x_exp, y_exp)); + m.mk_eq(x_exp, y_exp)); } else c = m.mk_eq(xc, yc); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 989ad64ff..78ba64111 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), exp, true); bv_mdl->eval(a->get_arg(2), sig, true); - SASSERT(a->is_app_of(fu.get_family_id(), OP_FLOAT_TO_FP)); + SASSERT(a->is_app_of(fu.get_family_id(), OP_FPA_TO_FP)); #ifdef Z3DEBUG SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 919cf0c1b..c02166c18 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -26,21 +26,23 @@ Notes: #include"qffpa_tactic.h" tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { - params_ref sat_simp_p = p; - sat_simp_p .set_bool("elim_and", true); + params_ref simp_p = p; + simp_p.set_bool("arith_lhs", true); + simp_p.set_bool("elim_and", true); - tactic * st = - cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - and_then(mk_simplify_tactic(m), - mk_smt_tactic()), - and_then( - mk_simplify_tactic(m, p), - mk_fpa2bv_tactic(m, p), - using_params(mk_simplify_tactic(m, p), sat_simp_p), - mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), sat_simp_p), - mk_sat_tactic(m, p), - mk_fail_if_undecided_tactic())); + tactic * st = cond( mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + and_then(mk_simplify_tactic(m, simp_p), + mk_smt_tactic()), + and_then( + mk_simplify_tactic(m, p), + mk_fpa2bv_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + mk_bit_blaster_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + cond(mk_is_propositional_probe(), + mk_sat_tactic(m, p), + mk_smt_tactic(p)), + mk_fail_if_undecided_tactic())); st->updt_params(p); return st; @@ -70,6 +72,8 @@ struct is_non_qffp_predicate { return; if (is_uninterp_const(n)) return; + if (au.is_real(s) && au.is_numeral(n)) + return; throw found(); } diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 660622fb8..3ab95798f 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - qffpa_tactic.h + qffp_tactic.h Abstract: - Tactic QF_FPA benchmarks. + Tactic for QF_FP benchmarks. Author: