Date: Thu, 6 Jun 2024 08:49:07 GMT From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 8a303fe89de3 - main - math/bitwuzla: New port: SMT solver for the theories of fixed-size bit-vectors Message-ID: <202406060849.4568n7Iq002944@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=8a303fe89de3c080262c0de67bed1810f978e8eb commit 8a303fe89de3c080262c0de67bed1810f978e8eb Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2024-06-06 06:17:54 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2024-06-06 08:48:58 +0000 math/bitwuzla: New port: SMT solver for the theories of fixed-size bit-vectors --- math/Makefile | 1 + math/bitwuzla/Makefile | 33 +++++++++++++++++++++++++++++ math/bitwuzla/distinfo | 5 +++++ math/bitwuzla/files/patch-src_meson.build | 35 +++++++++++++++++++++++++++++++ math/bitwuzla/pkg-descr | 4 ++++ math/bitwuzla/pkg-plist | 13 ++++++++++++ 6 files changed, 91 insertions(+) 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202406060849.4568n7Iq002944>