From a76397d3b8174583db90c75f84ab60f8fa0c831f Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 17:38:09 +0700 Subject: [PATCH] Refer to macOS rather than Mac OS / OSX. --- CMakeLists.txt | 2 +- README.md | 6 +++--- examples/c++/README | 4 ++-- examples/c/README | 4 ++-- examples/java/README | 2 +- examples/maxsat/README | 4 ++-- examples/ml/README | 2 +- examples/python/example.py | 2 +- examples/tptp/README | 4 ++-- src/api/python/README.txt | 4 ++-- src/api/python/setup.py | 2 +- src/cmd_context/pdecl.h | 2 +- src/math/polynomial/polynomial.cpp | 2 +- src/shell/main.cpp | 2 +- src/util/hwf.cpp | 12 ++++++------ src/util/scoped_timer.cpp | 10 +++++----- src/util/stopwatch.h | 2 +- 17 files changed, 33 insertions(+), 33 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 28cd9fa33..500b67100 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -240,7 +240,7 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") endif() elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") - # Does OSX really not need any special flags? + # Does macOS really not need any special flags? message(STATUS "Platform: Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") diff --git a/README.md b/README.md index 447034a84..e02719161 100644 --- a/README.md +++ b/README.md @@ -12,8 +12,8 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI | -| ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- | +| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | macOS | TravisCI | +| ----------- | ----------- | ----------- | ---------- | ---------- | ----- | -------- | [![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt @@ -75,7 +75,7 @@ A 32 bit build should work similarly (but is untested); the same is true for 32/ By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix if inferred by the ``mk_make.py`` script. It is usually -``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use +``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and macOS. Use the ``--prefix=`` command line option to change the install prefix. For example: ```bash diff --git a/examples/c++/README b/examples/c++/README index 56775e537..2b3c5affc 100644 --- a/examples/c++/README +++ b/examples/c++/README @@ -5,6 +5,6 @@ in the build directory. This command will create the executable cpp_example. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. \ No newline at end of file +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/examples/c/README b/examples/c/README index 4ca71e0f8..af9dd39f6 100644 --- a/examples/c/README +++ b/examples/c/README @@ -5,7 +5,7 @@ in the build directory. This command will create the executable c_example. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/examples/java/README b/examples/java/README index 1939afc49..d3ff93fe0 100644 --- a/examples/java/README +++ b/examples/java/README @@ -10,5 +10,5 @@ which can be run on Windows via On Linux and FreeBSD, we must use LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample -On OSX, the corresponding option is DYLD_LIBRARY_PATH: +On macOS, the corresponding option is DYLD_LIBRARY_PATH: DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample diff --git a/examples/maxsat/README b/examples/maxsat/README index 6c24da66b..8c7d3b0f7 100644 --- a/examples/maxsat/README +++ b/examples/maxsat/README @@ -5,8 +5,8 @@ in the build directory. This command will create the executable maxsat. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. This directory contains a test file (ex.smt) that can be used as input for the maxsat test application. diff --git a/examples/ml/README b/examples/ml/README index 1c474fe33..9797b85e3 100644 --- a/examples/ml/README +++ b/examples/ml/README @@ -20,4 +20,4 @@ ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml Note that the resulting binaries depend on the shared z3 library (libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH -(Linux), or DYLD_LIBRARY_PATH (OSX). +(Linux), or DYLD_LIBRARY_PATH (macOS). diff --git a/examples/python/example.py b/examples/python/example.py index a17668506..761ae10be 100644 --- a/examples/python/example.py +++ b/examples/python/example.py @@ -20,7 +20,7 @@ # export PYTHONPATH=MYZ3/bin/python # python example.py -# Running this example on OSX: +# Running this example on macOS: # export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin # export PYTHONPATH=MYZ3/bin/python # python example.py diff --git a/examples/tptp/README b/examples/tptp/README index c28a53da4..b3edfe6a8 100644 --- a/examples/tptp/README +++ b/examples/tptp/README @@ -5,9 +5,9 @@ in the build directory. This command will create the executable tptp. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/src/api/python/README.txt b/src/api/python/README.txt index 9831c6fc6..9312b1119 100644 --- a/src/api/python/README.txt +++ b/src/api/python/README.txt @@ -12,8 +12,8 @@ If you are using a 64-bit Python interpreter, you should use msbuild /p:configuration=external /p:platform=x64 -On Linux and OSX, you must install Z3Py, before trying example.py. -To install Z3Py on Linux and OSX, you should execute the following +On Linux and macOS, you must install Z3Py, before trying example.py. +To install Z3Py on Linux and macOS, you should execute the following command in the Z3 root directory sudo make install-z3py diff --git a/src/api/python/setup.py b/src/api/python/setup.py index bce681584..2a750fee6 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -73,7 +73,7 @@ def _build_z3(): if subprocess.call(['nmake'], env=build_env, cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") - else: # linux and osx + else: # linux and macOS if subprocess.call(['make', '-j', str(multiprocessing.cpu_count())], env=build_env, cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 12e6399fe..d994a1e8f 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -53,7 +53,7 @@ public: class psort_inst_cache; #if defined(__APPLE__) && defined(__MACH__) -// CMW: for some unknown reason, llvm on OSX does not like the name `psort' +// CMW: for some unknown reason, llvm on macOS does not like the name `psort' #define psort Z3_psort #endif diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 35a95ce82..24658fdcf 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -100,7 +100,7 @@ namespace polynomial { struct lt_var { bool operator()(power const & p1, power const & p2) { - // CMW: The assertion below does not hold on OSX, because + // CMW: The assertion below does not hold on macOS, because // their implementation of std::sort will try to compare // two items at the same index instead of comparing // the indices directly. I suspect that the purpose of diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 1c8b6908d..3b97d4462 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -91,7 +91,7 @@ void display_usage() { std::cout << " -pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n"; std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; std::cout << "\nResources:\n"; - // timeout and memout are now available on Linux and OSX too. + // timeout and memout are now available on Linux and macOS too. std::cout << " -T:timeout set the timeout (in seconds).\n"; std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n"; std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n"; diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index b8f481329..32b1343e3 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -45,7 +45,7 @@ Revision History: // For SSE2, it is best to use compiler intrinsics because this makes it completely // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects // the x87 FPU, even when /arch:SSE2 is on. -// Luckily, these are kind of standardized, at least for Windows/Linux/OSX. +// Luckily, these are kind of standardized, at least for Windows/Linux/macOS. #ifdef __clang__ #undef USE_INTRINSICS #endif @@ -75,14 +75,14 @@ hwf_manager::hwf_manager() : #endif #endif #else - // OSX/Linux: Nothing. + // macOS/Linux: Nothing. #endif // We only set the precision of the FPU here in the constructor. At the moment, there are no // other parts of the code that could overwrite this, and Windows takes care of context switches. // CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared). - // I have yet to discover whether Linux and OSX save the FPU state when switching context. + // I have yet to discover whether Linux and macOS save the FPU state when switching context. // As long as we stick to using the SSE2 FPU though, there shouldn't be any problems with respect // to the precision (not sure about the rounding modes though). } @@ -279,7 +279,7 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co #endif #endif #else - // Linux, OSX + // Linux, macOS o.value = ::fma(x.value, y.value, z.value); #endif #endif @@ -331,7 +331,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o } #endif #else - // Linux, OSX. + // Linux, macOS. o.value = nearbyint(x.value); #endif } @@ -623,7 +623,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm) UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! } #endif -#else // OSX/Linux +#else // macOS/Linux switch (rm) { case MPF_ROUND_NEAREST_TEVEN: SETRM(FE_TONEAREST); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 8078c46ee..9850699be 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -27,7 +27,7 @@ Revision History: // Windows #include #elif defined(__APPLE__) && defined(__MACH__) -// Mac OS X +// macOS #include #include #include @@ -59,7 +59,7 @@ struct scoped_timer::imp { HANDLE m_timer; bool m_first; #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS pthread_t m_thread_id; pthread_attr_t m_attributes; unsigned m_interval; @@ -89,7 +89,7 @@ struct scoped_timer::imp { } } #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS static void * thread_func(void * arg) { scoped_timer::imp * st = static_cast(arg); @@ -153,7 +153,7 @@ struct scoped_timer::imp { ms, WT_EXECUTEINTIMERTHREAD); #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS m_interval = ms?ms:0xFFFFFFFF; if (pthread_attr_init(&m_attributes) != 0) throw default_exception("failed to initialize timer thread attributes"); @@ -194,7 +194,7 @@ struct scoped_timer::imp { m_timer, INVALID_HANDLE_VALUE); #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS // If the waiting-thread is not up and waiting yet, // we can make sure that it finishes quickly by diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index c606824b4..2c7551df0 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -70,7 +70,7 @@ public: #undef min -#elif defined(__APPLE__) && defined (__MACH__) // Mac OS X +#elif defined(__APPLE__) && defined (__MACH__) // macOS #include #include