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<jni.h>\n')
java_wrapper.write('#include<stdlib.h>\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<int>(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<unsigned>(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<Z3_bool> _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 <stdio.h>
#include <stdbool.h>
+#include <stdint.h>
#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<char> 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<int>(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<unsigned>(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<int*>(&(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<unsigned*>(&(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);