diff options
-rw-r--r-- | Makefile.builds.in | 3 | ||||
-rw-r--r-- | configure.ac | 14 | ||||
-rw-r--r-- | contrib/Makefile.am | 1 | ||||
-rwxr-xr-x | contrib/get-antlr-3.4 | 4 | ||||
-rwxr-xr-x | contrib/win32-build | 95 | ||||
-rw-r--r-- | src/include/cvc4_public.h | 14 | ||||
-rw-r--r-- | src/lib/Makefile.am | 7 | ||||
-rw-r--r-- | src/lib/clock_gettime.c | 23 | ||||
-rw-r--r-- | src/lib/clock_gettime.h | 6 | ||||
-rw-r--r-- | src/lib/ffs.c | 40 | ||||
-rw-r--r-- | src/lib/ffs.h | 42 | ||||
-rw-r--r-- | src/lib/strtok_r.c | 41 | ||||
-rw-r--r-- | src/lib/strtok_r.h | 42 | ||||
-rw-r--r-- | src/main/util.cpp | 20 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.cpp | 17 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 1 | ||||
-rw-r--r-- | src/theory/theory.h | 1 | ||||
-rw-r--r-- | src/util/statistics_registry.cpp | 8 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 22 |
19 files changed, 368 insertions, 33 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in index 6f9c7aaab..9f83ba5dc 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -33,6 +33,7 @@ libdir = @libdir@ abs_builddir = @abs_builddir@ distdir = @PACKAGE@-@VERSION@ AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +EXEEXT = @EXEEXT@ SHELL = @SHELL@ LIBTOOL = $(CURRENT_BUILD)/libtool @@ -79,7 +80,7 @@ am__v_relink_1 = : # all the binaries that might need to be installed # (it's not a fatal error for one/some don't exist in a given build # configuration) -CVC4_BINARIES = cvc4 pcvc4 +CVC4_BINARIES = cvc4$(EXEEXT) pcvc4$(EXEEXT) .PHONY: _default_build_ all examples _default_build_: all diff --git a/configure.ac b/configure.ac index 39672a554..6af7cf97c 100644 --- a/configure.ac +++ b/configure.ac @@ -220,7 +220,8 @@ esac AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111]) # Initialize libtool's configuration options. -_LT_SET_OPTION([LT_INIT],[win32-dll]) +# we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport) +# _LT_SET_OPTION([LT_INIT],[win32-dll]) LT_INIT # Checks for programs. @@ -900,6 +901,12 @@ 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])]) +AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1], + [Defined to 1 if strtok_r() is supported by the platform.])], + [AC_LIBOBJ([strtok_r])]) +AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1], + [Defined to 1 if ffs() is supported by the platform.])], + [AC_LIBOBJ([ffs])]) # Check for the presence of CUDD libraries CVC4_CHECK_CUDD @@ -1117,6 +1124,11 @@ CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" +# visibility flag not supported for Windows builds +case $host_os in + (*mingw*) FLAG_VISIBILITY_HIDDEN= +esac + AC_SUBST(FLAG_VISIBILITY_HIDDEN) # mk_include diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 0d7aa65ce..6f977caec 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -14,6 +14,7 @@ EXTRA_DIST = \ build-cudd-2.4.2-with-libtool.sh \ build-cudd-2.5.0-with-libtool.sh \ mac-build \ + win32-build \ run-script-smtcomp2012 \ theoryskel/kinds \ theoryskel/Makefile \ diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 7928690fa..6c8e5de46 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -49,10 +49,10 @@ cd libantlr3c-3.4 if [ ${MACHINE_TYPE} == 'x86_64' ]; then # 64-bit stuff here - ./configure --enable-64bit --disable-antlrdebug --prefix=`pwd`/../.. + ./configure --enable-64bit --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS else # 32-bit stuff here - ./configure --disable-antlrdebug --prefix=`pwd`/../.. + ./configure --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS fi cp Makefile Makefile.orig diff --git a/contrib/win32-build b/contrib/win32-build new file mode 100755 index 000000000..65e6dd67c --- /dev/null +++ b/contrib/win32-build @@ -0,0 +1,95 @@ +#!/bin/bash +# +# win32-build script +# Morgan Deters <mdeters@cs.nyu.edu> +# Tue, 15 Jan 2013 11:11:24 -0500 +# + +if [ -z "$HOST" ]; then + HOST=i586-mingw32msvc + echo "WARNING:" + echo "WARNING: Using default HOST value: $HOST" + echo "WARNING: You should probably run this script like this:" + echo "WARNING:" + echo "WARNING: HOST=i586-mingw32msvc win32-build" + echo "WARNING:" + echo "WARNING: (replacing the i586-mingw32msvc with your build host)" + echo "WARNING: to ensure the script builds correctly." + echo "WARNING:" +fi + +GMPVERSION=5.1.0 + +if [ $# -ne 0 ]; then + echo "usage: `basename $0`" >&2 + echo >&2 + echo "This script attempts to build CVC4 for Win32 using mingw." >&2 + exit 1 +fi + +function reporterror { + echo + echo ============================================================================= + echo + echo "There was an error setting up the prerequisites. Look above for details." + echo + exit 1 +} + +function webget { + if which wget &>/dev/null; then + wget -c -O "$2" "$1" + elif which curl &>/dev/null; then + curl "$1" >"$2" + else + echo "Can't figure out how to download from web. Please install wget or curl." >&2 + exit 1 + fi +} + +for dir in antlr-3.4 gmp-$GMPVERSION boost-include; do + if [ -e "$dir" ]; then + echo "error: $dir directory exists; please move it out of the way." >&2 + exit 1 + fi +done + +echo ============================================================================= +echo +echo "Setting up ANTLR 3.4..." +echo +MACHINE_TYPE=x86 ANTLR_CONFIGURE_ARGS=--host=$HOST contrib/get-antlr-3.4 | grep -v 'Now configure CVC4 with' | grep -v '\./configure --with-antlr-dir=' +[ ${PIPESTATUS[0]} -eq 0 ] || reporterror +echo +echo ============================================================================= +echo +echo "Setting up GMP $GMPVERSION..." +echo +( set -ex + mkdir gmp-$GMPVERSION + cd gmp-$GMPVERSION + gmpprefix=`pwd` && + mkdir src && + cd src && + webget ftp://ftp.gmplib.org/pub/gmp-$GMPVERSION/gmp-$GMPVERSION.tar.bz2 gmp-$GMPVERSION.tar.bz2 && + tar xfj gmp-$GMPVERSION.tar.bz2 && + cd gmp-$GMPVERSION && + ./configure --host=$HOST --prefix="$gmpprefix" --enable-cxx && + make && + make install +) || exit 1 +echo +echo ============================================================================= +echo +echo "Setting up BOOST includes..." +echo +( mkdir boost-include && + ln -sv /usr/include/boost boost-include/boost ) || exit 1 +echo +echo ============================================================================= +echo +echo 'Now just run:' +echo " ./configure --host=$HOST LDFLAGS=\"-L`pwd`/gmp-$GMPVERSION/lib -L`pwd`/antlr-3.4/lib\" CPPFLAGS=\"-I`pwd`/gmp-$GMPVERSION/include -I`pwd`/antlr-3.4/include -I`pwd`/boost-include\" ANTLR_HOME=\"`pwd`/antlr-3.4\"" +echo ' make' +echo +echo ============================================================================= diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 6c546a147..9993e5f18 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -22,19 +22,7 @@ #include <stdint.h> #if defined _WIN32 || defined __CYGWIN__ -# ifdef BUILDING_DLL -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((__dllexport__)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllexport) -# endif /* __GNUC__ */ -# else /* BUILDING_DLL */ -# ifdef __GNUC__ -# define CVC4_PUBLIC __attribute__((__dllimport__)) -# else /* ! __GNUC__ */ -# define CVC4_PUBLIC __declspec(dllimport) -# endif /* __GNUC__ */ -# endif /* BUILDING_DLL */ +# define CVC4_PUBLIC #else /* !( defined _WIN32 || defined __CYGWIN__ ) */ # if __GNUC__ >= 4 # define CVC4_PUBLIC __attribute__ ((__visibility__("default"))) diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am index a6ea59e95..61f9e2d70 100644 --- a/src/lib/Makefile.am +++ b/src/lib/Makefile.am @@ -15,5 +15,8 @@ libreplacements_la_LIBADD = \ EXTRA_DIST = \ replacements.h \ clock_gettime.c \ - clock_gettime.h - + clock_gettime.h \ + strtok_r.c \ + strtok_r.h \ + ffs.c \ + ffs.h diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c index 77409c71a..e9d347438 100644 --- a/src/lib/clock_gettime.c +++ b/src/lib/clock_gettime.c @@ -18,20 +18,20 @@ #include "cvc4_private.h" -#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__ */ +#if !(defined(__APPLE__) || defined(__WIN32__)) +# warning "This code assumes you're on Mac OS X or Win32, and you don't seem to be. You'll likely have problems." +#endif /* !(__APPLE__ || __WIN32__) */ +#ifdef __APPLE__ + +#include <stdio.h> +#include <errno.h> #include <mach/mach_time.h> static double s_clockconv = 0.0; @@ -64,6 +64,15 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp) { return 0; } +#else /* else we're __WIN32__ */ + +long clock_gettime(clockid_t which_clock, struct timespec *tp) { + // unsupported on Windows + return 0; +} + +#endif /* __APPLE__ / __WIN32__ */ + #ifdef __cplusplus }/* extern "C" */ #endif /* __cplusplus */ diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index ac4ca1f85..ea14f885c 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -30,13 +30,19 @@ /* otherwise, we have to define it */ +#ifndef __WIN32__ + /* get timespec from <time.h> */ #include <time.h> +#endif /* ! __WIN32__ */ + #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ +struct timespec; + typedef enum { CLOCK_REALTIME, CLOCK_MONOTONIC, diff --git a/src/lib/ffs.c b/src/lib/ffs.c new file mode 100644 index 000000000..5c25211ce --- /dev/null +++ b/src/lib/ffs.c @@ -0,0 +1,40 @@ +/********************* */ +/*! \file ffs.c + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for ffs() for systems without it (like Win32) + ** + ** Replacement for ffs() for systems without it (like Win32). + **/ + +#include "cvc4_private.h" + +#include "lib/ffs.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +int ffs(int i) { + long mask = 0x1; + int pos = 1; + while(pos <= sizeof(int) * 8) { + if((mask & i) != 0) { + return pos; + } + ++pos; + mask <<= 1; + } + return 0; +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/ffs.h b/src/lib/ffs.h new file mode 100644 index 000000000..9b038d429 --- /dev/null +++ b/src/lib/ffs.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file ffs.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for ffs() for systems without it (like Win32) + ** + ** Replacement for ffs() for systems without it (like Win32). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LIB__FFS_H +#define __CVC4__LIB__FFS_H + +#ifdef HAVE_FFS + +// available in strings.h +#include <strings.h> + +#else /* ! HAVE_FFS */ + +#include "lib/replacements.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +int ffs(int i); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_FFS */ +#endif /* __CVC4__LIB__FFS_H */ diff --git a/src/lib/strtok_r.c b/src/lib/strtok_r.c new file mode 100644 index 000000000..b8df95359 --- /dev/null +++ b/src/lib/strtok_r.c @@ -0,0 +1,41 @@ +/********************* */ +/*! \file strtok_r.c + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for strtok_r() for systems without it (like Win32) + ** + ** Replacement for strtok_r() for systems without it (like Win32). + **/ + +#include "cvc4_private.h" + +#include "lib/strtok_r.h" +#include <stdio.h> +#include <string.h> + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +char* strtok_r(char *str, const char *delim, char **saveptr) { + if(str == NULL) { + char* retval = strtok(*saveptr, delim); + *saveptr = retval + strlen(retval) + 1; + return retval; + } else { + char* retval = strtok(str, delim); + *saveptr = retval + strlen(retval) + 1; + return retval; + } +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/strtok_r.h b/src/lib/strtok_r.h new file mode 100644 index 000000000..6b3387e6b --- /dev/null +++ b/src/lib/strtok_r.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file strtok_r.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for strtok_r() for systems without it (like Win32) + ** + ** Replacement for strtok_r() for systems without it (like Win32). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LIB__STRTOK_R_H +#define __CVC4__LIB__STRTOK_R_H + +#ifdef HAVE_STRTOK_R + +// available in string.h +#include <string.h> + +#else /* ! HAVE_STRTOK_R */ + +#include "lib/replacements.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +char* strtok_r(char *str, const char *delim, char **saveptr); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_STRTOK_R */ +#endif /* __CVC4__LIB__STRTOK_R_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 5e7436580..9ade23630 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -19,10 +19,15 @@ #include <cerrno> #include <exception> #include <string.h> + +#ifndef __WIN32__ + #include <signal.h> #include <sys/resource.h> #include <unistd.h> +#endif /* __WIN32__ */ + #include "util/exception.h" #include "options/options.h" #include "util/statistics.h" @@ -44,9 +49,6 @@ namespace CVC4 { namespace main { -size_t cvc4StackSize; -void* cvc4StackBase; - /** * If true, will not spin on segfault even when CVC4_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs @@ -54,6 +56,11 @@ void* cvc4StackBase; */ bool segvNoSpin = false; +#ifndef __WIN32__ + +size_t cvc4StackSize; +void* cvc4StackBase; + /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); @@ -144,10 +151,12 @@ void ill_handler(int sig, siginfo_t* info, void*) { #endif /* CVC4_DEBUG */ } +#endif /* __WIN32__ */ + static terminate_handler default_terminator; void cvc4unexpected() { -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && !defined(__WIN32__) fprintf(stderr, "\n" "CVC4 threw an \"unexpected\" exception (one that wasn't properly " "specified\nin the throws() specifier for the throwing function)." @@ -204,6 +213,7 @@ void cvc4terminate() { /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception) { +#ifndef __WIN32__ stack_t ss; ss.ss_sp = malloc(SIGSTKSZ); if(ss.ss_sp == NULL) { @@ -262,6 +272,8 @@ void cvc4_init() throw(Exception) { throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); } +#endif /* __WIN32__ */ + set_unexpected(cvc4unexpected); default_terminator = set_terminate(cvc4terminate); } diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 9f72ac51c..f110b1145 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -18,10 +18,15 @@ #include <stdio.h> #include <stdint.h> +#include <antlr3input.h> + +#ifndef _WIN32 + #include <cerrno> #include <sys/mman.h> #include <sys/stat.h> -#include <antlr3input.h> + +#endif /* _WIN32 */ #include "parser/memory_mapped_input_buffer.h" #include "util/exception.h" @@ -31,6 +36,14 @@ namespace parser { extern "C" { +#ifdef _WIN32 + +pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) { + return 0; +} + +#else /* ! _WIN32 */ + static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename); @@ -112,6 +125,8 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) { input->close(input); } +#endif /* _WIN32 */ + }/* extern "C" */ }/* CVC4::parser namespace */ diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index a3065f29b..a0a6429a8 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -23,6 +23,7 @@ #include "util/dump.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" +#include "lib/strtok_r.h" #include <cerrno> #include <cstring> diff --git a/src/theory/theory.h b/src/theory/theory.h index f317d4b92..e76441f6b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -33,6 +33,7 @@ #include "options/options.h" #include "util/statistics_registry.h" #include "util/dump.h" +#include "lib/ffs.h" #include <string> #include <iostream> diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index b86b557e2..8f9f05031 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -17,7 +17,9 @@ #include "util/statistics_registry.h" #include "expr/expr_manager.h" -#include "lib/clock_gettime.h" +#ifndef __WIN32__ +# include "lib/clock_gettime.h" +#endif /* ! __WIN32__ */ #include "smt/smt_engine.h" #ifndef __BUILDING_STATISTICS_FOR_EXPORT @@ -102,14 +104,17 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { } void TimerStat::start() { +#ifndef __WIN32__ if(__CVC4_USE_STATISTICS) { CheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } +#endif /* ! __WIN32__ */ }/* TimerStat::start() */ void TimerStat::stop() { +#ifndef __WIN32__ if(__CVC4_USE_STATISTICS) { CheckArgument(d_running, *this, "timer not running"); ::timespec end; @@ -117,6 +122,7 @@ void TimerStat::stop() { d_data += end - d_start; d_running = false; } +#endif /* ! __WIN32__ */ }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 3bf990dbb..0a5450b8a 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -612,6 +612,8 @@ public: };/* class StatisticsRegistry */ +#ifndef __WIN32__ + /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ @@ -765,6 +767,25 @@ public: };/* class TimerStat */ +#else /* __WIN32__ */ + +class CodeTimer; + +class TimerStat : public IntStat { +public: + + typedef CVC4::CodeTimer CodeTimer; + + TimerStat(const std::string& name) : + IntStat(name, 0) { + } + + void start(); + void stop(); + +};/* class TimerStat */ + +#endif /* __WIN32__ */ /** * Utility class to make it easier to call stop() at the end of a @@ -788,7 +809,6 @@ public: } };/* class CodeTimer */ - /** * To use a statistic, you need to declare it, initialize it in your * constructor, register it in your constructor, and deregister it in |