mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

Use stdint.h for int64_t / uint64_t in API.

Browse source 
Now that we can use stdint.h, we can use it to portably define
64 bit integer types for use in the API.
This commit is contained in:
Bruce Mitchener 2018-03-30 23:06:24 +07:00
parent bb7ad4e938
commit 16a2ad9afd
12 changed files with 79 additions and 89 deletions
Download patch file Download diff file Expand all files Collapse all files

5
scripts/update_api.py
View file

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

4
src/api/api_datalog.cpp
View file

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

6
src/api/api_fpa.cpp
View file

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

16
src/api/api_numeral.cpp
View file

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

2
src/api/api_stats.cpp
View file

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

48
src/api/c++/z3++.h
View file

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

1
src/api/z3.h
View file

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

36
src/api/z3_api.h
View file

@ -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);
/*@}*/

6
src/api/z3_fpa.h
View file

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

4
src/api/z3_logger.h
View file

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

32
src/api/z3_replayer.cpp
View file

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

8
src/api/z3_replayer.h
View file

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