case $ac_option in
-*|*=*) ;;
production|production-*|debug|debug-*|default|default-*|competition|competition-*)
- ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\?'`
+ # regexp `\?' not supported on Mac OS X
+ ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
ac_cvc4_build_profile_set=yes
AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
for x in optimized statistics assertions tracing muzzle coverage profiling; do
- if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then
+ if expr "$ac_option" : '.*-no'$x'-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""'
fi
- if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then
+ if expr "$ac_option" : '.*-'$x'-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-$x\""'
fi
done
- if expr "$ac_option" : '.*-nostaticbinary-\|.*-nostaticbinary$' >/dev/null; then
+ if expr "$ac_option" : '.*-nostaticbinary-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-static-binary\""'
fi
- if expr "$ac_option" : '.*-staticbinary-\|.*-staticbinary$' >/dev/null; then
+ if expr "$ac_option" : '.*-staticbinary-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-static-binary\""'
fi
- if expr "$ac_option" : '.*-nodebugsymbols-\|.*-nodebugsymbols$' >/dev/null; then
+ if expr "$ac_option" : '.*-nodebugsymbols-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-debug-symbols\""'
fi
- if expr "$ac_option" : '.*-debugsymbols-\|.*-debugsymbols$' >/dev/null; then
+ if expr "$ac_option" : '.*-debugsymbols-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""'
fi
for x in cln gmp; do
- if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then
+ if expr "$ac_option" : '.*-no'$x'-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""'
fi
- if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then
+ if expr "$ac_option" : '.*-'$x'-\{0,1\}$' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-$x\""'
fi
done
AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
AC_CONFIG_AUX_DIR([config])
AC_CONFIG_MACRO_DIR([config])
+AC_CONFIG_LIBOBJ_DIR([src/lib])
m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
AC_CHECK_LIB(z, gzread, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])])
AC_CHECK_HEADER(zlib.h, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])])
-AC_CHECK_LIB(rt, clock_gettime, , [AC_MSG_ERROR([can't find clock_gettime() in librt])])
+AC_SEARCH_LIBS([clock_gettime], [rt],
+ [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
+ [Defined to 1 if clock_gettime() is supported by the platform.])],
+ [AC_LIBOBJ([clock_gettime])])
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
#AC_TYPE_SIZE_T
# Check for availability of TLS support (e.g. __thread storage class)
-AC_MSG_CHECKING([whether user wants wants to use compiler-supported TLS])
+AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
AC_MSG_RESULT([yes])
CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
-CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -fexceptions"
LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
AC_SUBST(FLAG_VISIBILITY_HIDDEN)
AC_CONFIG_FILES([
Makefile.builds
Makefile]
- m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,'])
+ m4_esyscmd([find contrib lib src test -name Makefile.am | sort | sed 's,\.am$,,'])
src/util/rational.h
src/util/integer.h
src/util/tls.h
#
LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
-AM_CPPFLAGS =
+AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
-I@srcdir@/include -I@srcdir@ -I@builddir@
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-SUBDIRS = expr util context theory prop smt . parser main
+SUBDIRS = lib expr util context theory prop smt . parser main
lib_LTLIBRARIES = libcvc4.la
@builddir@/prop/libprop.la \
@builddir@/prop/minisat/libminisat.la \
@builddir@/smt/libsmt.la \
- @builddir@/theory/libtheory.la
+ @builddir@/theory/libtheory.la \
+ @builddir@/lib/libreplacements.la
EXTRA_DIST = \
include/cvc4parser_private.h \
# endif /* __GNUC__ >= 4 */
#endif /* defined _WIN32 || defined __CYGWIN__ */
-#define EXPECT_TRUE(x) __builtin_expect( (x), true)
-#define EXPECT_FALSE(x) __builtin_expect( (x), false)
+#define EXPECT_TRUE(x) __builtin_expect( (x), true )
+#define EXPECT_FALSE(x) __builtin_expect( (x), false )
#define NORETURN __attribute__ ((noreturn))
#ifndef NULL
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libreplacements.la
+
+libreplacements_la_SOURCES = empty.c
+libreplacements_la_LIBADD = \
+ $(LTLIBOBJS)
+
+EXTRA_DIST = \
+ replacements.h \
+ clock_gettime.c \
+ clock_gettime.h
+
+# empty.c hack -- need *some* source file so that library make rules are built
+empty.c:; touch empty.c
--- /dev/null
+/********************* */
+/*! \file clock_gettime.c
+ ** \verbatim
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for clock_gettime() for systems without it (like
+ ** Mac OS X)
+ **
+ ** Replacement for clock_gettime() for systems without it (like Mac
+ ** OS X).
+ **/
+
+#include <stdio.h>
+#include <errno.h>
+#include <time.h>
+
+#include "lib/clock_gettime.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+#ifndef __APPLE__
+# warning This code assumes you're on Mac OS X, and you don't seem to be. You'll likely have problems.
+#endif /* __APPLE__ */
+
+#include <mach/mach_time.h>
+
+static double s_clockconv = 0.0;
+
+long clock_gettime(clockid_t which_clock, struct timespec *tp) {
+ if( s_clockconv == 0.0 ) {
+ mach_timebase_info_data_t tb;
+ kern_return_t err = mach_timebase_info(&tb);
+ if(err == 0) {
+ s_clockconv = ((double) tb.numer) / tb.denom;
+ } else {
+ return -EINVAL;
+ }
+ }
+
+ switch(which_clock) {
+ case CLOCK_REALTIME:
+ case CLOCK_REALTIME_HR:
+ case CLOCK_MONOTONIC:
+ case CLOCK_MONOTONIC_HR: {
+ uint64_t t = mach_absolute_time() * s_clockconv;
+ tp->tv_sec = t / 1000000000ul;
+ tp->tv_nsec = t % 1000000000ul;
+ }
+ break;
+ default:
+ return -EINVAL;
+ }
+
+ return 0;
+}
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
--- /dev/null
+/********************* */
+/*! \file clock_gettime.h
+ ** \verbatim
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for clock_gettime() for systems without it (like Mac OS X)
+ **
+ ** Replacement for clock_gettime() for systems without it (like Mac OS X).
+ **/
+
+#ifndef __CVC4__LIB__CLOCK_GETTIME_H
+#define __CVC4__LIB__CLOCK_GETTIME_H
+
+#include "lib/replacements.h"
+
+#ifdef HAVE_CLOCK_GETTIME
+
+/* it should be available from <time.h> */
+#include <time.h>
+
+#else /* HAVE_CLOCK_GETTIME */
+
+/* otherwise, we have to define it */
+
+/* get timespec from <time.h> */
+#include <time.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+typedef enum {
+ CLOCK_REALTIME,
+ CLOCK_MONOTONIC,
+ CLOCK_REALTIME_HR,
+ CLOCK_MONOTONIC_HR
+} clockid_t;
+
+long clock_gettime(clockid_t which_clock, struct timespec *tp);
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#endif /* HAVE_CLOCK_GETTIME */
+#endif /*__CVC4__LIB__CLOCK_GETTIME_H */
+
--- /dev/null
+/********************* */
+/*! \file replacements.h
+ ** \verbatim
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Common header for replacement function sources
+ **
+ ** Common header for replacement function sources.
+ **/
+
+#ifndef __CVC4__LIB__REPLACEMENTS_H
+#define __CVC4__LIB__REPLACEMENTS_H
+
+#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+# include "cvc4_private.h"
+#else
+# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)
+# include "cvc4parser_private.h"
+# else
+# if defined(__BUILDING_CVC4DRIVER)
+# include "cvc4autoconfig.h"
+# else
+# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'.
+# endif
+# endif
+#endif
+
+#endif /* __CVC4__LIB__REPLACEMENTS_H */
AM_CPPFLAGS = \
+ -D__BUILDING_CVC4DRIVER \
-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
cvc4_LDADD = \
../parser/libcvc4parser.la \
- ../libcvc4.la
+ ../libcvc4.la \
+ ../lib/libreplacements.la
if STATIC_BINARY
cvc4_LINK = $(CXXLINK) -all-static
#endif /* CVC4_DEBUG */
}
+/** Handler for SIGILL (illegal instruction). */
+void ill_handler(int sig, siginfo_t* info, void*) {
+#ifdef CVC4_DEBUG
+ fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
+ if(segvNoSpin) {
+ fprintf(stderr, "No-spin requested, aborting...\n");
+ abort();
+ } else {
+ fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+ fprintf(stderr, "Try: gdb %s %u\n", progName, getpid());
+ for(;;) {
+ sleep(60);
+ }
+ }
+#else /* CVC4_DEBUG */
+ fprintf(stderr, "CVC4 executed an illegal instruction.\n");
+ abort();
+#endif /* CVC4_DEBUG */
+}
+
static terminate_handler default_terminator;
void cvc4unexpected() {
act1.sa_sigaction = sigint_handler;
act1.sa_flags = SA_SIGINFO;
sigemptyset(&act1.sa_mask);
- if(sigaction(SIGINT, &act1, NULL))
+ if(sigaction(SIGINT, &act1, NULL)) {
throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
+ }
struct sigaction act2;
act2.sa_sigaction = timeout_handler;
act2.sa_flags = SA_SIGINFO;
sigemptyset(&act2.sa_mask);
- if(sigaction(SIGXCPU, &act2, NULL))
+ if(sigaction(SIGXCPU, &act2, NULL)) {
throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno));
+ }
struct sigaction act3;
act3.sa_sigaction = segv_handler;
act3.sa_flags = SA_SIGINFO;
sigemptyset(&act3.sa_mask);
- if(sigaction(SIGSEGV, &act3, NULL))
+ if(sigaction(SIGSEGV, &act3, NULL)) {
throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+ }
+
+ struct sigaction act4;
+ act4.sa_sigaction = segv_handler;
+ act4.sa_flags = SA_SIGINFO;
+ sigemptyset(&act4.sa_mask);
+ if(sigaction(SIGILL, &act4, NULL)) {
+ throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
+ }
set_unexpected(cvc4unexpected);
default_terminator = set_terminate(cvc4terminate);
libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS)
libcvc4parser_noinst_la_LIBADD = \
@builddir@/smt/libparsersmt.la \
- @builddir@/smt2/libparsersmt2.la \
- @builddir@/cvc/libparsercvc.la
+ @builddir@/smt2/libparsersmt2.la \
+ @builddir@/../lib/libreplacements.la
libcvc4parser_la_SOURCES =
libcvc4parser_noinst_la_SOURCES = \
- antlr_input.h \
- antlr_input.cpp \
+ antlr_input.h \
+ antlr_input.cpp \
antlr_input_imports.cpp \
bounded_token_buffer.h \
bounded_token_buffer.cpp \
input.cpp \
memory_mapped_input_buffer.h \
memory_mapped_input_buffer.cpp \
- parser.h \
- parser.cpp \
- parser_builder.h \
- parser_builder.cpp \
- parser_options.h \
- parser_exception.h
+ parser.h \
+ parser.cpp \
+ parser_builder.h \
+ parser_builder.cpp \
+ parser_options.h \
+ parser_exception.h
#include <ctime>
#include "util/Assert.h"
+#include "lib/clock_gettime.h"
namespace CVC4 {
}
-#ifdef __APPLE__
-
-class TimerStat : public BackedStat< ::timespec > {
- bool d_running;
-
-public:
-
- TimerStat(const std::string& s) :
- BackedStat< ::timespec >(s, ::timespec()),
- d_running(false) {
- }
-
- void start() {
- if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(!d_running);
- d_running = true;
- }
- }
-
- void stop() {
- if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(d_running);
- ++d_data.tv_sec;
- d_running = false;
- }
- }
-};/* class TimerStat */
-
-#else /* __APPLE__ */
-
class TimerStat : public BackedStat< ::timespec > {
// strange: timespec isn't placed in 'std' namespace ?!
::timespec d_start;
}
};/* class TimerStat */
-#endif /* __APPLE__ */
#undef __CVC4_USE_STATISTICS
if HAVE_CXXTESTGEN
AM_CPPFLAGS = \
- -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" \
- "-I@top_srcdir@/src" "-I@top_builddir@/src" \
+ -I. \
+ "-I@CXXTEST@" \
+ "-I@top_srcdir@/src/include" \
+ "-I@top_srcdir@/lib" \
+ "-I@top_srcdir@/src" \
+ "-I@top_builddir@/src" \
"-I@top_srcdir@/src/prop/minisat" \
-D __STDC_LIMIT_MACROS \
-D __STDC_FORMAT_MACROS \
- $(ANTLR_INCLUDES) $(TEST_CPPFLAGS)
+ $(ANTLR_INCLUDES) \
+ $(TEST_CPPFLAGS)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
projects / cvc5.git / commitdiff