mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity

Refer to macOS rather than Mac OS / OSX.

Browse source
This commit is contained in:
Bruce Mitchener 2018-10-02 17:38:09 +07:00
parent 620c5d1d81
commit a76397d3b8
17 changed files with 33 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CMakeLists.txt
View file

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

6
README.md
View file

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

4
examples/c++/README
View file

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

4
examples/c/README
View file

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

2
examples/java/README
View file

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

4
examples/maxsat/README
View file

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

2
examples/ml/README
View file

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

2
examples/python/example.py
View file

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

4
examples/tptp/README
View file

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

4
src/api/python/README.txt
View file

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

2
src/api/python/setup.py
View file

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

2
src/cmd_context/pdecl.h
View file

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

2
src/math/polynomial/polynomial.cpp
View file

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

2
src/shell/main.cpp
View file

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

12
src/util/hwf.cpp
View file

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

10
src/util/scoped_timer.cpp
View file

@ -27,7 +27,7 @@ Revision History:
// Windows
#include<windows.h>
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
// macOS
#include<mach/mach.h>
#include<mach/clock.h>
#include<sys/time.h>
@ -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<scoped_timer::imp*>(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

2
src/util/stopwatch.h
View file

@ -70,7 +70,7 @@ public:
#undef min
#elif defined(__APPLE__) && defined (__MACH__) // Mac OS X
#elif defined(__APPLE__) && defined (__MACH__) // macOS
#include<mach/mach.h>
#include<mach/clock.h>