Bitwuzla initial commit

- Tested in clean chroot
- Tested in action

5 files changed, 228 insertions, 0 deletions

diff --git a/.SRCINFO b/.SRCINFO
new file mode 100644
index 000000000000..e897012e6788
--- /dev/null
+++ b/.SRCINFO
@@ -0,0 +1,50 @@
+pkgbase = bitwuzla
+	pkgdesc = SMT solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations
+	pkgver = 0.4.0
+	pkgrel = 1
+	url = https://bitwuzla.github.io
+	arch = x86_64
+	license = MIT
+	checkdepends = gtest
+	checkdepends = python-pytest
+	makedepends = cadical>=1.5.0
+	makedepends = cmake
+	makedepends = cython
+	makedepends = doxygen
+	makedepends = meson>=0.64
+	makedepends = ninja
+	makedepends = python-breathe
+	makedepends = python-sphinx
+	makedepends = python-sphinx-tabs
+	makedepends = python-sphinx_rtd_theme
+	makedepends = python-sphinxcontrib-bibtex
+	makedepends = python>=3.7
+	makedepends = python-sphinx
+	makedepends = symfpu-cvc5
+	depends = gcc-libs
+	depends = glibc
+	depends = gmp>=6.1
+	depends = kissat
+	optdepends = cryptominisat5: Support for the CryptoMiniSat SAT solver
+	optdepends = python>=3.7: Python bindings
+	provides = bitwuzla.cpython-311-x86_64-linux-gnu.so
+	provides = libbitwuzlabv.so
+	provides = libbitwuzlabb.so
+	provides = libbitwuzlals.so
+	provides = libbitwuzla.so
+	options = !lto
+	source = bitwuzla-0.4.0.tar.gz::https://github.com/bitwuzla/bitwuzla/archive/refs/tags/0.4.0.tar.gz
+	source = 0001-Use-installed-libraries.patch
+	source = 0002-Skip-Test-based-on-timeout.patch
+	source = 0003-Do-not-require-git.patch
+	b2sums = 135ed8dbe8ada22ca36f872ccc062622bfdfa87592cfcad596f9c1c0c92c99a486a7ff52707fe7dba33531405cd6c84a20a3f546d3614585721f6b7468dc2894
+	b2sums = 0ebea6754d4fc270c268d4088af9bcb93596fe5ec7b1065f83d39e5c56eef93d567592443ec0a460a34bf5829b5b54f2c9971644f6fbbebbf9c43a1b440ac54d
+	b2sums = 7728ab77cb234b4427e7cf493817a24bf97440304efb4fc4300125ec470a0bf15430b4416d3c5fdea51dc91441640d05995ed4a08d4c628f97f4d4dc08538d7e
+	b2sums = 7c80c06aec86c5c75a72786cfafa03d703950efa5639726abec5466b82928ae231eed75bff29d056d6e47bf2e4ab1ce4f9634fd96f9454d0b92d90c30fd26f37
+
+pkgname = bitwuzla
+
+pkgname = bitwuzla-doc
+	pkgdesc = Documentation for the Bitwuzla SMT solver
+	arch = any
+	depends = 
diff --git a/0001-Use-installed-libraries.patch b/0001-Use-installed-libraries.patch
new file mode 100644
index 000000000000..dc89c9e60a2b
--- /dev/null
+++ b/0001-Use-installed-libraries.patch
@@ -0,0 +1,45 @@
+diff --unified --recursive --text bitwuzla-0.4.0.orig/src/meson.build bitwuzla-0.4.0/src/meson.build
+--- bitwuzla-0.4.0.orig/src/meson.build	2024-03-06 17:54:03.000000000 +0000
++++ bitwuzla-0.4.0/src/meson.build	2024-03-24 17:48:19.062284270 +0000
+@@ -17,24 +17,25 @@
+ # CaDiCaL does not provide pkg-config to find dependency
+ cadical_dep = cpp_compiler.find_library('cadical',
+                                         has_headers: 'cadical.hpp',
+-                                        static: build_static,
++                                        static: true,
+                                         required: false)
+ if not cadical_dep.found()
+   cadical_dep = dependency('cadical', required: true)
+ endif
+
++kissat_inc = include_directories('/usr/include/kissat')
++
+ # Kissat does not provide pkg-config to find dependency
+ kissat_dep = cpp_compiler.find_library('kissat',
+-                                        has_headers: 'kissat.h',
+-                                        static: build_static,
+-                                        required: false)
++                                       header_include_directories: [kissat_inc],
++                                       has_headers: 'kissat.h',
++                                        required: true)
+ if not kissat_dep.found()
+   kissat_dep = dependency('kissat', required: get_option('kissat'))
+ endif
+
+-# Using system include type suppresses compile warnings originating from the
+-# symfpu headers
+-symfpu_dep = dependency('symfpu', include_type: 'system', required: true)
++symfpu_inc = include_directories('/usr/include/symfpu')
++symfpu_dep = declare_dependency(include_directories: symfpu_inc)
+
+ dependencies = [symfpu_dep, cadical_dep, kissat_dep, gmp_dep]
+
+@@ -210,7 +211,7 @@
+ ])
+
+ # Public header include directory
+-bitwuzla_inc = include_directories('../include', 'lib')
++bitwuzla_inc = include_directories('../include', 'lib', '/usr/include/kissat')
+
+ bitwuzla_lib = library('bitwuzla',
+                       sources,
diff --git a/0002-Skip-Test-based-on-timeout.patch b/0002-Skip-Test-based-on-timeout.patch
new file mode 100644
index 000000000000..46ad057ccd41
--- /dev/null
+++ b/0002-Skip-Test-based-on-timeout.patch
@@ -0,0 +1,12 @@
+diff --unified --recursive --text bitwuzla-0.4.0.orig/test/regress/meson.build bitwuzla-0.4.0/test/regress/meson.build
+--- bitwuzla-0.4.0.orig/test/regress/meson.build	2024-03-06 17:54:03.000000000 +0000
++++ bitwuzla-0.4.0/test/regress/meson.build	2024-03-30 12:48:22.907704008 +0000
+@@ -1393,7 +1393,7 @@
+   ['solver/process_term1.smt2'],
+   ['solver/process_term2.smt2'],
+   ['solver/time_limit_per1.smt2'],
+-  ['solver/time_limit_per2.smt2'],
++#  ['solver/time_limit_per2.smt2'],
+   ['solver/quant/duplicatelemma1.smt2'],
+   ['solver/quant/issue96.smt2'],
+   ['solver/quant/issue97.smt2'],
diff --git a/0003-Do-not-require-git.patch b/0003-Do-not-require-git.patch
new file mode 100644
index 000000000000..a90334cc4af0
--- /dev/null
+++ b/0003-Do-not-require-git.patch
@@ -0,0 +1,12 @@
+diff --unified --recursive --text bitwuzla-0.4.0.orig/src/meson.build bitwuzla-0.4.0/src/meson.build
+--- bitwuzla-0.4.0.orig/src/meson.build	2024-03-30 15:53:33.155005989 +0100
++++ bitwuzla-0.4.0/src/meson.build	2024-03-30 16:18:42.411278668 +0100
+@@ -49,7 +49,7 @@
+ # ---
+ 
+ # Get git information
+-git = find_program('git')
++git = find_program('git', required : false)
+ git_id = ''
+ if git.found()
+   repo = meson.project_source_root()
diff --git a/PKGBUILD b/PKGBUILD
new file mode 100644
index 000000000000..6b77d8561d75
--- /dev/null
+++ b/PKGBUILD
@@ -0,0 +1,109 @@
+# Maintainer: Manuel Wiesinger <m {you know what belongs here} mmap {and here} at>
+
+pkgbase=bitwuzla
+pkgname=("${pkgbase}" "${pkgbase}-doc")
+pkgver=0.4.0
+pkgrel=1
+pkgdesc='SMT solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations'
+arch=('x86_64')
+url='https://bitwuzla.github.io'
+license=('MIT')
+source=("$pkgname-$pkgver.tar.gz::https://github.com/bitwuzla/bitwuzla/archive/refs/tags/${pkgver}.tar.gz"
+	"0001-Use-installed-libraries.patch"
+	"0002-Skip-Test-based-on-timeout.patch"
+	"0003-Do-not-require-git.patch" # git is only used to pull not installed dependencies
+       )
+depends=('gcc-libs' 'glibc' 'gmp>=6.1' 'kissat')
+makedepends=(
+    'cadical>=1.5.0'
+    'cmake'
+    'cython'
+    'doxygen'
+    'meson>=0.64'
+    'ninja'
+    'python-breathe'
+    'python-sphinx'
+    'python-sphinx-tabs'
+    'python-sphinx_rtd_theme'
+    'python-sphinxcontrib-bibtex'
+    'python>=3.7'
+    'python-sphinx'
+    'symfpu-cvc5'
+)
+checkdepends=('gtest' 'python-pytest')
+optdepends=(
+    'cryptominisat5: Support for the CryptoMiniSat SAT solver'
+    'python>=3.7: Python bindings'
+)
+provides=(
+    'bitwuzla.cpython-311-x86_64-linux-gnu.so'
+    'libbitwuzlabv.so'
+    'libbitwuzlabb.so'
+    'libbitwuzlals.so'
+    'libbitwuzla.so')
+b2sums=('135ed8dbe8ada22ca36f872ccc062622bfdfa87592cfcad596f9c1c0c92c99a486a7ff52707fe7dba33531405cd6c84a20a3f546d3614585721f6b7468dc2894'
+        '0ebea6754d4fc270c268d4088af9bcb93596fe5ec7b1065f83d39e5c56eef93d567592443ec0a460a34bf5829b5b54f2c9971644f6fbbebbf9c43a1b440ac54d'
+        '7728ab77cb234b4427e7cf493817a24bf97440304efb4fc4300125ec470a0bf15430b4416d3c5fdea51dc91441640d05995ed4a08d4c628f97f4d4dc08538d7e'
+        '7c80c06aec86c5c75a72786cfafa03d703950efa5639726abec5466b82928ae231eed75bff29d056d6e47bf2e4ab1ce4f9634fd96f9454d0b92d90c30fd26f37')
+options=('!lto')
+
+prepare() {
+    cd "${srcdir}/${pkgname}-${pkgver}"
+    patch --forward --strip=1 --input=../0001-Use-installed-libraries.patch
+    patch --forward --strip=1 --input=../0002-Skip-Test-based-on-timeout.patch
+    patch --forward --strip=1 --input=../0003-Do-not-require-git.patch
+}
+
+build() {
+    cd "${srcdir}/${pkgname}-${pkgver}"
+
+    ./configure.py --prefix /usr --shared --python --testing --docs --kissat
+
+    cd build
+    ninja
+}
+
+check() {
+    cd "${srcdir}/${pkgname}-${pkgver}"
+    meson test -C build
+}
+
+package_bitwuzla() {
+    cd "${srcdir}/${pkgbase}-${pkgver}"
+
+    install -Dm644 COPYING "${pkgdir}/usr/share/licenses/${pkgname}/COPYING"
+    install -Dm644 CONTRIBUTING.md "${pkgdir/}usr/share/doc/${pkgname}/CONTRIBUTING.md"
+
+    install -Dm644 NEWS.md "${pkgdir}/usr/share/doc/${pkgname}/NEWS.md"
+
+    cd build
+
+    DESTDIR="${pkgdir}" ninja install
+}
+
+package_bitwuzla-doc() {
+    pkgdesc="Documentation for the Bitwuzla SMT solver"
+    arch=('any')
+    depends=()
+
+    cd "${srcdir}/${pkgbase}-${pkgver}"
+
+    install -Dm644 COPYING "${pkgdir}/usr/share/licenses/${pkgname}/COPYING"
+    install -Dm644 CONTRIBUTING.md "${pkgdir}/usr/share/doc/${pkgname}/CONTRIBUTING.md"
+
+    cd build/docs
+
+    # Do not copy documentation source files
+    find . \
+	 -not -path "./.*" \
+	 -not -path "./_sources*" \
+	 -not -path "./conf.py" \
+	 -not -path "./cli_usage.txt" \
+	 -not -path "./c/xml*" \
+	 -not -path "./c/Doxyfile" \
+	 -not -path "./cpp/xml*" \
+	 -not -path "./cpp/Doxyfile" \
+	 -exec install -Dm644 {} "${pkgdir}/usr/share/doc/${pkgbase}/html/{}" \;
+
+    install -Dm644 cli_usage.txt "${pkgdir}/usr/share/doc/${pkgbase}/cli_usage.txt"
+}