diff --git a/CMakeLists.txt b/CMakeLists.txt index 34d2c689d..9877af89e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -205,9 +205,6 @@ message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}") include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake) detect_target_architecture(TARGET_ARCHITECTURE) message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}") -if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_") -endif() ################################################################################ diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ad643c9ba..023158573 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2706,7 +2706,7 @@ def mk_config(): 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) @@ -2731,7 +2731,7 @@ def mk_config(): extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) @@ -2853,7 +2853,6 @@ def mk_config(): if is64(): if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): CXXFLAGS = '%s -fPIC' % CXXFLAGS - CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS if sysname == 'Linux': CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS elif not LINUX_X64: diff --git a/scripts/update_api.py b/scripts/update_api.py index 13f1aaf9c..161c783e8 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -584,7 +584,7 @@ def mk_java(java_dir, package_name): java_wrapper.write('extern "C" {\n') java_wrapper.write('#endif\n\n') java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n') - java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') + java_wrapper.write('#if defined(__LP64__) || defined(_WIN64)\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 302b3d5bd..c2d73ffb1 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -39,8 +39,7 @@ add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP}) target_link_libraries(z3java PRIVATE libz3) # FIXME: # Not sure if using all the flags used by the Z3 components is really necessary -# here. At the bare minimum setting _AMD64_ depending on the target is -# necessary but seeing as the Python build system uses all the flags used for building +# here. The Python build system uses all the flags used for building # Z3's components to build ``Native.cpp`` lets do the same for now. target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 3cbd3015b..31a4bba72 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -111,7 +111,7 @@ namespace sat { clause_offset clause::get_new_offset() const { unsigned o1 = m_lits[0].index(); -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(__LP64__) || defined(_WIN64) if (sizeof(clause_offset) == 8) { unsigned o2 = m_lits[1].index(); return (clause_offset)o1 + (((clause_offset)o2) << 32); @@ -122,7 +122,7 @@ namespace sat { void clause::set_new_offset(clause_offset offset) { m_lits[0] = to_literal(static_cast(offset)); -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(__LP64__) || defined(_WIN64) if (sizeof(offset) == 8) { m_lits[1] = to_literal(static_cast(offset >> 32)); } diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 3b97d4462..b036628b1 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -60,7 +60,7 @@ void error(const char * msg) { void display_usage() { std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER; std::cout << " - "; -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) std::cout << "64"; #else std::cout << "32"; @@ -161,7 +161,7 @@ void parse_cmd_line_args(int argc, char ** argv) { if (strcmp(opt_name, "version") == 0) { std::cout << "Z3 version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER; std::cout << " - "; -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) std::cout << "64"; #else std::cout << "32"; diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 778e93021..f95e1c571 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -21,7 +21,7 @@ Revision History: namespace smt { #define DEFAULT_WATCH_LIST_SIZE (sizeof(clause *) * 4) -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) // make sure data is aligned in 64 bit machines #define HEADER_SIZE (4 * sizeof(unsigned)) #else @@ -38,7 +38,7 @@ namespace smt { if (m_data == nullptr) { unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned * mem = reinterpret_cast(alloc_svect(char, size)); -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) ++mem; // make sure data is aligned in 64 bit machines #endif *mem = 0; @@ -61,7 +61,7 @@ namespace smt { unsigned new_capacity = (((curr_capacity * 3 + sizeof(clause *)) >> 1)+3)&~3U; unsigned * mem = reinterpret_cast(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) ++mem; // make sure data is aligned in 64 bit machines #endif *mem = curr_end_cls; diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index e6393adbd..4a7a0b7e4 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -61,7 +61,7 @@ hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) { #ifdef _WINDOWS -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(_WIN64) // Precision control is not supported on x64. // See: http://msdn.microsoft.com/en-us/library/e9b52ceh(VS.110).aspx // CMW: I think this is okay though, the compiler will chose the right instructions @@ -557,7 +557,7 @@ void hwf_manager::mk_ninf(hwf & o) { } #ifdef _WINDOWS -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(_WIN64) #ifdef USE_INTRINSICS #define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) #else diff --git a/src/util/machine.h b/src/util/machine.h index 70baee41e..1ccff6330 100644 --- a/src/util/machine.h +++ b/src/util/machine.h @@ -20,7 +20,7 @@ Revision History: #ifndef MACHINE_H_ #define MACHINE_H_ -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) #define PTR_ALIGNMENT 3 #else #define PTR_ALIGNMENT 2 diff --git a/src/util/mpn.h b/src/util/mpn.h index ea20fc42b..bae972b0c 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -61,7 +61,7 @@ public: char * to_string(mpn_digit const * a, size_t lng, char * buf, size_t lbuf) const; private: - #ifdef _AMD64_ + #if defined(__LP64__) || defined(_WIN64) class mpn_sbuffer : public sbuffer { public: mpn_sbuffer() : sbuffer() {} diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index af95e1a2a..0d3a6040d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -56,7 +56,7 @@ Revision History: #define _trailing_zeros32(X) _tzcnt_u32(X) #endif -#if defined(_AMD64_) +#if defined(__LP64__) || defined(_WIN64) #if defined(__GNUC__) #define _trailing_zeros64(X) __builtin_ctzll(X) #else diff --git a/src/util/symbol.h b/src/util/symbol.h index 40844cf3b..90a4eeb38 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -56,7 +56,7 @@ public: explicit symbol(char const * d); explicit symbol(unsigned idx): m_data(BOXTAGINT(char const *, idx, 1)) { -#ifndef _AMD64_ +#if !defined(__LP64__) && !defined(_WIN64) SASSERT(idx < (SIZE_MAX >> PTR_ALIGNMENT)); #endif }