Add bitwuzla-0.3.0

.github/ci.sh

@@ -42,6 +42,24 @@ build_abc() {
   cleanup_bins
 }
 
+build_bitwuzla() {
+  pushd repos/bitwuzla
+  if [ "$GITHUB_MATRIX_OS" == 'ubuntu-20.04' ] ; then
+    # Ubuntu 20.04 uses an older version of glibc that is susceptible to
+    # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909, so we must apply a
+    # crude workaround for it. Thankfully, this is not required for the version
+    # of glibc that ships with Ubuntu 22.04.
+    patch -p1 -i $PATCHES/bitwuzla-T58909-workaround.patch
+  fi
+  ./configure.py
+  cd build
+  ninja -j4
+  cp src/main/bitwuzla$EXT $BIN
+  (cd $BIN && ./bitwuzla$EXT --version && deps bitwuzla$EXT && ./bitwuzla$EXT $PROBLEM)
+  popd
+  cleanup_bins
+}
+
 build_boolector() {
   pushd repos/boolector
   if $IS_WIN ; then

.github/workflows/ci.yml

@@ -17,7 +17,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019]
-        solver: [abc, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14]
+        solver: [abc, bitwuzla, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14]
     steps:
       - uses: actions/checkout@v2
         with:
@@ -72,7 +72,7 @@ jobs:
       - name: Install Python libraries
         run: |
           python -m pip install --upgrade pip
-          pip install pyparsing toml tomli
+          pip install meson pyparsing toml tomli
 
       - name: Install Java
         uses: actions/setup-java@v3
@@ -83,11 +83,15 @@ jobs:
       - name: build_solver (non-Windows)
         shell: bash
         run: .github/ci.sh build_${{ matrix.solver }}
+        env:
+          GITHUB_MATRIX_OS: ${{ matrix.os }}
         if: runner.os != 'Windows'
 
       - name: build_solver (Windows)
         shell: msys2 {0}
         run: .github/ci.sh build_${{ matrix.solver }}
+        env:
+          GITHUB_MATRIX_OS: ${{ matrix.os }}
         if: runner.os == 'Windows'
 
       - uses: actions/upload-artifact@v2
@@ -108,6 +112,11 @@ jobs:
           name: "${{ matrix.os }}-${{ runner.arch }}-abc-bin"
           path: bin
 
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-${{ runner.arch }}-bitwuzla-bin"
+          path: bin
+
       - uses: actions/download-artifact@v2
         with:
           name: "${{ matrix.os }}-${{ runner.arch }}-boolector-bin"

.gitmodules

@@ -25,3 +25,6 @@
 [submodule "repos/cvc5"]
 	path = repos/cvc5
 	url = https://github.com/cvc5/cvc5
+[submodule "repos/bitwuzla"]
+	path = repos/bitwuzla
+	url = https://github.com/bitwuzla/bitwuzla

README.md

@@ -10,6 +10,7 @@ Binary distributions can be found at the
 Currently, `what4-solvers` offers the following solver versions:
 
 * ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674)
+* Bitwuzla - [0.3.0](https://github.com/bitwuzla/bitwuzla/tree/2b5a4a867f3717ba1adc325adf8e69577e3cee5c)
 * 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.8](https://github.com/cvc5/cvc5/tree/c8e12cd12b4d1a2b78c29f97ca54b1188557fae0)

patches/bitwuzla-T58909-workaround.patch

@@ -0,0 +1,31 @@
+diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
+index 45238be4..f1ee25cb 100644
+--- a/src/main/time_limit.cpp
++++ b/src/main/time_limit.cpp
+@@ -6,6 +6,7 @@
+ #include <cstdlib>
+ #include <iostream>
+ #include <thread>
++#include <pthread.h>
+
+ namespace bzla::main {
+
+@@ -15,6 +16,18 @@ std::condition_variable cv;
+ std::mutex cv_m;
+ bool time_limit_set = false;
+
++// Work around https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909
++// on old versions of glibc
++void pthread_cond_bug() {
++  pthread_cond_signal((pthread_cond_t *) nullptr);
++  pthread_cond_init((pthread_cond_t *) nullptr,
++                    (const pthread_condattr_t *) nullptr);
++  pthread_cond_destroy((pthread_cond_t *) nullptr);
++  pthread_cond_timedwait((pthread_cond_t *) nullptr, (pthread_mutex_t *)
++                         nullptr, (const struct timespec *) nullptr);
++  pthread_cond_wait((pthread_cond_t *) nullptr, (pthread_mutex_t *) nullptr);
++}
++
+ void
+ timeout_reached()
+ {