mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Merge pull request #1861 from waywardmonkeys/macos-naming
Refer to macOS rather than Mac OS / OSX.
This commit is contained in:
commit
cc312d2f68
17 changed files with 33 additions and 33 deletions
|
@ -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
|
||||
|
|
|
@ -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.")
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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";
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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>
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue