diff --git a/math/bitwuzla/Makefile b/math/bitwuzla/Makefile index 37ae02bfaa1a..48e9f97db5a1 100644 --- a/math/bitwuzla/Makefile +++ b/math/bitwuzla/Makefile @@ -1,47 +1,49 @@ PORTNAME= bitwuzla # successor of Boolector -DISTVERSION= 0.8.2 +DISTVERSION= 0.9.0 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org COMMENT= SMT solver for the theories of fixed-size bit-vectors WWW= https://bitwuzla.github.io/ \ https://github.com/bitwuzla/bitwuzla LICENSE= MIT LICENSE_FILE= ${WRKSRC}/COPYING BUILD_DEPENDS= gmp>0:math/gmp \ ${LOCALBASE}/lib/symfpu.a:math/symfpu LIB_DEPENDS= libcadical.so:math/cadical \ libcryptominisat5.so:math/cryptominisat \ - libgmp.so:math/gmp + libgmp.so:math/gmp \ + libmpfr.so:math/mpfr TEST_DEPENDS= googletest>0:devel/googletest USES= compiler:c++17-lang localbase:ldflags meson pkgconfig python:build USE_GITHUB= yes USE_LDCONFIG= yes CFLAGS+= -I${LOCALBASE}/include/cadical CXXFLAGS+= -I${LOCALBASE}/include/cadical LDFLAGS+= -lcadical MESON_ARGS= -Ddefault_library=shared \ -Dtesting=disabled BINARY_ALIAS= git=false 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 -# tests as of 0.8.2: -# Ok: 3935 -# Expected Fail: 0 -# Fail: 0 -# Unexpected Pass: 0 -# Skipped: 0 +# tests as of 0.9.0: +# Ok: 4214 +# Expected Fail: 0 +# Fail: 0 +# Unexpected Pass: 0 +# Skipped: 0 +# Timeout: 0 # Timeout: 0 .include diff --git a/math/bitwuzla/distinfo b/math/bitwuzla/distinfo index 2f5d9ee92031..c3583c56387c 100644 --- a/math/bitwuzla/distinfo +++ b/math/bitwuzla/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1762322302 -SHA256 (bitwuzla-bitwuzla-0.8.2_GH0.tar.gz) = 637ed0b8d43291004089543b8c7bb744d325231113cab9bfa07f7bb7a154eeb5 -SIZE (bitwuzla-bitwuzla-0.8.2_GH0.tar.gz) = 2080406 +TIMESTAMP = 1773732799 +SHA256 (bitwuzla-bitwuzla-0.9.0_GH0.tar.gz) = e15420eaaef586c0d02d4b46cf3bdf203ba2511147b0decab99a9df9c9f115ca +SIZE (bitwuzla-bitwuzla-0.9.0_GH0.tar.gz) = 2494794 diff --git a/math/bitwuzla/files/patch-src_meson.build b/math/bitwuzla/files/patch-src_meson.build index 0220847c7c2c..bdb1df0d3d8e 100644 --- a/math/bitwuzla/files/patch-src_meson.build +++ b/math/bitwuzla/files/patch-src_meson.build @@ -1,35 +1,46 @@ ---- src/meson.build.orig 2024-12-13 03:01:05 UTC +--- src/meson.build.orig 2026-03-16 21:34:48 UTC +++ src/meson.build -@@ -15,13 +15,13 @@ gmp_dep = dependency('gmp', +@@ -18,14 +18,14 @@ mpfr_dep = dependency('mpfr', # Subproject dependencies # CaDiCaL does not provide pkg-config to find dependency -cadical_dep = cpp_compiler.find_library('cadical', -- has_headers: 'cadical.hpp', +- has_headers: ['cadical/cadical.hpp', +- 'cadical/tracer.hpp'], - static: build_static, - required: false) -if not cadical_dep.found() -- cadical_dep = dependency('cadical', required: true) +- cadical_dep = dependency('cadical', required: get_option('cadical')) -endif +#cadical_dep = cpp_compiler.find_library('cadical', -+# has_headers: 'cadical.hpp', ++# has_headers: ['cadical/cadical.hpp', ++# 'cadical/tracer.hpp'], +# static: build_static, +# required: false) +#if not cadical_dep.found() -+# cadical_dep = dependency('cadical', required: true) ++# cadical_dep = dependency('cadical', required: get_option('cadical')) +#endif cms_dep = dependency('cryptominisat5', version: '5.11.21', -@@ -39,9 +39,9 @@ endif +@@ -45,15 +45,15 @@ gimsatul_dep = dependency('gimsatul', required: get_op # 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, cms_dep, kissat_dep, gmp_dep] -+dependencies = [cms_dep, kissat_dep, gmp_dep] + dependencies = [ +- gmp_dep, mpfr_dep, symfpu_dep, cadical_dep, cms_dep, kissat_dep, gimsatul_dep] ++ gmp_dep, mpfr_dep, cms_dep, kissat_dep, gimsatul_dep] cpp_args = [] +-if cadical_dep.found() +- cpp_args += ['-DBZLA_USE_CADICAL'] +-endif ++#if cadical_dep.found() ++cpp_args += ['-DBZLA_USE_CADICAL'] ++#endif if cms_dep.found() + cpp_args += ['-DBZLA_USE_CMS'] + endif diff --git a/math/bitwuzla/files/patch-test_unit_meson.build b/math/bitwuzla/files/patch-test_unit_meson.build new file mode 100644 index 000000000000..73d1601ff29c --- /dev/null +++ b/math/bitwuzla/files/patch-test_unit_meson.build @@ -0,0 +1,13 @@ +--- test/unit/meson.build.orig 2026-03-17 07:48:04 UTC ++++ test/unit/meson.build +@@ -147,9 +147,7 @@ cpp_args = ['-fno-access-control', '-DBZLA_ENABLE_UNIT + endif + + cpp_args = ['-fno-access-control', '-DBZLA_ENABLE_UNIT_TESTING'] +-if cadical_dep.found() +- cpp_args += ['-DBZLA_USE_CADICAL'] +-endif ++cpp_args += ['-DBZLA_USE_CADICAL'] + if cms_dep.found() + cpp_args += ['-DBZLA_USE_CMS'] + endif diff --git a/math/bitwuzla/pkg-plist b/math/bitwuzla/pkg-plist index 87fbadc37939..f9af9c3aa1ec 100644 --- a/math/bitwuzla/pkg-plist +++ b/math/bitwuzla/pkg-plist @@ -1,13 +1,16 @@ bin/bitwuzla include/bitwuzla/c/bitwuzla.h include/bitwuzla/c/parser.h include/bitwuzla/cpp/bitwuzla.h include/bitwuzla/cpp/parser.h +include/bitwuzla/cpp/sat_solver.h +include/bitwuzla/cpp/terminator.h include/bitwuzla/enums.h include/bitwuzla/option.h +include/bitwuzla/result.h lib/libbitwuzla.so lib/libbitwuzla.so.0 lib/libbitwuzlabb.so lib/libbitwuzlabv.so lib/libbitwuzlals.so libdata/pkgconfig/bitwuzla.pc