sci-mathematics/boolector: new package; add 3.2.2_p20220110

Signed-off-by: Maciej Barć <xgqt@gentoo.org>

3 files changed, 110 insertions, 0 deletions

diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
new file mode 100644
index 000000000000..14c297d8f681
--- /dev/null
+++ b/sci-mathematics/boolector/Manifest
@@ -0,0 +1 @@
+DIST boolector-3.2.2_p20220110.tar.gz 1567668 BLAKE2B 6816f0434d88c790a27b9afe4c3b63c18a55b14f9f13b092f2940309e34842fe4868bf8d378bad130c4561d25e7d79b356fc27d9422bd42ba1b74ff98be36f72 SHA512 b1b964c155c8227e631025cf6bff69cf54728b1d875c2bd44a5a1ddb2857de2ab8fefc96d194faa5f98015e730b417d46a415ea601740e890df07ad5e50ad656
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>