abs_builddir = @abs_builddir@
distdir = @PACKAGE@-@VERSION@
AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
+EXEEXT = @EXEEXT@
SHELL = @SHELL@
LIBTOOL = $(CURRENT_BUILD)/libtool
# 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
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.
[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
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
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 \
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
--- /dev/null
+#!/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 =============================================================================
#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")))
EXTRA_DIST = \
replacements.h \
clock_gettime.c \
- clock_gettime.h
-
+ clock_gettime.h \
+ strtok_r.c \
+ strtok_r.h \
+ ffs.c \
+ ffs.h
#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;
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 */
/* 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,
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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
*/
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");
#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)."
/** 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) {
throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
}
+#endif /* __WIN32__ */
+
set_unexpected(cvc4unexpected);
default_terminator = set_terminate(cvc4terminate);
}
#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"
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);
input->close(input);
}
+#endif /* _WIN32 */
+
}/* extern "C" */
}/* CVC4::parser namespace */
#include "util/dump.h"
#include "smt/modal_exception.h"
#include "smt/smt_engine.h"
+#include "lib/strtok_r.h"
#include <cerrno>
#include <cstring>
#include "options/options.h"
#include "util/statistics_registry.h"
#include "util/dump.h"
+#include "lib/ffs.h"
#include <string>
#include <iostream>
#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
}
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;
d_data += end - d_start;
d_running = false;
}
+#endif /* ! __WIN32__ */
}/* TimerStat::stop() */
RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
};/* class StatisticsRegistry */
+#ifndef __WIN32__
+
/****************************************************************************/
/* Some utility functions for timespec */
/****************************************************************************/
};/* 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
}
};/* 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
projects / cvc5.git / commitdiff