mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

FPA API cosmetics

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-01 19:16:02 +00:00
parent 076c709453
commit 6e849d7f73
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_fpa.cpp
View file

@ -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);

4
src/api/z3_fpa.h
View file

@ -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