diff options
| -rw-r--r-- | cmake/ConfigureCVC4.cmake | 13 | ||||
| -rw-r--r-- | cmake/Toolchain-mingw64.cmake | 23 | ||||
| -rwxr-xr-x | configure.sh | 27 | ||||
| -rwxr-xr-x | contrib/get-win-dependencies | 2 | ||||
| -rw-r--r-- | src/parser/CMakeLists.txt | 10 |
5 files changed, 72 insertions, 3 deletions
diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake index 18061c778..f60e9043e 100644 --- a/cmake/ConfigureCVC4.cmake +++ b/cmake/ConfigureCVC4.cmake @@ -43,7 +43,18 @@ endif() check_include_file(unistd.h HAVE_UNISTD_H) check_include_file_cxx(ext/stdio_filebuf.h HAVE_EXT_STDIO_FILEBUF_H) -check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME) +# For Windows builds check if clock_gettime is available via -lpthread +# (pthread_time.h). +if(CVC4_WINDOWS_BUILD) + set(CMAKE_REQUIRED_FLAGS -pthread) + check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME) + unset(CMAKE_REQUIRED_FLAGS) + if(HAVE_CLOCK_GETTIME) + add_c_cxx_flag(-pthread) + endif() +else() + check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME) +endif() check_symbol_exists(ffs "strings.h" HAVE_FFS) check_symbol_exists(optreset "getopt.h" HAVE_DECL_OPTRESET) check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK) diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake new file mode 100644 index 000000000..85c0622ed --- /dev/null +++ b/cmake/Toolchain-mingw64.cmake @@ -0,0 +1,23 @@ +# Toolchain file for building for Windows from Ubuntu. +# +# Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake + +SET(CMAKE_SYSTEM_NAME Windows) + +set(TOOLCHAIN_PREFIX x86_64-w64-mingw32) + +SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc) +SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++) +SET(CMAKE_RC_COMPILER ${TOOLCHAIN_PREFIX}-windres) + +# Set target environment path +SET(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX}) + +# Adjust the default behaviour of the find_XXX() commands: +# search headers and libraries in the target environment, search +# programs in the host environment +set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) +set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY BOTH) +set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE BOTH) + +set(CVC4_WINDOWS_BUILD TRUE) diff --git a/configure.sh b/configure.sh index 8c41f9c7e..52c280a56 100755 --- a/configure.sh +++ b/configure.sh @@ -19,6 +19,7 @@ General options; --name=STR use custom build directory name --best turn on dependences known to give best performance --gpl permit GPL dependences, if available + --win64 cross-compile for Windows 64 bit Features: @@ -66,6 +67,7 @@ Optional Path to Optional Packages: --cryptominisat-dir=PATH path to top level of cryptominisat source tree --cxxtest-dir=DIR path to CxxTest installation --glpk-dir=PATH path to top level of glpk installation + --gmp-dir=PATH path to top level of GMP installation --lfsc-dir=PATH path to top level of lfsc source tree --symfpu-dir=PATH path to top level of symfpu source tree @@ -112,6 +114,7 @@ debug_symbols=default debug_context_mm=default dumping=default gpl=default +win64=default glpk=default lfsc=default muzzle=default @@ -137,6 +140,7 @@ antlr_dir=default cadical_dir=default cryptominisat_dir=default glpk_dir=default +gmp_dir=default lfsc_dir=default symfpu_dir=default @@ -201,6 +205,9 @@ do --gpl) gpl=ON;; --no-gpl) gpl=OFF;; + --win64) win64=ON;; + --no-win64) win64=OFF;; + --glpk) glpk=ON;; --no-glpk) glpk=OFF;; @@ -281,6 +288,9 @@ do --glpk-dir) die "missing argument to $1 (try -h)" ;; --glpk-dir=*) glpk_dir=${1##*=} ;; + --gmp-dir) die "missing argument to $1 (try -h)" ;; + --gmp-dir=*) gmp_dir=${1##*=} ;; + --lfsc-dir) die "missing argument to $1 (try -h)" ;; --lfsc-dir=*) lfsc_dir=${1##*=} ;; @@ -305,7 +315,8 @@ done cmake_opts="" -[ $buildtype != default ] && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype" +[ $buildtype != default ] \ + && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype" [ $asan != default ] \ && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" \ @@ -331,6 +342,9 @@ cmake_opts="" [ $gpl != default ] \ && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" \ && [ $gpl = ON ] && build_dir="$build_dir-gpl" +[ $win64 != default ] \ + && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" \ + && [ $win64 = ON ] && build_dir="$build_dir-win64" [ $muzzle != default ] \ && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" \ && [ $muzzle = ON ] && build_dir="$build_dir-muzzle" @@ -407,6 +421,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir" [ "$glpk_dir" != default ] \ && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir" +[ "$gmp_dir" != default ] \ + && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir" [ "$lfsc_dir" != default ] \ && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir" [ "$symfpu_dir" != default ] \ @@ -420,12 +436,21 @@ if [ -n "$build_name" ]; then # If a build name is specified just create directory 'build_name' for the # current build. build_dir=$build_name + + # The cmake toolchain can't be changed once it is configured in $build_dir. + # Thus, remove $build_dir and create an empty directory. + [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir" mkdir -p "$build_name" else # If no build name is specified create 'cmake-builds' directory and create # the current build directory. Set symlink 'cmake-builds/build/' to current # build. build_dir="$build_prefix$build_dir" + + # The cmake toolchain can't be changed once it is configured in $build_dir. + # Thus, remove $build_dir and create an empty directory. + [ $win64 = ON ] && [ -e "cmake-build/$build_dir" ] \ + && rm -r "cmake-builds/$build_dir" mkdir -p "cmake-builds/$build_dir" cd cmake-builds || exit 1 [ -e build ] && rm build diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies index 5ca969f6b..f3fbd6cf7 100755 --- a/contrib/get-win-dependencies +++ b/contrib/get-win-dependencies @@ -24,7 +24,7 @@ while getopts ":s" opt; do done if [ -z "$HOST" ]; then - HOST=i686-w64-mingw32 + HOST=x86_64-w64-mingw32 echo "WARNING:" echo "WARNING: Using default HOST value: $HOST" echo "WARNING: You should probably run this script like this:" diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index b18573fe5..6cde56c62 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -95,3 +95,13 @@ target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB) target_link_libraries(cvc4parser cvc4 ${ANTLR_LIBRARIES}) target_include_directories(cvc4parser PRIVATE ${ANTLR_INCLUDE_DIR}) install(TARGETS cvc4parser DESTINATION lib) + +# The generated lexer/parser files define some functions as +# __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of +# unresolved symbols when linking against libcvc4parser. +# -Wl,--export-all-symbols makes sure that all symbols are exported when +# building a DLL. +if(CVC4_WINDOWS_BUILD) + set_target_properties(cvc4parser + PROPERTIES LINK_FLAGS "-Wl,--export-all-symbols") +endif() |