mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-01-23 17:04:18 +00:00
parent 724e04174e 3d91510565
commit 3bf3de17e9
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_fpa.cpp
View file

@ -269,9 +269,9 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(Z3_context c, Z3_bool sgn, unsigned sig, signed exp, Z3_sort ty) {
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, Z3_bool sgn, signed exp, unsigned sig, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->fpautil().fm());
@ -284,9 +284,9 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(Z3_context c, Z3_bool sgn, __uint64 sig, __int64 exp, Z3_sort ty) {
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, __int64 exp, __uint64 sig, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->fpautil().fm());

8
src/api/z3_fpa.h
View file

@ -337,9 +337,9 @@ extern "C" {
\sa Z3_mk_numeral
def_API('Z3_mk_fpa_numeral_uint_int', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(INT), _in(SORT)))
def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
*/
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);
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(__in Z3_context c, __in Z3_bool sgn, __in signed exp, __in unsigned sig, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
@ -354,9 +354,9 @@ extern "C" {
\sa Z3_mk_numeral
def_API('Z3_mk_fpa_numeral_uint64_int64', AST, (_in(CONTEXT), _in(BOOL), _in(UINT64), _in(INT64), _in(SORT)))
def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
*/
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);
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(__in Z3_context c, __in Z3_bool sgn, __in __int64 exp, __in __uint64 sig, Z3_sort ty);
/**
\brief Floating-point absolute value