gentoo auto-resync : 11:01:2023 - 05:43:34

3 files changed, 112 insertions, 0 deletions

diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
new file mode 100644
index 000000000000..01c7a42e9bbe
--- /dev/null
+++ b/sci-mathematics/boolector/Manifest
@@ -0,0 +1,3 @@
+DIST boolector-3.2.2_p20220110.tar.gz 1567668 BLAKE2B 6816f0434d88c790a27b9afe4c3b63c18a55b14f9f13b092f2940309e34842fe4868bf8d378bad130c4561d25e7d79b356fc27d9422bd42ba1b74ff98be36f72 SHA512 b1b964c155c8227e631025cf6bff69cf54728b1d875c2bd44a5a1ddb2857de2ab8fefc96d194faa5f98015e730b417d46a415ea601740e890df07ad5e50ad656
+EBUILD boolector-3.2.2_p20220110.ebuild 1791 BLAKE2B cf124ec570c488760e50384cb59131557fb5860729e7204ee84b3f123fe9a4a4ce79df946f4038bc018d25c635abe57ec8d29528e108e4ecb80705ad8beeb8fc SHA512 a8c0c27f80e29f5177bc1026f1598d86f12fd0142d983e8f65a064312d55234ab59213f658dcee9bb9345502201c64c3b813e48dea315471c6d23a0fec68868a
+MISC metadata.xml 1245 BLAKE2B a04e1e5a6af857100b8b569f57f4d2610593e9eb741513e4e6405a8fa9828471b92aaa1ad57a3163dc2f251b5664493692f92477b7191621ff8fd76eed9f57e7 SHA512 81257f7be3b21bf10caad654d5747ef2d978c0df5a05049b890420e2d170b7a4fa06151da0604a8b1b6e7daf2fb01344003c9243205a94b4040c580beb414836
diff --git a/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild
new file mode 100644
index 000000000000..289c5358a5b9
--- /dev/null
+++ b/sci-mathematics/boolector/boolector-3.2.2_p20220110.ebuild
@@ -0,0 +1,77 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+H=13a8a06d561041cafcaf5458e404c1ec354b2841
+PYTHON_COMPAT=( python3_{8..11} )
+
+inherit python-single-r1 cmake
+
+DESCRIPTION="Fast SMT solver for bit-vectors, arrays and uninterpreted functions"
+HOMEPAGE="https://boolector.github.io/
+	https://github.com/Boolector/boolector/"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/Boolector/${PN}.git"
+else
+	SRC_URI="https://github.com/Boolector/${PN}/archive/${H}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}"/${PN}-${H}
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="cryptominisat examples +gmp minisat +picosat python test"
+REQUIRED_USE="
+	python? ( ${PYTHON_REQUIRED_USE} )
+	|| ( cryptominisat minisat picosat )
+"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	sci-mathematics/btor2tools:=
+	cryptominisat? ( sci-mathematics/cryptominisat:= )
+	gmp? ( dev-libs/gmp:= )
+	minisat? ( sci-mathematics/minisat:= )
+	picosat? ( sci-mathematics/picosat:= )
+	python? ( ${PYTHON_DEPS} )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="test? ( dev-cpp/gtest )"
+
+pkg_setup() {
+	use python && python-single-r1_pkg_setup
+}
+
+src_configure() {
+	local mycmakeargs=(
+		-DBUILD_SHARED_LIBS=ON
+		-DUSE_PYTHON2=OFF
+		-DPYTHON=$(usex python)
+		-DTESTING=$(usex test)
+		-DUSE_GMP=$(usex gmp)
+		-DUSE_PYTHON3=$(usex python)
+
+		# Integration with other SMT solvers
+		-DUSE_LINGELING=OFF  # Not packaged yet.
+		-DUSE_CADICAL=OFF  # Fails to link.
+		-DUSE_CMS=$(usex cryptominisat)
+		-DUSE_MINISAT=$(usex minisat)
+		-DUSE_PICOSAT=$(usex picosat)
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	dodir /usr/$(get_libdir)
+	mv "${ED}"/usr/lib/*.so "${ED}"/usr/$(get_libdir)/ || die
+
+	if use examples ; then
+		dodoc -r examples
+	fi
+}
diff --git a/sci-mathematics/boolector/metadata.xml b/sci-mathematics/boolector/metadata.xml
new file mode 100644
index 000000000000..b61474ce8353
--- /dev/null
+++ b/sci-mathematics/boolector/metadata.xml
@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories
+    of fixed-size bit-vectors, arrays and uninterpreted functions. It supports
+    the SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector
+    provides a rich C and Python API and supports incremental solving, both
+    with the SMT-LIB commands push and pop, and as solving under assumptions.
+  </longdescription>
+  <use>
+    <flag name="cryptominisat">
+      Enable support for <pkg>sci-mathematics/cryptominisat</pkg>
+    </flag>
+    <flag name="minisat">
+      Enable support for <pkg>sci-mathematics/minisat</pkg>
+    </flag>
+    <flag name="picosat">
+      Enable support for <pkg>sci-mathematics/picosat</pkg>
+    </flag>
+  </use>
+  <upstream>
+    <bugs-to>https://github.com/Boolector/boolector/issues/</bugs-to>
+    <doc>https://boolector.github.io/docs/index.html</doc>
+    <remote-id type="github">Boolector/boolector</remote-id>
+  </upstream>
+</pkgmetadata>