From nobody Thu Jun 6 08:49:07 2024 X-Original-To: dev-commits-ports-all@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4Vvyg75Gy1z5M52D; Thu, 06 Jun 2024 08:49:07 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4Vvyg73yvsz4TF9; Thu, 6 Jun 2024 08:49:07 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1717663747; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=h4wXt59BEXDEQ9Z1PnvUYDPz1EcoJcZW5qK4H1kYcww=; b=WevX//IDKT2RBrOI5IIBlvqlxUB8XGkLjDdLnjG6FzS50JCDR7pURfd6wEWe/OHGVfllFj 2vo0o8HieOjHKqs8pByL2AtLSV7U/kvShEDpnWDZSMTUsd4yCson0ODjo6Q7pcACqwrj6+ c9q8OyFaCumEVLzWWMV1AKY6tK2MVg7SIj5LeiTiSUDQCctyEKG9R3wkGmOxN28X2y25Wj cCwZkeapoSrMHeldhzAMZD4RCsOqozf7Pg7kIpqsM0DDVNHLUJcTBycJzzHjCcH8X8XinZ E7/V7SuMAFitRW7u8MU4hv0ziTGFkcvwu0tVBI0JGnAp3rHJ4SL3e+NXJtXRWg== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1717663747; a=rsa-sha256; cv=none; b=OrbGuvU5Gf1XudW4vtbVSXRAjqUOWDzXaFW8Y+b5SCoRvr8qtM0Qc9b4rdOtLEVqSAbsU6 /tWau9OIK0MpB9bv9LW5WaqgWi0lr/vDVxWNd6Ng9ue3JKNgpv/X4H1rvKz5UeFv4SLhdJ QL5IXMcUVQo1HecQjZ4tk2fiBnndztyvZmscxZg8GgFjtkColv0CimZA6juZcJVk16PZny /TdfFgzM+zVOeU+xzo2I/5LNrxhTV322HrNYeQ0jvWP0xu/ATgvzF/dHL195bYg5CEZkQ/ +hZDaoI0EmGPfy54MItlCrjYWYLkUfgEVtQExZt60CGKOtRIolalia0lQkFPMw== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1717663747; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=h4wXt59BEXDEQ9Z1PnvUYDPz1EcoJcZW5qK4H1kYcww=; b=sjICXDRk0VbSbI/NFFJDQQP9Py3NXUaKQ8u/6cTkWvc5ln98NJlNbmqdei2U+FfLb02+pO u3tVu53eddUUSYWXbqbCRURvaxO273P90tSpMnEuemyGt5jsiB0PuQWDkqIb6LL6/w21NY ndToO9aLIbmc0cC21XcRrJfa4klju8YS/qYvFDD2TqBo1a2KKgfq2TzI/0xxMXNCZ+zFzc RdQceUPjqVuSo7/sxgU8OHXh8qh4eAtN0k13VPH5eO/CGkGEcYAwar1R+IQ58CGnfF7eIP 1VFK4uHysVhWZoXq9fu9ngdBB9m/CDp0fP3gG4txwEATsMytG3TV5WBecZXuSw== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4Vvyg73S6wzfXk; Thu, 6 Jun 2024 08:49:07 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.17.1/8.17.1) with ESMTP id 4568n7Ew002947; Thu, 6 Jun 2024 08:49:07 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.17.1/8.17.1/Submit) id 4568n7Iq002944; Thu, 6 Jun 2024 08:49:07 GMT (envelope-from git) Date: Thu, 6 Jun 2024 08:49:07 GMT Message-Id: <202406060849.4568n7Iq002944@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: 8a303fe89de3 - main - math/bitwuzla: New port: SMT solver for the theories of fixed-size bit-vectors List-Id: Commit messages for all branches of the ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-all List-Help: List-Post: List-Subscribe: List-Unsubscribe: X-BeenThere: dev-commits-ports-all@freebsd.org Sender: owner-dev-commits-ports-all@FreeBSD.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 8a303fe89de3c080262c0de67bed1810f978e8eb Auto-Submitted: auto-generated The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=8a303fe89de3c080262c0de67bed1810f978e8eb commit 8a303fe89de3c080262c0de67bed1810f978e8eb Author: Yuri Victorovich AuthorDate: 2024-06-06 06:17:54 +0000 Commit: Yuri Victorovich 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 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