From 573ec293dc0fc6d9dc9408c832b62f55b4bfd909 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 19:09:41 +0100 Subject: [PATCH] FPA: Added core C API. Signed-off-by: Christoph M. Wintersteiger --- src/api/api_fpa.cpp | 253 +++++++++++++++++++++++++++++++++++- src/api/z3_fpa.h | 220 ++++++++++++++++++++++++++++++- src/ast/float_decl_plugin.h | 3 +- 3 files changed, 469 insertions(+), 7 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 8e8493d63..74030a0b0 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -33,7 +33,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(__in Z3_context c) + Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); @@ -44,7 +44,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(__in Z3_context c) + Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); @@ -55,7 +55,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c) + Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); @@ -66,7 +66,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c) + Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); @@ -77,7 +77,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c) + Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); @@ -102,6 +102,249 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + LOG_Z3_mk_fpa_leq(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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + LOG_Z3_mk_fpa_geq(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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_is_inf(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + 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))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_convert(Z3_context c, Z3_sort s, Z3_ast rm, Z3_ast t) { + 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()); + 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, + to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(), + 2, args)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } }; diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index a3e61931b..c9feb0778 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -65,7 +65,6 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c); - /** \brief Create a floating point sort. @@ -74,7 +73,226 @@ extern "C" { \remark ebits must be larger than 1 and sbits must be larger than 2. */ Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits); + + /** + \brief Create a NaN of sort s. + + def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s); + + /** + \brief Create a floating point infinity of sort s. + + When \c negative is true, -Inf will be generated instead of +Inf. + + def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL))) + */ + Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative); + /** + \brief Floating-point absolute value + + t must have floating point sort. + + def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t); + + /** + \brief Floating-point negation + + t must have floating point sort. + + def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t); + + /** + \brief Floating-point addition + + rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_add(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point subtraction + + rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_sub(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point multiplication + + rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_mul(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point division + + The nodes rm must be of FPA rounding mode sort t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_div(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point fused multiply-add. + + The result is round((t1 * t2) + t3) + + rm must be of FPA rounding mode sort, t1, t2, and t3 must have floating point sort. + + def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_fma(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3); + + /** + \brief Floating-point square root + + rm must be of FPA rounding mode sort, t must have floating point sort. + + def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t); + + /** + \brief Floating-point remainder + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point equality + + Note that this is IEEE 754 equality (as opposed to SMT-LIB =). + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point less-than or equal + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point less-than + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + + /** + \brief Floating-point greater-than or equal + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Floating-point greater-than + + t1 and t2 must have floating point sort. + + def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Predicate indicating whether t is a normal floating point number + + t must have floating point sort. + + def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t); + + /** + \brief Predicate indicating whether t is a subnormal floating point number + + t must have floating point sort. + + def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t); + + /** + \brief Predicate indicating whether t is a floating point number with zero value, i.e., +0 or -0. + + t must have floating point sort. + + def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t); + + /** + \brief Predicate indicating whether t is a floating point number representing +Inf or -Inf + + t must have floating point sort. + + def_API('Z3_mk_fpa_is_inf', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_inf(__in Z3_context c, __in Z3_ast t); + + /** + \brief Predicate indicating whether t is a NaN + + t must have floating point sort. + + def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t); + + /** + \brief Minimum of floating point numbers + + t1, t2 must have floating point sort. + + def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Maximum of floating point numbers + + t1, t2 must have floating point sort. + + def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Conversion of a floating point number to sort s. + + s must be a floating point sort, rm must have rounding mode sort, and t must have floating point sort. + + def_API('Z3_mk_fpa_convert', AST, (_in(CONTEXT),_in(SORT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t); + #ifdef __cplusplus }; #endif // __cplusplus diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index f1b60a91b..deda7e045 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -178,6 +178,7 @@ public: family_id get_fid() const { return m_fid; } family_id get_family_id() const { return m_fid; } arith_util & au() { return m_a_util; } + float_decl_plugin & plugin() { return *m_plugin; } sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); } @@ -211,7 +212,7 @@ public: bool is_nan(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nan(v); } bool is_plus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); } - bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); } + bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); } bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); } 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); }