diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 2085de296..c75553e7b 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2022,6 +2022,17 @@ namespace test_mapi // Console.WriteLine("{0}", ctx.MkEq(s1, t1)); } + public static void FloatingPointExample(Context ctx) + { + Console.WriteLine("FloatingPointExample"); + + FPSort s = ctx.MkFPSort(11, 53); + Console.WriteLine("Sort: {0}", s); + + FPNum n = (FPNum) ctx.MkNumeral("0.125", s); + Console.WriteLine("Numeral: {0}", n.ToString()); + } + static void Main(string[] args) { try @@ -2063,6 +2074,7 @@ namespace test_mapi FindSmallModelExample(ctx); SimplifierExample(ctx); FiniteDomainExample(ctx); + FloatingPointExample(ctx); } // These examples need proof generation turned on. diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 6855f6209..ccc2cbf88 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -647,6 +647,12 @@ 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) { + 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; + } else { return Z3_UNKNOWN_SORT; } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index cf179332a..f4314dcca 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -88,6 +88,7 @@ namespace api { m_arith_util(m()), m_bv_util(m()), m_datalog_util(m()), + m_float_util(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack() { @@ -112,6 +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_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 e0c95b07b..f409a4ece 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -27,6 +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"smt_kernel.h" #include"smt_params.h" #include"event_handler.h" @@ -56,6 +57,7 @@ namespace api { arith_util m_arith_util; bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; + float_util m_float_util; // Support for old solver API smt_params m_fparams; @@ -75,6 +77,7 @@ namespace api { family_id m_bv_fid; family_id m_dt_fid; family_id m_datalog_fid; + family_id m_fpa_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -115,12 +118,14 @@ namespace api { arith_util & autil() { return m_arith_util; } bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } + float_util & float_util() { return m_float_util; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } family_id get_bv_fid() const { return m_bv_fid; } family_id get_dt_fid() const { return m_dt_fid; } family_id get_datalog_fid() const { return m_datalog_fid; } + family_id get_fpa_fid() const { return m_fpa_fid; } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } Z3_error_code get_error_code() const { return m_error_code; } diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index cfb5a2624..278a0556a 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -28,7 +28,7 @@ extern "C" { LOG_Z3_mk_fpa_rounding_mode_sort(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_sort r = of_sort(float_util(ctx->m()).mk_rm_sort()); + Z3_sort r = of_sort(ctx->float_util().mk_rm_sort()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -39,7 +39,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_round_nearest_ties_to_even()); + Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_even()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -50,7 +50,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_round_nearest_ties_to_away()); + Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_away()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -61,7 +61,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_positive()); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_positive()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -72,7 +72,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_negative()); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_negative()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -83,7 +83,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_zero()); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_zero()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -95,9 +95,8 @@ extern "C" { if (ebits < 2 || sbits < 3) { SET_ERROR_CODE(Z3_INVALID_ARG); } - api::context * ctx = mk_c(c); - float_util fu(ctx->m()); - Z3_sort r = of_sort(fu.mk_float_sort(ebits, sbits)); + api::context * ctx = mk_c(c); + Z3_sort r = of_sort(ctx->float_util().mk_float_sort(ebits, sbits)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -107,7 +106,7 @@ extern "C" { LOG_Z3_mk_fpa_nan(c, s); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_nan(to_sort(s))); + Z3_ast r = of_ast(ctx->float_util().mk_nan(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -117,8 +116,7 @@ extern "C" { LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - float_util fu(ctx->m()); - Z3_ast r = of_ast(negative != 0 ? fu.mk_minus_inf(to_sort(s)) : fu.mk_plus_inf(to_sort(s))); + Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_minus_inf(to_sort(s)) : ctx->float_util().mk_plus_inf(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -128,10 +126,9 @@ extern "C" { LOG_Z3_mk_double(c, v, ty); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - float_util fu(ctx->m()); - mpf tmp; - fu.fm().set(tmp, fu.get_ebits(to_sort(ty)), fu.get_sbits(to_sort(ty)), v); - Z3_ast r = of_ast(fu.mk_value(tmp)); + scoped_mpf tmp(ctx->float_util().fm()); + ctx->float_util().fm().set(tmp, ctx->float_util().get_ebits(to_sort(ty)), ctx->float_util().get_sbits(to_sort(ty)), v); + Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -141,7 +138,7 @@ extern "C" { LOG_Z3_mk_fpa_abs(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_abs(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_abs(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -151,7 +148,7 @@ extern "C" { LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_uminus(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_uminus(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -161,7 +158,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -171,7 +168,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -181,7 +178,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -191,7 +188,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -201,7 +198,7 @@ extern "C" { LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); + Z3_ast r = of_ast(ctx->float_util().mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -211,7 +208,7 @@ extern "C" { LOG_Z3_mk_fpa_sqrt(c, rm, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_sqrt(to_expr(rm), to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_sqrt(to_expr(rm), to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -221,7 +218,7 @@ extern "C" { LOG_Z3_mk_fpa_rem(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_rem(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_rem(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -231,7 +228,7 @@ extern "C" { LOG_Z3_mk_fpa_eq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_float_eq(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_float_eq(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -241,7 +238,7 @@ extern "C" { LOG_Z3_mk_fpa_le(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_le(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_le(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -251,7 +248,7 @@ extern "C" { LOG_Z3_mk_fpa_lt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_lt(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_lt(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -261,7 +258,7 @@ extern "C" { LOG_Z3_mk_fpa_ge(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_ge(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_ge(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -271,7 +268,7 @@ extern "C" { LOG_Z3_mk_fpa_gt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_gt(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_gt(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -281,7 +278,7 @@ extern "C" { LOG_Z3_mk_fpa_is_normal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_is_normal(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_is_normal(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -291,7 +288,7 @@ extern "C" { LOG_Z3_mk_fpa_is_subnormal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_is_subnormal(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_is_subnormal(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -301,7 +298,7 @@ extern "C" { LOG_Z3_mk_fpa_is_zero(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_is_zero(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_is_zero(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -311,7 +308,7 @@ extern "C" { LOG_Z3_mk_fpa_is_inf(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_is_inf(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_is_inf(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -321,7 +318,7 @@ extern "C" { LOG_Z3_mk_fpa_is_nan(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_is_nan(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_is_nan(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -331,7 +328,7 @@ extern "C" { LOG_Z3_mk_fpa_min(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_min(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_min(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -341,7 +338,7 @@ extern "C" { LOG_Z3_mk_fpa_max(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_max(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_max(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -350,10 +347,9 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_convert(c, s, rm, t); RESET_ERROR_CODE(); - api::context * ctx = mk_c(c); - float_util fu(ctx->m()); + api::context * ctx = mk_c(c); expr * args [2] = { to_expr(rm), to_expr(t) }; - Z3_ast r = of_ast(ctx->m().mk_app(fu.get_family_id(), OP_TO_FLOAT, + Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_TO_FLOAT, to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(), 2, args)); RETURN_Z3(r); @@ -365,7 +361,7 @@ extern "C" { LOG_Z3_mk_fpa_to_ieee_bv(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(float_util(ctx->m()).mk_to_ieee_bv(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_to_ieee_bv(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index d4a6587bc..6924afff3 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -23,13 +23,15 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"algebraic_numbers.h" +#include"float_decl_plugin.h" bool is_numeral_sort(Z3_context c, Z3_sort ty) { sort * _ty = to_sort(ty); family_id fid = _ty->get_family_id(); if (fid != mk_c(c)->get_arith_fid() && fid != mk_c(c)->get_bv_fid() && - fid != mk_c(c)->get_datalog_fid()) { + fid != mk_c(c)->get_datalog_fid() && + fid != mk_c(c)->get_fpa_fid()) { return false; } return true; @@ -69,7 +71,19 @@ extern "C" { } ++m; } - ast * a = mk_c(c)->mk_numeral_core(rational(n), to_sort(ty)); + ast * a = 0; + sort * _ty = to_sort(ty); + if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) + { + // avoid expanding floats into huge rationals. + float_util & fu = mk_c(c)->float_util(); + scoped_mpf t(fu.fm()); + fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_TOWARD_ZERO, n); + a = fu.mk_value(t); + mk_c(c)->save_ast_trail(a); + } + else + a = mk_c(c)->mk_numeral_core(rational(n), _ty); RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(0); } @@ -131,7 +145,8 @@ extern "C" { expr* e = to_expr(a); return mk_c(c)->autil().is_numeral(e) || - mk_c(c)->bvutil().is_numeral(e); + mk_c(c)->bvutil().is_numeral(e) || + mk_c(c)->float_util().is_value(e); Z3_CATCH_RETURN(Z3_FALSE); } @@ -155,7 +170,7 @@ extern "C" { if (mk_c(c)->datalog_util().is_numeral(e, v)) { r = rational(v, rational::ui64()); return Z3_TRUE; - } + } return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } @@ -172,8 +187,16 @@ extern "C" { return mk_c(c)->mk_external_string(r.to_string()); } else { - SET_ERROR_CODE(Z3_INVALID_ARG); - return ""; + // floats are separated from all others to avoid huge rationals. + float_util & fu = mk_c(c)->float_util(); + scoped_mpf tmp(fu.fm()); + if (mk_c(c)->float_util().is_numeral(to_expr(a), tmp)) { + return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); + } + else { + SET_ERROR_CODE(Z3_INVALID_ARG); + return ""; + } } Z3_CATCH_RETURN(""); } diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index b2927e2c3..367e62666 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1532,7 +1532,9 @@ namespace Microsoft.Z3 { case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); 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_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); } } @@ -1543,7 +1545,9 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj); case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj); 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_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); } return new Expr(ctx, obj); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 6d59cf650..a761c89eb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -194,6 +194,8 @@ typedef enum Z3_DATATYPE_SORT, Z3_RELATION_SORT, Z3_FINITE_DOMAIN_SORT, + Z3_FLOATING_POINT_SORT, + Z3_FLOATING_POINT_ROUNDING_MODE_SORT, Z3_UNKNOWN_SORT = 1000 } Z3_sort_kind; diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index deda7e045..0b8349793 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -201,9 +201,11 @@ public: app * mk_minus_inf(sort * s) { return mk_minus_inf(get_ebits(s), get_sbits(s)); } app * mk_value(mpf const & v) { return m_plugin->mk_value(v); } - bool is_value(expr * n) { return m_plugin->is_value(n); } - bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); } - bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); } + bool is_value(expr * n) const { return m_plugin->is_value(n); } + bool is_numeral(expr * n) const { return is_value(n); } + bool is_value(expr * n, mpf & v) const { return m_plugin->is_value(n, v); } + bool is_numeral(expr * n, mpf & v) const { return is_value(n, v); } + bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); } app * mk_pzero(unsigned ebits, unsigned sbits); app * mk_nzero(unsigned ebits, unsigned sbits);