From 6e849d7f73905d415a9fd4e07970a52baa1972bf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 1 Jan 2015 19:16:02 +0000 Subject: [PATCH] FPA API cosmetics Signed-off-by: Christoph M. Wintersteiger --- src/api/api_fpa.cpp | 8 ++++---- src/api/z3_fpa.h | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 89b278c91..97225f0f3 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -264,7 +264,7 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(Z3_context c, bool sgn, unsigned sig, signed exp, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(Z3_context c, Z3_bool sgn, unsigned sig, signed exp, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty); RESET_ERROR_CODE(); @@ -273,13 +273,13 @@ extern "C" { ctx->float_util().fm().set(tmp, ctx->float_util().get_ebits(to_sort(ty)), ctx->float_util().get_sbits(to_sort(ty)), - sgn, sig, exp); + sgn != 0, sig, exp); Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(Z3_context c, bool sgn, __uint64 sig, __int64 exp, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(Z3_context c, Z3_bool sgn, __uint64 sig, __int64 exp, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty); RESET_ERROR_CODE(); @@ -288,7 +288,7 @@ extern "C" { ctx->float_util().fm().set(tmp, ctx->float_util().get_ebits(to_sort(ty)), ctx->float_util().get_sbits(to_sort(ty)), - sgn, sig, exp); + sgn != 0, sig, exp); Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 48d3e790d..61ee0bd7f 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -344,7 +344,7 @@ extern "C" { def_API('Z3_mk_fpa_numeral_uint_int', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(INT), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(__in Z3_context c, __in bool sgn, __in unsigned sig, __in signed exp, Z3_sort ty); + Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(__in Z3_context c, __in Z3_bool sgn, __in unsigned sig, __in signed exp, Z3_sort ty); /** \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. @@ -360,7 +360,7 @@ extern "C" { def_API('Z3_mk_fpa_numeral_uint64_int64', AST, (_in(CONTEXT), _in(BOOL), _in(UINT64), _in(INT64), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(__in Z3_context c, __in bool sgn, __in __uint64 sig, __in __int64 exp, Z3_sort ty); + Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(__in Z3_context c, __in Z3_bool sgn, __in __uint64 sig, __in __int64 exp, Z3_sort ty); /** \brief Floating-point absolute value