Upgrade CVC5 to 1.0.8

This includes several fixes that we previously needed patches for, so we can
delete several hacks in the `patches/` subdirectory. Moreover, this version of
`cvc5` no longer includes `flex` as a dependency, so this fixes #43.

.github/ci.sh

@@ -89,21 +89,13 @@ build_cvc4() {
 
 build_cvc5() {
   pushd repos/cvc5
-  # Work around https://github.com/cvc5/cvc5/issues/9778
-  patch -p1 -i $PATCHES/cvc5-gcc-13-fix.patch
   if $IS_WIN ; then
-    # 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
-    # Fix a Windows-only segfault reported in
-    # https://github.com/cvc5/cvc5/issues/9567. This backports the fix from
-    # https://github.com/cvc5/cvc5/pull/9580.
-    patch -p1 -i $PATCHES/cvc5-upgrade-libpoly.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

.github/workflows/ci.yml

@@ -27,13 +27,13 @@ jobs:
       - name: Install dependencies (Ubuntu)
         run: |
           sudo apt-get update
-          sudo apt-get install libfl-dev gperf automake autoconf lzip ninja-build
+          sudo apt-get install gperf automake autoconf lzip ninja-build
         if: runner.os == 'Linux'
 
       - name: Install dependencies (macOS)
         run: |
           brew update
-          brew install flex gperf automake autoconf ninja gnu-sed
+          brew install 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.
@@ -51,7 +51,6 @@ jobs:
             automake
             curl
             dos2unix
-            flex
             git
             gperf
             lzip
@@ -73,7 +72,7 @@ jobs:
       - name: Install Python libraries
         run: |
           python -m pip install --upgrade pip
-          pip install pyparsing toml
+          pip install pyparsing tomli
 
       - name: Install Java
         uses: actions/setup-java@v3

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.5](https://github.com/cvc5/cvc5/tree/4cb2ab9eb36f64295272a50f61dd1c62903aca4b)
+* CVC5 - [1.0.8](https://github.com/cvc5/cvc5/tree/c8e12cd12b4d1a2b78c29f97ca54b1188557fae0)
 * 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/cvc5-no-ld-gold.patch

@@ -1,22 +1,36 @@
 diff --git a/CMakeLists.txt b/CMakeLists.txt
-index bbd49612a..fb9b416f9 100644
+index aa1dc8a0b..39dbaac7d 100644
 --- a/CMakeLists.txt
 +++ b/CMakeLists.txt
-@@ -229,19 +229,6 @@ if (WIN32)
-   add_check_c_cxx_flag("-Wno-error=unknown-pragmas")
+@@ -233,33 +233,6 @@ if (WIN32)
+   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
  endif ()
 
 -#-----------------------------------------------------------------------------#
--# Use ld.gold if available
+-# Use ld.mold if available, otherwise use ld.gold if available
 -
+-set(USE_EXPLICIT_LINKER_FLAG FALSE)
 -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.")
+-                -fuse-ld=mold
+-                -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_MOLD_VERSION)
+-if ("${LD_MOLD_VERSION}" MATCHES "mold")
+-  set(USE_EXPLICIT_LINKER_FLAG TRUE)
+-  set(EXPLICIT_LINKER_FLAG " -fuse-ld=mold")
+-  message(STATUS "Using mold linker.")
+-else ()
+-  execute_process(COMMAND ${CMAKE_C_COMPILER}
+-                  -fuse-ld=gold
+-                  -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_GOLD_VERSION)
+-  if ("${LD_GOLD_VERSION}" MATCHES "GNU gold")
+-    set(USE_EXPLICIT_LINKER_FLAG TRUE)
+-    set(EXPLICIT_LINKER_FLAG " -fuse-ld=gold")
+-    message(STATUS "Using GNU gold linker.")
+-  endif ()
+-endif ()
+-if (USE_EXPLICIT_LINKER_FLAG)
+-  string(APPEND CMAKE_EXE_LINKER_FLAGS ${EXPLICIT_LINKER_FLAG})
+-  string(APPEND CMAKE_SHARED_LINKER_FLAGS ${EXPLICIT_LINKER_FLAG})
+-  string(APPEND CMAKE_MODULE_LINKER_FLAGS ${EXPLICIT_LINKER_FLAG})
 -endif ()
 -
  #-----------------------------------------------------------------------------#