math/bitwuzla: New port: SMT solver for the theories of fixed-size bit-vectors

6 files changed, 91 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 370f622f3f81..ebf3004b2fb2 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -189,6 +189,7 @@
     SUBDIR += bcal
     SUBDIR += bcps
     SUBDIR += bitwise
+    SUBDIR += bitwuzla
     SUBDIR += blacs
     SUBDIR += blahtexml
     SUBDIR += blas
diff --git a/math/bitwuzla/Makefile b/math/bitwuzla/Makefile
new file mode 100644
index 000000000000..aecc4a302cd4
--- /dev/null
+++ b/math/bitwuzla/Makefile
@@ -0,0 +1,33 @@
+PORTNAME=	bitwuzla
+DISTVERSION=	0.5.0
+CATEGORIES=	math
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	SMT solver for the theories of fixed-size bit-vectors
+WWW=		https://bitwuzla.github.io/
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/COPYING
+
+BUILD_DEPENDS=	gmp>0:math/gmp \
+		${LOCALBASE}/lib/symfpu.a:math/symfpu
+LIB_DEPENDS=	libcadical.so:math/cadical \
+		libgmp.so:math/gmp
+TEST_DEPENDS=	googletest>0:devel/googletest
+
+USES=		compiler:c++17-lang localbase:ldflags meson pkgconfig python:build
+USE_GITHUB=	yes
+USE_LDCONFIG=	yes
+
+LDFLAGS+=	-lcadical
+
+MESON_ARGS=	-Ddefault_library=shared \
+		-Dtesting=disabled
+
+do-test: # 1 test hangs, see https://github.com/bitwuzla/bitwuzla/issues/117
+	@cd ${WRKSRC} && \
+		${SETENV} ${CONFIGURE_ENV} ${CONFIGURE_CMD} ${CONFIGURE_ARGS} -Dtesting=enabled && \
+		cd ${BUILD_WRKSRC} && \
+		${DO_MAKE_BUILD} test
+
+.include <bsd.port.mk>
diff --git a/math/bitwuzla/distinfo b/math/bitwuzla/distinfo
new file mode 100644
index 000000000000..ea385f26ab87
--- /dev/null
+++ b/math/bitwuzla/distinfo
@@ -0,0 +1,5 @@
+TIMESTAMP = 1717606902
+SHA256 (rel-1.7.4.tar.gz) = 866c8a1332ff1ad5dc7ad403bdef3164420f3f947816b5c9509aad1d18ada7a1
+SIZE (rel-1.7.4.tar.gz) = 647830
+SHA256 (bitwuzla-bitwuzla-0.5.0_GH0.tar.gz) = a477a5973883a8c174ffca8174cd7493a4aae6c95c72397628d395c32226392b
+SIZE (bitwuzla-bitwuzla-0.5.0_GH0.tar.gz) = 2010240
diff --git a/math/bitwuzla/files/patch-src_meson.build b/math/bitwuzla/files/patch-src_meson.build
new file mode 100644
index 000000000000..43c57c11408e
--- /dev/null
+++ b/math/bitwuzla/files/patch-src_meson.build
@@ -0,0 +1,35 @@
+--- src/meson.build.orig	2024-05-29 23:47:56 UTC
++++ src/meson.build
+@@ -15,13 +15,13 @@ gmp_dep = dependency('gmp',
+ # Subproject dependencies
+ 
+ # CaDiCaL does not provide pkg-config to find dependency
+-cadical_dep = cpp_compiler.find_library('cadical',
+-                                        has_headers: 'cadical.hpp',
+-                                        static: build_static,
+-                                        required: false)
+-if not cadical_dep.found()
+-  cadical_dep = dependency('cadical', required: true)
+-endif
++#cadical_dep = cpp_compiler.find_library('cadical',
++#                                        has_headers: 'cadical.hpp',
++#                                        static: build_static,
++#                                        required: false)
++#if not cadical_dep.found()
++#  cadical_dep = dependency('cadical', required: true)
++#endif
+ 
+ # Kissat does not provide pkg-config to find dependency
+ kissat_dep = cpp_compiler.find_library('kissat',
+@@ -34,9 +34,9 @@ endif
+ 
+ # Using system include type suppresses compile warnings originating from the
+ # symfpu headers
+-symfpu_dep = dependency('symfpu', include_type: 'system', required: true)
++#symfpu_dep = dependency('symfpu', include_type: 'system', required: true)
+ 
+-dependencies = [symfpu_dep, cadical_dep, kissat_dep, gmp_dep]
++dependencies = [kissat_dep, gmp_dep]
+ 
+ cpp_args = []
+ if kissat_dep.found()
diff --git a/math/bitwuzla/pkg-descr b/math/bitwuzla/pkg-descr
new file mode 100644
index 000000000000..cc9919ac6f81
--- /dev/null
+++ b/math/bitwuzla/pkg-descr
@@ -0,0 +1,4 @@
+Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of
+fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted
+functions and their combinations. Its name is derived from an Austrian dialect
+expression that can be translated as "someone who tinkers with bits".
diff --git a/math/bitwuzla/pkg-plist b/math/bitwuzla/pkg-plist
new file mode 100644
index 000000000000..87fbadc37939
--- /dev/null
+++ b/math/bitwuzla/pkg-plist
@@ -0,0 +1,13 @@
+bin/bitwuzla
+include/bitwuzla/c/bitwuzla.h
+include/bitwuzla/c/parser.h
+include/bitwuzla/cpp/bitwuzla.h
+include/bitwuzla/cpp/parser.h
+include/bitwuzla/enums.h
+include/bitwuzla/option.h
+lib/libbitwuzla.so
+lib/libbitwuzla.so.0
+lib/libbitwuzlabb.so
+lib/libbitwuzlabv.so
+lib/libbitwuzlals.so
+libdata/pkgconfig/bitwuzla.pc