diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 6eb7a2e11..1aef9eb1b 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2618,7 +2618,7 @@ void fpa_example() { symbol_y = Z3_mk_string_symbol(ctx, "y"); x = Z3_mk_const(ctx, symbol_x, double_sort); y = Z3_mk_const(ctx, symbol_y, double_sort); - n = Z3_mk_fpa_double(ctx, 42.0, double_sort); + n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort); symbol_q = Z3_mk_string_symbol(ctx, "q"); q = Z3_mk_const(ctx, symbol_q, double_sort); diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 8bcc4c1af..df0dd232a 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -99,7 +99,23 @@ extern "C" { Z3_sort r = of_sort(ctx->float_util().mk_float_sort(ebits, sbits)); RETURN_Z3(r); Z3_CATCH_RETURN(0); - } + } + + Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 5, 11); + } + + Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 8, 24); + } + + Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 11, 53); + } + + Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c) { + return Z3_mk_fpa_sort(c, 15, 113); + } Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) { Z3_TRY; @@ -131,9 +147,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_double(Z3_context c, double v, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty) { Z3_TRY; - LOG_Z3_mk_fpa_double(c, v, ty); + LOG_Z3_mk_fpa_numeral_double(c, v, ty); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->float_util().fm()); @@ -158,7 +174,7 @@ extern "C" { LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_uminus(to_expr(t))); + Z3_ast r = of_ast(ctx->float_util().mk_neg(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -208,7 +224,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(ctx->float_util().mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); + Z3_ast r = of_ast(ctx->float_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b1e60d34f..19f6d582c 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3533,7 +3533,7 @@ namespace Microsoft.Z3 public FPNum MkFP(double v, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_double(this.nCtx, v, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_double(this.nCtx, v, s.NativeObject)); } /// diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 265657bf4..63b489c83 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -23,6 +23,18 @@ Notes: extern "C" { #endif // __cplusplus + /** + \defgroup capi C API + + */ + + /*@{*/ + + /** + @name Floating-Point API + */ + /*@{*/ + /** \brief Create a rounding mode sort. @@ -92,6 +104,59 @@ extern "C" { */ Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits); + /** + \brief Create the half-precision (16-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c); + + /** + \brief Create the single-precision (32-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c); + + /** + \brief Create the double-precision (64-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c); + + /** + \brief Create the quadruple-precision (128-bit) floating point sort. + + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits + + \remark ebits must be larger than 1 and sbits must be larger than 2. + + def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),)) + */ + Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c); + + /** \brief Create a NaN of sort s. @@ -129,7 +194,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative); /** - \brief Create a numeral of floating point sort. + \brief Create a numeral of floating point sort from a double. This function can be use to create numerals that fit in a double value. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. @@ -142,27 +207,9 @@ extern "C" { \sa Z3_mk_numeral - def_API('Z3_mk_fpa_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) + def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty); - - /** - \brief Create a numeral of floating point sort. - - This function can be use to create numerals that fit in a double value. - It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. - - \params c logical context. - \params v value. - \params ty sort. - - ty must be a floating point sort - - \sa Z3_mk_numeral - - def_API('Z3_mk_fpa_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) - */ - Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty); + Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty); /** \brief Floating-point absolute value @@ -468,7 +515,10 @@ extern "C" { def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t); - + + /*@}*/ + /*@}*/ + #ifdef __cplusplus }; #endif // __cplusplus diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 20d8a00e1..de4797f80 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1858,14 +1858,6 @@ void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const result = m.mk_and(m.mk_not(t1), t2); } -void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 1); - expr_ref t1(m), t2(m); - mk_is_nan(args[0], t1); - mk_is_pos(args[0], t2); - result = m.mk_and(m.mk_not(t1), t2); -} - void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; );