commit: 8c125ea193d4cdad739e556558e28605fe455bf1
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed Jan 11 03:39:41 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed Jan 11 03:44:07 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8c125ea1
sci-mathematics/boolector: new package; add 3.2.2_p20220110
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/boolector/Manifest | 1 +
.../boolector/boolector-3.2.2_p20220110.ebuild | 77 ++++++++++++++++++++++
sci-mathematics/boolector/metadata.xml | 32 +++++++++
3 files changed, 110 insertions(+)
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>[email protected]</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>
