mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Added support for FreeBSD

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-18 00:04:53 -08:00 committed by Leonardo de Moura
parent 89c1785b73
commit 1a3eb3a2ed
4 changed files with 56 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
configure.ac
View file

@ -101,15 +101,15 @@ AC_PROG_SED
AS_IF([test "$CXX" = "g++"], [
# Enable OpenMP
CXXFLAGS+=" -fopenmp"
LDFLAGS+=" -fopenmp"
SLIBEXTRAFLAGS+=" -fopenmp"
CXXFLAGS="$CXXFLAGS -fopenmp"
LDFLAGS="$LDFLAGS -fopenmp"
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -fopenmp"
# Use -mfpmath=sse
CXXFLAGS+=" -mfpmath=sse"
CXXFLAGS="$CXXFLAGS -mfpmath=sse"
],
[test "$CXX" = "clang++"], [
# OpenMP is not supported in clang++
CXXFLAGS+=" -D _NO_OMP_"
CXXFLAGS="$CXXFLAGS -D _NO_OMP_"
],
[
AC_MSG_ERROR([Unsupported compiler: $CXX])
@ -128,28 +128,38 @@ host_os=`uname -s`
AS_IF([test "$host_os" = "Darwin"], [
PLATFORM=osx
SO_EXT=.dylib
SLIBFLAGS+="-dynamiclib"
SLIBFLAGS="$SLIBFLAGS -dynamiclib"
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
STATIC_FLAGS=
], [test "$host_os" = "Linux"], [
CXXFLAGS=$CXXFLAGS -D _LINUX_
PLATFORM=linux
SO_EXT=.so
LDFLAGS+=" -lrt"
SLIBFLAGS+=" -shared"
LDFLAGS="$LDFLAGS -lrt"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
STATIC_FLAGS=-static
CXXFLAGS+=" -fno-strict-aliasing"
CXXFLAGS="$CXXFLAGS -fno-strict-aliasing"
if test "$CXX" = "clang++"; then
# More flags for clang++ for Linux
CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
CXXFLAGS="$CXXFLAGS -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
fi
SLIBEXTRAFLAGS+=" -lrt"
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
], [test "$host_os" = "FreeBSD"], [
CXXFLAGS="$CXXFLAGS -D _FREEBSD_"
PLATFORM=bsd
SO_EXT=.so
LDFLAGS="$LDFLAGS -lrt"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
STATIC_FLAGS=-static
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
], [test "${host_os:0:6}" = "CYGWIN"], [
PLATFORM=win
SO_EXT=.dll
SLIBFLAGS+="-shared"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing"
CXXFLAGS="$CXXFLAGS -D_CYGWIN -fno-strict-aliasing"
],
[
AC_MSG_ERROR([Unknown host platform: $host_os])
@ -169,11 +179,11 @@ AC_CHECK_SIZEOF(int *)
if test $ac_cv_sizeof_int_p -eq 8; then
dnl In 64-bit systems we have to compile using -fPIC
CXXFLAGS+=" -fPIC"
CPPFLAGS+=" -D_AMD64_"
CXXFLAGS="$CXXFLAGS -fPIC"
CPPFLAGS="$CPPFLAGS -D_AMD64_"
dnl Only enable use of thread local storage for 64-bit Linux. It is disabled for OSX and 32-bit Linux
if test $PLATFORM = "linux"; then
CPPFLAGS+=" -D_USE_THREAD_LOCAL"
CPPFLAGS="$CPPFLAGS -D_USE_THREAD_LOCAL"
fi
IS_X64="yes"
else

2
src/tactic/fpa/fpa2bv_converter.h
View file

@ -197,4 +197,4 @@ protected:
void convert(model * bv_mdl, model * float_mdl);
};
#endif
#endif

2
src/tactic/fpa/qffpa_tactic.cpp
View file

@ -35,4 +35,4 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m, p), sat_simp_p),
mk_sat_tactic(m, p),
mk_fail_if_undecided_tactic());
}
}

39
src/util/scoped_timer.cpp
View file

@ -33,15 +33,22 @@ Revision History:
#include<sys/time.h>
#include<sys/errno.h>
#include<pthread.h>
#else
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux
#include<csignal>
#include<ctime>
#include<memory.h>
#include"warning.h"
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
#ifdef _LINUX_
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
#else
// FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID
#define CLOCKID CLOCK_PROF
#endif
#define SIG SIGRTMIN
// ---------
#else
// Other platforms
#endif
#include"scoped_timer.h"
@ -63,12 +70,14 @@ struct scoped_timer::imp {
pthread_attr_t m_attributes;
unsigned m_interval;
pthread_cond_t m_condition_var;
#else
// Linux
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
static void * g_timer;
void (*m_old_handler)(int);
void * m_old_timer;
timer_t m_timerid;
#else
// Other
#endif
#if defined(_WINDOWS) || defined(_CYGWIN)
@ -117,10 +126,12 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread condition variable");
return st;
}
#else
#elif defined(_LINUX_)
static void sig_handler(int) {
static_cast<imp*>(g_timer)->m_eh->operator()();
}
#else
// Other
#endif
@ -142,8 +153,8 @@ struct scoped_timer::imp {
throw default_exception("failed to initialize timer thread attributes");
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
throw default_exception("failed to start timer thread");
#else
// Linux version
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
if (omp_in_parallel()) {
// It doesn't work in with more than one thread.
// SIGEV_SIGNAL: the event is handled by the process not by the thread that installed the handler.
@ -172,6 +183,8 @@ struct scoped_timer::imp {
its.it_interval.tv_nsec = 0;
if (timer_settime(m_timerid, 0, &its, NULL) == -1)
throw default_exception("failed to set timer");
#else
// Other platforms
#endif
}
@ -187,14 +200,16 @@ struct scoped_timer::imp {
throw default_exception("failed to join thread");
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
#else
// Linux version
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
if (omp_in_parallel())
return; // see comments in the constructor.
timer_delete(m_timerid);
if (m_old_handler != SIG_ERR)
signal(SIG, m_old_handler);
g_timer = m_old_timer;
#else
// Other Platforms
#endif
}
@ -203,9 +218,11 @@ struct scoped_timer::imp {
#if defined(_WINDOWS) || defined(_CYGWIN)
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
#else
// Linux
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
void * scoped_timer::imp::g_timer = 0;
#else
// Other platforms
#endif
scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {