From 16a2ad9afd8bed86fc7d5d2f40ca3d48b7fedd07 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 30 Mar 2018 23:06:24 +0700 Subject: [PATCH] Use stdint.h for int64_t / uint64_t in API. Now that we can use stdint.h, we can use it to portably define 64 bit integer types for use in the API. --- scripts/update_api.py | 5 +---- src/api/api_datalog.cpp | 4 ++-- src/api/api_fpa.cpp | 6 +++--- src/api/api_numeral.cpp | 16 +++++++------- src/api/api_stats.cpp | 2 +- src/api/c++/z3++.h | 48 ++++++++++++++++++++--------------------- src/api/z3.h | 1 + src/api/z3_api.h | 36 ++++++++++++------------------- src/api/z3_fpa.h | 6 +++--- src/api/z3_logger.h | 4 ++-- src/api/z3_replayer.cpp | 32 +++++++++++++-------------- src/api/z3_replayer.h | 8 +++---- 12 files changed, 79 insertions(+), 89 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 0a86db18d..8a7b33efd 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -60,7 +60,7 @@ FIRST_OBJ_ID = 100 def is_obj(ty): return ty >= FIRST_OBJ_ID -Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : '__int64', UINT64 : '__uint64', DOUBLE : 'double', +Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double', FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol', PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code' } @@ -577,9 +577,6 @@ def mk_java(java_dir, package_name): java_wrapper = open(java_wrapperf, 'w') pkg_str = package_name.replace('.', '_') java_wrapper.write('// Automatically generated file\n') - java_wrapper.write('#ifdef _CYGWIN\n') - java_wrapper.write('typedef long long __int64;\n') - java_wrapper.write('#endif\n') java_wrapper.write('#include\n') java_wrapper.write('#include\n') java_wrapper.write('#include"z3.h"\n') diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 5e0082f09..ce2373498 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -189,7 +189,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size) { + Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size) { Z3_TRY; LOG_Z3_mk_finite_domain_sort(c, name, size); RESET_ERROR_CODE(); @@ -199,7 +199,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64 * out) { + Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t * out) { Z3_TRY; if (out) { *out = 0; diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 972505ca2..261198354 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -358,7 +358,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, __int64 exp, __uint64 sig, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, int64_t exp, uint64_t sig, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty); RESET_ERROR_CODE(); @@ -1035,7 +1035,7 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n) { + Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n) { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n); RESET_ERROR_CODE(); @@ -1113,7 +1113,7 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased) { + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, Z3_bool biased) { Z3_TRY; LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased); RESET_ERROR_CODE(); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 5aa762a96..ab379c3de 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -116,7 +116,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_API Z3_mk_int64(Z3_context c, long long value, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t value, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_int64(c, value, ty); RESET_ERROR_CODE(); @@ -129,7 +129,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned long long value, Z3_sort ty) { + Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t value, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_unsigned_int64(c, value, ty); RESET_ERROR_CODE(); @@ -262,7 +262,7 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, long long* num, long long* den) { + Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_small(c, a, num, den); @@ -296,7 +296,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return Z3_FALSE; } - long long l; + int64_t l; if (Z3_get_numeral_int64(c, v, &l) && l >= INT_MIN && l <= INT_MAX) { *i = static_cast(l); return Z3_TRUE; @@ -314,7 +314,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return Z3_FALSE; } - unsigned long long l; + uint64_t l; if (Z3_get_numeral_uint64(c, v, &l) && (l <= 0xFFFFFFFF)) { *u = static_cast(l); return Z3_TRUE; @@ -323,7 +323,7 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } - Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned long long* u) { + Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_uint64(c, v, u); @@ -343,7 +343,7 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } - Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, long long* i) { + Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_int64(c, v, i); @@ -362,7 +362,7 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } - Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, long long* num, long long* den) { + Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_rational_int64(c, v, num, den); diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index a92b908dc..2e1dac4de 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -130,7 +130,7 @@ extern "C" { Z3_CATCH_RETURN(0.0); } - __uint64 Z3_API Z3_get_estimated_alloc_size(void) { + uint64_t Z3_API Z3_get_estimated_alloc_size(void) { return memory::get_allocation_size(); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 42467cb22..b3df2d53a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -294,21 +294,21 @@ namespace z3 { expr int_val(int n); expr int_val(unsigned n); - expr int_val(__int64 n); - expr int_val(__uint64 n); + expr int_val(int64_t n); + expr int_val(uint64_t n); expr int_val(char const * n); expr real_val(int n, int d); expr real_val(int n); expr real_val(unsigned n); - expr real_val(__int64 n); - expr real_val(__uint64 n); + expr real_val(int64_t n); + expr real_val(uint64_t n); expr real_val(char const * n); expr bv_val(int n, unsigned sz); expr bv_val(unsigned n, unsigned sz); - expr bv_val(__int64 n, unsigned sz); - expr bv_val(__uint64 n, unsigned sz); + expr bv_val(int64_t n, unsigned sz); + expr bv_val(uint64_t n, unsigned sz); expr bv_val(char const * n, unsigned sz); expr bv_val(unsigned n, bool const* bits); @@ -660,8 +660,8 @@ namespace z3 { small integers, 64 bit integers or rational or decimal strings. */ bool is_numeral() const { return kind() == Z3_NUMERAL_AST; } - bool is_numeral_i64(__int64& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;} - bool is_numeral_u64(__uint64& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral_i64(int64_t& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;} + bool is_numeral_u64(uint64_t& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;} bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;} bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;} bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; } @@ -744,35 +744,35 @@ namespace z3 { } /** - \brief Return __int64 value of numeral, throw if result cannot fit in - __int64 + \brief Return \c int64_t value of numeral, throw if result cannot fit in + \c int64_t. \pre is_numeral() */ - __int64 get_numeral_int64() const { + int64_t get_numeral_int64() const { assert(is_numeral()); - __int64 result = 0; + int64_t result = 0; if (!is_numeral_i64(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - Z3_THROW(exception("numeral does not fit in machine __int64")); + Z3_THROW(exception("numeral does not fit in machine int64_t")); } return result; } /** - \brief Return __uint64 value of numeral, throw if result cannot fit in - __uint64 + \brief Return \c uint64_t value of numeral, throw if result cannot fit in + \c uint64_t. \pre is_numeral() */ - __uint64 get_numeral_uint64() const { + uint64_t get_numeral_uint64() const { assert(is_numeral()); - __uint64 result = 0; + uint64_t result = 0; if (!is_numeral_u64(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - Z3_THROW(exception("numeral does not fit in machine __uint64")); + Z3_THROW(exception("numeral does not fit in machine uint64_t")); } return result; } @@ -2526,21 +2526,21 @@ namespace z3 { inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } - inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } - inline expr context::int_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } + inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } + inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(int n, int d) { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); } inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } - inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } - inline expr context::real_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } + inline expr context::real_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } + inline expr context::real_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::bv_val(int n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); } inline expr context::bv_val(unsigned n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); } - inline expr context::bv_val(__int64 n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); } - inline expr context::bv_val(__uint64 n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); } + inline expr context::bv_val(int64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); } + inline expr context::bv_val(uint64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); } inline expr context::bv_val(char const * n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); } inline expr context::bv_val(unsigned n, bool const* bits) { array _bits(n); diff --git a/src/api/z3.h b/src/api/z3.h index b29f1d6ba..37ea68f84 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -23,6 +23,7 @@ Notes: #include #include +#include #include "z3_macros.h" #include "z3_api.h" #include "z3_ast_containers.h" diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2b46127fa..ac6c39137 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -36,14 +36,6 @@ DEFINE_TYPE(Z3_fixedpoint); DEFINE_TYPE(Z3_optimize); DEFINE_TYPE(Z3_rcf_num); -#ifndef __int64 -#define __int64 long long -#endif - -#ifndef __uint64 -#define __uint64 unsigned long long -#endif - /** \defgroup capi C API */ /*@{*/ @@ -1843,7 +1835,7 @@ extern "C" { def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64))) */ - Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size); + Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size); /** \brief Create an array type. @@ -3200,26 +3192,26 @@ extern "C" { /** \brief Create a numeral of a int, bit-vector, or finite-domain sort. - This function can be used to create numerals that fit in a machine __int64 integer. + This function can be used to create numerals that fit in a machine \c int64_t integer. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. \sa Z3_mk_numeral def_API('Z3_mk_int64', AST, (_in(CONTEXT), _in(INT64), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_int64(Z3_context c, __int64 v, Z3_sort ty); + Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty); /** \brief Create a numeral of a int, bit-vector, or finite-domain sort. - This function can be used to create numerals that fit in a machine __uint64 integer. + This function can be used to create numerals that fit in a machine \c uint64_t integer. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. \sa Z3_mk_numeral def_API('Z3_mk_unsigned_int64', AST, (_in(CONTEXT), _in(UINT64), _in(SORT))) */ - Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty); + Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty); /** \brief create a bit-vector numeral from a vector of Booleans. @@ -3868,7 +3860,7 @@ extern "C" { def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) */ - Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64* r); + Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); /** \brief Return the domain of the given array sort. @@ -4425,7 +4417,7 @@ extern "C" { def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) */ - Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, __int64* num, __int64* den); + Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den); /** \brief Similar to #Z3_get_numeral_string, but only succeeds if @@ -4453,7 +4445,7 @@ extern "C" { /** \brief Similar to #Z3_get_numeral_string, but only succeeds if - the value can fit in a machine __uint64 int. Return Z3_TRUE if the call succeeded. + the value can fit in a machine \c uint64_t int. Return Z3_TRUE if the call succeeded. \pre Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST @@ -4461,11 +4453,11 @@ extern "C" { def_API('Z3_get_numeral_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64))) */ - Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, __uint64* u); + Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u); /** \brief Similar to #Z3_get_numeral_string, but only succeeds if - the value can fit in a machine __int64 int. Return Z3_TRUE if the call succeeded. + the value can fit in a machine \c int64_t int. Return Z3_TRUE if the call succeeded. \pre Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST @@ -4473,11 +4465,11 @@ extern "C" { def_API('Z3_get_numeral_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) */ - Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64* i); + Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i); /** \brief Similar to #Z3_get_numeral_string, but only succeeds if - the value can fit as a rational number as machine __int64 int. Return Z3_TRUE if the call succeeded. + the value can fit as a rational number as machine \c int64_t int. Return Z3_TRUE if the call succeeded. \pre Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST @@ -4485,7 +4477,7 @@ extern "C" { def_API('Z3_get_numeral_rational_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) */ - Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, __int64* num, __int64* den); + Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den); /** \brief Return a lower bound for the given real algebraic number. @@ -6248,7 +6240,7 @@ extern "C" { def_API('Z3_get_estimated_alloc_size', UINT64, ()) */ - __uint64 Z3_API Z3_get_estimated_alloc_size(void); + uint64_t Z3_API Z3_get_estimated_alloc_size(void); /*@}*/ diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 7d237c6e7..f6001e87d 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -349,7 +349,7 @@ extern "C" { 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_int64_uint64(Z3_context c, Z3_bool sgn, __int64 exp, __uint64 sig, Z3_sort ty); + Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, int64_t exp, uint64_t sig, Z3_sort ty); /** \brief Floating-point absolute value @@ -956,7 +956,7 @@ extern "C" { def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64))) */ - Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n); + Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n); /** \brief Return the exponent value of a floating-point numeral as a string. @@ -985,7 +985,7 @@ extern "C" { def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL))) */ - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased); + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, Z3_bool biased); /** \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index dd2816bff..357d79bcb 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -23,8 +23,8 @@ static std::ostream & operator<<(std::ostream & out, ll_escaped const & d); static void __declspec(noinline) R() { *g_z3_log << "R\n"; g_z3_log->flush(); } static void __declspec(noinline) P(void * obj) { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) I(__int64 i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } -static void __declspec(noinline) U(__uint64 u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) I(int64_t i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) U(uint64_t u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } static void __declspec(noinline) D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } static void __declspec(noinline) Sy(Z3_symbol sym) { diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index fde9b1f48..0e8297879 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -40,8 +40,8 @@ struct z3_replayer::imp { int m_line; // line svector m_string; symbol m_id; - __int64 m_int64; - __uint64 m_uint64; + int64_t m_int64; + uint64_t m_uint64; double m_double; float m_float; size_t m_ptr; @@ -85,8 +85,8 @@ struct z3_replayer::imp { struct value { value_kind m_kind; union { - __int64 m_int; - __uint64 m_uint; + int64_t m_int; + uint64_t m_uint; double m_double; char const * m_str; void * m_obj; @@ -95,8 +95,8 @@ struct z3_replayer::imp { value():m_kind(OBJECT), m_int(0) {} value(void * obj):m_kind(OBJECT), m_obj(obj) {} value(value_kind k, char const * str):m_kind(k), m_str(str) {} - value(value_kind k, __uint64 u):m_kind(k), m_uint(u) {} - value(value_kind k, __int64 i):m_kind(k), m_int(i) {} + value(value_kind k, uint64_t u):m_kind(k), m_uint(u) {} + value(value_kind k, int64_t i):m_kind(k), m_int(i) {} value(value_kind k, double d):m_kind(k), m_double(d) {} value(value_kind k, float f):m_kind(k), m_float(f) {} }; @@ -342,7 +342,7 @@ struct z3_replayer::imp { unsigned asz = m_args.size(); if (sz > asz) throw z3_replayer_exception("invalid array size"); - __uint64 aidx; + uint64_t aidx; value_kind nk; for (unsigned i = asz - sz; i < asz; i++) { if (m_args[i].m_kind != k) @@ -400,7 +400,7 @@ struct z3_replayer::imp { #define TICK_FREQUENCY 100000 void parse() { - unsigned long long counter = 0; + uint64_t counter = 0; unsigned tick = 0; while (true) { IF_VERBOSE(1, { @@ -577,7 +577,7 @@ struct z3_replayer::imp { return static_cast(m_args[pos].m_int); } - __int64 get_int64(unsigned pos) const { + int64_t get_int64(unsigned pos) const { check_arg(pos, INT64); return m_args[pos].m_int; } @@ -587,7 +587,7 @@ struct z3_replayer::imp { return static_cast(m_args[pos].m_uint); } - __uint64 get_uint64(unsigned pos) const { + uint64_t get_uint64(unsigned pos) const { check_arg(pos, UINT64); return m_args[pos].m_uint; } @@ -656,7 +656,7 @@ struct z3_replayer::imp { return reinterpret_cast(&(m_args[pos].m_int)); } - __int64 * get_int64_addr(unsigned pos) { + int64_t * get_int64_addr(unsigned pos) { check_arg(pos, INT64); return &(m_args[pos].m_int); } @@ -666,7 +666,7 @@ struct z3_replayer::imp { return reinterpret_cast(&(m_args[pos].m_uint)); } - __uint64 * get_uint64_addr(unsigned pos) { + uint64_t * get_uint64_addr(unsigned pos) { check_arg(pos, UINT64); return &(m_args[pos].m_uint); } @@ -731,11 +731,11 @@ unsigned z3_replayer::get_uint(unsigned pos) const { return m_imp->get_uint(pos); } -__int64 z3_replayer::get_int64(unsigned pos) const { +int64_t z3_replayer::get_int64(unsigned pos) const { return m_imp->get_int64(pos); } -__uint64 z3_replayer::get_uint64(unsigned pos) const { +uint64_t z3_replayer::get_uint64(unsigned pos) const { return m_imp->get_uint64(pos); } @@ -783,7 +783,7 @@ int * z3_replayer::get_int_addr(unsigned pos) { return m_imp->get_int_addr(pos); } -__int64 * z3_replayer::get_int64_addr(unsigned pos) { +int64_t * z3_replayer::get_int64_addr(unsigned pos) { return m_imp->get_int64_addr(pos); } @@ -791,7 +791,7 @@ unsigned * z3_replayer::get_uint_addr(unsigned pos) { return m_imp->get_uint_addr(pos); } -__uint64 * z3_replayer::get_uint64_addr(unsigned pos) { +uint64_t * z3_replayer::get_uint64_addr(unsigned pos) { return m_imp->get_uint64_addr(pos); } diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h index b81659945..8e423cc09 100644 --- a/src/api/z3_replayer.h +++ b/src/api/z3_replayer.h @@ -40,8 +40,8 @@ public: int get_int(unsigned pos) const; unsigned get_uint(unsigned pos) const; - __int64 get_int64(unsigned pos) const; - __uint64 get_uint64(unsigned pos) const; + int64_t get_int64(unsigned pos) const; + uint64_t get_uint64(unsigned pos) const; float get_float(unsigned pos) const; double get_double(unsigned pos) const; bool get_bool(unsigned pos) const; @@ -56,9 +56,9 @@ public: void ** get_obj_array(unsigned pos) const; int * get_int_addr(unsigned pos); - __int64 * get_int64_addr(unsigned pos); + int64_t * get_int64_addr(unsigned pos); unsigned * get_uint_addr(unsigned pos); - __uint64 * get_uint64_addr(unsigned pos); + uint64_t * get_uint64_addr(unsigned pos); Z3_string * get_str_addr(unsigned pos); void ** get_obj_addr(unsigned pos);