Build CVC{4,5} natively on Windows

.github/ci.sh

@@ -62,18 +62,25 @@ build_boolector() {
 
 build_cvc4() {
   pushd repos/CVC4-archived
+  ./contrib/get-antlr-3.4
+  ./contrib/get-symfpu
   if $IS_WIN ; then
-    echo "Downloading pre-built CVC4 binary for Windows"
-    curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-win64-opt.exe"
-    cp cvc4$EXT $BIN
+    # Backport changes from https://github.com/cvc5/cvc5/pull/7512 needed to
+    # build CVC4 natively on Windows.
+    patch -p1 -i $PATCHES/cvc4-win64-native.patch
+    # GitHub Actions comes preinstalled with Chocolatey's mingw package, which
+    # includes the ld.gold linker. This does not play nicely with MSYS2's
+    # mingw-w64-x86_64-gcc, so we must prevent CMake from using ld.gold.
+    # (Ideally, there would be a CMake configuration option to accomplish this,
+    # but I have not found one.)
+    patch -p1 -i $PATCHES/cvc4-no-ld-gold.patch
+    ./configure.sh --static --static-binary --symfpu --win64-native production
   else
-    ./contrib/get-antlr-3.4
-    ./contrib/get-symfpu
     ./configure.sh --static --no-static-binary --symfpu production
-    cd build
-    make -j4
-    cp bin/cvc4$EXT $BIN
   fi
+  cd build
+  make -j4
+  cp bin/cvc4$EXT $BIN
   (cd $BIN && ./cvc4$EXT --version && deps cvc4$EXT && ./cvc4$EXT $PROBLEM)
   popd
   cleanup_bins
@@ -82,17 +89,25 @@ build_cvc4() {
 build_cvc5() {
   pushd repos/cvc5
   if $IS_WIN ; then
-    # TODO: Once https://github.com/cvc5/cvc5/pull/7512 lands, build a native
-    # Windows version of CVC5 instead.
-    echo "Downloading pre-built CVC5 binary for Windows"
-    curl -o cvc5$EXT -sL "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.2/cvc5-Win64.exe"
-    cp cvc5$EXT $BIN
+    # Work around https://github.com/cvc5/cvc5/issues/9564
+    patch -p1 -i $PATCHES/cvc5-win64-native.patch
+    # GitHub Actions comes preinstalled with Chocolatey's mingw package, which
+    # includes the ld.gold linker. This does not play nicely with MSYS2's
+    # mingw-w64-x86_64-gcc, so we must prevent CMake from using ld.gold.
+    # (Ideally, there would be a CMake configuration option to accomplish this,
+    # but I have not found one.)
+    patch -p1 -i $PATCHES/cvc5-no-ld-gold.patch
+    # Why do we manually override Python_EXECUTABLE below? GitHub Actions comes
+    # with multiple versions of Python pre-installed, and for some bizarre
+    # reason, CMake always tries to pick the latest version, even if it is not
+    # on the PATH. Manually overriding this option avoids this oddity.
+    ./configure.sh -DPython_EXECUTABLE=${pythonLocation}/python${EXT} --static --static-binary --auto-download --win64-native production
   else
-    ./configure.sh --static --no-static-binary --auto-download production
-    cd build
-    make -j4
-    cp bin/cvc5$EXT $BIN
+    ./configure.sh -DPython_EXECUTABLE=${pythonLocation}/python${EXT} --static --no-static-binary --auto-download production
   fi
+  cd build
+  make -j4
+  cp bin/cvc5$EXT $BIN
   (cd $BIN && ./cvc5$EXT --version && deps cvc5$EXT && ./cvc5$EXT $PROBLEM)
   popd
   cleanup_bins
@@ -180,11 +195,15 @@ build_z3-4.8.14() {
 build_z3() {
   Z3_BIN="z3-$1"
   pushd repos/$Z3_BIN
+  mkdir build
+  cd build
   if $IS_WIN ; then
-    sed -i.bak -e 's/STATIC_BIN=False/STATIC_BIN=True/' scripts/mk_util.py
+    cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_EXE_LINKER_FLAGS:STRING='-static' -GNinja
+  else
+    cmake .. -DCMAKE_BUILD_TYPE=Release -GNinja
   fi
-  python scripts/mk_make.py
-  (cd build && make -j4 && cp z3$EXT $BIN/$Z3_BIN$EXT)
+  ninja -j4
+  cp z3$EXT $BIN/$Z3_BIN$EXT
   popd
   (cd $BIN && ./$Z3_BIN$EXT --version && deps $Z3_BIN$EXT && ./$Z3_BIN$EXT $PROBLEM)
   cleanup_bins

.github/workflows/ci.yml

@@ -27,13 +27,13 @@ jobs:
       - name: Install dependencies (Ubuntu)
         run: |
           sudo apt-get update
-          sudo apt-get install gperf automake autoconf lzip ninja-build
+          sudo apt-get install libfl-dev gperf automake autoconf lzip ninja-build
         if: runner.os == 'Linux'
 
       - name: Install dependencies (macOS)
         run: |
           brew update
-          brew install gperf automake autoconf ninja gnu-sed
+          brew install flex gperf automake autoconf ninja gnu-sed
           # macOS's version of sed lacks the -r option, which CVC5 requires. To
           # work around this, we install put GNU sed before macOS's sed on the
           # PATH.
@@ -45,11 +45,13 @@ jobs:
         with:
           update: true
           msystem: MINGW64
+          path-type: inherit
           install: |
             autoconf
             automake
             curl
             dos2unix
+            flex
             git
             gperf
             lzip
@@ -59,19 +61,25 @@ jobs:
             mingw-w64-x86_64-gcc
             mingw-w64-x86_64-ninja
             patch
-            python
             tar
             unzip
         if: runner.os == 'Windows'
 
-      - uses: actions/setup-python@v2
+      - name: Install Python
+        uses: actions/setup-python@v4
         with:
           python-version: '3.9'
 
-      - uses: BSFishy/pip-action@v1
+      - name: Install Python libraries
+        run: |
+          python -m pip install --upgrade pip
+          pip install pyparsing toml
+
+      - name: Install Java
+        uses: actions/setup-java@v3
         with:
-          packages: |
-            toml
+          distribution: 'temurin'
+          java-version: '17'
 
       - name: build_solver (non-Windows)
         shell: bash

README.md

@@ -12,7 +12,7 @@ Currently, `what4-solvers` offers the following solver versions:
 * ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674)
 * Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3)
 * CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379)
-* CVC5 - [1.0.2](https://github.com/cvc5/cvc5/tree/ef35c1131976e5a3d981dace510d90aed2d11cef)
+* CVC5 - [1.0.5](https://github.com/cvc5/cvc5/tree/4cb2ab9eb36f64295272a50f61dd1c62903aca4b)
 * Yices - [2.6.2](https://github.com/SRI-CSL/yices2/tree/8509cfb5c294df3c0ac3a4814483f39c58879606)
 * Z3 - [4.8.8](https://github.com/Z3Prover/z3/tree/ad55a1f1c617a7f0c3dd735c0780fc758424c7f1) and
        [4.8.14](https://github.com/Z3Prover/z3/tree/df8f9d7dcb8b9f9b3de1072017b7c2b7f63f0af8)

patches/cvc4-no-ld-gold.patch

@@ -0,0 +1,24 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index e4d4aaeda..c604ba989 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -238,19 +238,6 @@ if (WIN32)
+   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
+ endif ()
+
+-#-----------------------------------------------------------------------------#
+-# Use ld.gold if available
+-
+-execute_process(COMMAND ${CMAKE_C_COMPILER}
+-                -fuse-ld=gold
+-                -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
+-if ("${LD_VERSION}" MATCHES "GNU gold")
+-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
+-  message(STATUS "Using GNU gold linker.")
+-endif ()
+-
+ #-----------------------------------------------------------------------------#
+ # Option defaults (three-valued options (cvc4_option(...)))
+ #

patches/cvc4-win64-native.patch

@@ -0,0 +1,82 @@
+diff --git a/configure.sh b/configure.sh
+index 21a444082..8b30c8b14 100755
+--- a/configure.sh
++++ b/configure.sh
+@@ -23,6 +23,7 @@ General options;
+   --best                   turn on dependencies known to give best performance
+   --gpl                    permit GPL dependencies, if available
+   --win64                  cross-compile for Windows 64 bit
++  --win64-native           natively compile for Windows 64 bit
+   --ninja                  use Ninja build system
+
+
+@@ -146,6 +147,7 @@ ubsan=default
+ unit_testing=default
+ valgrind=default
+ win64=default
++win64_native=default
+
+ language_bindings_java=default
+ language_bindings_python=default
+@@ -238,6 +240,9 @@ do
+     --win64) win64=ON;;
+     --no-win64) win64=OFF;;
+
++    --win64-native) win64_native=ON;;
++    --no-win64-native) win64_native=OFF;;
++
+     --ninja) ninja=ON;;
+
+     --glpk) glpk=ON;;
+@@ -387,6 +392,9 @@ cmake_opts=""
+   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
+ [ $win64 != default ] \
+   && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
++# Because 'MSYS Makefiles' has a space in it, we set the variable vs. adding to 'cmake_opts'
++[ $win64_native != default ] \
++  && [ $ninja == default ] && export CMAKE_GENERATOR="MSYS Makefiles"
+ [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
+ [ $muzzle != default ] \
+   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
+diff --git a/src/expr/mkexpr b/src/expr/mkexpr
+index c5f12f487..b47c66753 100755
+--- a/src/expr/mkexpr
++++ b/src/expr/mkexpr
+@@ -14,6 +14,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+
+diff --git a/src/expr/mkkind b/src/expr/mkkind
+index fbf37eff4..aabc70afe 100755
+--- a/src/expr/mkkind
++++ b/src/expr/mkkind
+@@ -13,6 +13,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+
+diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
+index e2a733ec8..e56d076d7 100755
+--- a/src/expr/mkmetakind
++++ b/src/expr/mkmetakind
+@@ -16,6 +16,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+

patches/cvc5-no-ld-gold.patch

@@ -0,0 +1,24 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index bbd49612a..fb9b416f9 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -229,19 +229,6 @@ if (WIN32)
+   add_check_c_cxx_flag("-Wno-error=unknown-pragmas")
+ endif ()
+
+-#-----------------------------------------------------------------------------#
+-# Use ld.gold if available
+-
+-execute_process(COMMAND ${CMAKE_C_COMPILER}
+-                -fuse-ld=gold
+-                -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
+-if ("${LD_VERSION}" MATCHES "GNU gold")
+-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
+-  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
+-  message(STATUS "Using GNU gold linker.")
+-endif ()
+-
+ #-----------------------------------------------------------------------------#
+ # Use interprocedural optimization if requested
+

patches/cvc5-win64-native.patch

@@ -0,0 +1,20 @@
+diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
+index 3ff605948..d9dd4b70d 100644
+--- a/src/parser/CMakeLists.txt
++++ b/src/parser/CMakeLists.txt
+@@ -107,15 +107,6 @@ flex_target(Lexer
+             ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp)
+ set_source_files_properties(${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp PROPERTIES GENERATED TRUE)
+
+-# The FlexLexer.h header is installed to /usr/include/, but is not found by the
+-# cross-compilation environment. As a workaround we'll copy the header to the
+-# current build directory and set the FLEX_INCLUDE_DIRS variable accordingly.
+-if(WIN32)
+-  file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/flex)
+-  file(COPY /usr/include/FlexLexer.h DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/flex)
+-  set(FLEX_INCLUDE_DIRS ${CMAKE_CURRENT_BINARY_DIR}/flex)
+-endif()
+-
+ # We don't want to enable -Wall for code generated by Flex.
+ set(gen_src_files ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp)
+ set(GEN_SRC_FLAGS "")