14 files changed, 206 insertions, 4 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index d14edd8f8e92..c1c620364c1c 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/cgal/Manifest b/sci-mathematics/cgal/Manifest
index ec7c85667e2c..041dfbf45669 100644
--- a/sci-mathematics/cgal/Manifest
+++ b/sci-mathematics/cgal/Manifest
@@ -7,5 +7,5 @@ DIST CGAL-5.5-doc_html.tar.xz 53145672 BLAKE2B 7a575f09eed2fd97f3e68f37428d4ab41
 DIST CGAL-5.5.tar.xz 24156768 BLAKE2B e5f02cd082abfa8443e65430ed366cfdc3736c6a7af37284969ddd558ede1aa6c881d6928c65708504fd58f68ea01f56aa0749267d6dc83fd54f0b28e8c01374 SHA512 7fa6bf6c046727a9e0bce7cbde34cbe85979127a1ad0904f2865be83a80e89fa9af5118e5647572414f8096d29ecc808ee471d4bd3e7ecd41338be649b549290
 EBUILD cgal-5.2-r2.ebuild 1662 BLAKE2B a9b0ec72848616b2240e0c99b4237e0b451fe756e7c30f884d01e81ba2da45ab72a4bbce66caf44c2282dbf74285fbdc0459d239c8f9b8ba440a5d5e5d12fa6b SHA512 511271b99579a90906356b82c16a97e0652432c8c97987d0c2ff519702862693969c19b4c0e22cbea424d4377a8105b3db3852b4ebcca181d4f7ed64d6562d19
 EBUILD cgal-5.4.1.ebuild 1685 BLAKE2B 66e3698adbeb74179fd2e1f0bfa28affd46cfba76c4b17e7426604bff5cbc1358b01684491044b15d4f2c08277a87b5db13a43f45de73eb4c3a46f852c5a9cae SHA512 996a19e309b923452cf6be94d3214b9592984db7531ab0e74f1ca988c045499adfa495bb50549384efbb979431b6e7e378b4c846684466b6904133a386bc21f3
-EBUILD cgal-5.5.ebuild 1230 BLAKE2B e2a27d15851530dd5c6b19f9662d1ec9e1008b94f9ad05eccf27f52fda1cec32b65eefec33d425ae86c4c810ff83ec47456b72bec633cb99998b59ca2f397a3a SHA512 a52d2df01c6a8788cae02cc331cf31ceb2e969dbdf27dad0950b2445db9895324174b7e57aff30a446d688bcaab501e646f3e8130c25c90ea2ddc05b9d3f2135
+EBUILD cgal-5.5.ebuild 1229 BLAKE2B 5c810e807f9d28c9f7fb27c2724ae6af784a7d18ac910ff24773868252b7bbe9a7cf05fb9f6dc5cdb24088349657aacc33f8116d7e7ef04323f334aa2fe7d70e SHA512 35e0cd4f6baf57f8d4b02d8bdc19490cc7c5844bdb0575158d30ef43b4faa5123d64ce8047adef4805b77d83bd43885259aae237300e181ad2e028a09d39697e
 MISC metadata.xml 1373 BLAKE2B 7e3ecb8f36476edb32f20a03775f01f916fa82ab2c7a6e0554066a4b47019d3a13350e442ba4f9e6f184eb7678707a683339f223d5c86e18c08e9de5b359218c SHA512 a99c724624e7cdd71c65424adef18966dc6a88bd8e56e38fa5ba0ad4c40010481548d6d7f3e51044f62597096fdbf9e52a361d3c71d0ab870753526df664f7d2
diff --git a/sci-mathematics/cgal/cgal-5.5.ebuild b/sci-mathematics/cgal/cgal-5.5.ebuild
index 965fdeb16266..a20801ec0461 100644
--- a/sci-mathematics/cgal/cgal-5.5.ebuild
+++ b/sci-mathematics/cgal/cgal-5.5.ebuild
@@ -17,7 +17,7 @@ S="${WORKDIR}/${MY_P}"
 
 LICENSE="LGPL-3 GPL-3 Boost-1.0"
 SLOT="0/14"
-KEYWORDS="~amd64 ~arm64 x86 ~amd64-linux ~x86-linux"
+KEYWORDS="amd64 ~arm64 x86 ~amd64-linux ~x86-linux"
 IUSE="doc examples"
 
 RDEPEND="
diff --git a/sci-mathematics/cudd/Manifest b/sci-mathematics/cudd/Manifest
new file mode 100644
index 000000000000..bc4e55b487ca
--- /dev/null
+++ b/sci-mathematics/cudd/Manifest
@@ -0,0 +1,3 @@
+DIST cudd-3.0.0.tar.gz 1175302 BLAKE2B 9948495b4426e5931daafe0f48a1e1886bbadd6adbd5191b41aa7876522da7d29e84585a555184d5cf661a93e0d974b2caea79e135e7633eef1b7fdf173fdd1c SHA512 c0cb5fbdc4bb1793712e42c2e1377c3b1ae36f22ffc82bb3dd93a8a51f58bfe192fed9a37239a4c471326ef00a8f5e2f7fc801a2a6841be3db5a7e159e866f21
+EBUILD cudd-3.0.0.ebuild 525 BLAKE2B 5ec2884638fd5c83067e5506603804dc46365b331beec169ccea84786d4a73062eb0e849a222f7fad8efdf384f44aee3add056093eb41bf7a4f3a0c053563af4 SHA512 7530b2aa8a32bb8925632b39884ac895c66fd1eebf9b3f77763d7cab4dec1f626107296018b5d7a62739a9f41bcc8bd1af0a2f9dde41df2347a0bd6ecbb080e9
+MISC metadata.xml 529 BLAKE2B 579460e5cc8af597d1540cb12a6107dceb3b3635f2f2e13769851b46f59f13da63fae41f1d6dfae7e2940c292b70bdd3a9200c85939f554cef9f95d09e8cb10c SHA512 4408ca822d4b781b98c7906f98cc2afebde15057d82ee6d9b2efa1101bb4cb5f14be74303d34fd85193220a07282a46734125e81cdd90813c47174997d81c42a
diff --git a/sci-mathematics/cudd/cudd-3.0.0.ebuild b/sci-mathematics/cudd/cudd-3.0.0.ebuild
new file mode 100644
index 000000000000..23d19b084202
--- /dev/null
+++ b/sci-mathematics/cudd/cudd-3.0.0.ebuild
@@ -0,0 +1,27 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+DESCRIPTION="Colorado University binary Decision Diagram library"
+HOMEPAGE="https://davidkebo.com/cudd/"
+SRC_URI="https://davidkebo.com/source/cudd_versions/${P}.tar.gz"
+
+LICENSE="BSD"
+SLOT="0/${PV}"
+KEYWORDS="~amd64 ~x86"
+
+src_configure() {
+	local myconf=(
+		--enable-dddmp
+		--enable-obj
+		--enable-shared
+	)
+	econf ${myconf[@]}
+}
+
+src_install() {
+	default
+
+	find "${ED}" -name "*.la" -type f -delete || die
+}
diff --git a/sci-mathematics/cudd/metadata.xml b/sci-mathematics/cudd/metadata.xml
new file mode 100644
index 000000000000..63814133765d
--- /dev/null
+++ b/sci-mathematics/cudd/metadata.xml
@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci@gentoo.org</email>
+    <name>Gentoo Science Project</name>
+  </maintainer>
+  <longdescription>
+    CUDD stands for Colorado University Decision Diagram. It is a package for
+    the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision
+    Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs).
+  </longdescription>
+</pkgmetadata>
diff --git a/sci-mathematics/libpoly/Manifest b/sci-mathematics/libpoly/Manifest
new file mode 100644
index 000000000000..9ad5a5691b87
--- /dev/null
+++ b/sci-mathematics/libpoly/Manifest
@@ -0,0 +1,3 @@
+DIST libpoly-0.1.11.tar.gz 614216 BLAKE2B 42a2510a6a9f94e7170b5df97ec8f2b7b29cb9c95bd13c8c7abebc9e7db7fedcbeb7a928f22d173e154180acc199e081323d2f1cb23264bf31ac1bfc88494dc8 SHA512 df08a6bab33e27023316972e2496801cea4959faf403b5df8314fa45b4541cd1352583a44084bea130c1e3ca4ed86de032f7f96eeb915599f178e80976a68f7a
+EBUILD libpoly-0.1.11.ebuild 1240 BLAKE2B eb73ef53ad5ba372b2d03d6bfb8e8b98821444ada7f479d743f69c2d65bf0b039dc7615bea6a65a53a74421d590020954b1b3cf52113eb8cb9487c1660ff30ed SHA512 5a3dd9137eba45c30f803216d9fe3c5b7ef760ba1d9a00ac3326e0fa19a1fe1191213516c4244f33fd5cb4ac20d831a26a9acf6182b3edbcf3b2e3fefc09ae75
+MISC metadata.xml 757 BLAKE2B baf8c7cb139dff0a4fd382eee7583f5f921209ffcddcac77a85086bb5214bc24bc875343f4f4f363e3e72e8077361e2864419c05c28338df4e9dd80b5dc4ce97 SHA512 0d9b28c2900d806f2b4df86eb69e9a3c1491a564559d80fdf78fa77673634a1735a391beb89599caea26f3af1a22880cb91e0611297e9fa811e85495eb12ff02
diff --git a/sci-mathematics/libpoly/libpoly-0.1.11.ebuild b/sci-mathematics/libpoly/libpoly-0.1.11.ebuild
new file mode 100644
index 000000000000..e3b8fb247367
--- /dev/null
+++ b/sci-mathematics/libpoly/libpoly-0.1.11.ebuild
@@ -0,0 +1,60 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+PYTHON_COMPAT=( python3_{8,9,10} )
+
+inherit python-single-r1 cmake
+
+DESCRIPTION="C library for manipulating polynomials"
+HOMEPAGE="https://github.com/SRI-CSL/libpoly/"
+SRC_URI="https://github.com/SRI-CSL/${PN}/archive/v${PV}.tar.gz
+	-> ${P}.tar.gz"
+
+LICENSE="LGPL-3+"
+SLOT="0/${PV}"
+KEYWORDS="~amd64 ~x86"
+IUSE="+python"
+REQUIRED_USE="python? ( ${PYTHON_REQUIRED_USE} )"
+
+RDEPEND="
+	dev-libs/gmp:=
+	python? (
+		${PYTHON_DEPS}
+		$(python_gen_cond_dep 'dev-python/sympy[${PYTHON_USEDEP}]')
+	)
+"
+DEPEND="${RDEPEND}"
+BDEPEND="dev-util/patchelf"
+
+DOCS=( README.md examples )
+
+pkg_setup() {
+	use python && python-single-r1_pkg_setup
+}
+
+src_configure() {
+	local mycmakeargs=(
+		-DLIBPOLY_BUILD_PYTHON_API=$(usex python)
+		-DLIBPOLY_BUILD_STATIC=OFF
+		-DLIBPOLY_BUILD_STATIC_PIC=OFF
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	mv "${D}"/usr/lib "${D}"/usr/$(get_libdir) || die
+
+	if use python ; then
+		local sitedir="${D}"/"$(python_get_sitedir)"
+		local sopath="${BUILD_DIR}"/python/polypy.so
+
+		patchelf --remove-rpath "${sopath}" || die
+
+		mkdir -p "${sitedir}" || die
+		cp "${sopath}" "${sitedir}" || die
+	fi
+}
diff --git a/sci-mathematics/libpoly/metadata.xml b/sci-mathematics/libpoly/metadata.xml
new file mode 100644
index 000000000000..9d9fdde167c9
--- /dev/null
+++ b/sci-mathematics/libpoly/metadata.xml
@@ -0,0 +1,19 @@
+<?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>
+    LibPoly is a C library for manipulating polynomials. The target
+    applications are symbolic reasoning engines, such as SMT solvers, that need
+    to reason about polynomial constraints. It is research software under
+    development, so the features and the API might change rapidly.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/SRI-CSL/libpoly/issues/</bugs-to>
+    <remote-id type="github">SRI-CSL/libpoly</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/octave/Manifest b/sci-mathematics/octave/Manifest
index 8497b50a380f..c67799731818 100644
--- a/sci-mathematics/octave/Manifest
+++ b/sci-mathematics/octave/Manifest
@@ -9,5 +9,5 @@ DIST octave-7.3.0.tar.xz 26215288 BLAKE2B 53fff89e798f8b8795f83e46f66793f2cf37f9
 EBUILD octave-6.4.0-r3.ebuild 6043 BLAKE2B a99d2325249cbd29bcc3b00e734b28f7de4b61025f8f2133d5b7c53ad7bbb14bdbbd068ac204e3f7af80143c3797ec97688487b70361f8966dffd06569b3612d SHA512 559c07c35ecc7011e0f44a23fb2ad392a1562221f7218c0b5d89a2a9a2dd60e9f68e9cf3345b226d572d5da85d63cbe051643363bc9e1896ce4820817317f605
 EBUILD octave-6.4.0-r4.ebuild 6029 BLAKE2B 0bc2a9b11d237a51ea875b916e3dde0db429d3d577a20746d68d7dff43cf3755776a2c19c3bcc5987897e308850f9f570973d8c0abb0506a68d581b42ad3a50c SHA512 d6fef61f24420cbbc7a520ac42d9308f6e1824a68ed6bc928f9225fd5b5fa070ca091375445675d2e0654753b2d87d738e4c920d26bff2d245448a94c3a8b0c3
 EBUILD octave-7.2.0-r1.ebuild 5527 BLAKE2B 799a3175791ed82cc0f46bca34f6280a5b51b0e42381e627b748f195fa965a84fda6f562d8c6e6a20b3074a225d87a9b5ab1f8ba41b8978d3187d14df569ba0e SHA512 cfa3e263ce589e39b47b5c9240c63fe006a8751b81bf03850dc91848965fb46bc67db069550e86db5a4f3bc653ae7ab7744930753bbfbcfbcbde3efa91b4e5a0
-EBUILD octave-7.3.0-r1.ebuild 6642 BLAKE2B 9fd71ca76e0969c76fd43ac631713706b2feea06782947982c1dc2cc6d1429facfcccd9fc00664b55893adb2a3da78c8311f7d92075d8f52e645cdc281a5fb7b SHA512 c0a04936e0b6443d0d13605a17dbc9407b42d6474609e7a6c7b0c09b9c39c670b1cf3dc8bdab149170bd8efb371496d410fe8aa5c40790e539206b1448d99d90
+EBUILD octave-7.3.0-r1.ebuild 6638 BLAKE2B 4eaa8ca9ce1a7a0ce3bc91efa819aa8025d4d3ad32b7139b572d793f4b66c137adbaa952bb9a576adcfce3d9c48813522c36c7cd2e17e19dd33bda8092ef4a4e SHA512 80d0f6e43c6f45cdfb1e26d9a4c9e321fb254e1abf81f5f2cd40c64b56a9d33fe8cb6ce2062949c42742e0465d71bc56f589d374d0c3c8cfe2c884b315a09df1
 MISC metadata.xml 1703 BLAKE2B 0471bc1eeaa2ce86b8eeca5c3e831eb0d9207b5fd1d3c03aba017a257b7b98b313c42a1054471c79dab1b5d2d84df8a8d3b0ee68e772cbe6970ac92f07dc3269 SHA512 3c051ff80c958af4315faa1670cc5e1d6a53397b4182304b760cf4f2e14f716e187dd76879d094e35713ac115c47ea623530c2f4b114f7bf2eae1cdf28bc46b8
diff --git a/sci-mathematics/octave/octave-7.3.0-r1.ebuild b/sci-mathematics/octave/octave-7.3.0-r1.ebuild
index 0901c51c9f76..50d77f9706b7 100644
--- a/sci-mathematics/octave/octave-7.3.0-r1.ebuild
+++ b/sci-mathematics/octave/octave-7.3.0-r1.ebuild
@@ -12,7 +12,7 @@ SRC_URI="mirror://gnu/${PN}/${P}.tar.xz"
 LICENSE="GPL-3"
 SLOT="0/${PV}"
 IUSE="curl doc fftw fltk +glpk gnuplot gui hdf5 imagemagick java json opengl portaudio postscript +qhull +qrupdate readline sndfile +sparse ssl sundials X zlib"
-KEYWORDS="~amd64 ~arm ~arm64 ~ppc ~ppc64 ~riscv ~x86 ~amd64-linux ~x86-linux"
+KEYWORDS="amd64 arm arm64 ~ppc ~ppc64 ~riscv x86 ~amd64-linux ~x86-linux"
 
 # Although it is listed in INSTALL.OCTAVE as a build tool, Octave runs
 # "makeinfo" from sys-apps/texinfo at runtime to convert its texinfo
diff --git a/sci-mathematics/yices2/Manifest b/sci-mathematics/yices2/Manifest
new file mode 100644
index 000000000000..8203107f8a07
--- /dev/null
+++ b/sci-mathematics/yices2/Manifest
@@ -0,0 +1,3 @@
+DIST Yices-2.6.4.tar.gz 10186909 BLAKE2B 1c4b6297fd59924e9d99b9e17eb4b42e9bfbc24dcd56631beb9b72103c91578eb72b90cb9e228a5e9d489efc520a2e1d41185e9c3f4a8c43fc93f8dabba7414d SHA512 d8102c41fda0e200fd1336ae317b516d2797d10c187b8f7aecf0c9b08b4b487b90bef8c358099b2da51c0367326939f9610fd4e6d5a41a392cf1114bd04b8763
+EBUILD yices2-2.6.4.ebuild 741 BLAKE2B e1d7f1a4032bbd2d1079dc03817c87493da9ed284de22e3cfab9873ee975257eb005a395175d20acbfe4e76047da3598b082b502baf8510e067acc9d484d9f62 SHA512 f955e611c3394cb6773ec7172dfe1c2628247fee7ee3d77d4255914783eda78f1c16cf82422889db366714d6c82511610d231d5eef9059e4fb2bee5a9b0d00f1
+MISC metadata.xml 1103 BLAKE2B 1efa78a55c94698f41966873f4aaf9dc8b065fad8ddbb4d9cdec62490440f22179793edf602e26ffe84ad0bc983de9c11e22d8c75e5b4fe29bc0fb947d6040c6 SHA512 d785ee9807971857aa800896036e9a24035a17096f322ccc197cb924a61e2cc5982b4c913794e2edf0295672ce854b04dd686abc956cf625783a5a2b5aaab15d
diff --git a/sci-mathematics/yices2/metadata.xml b/sci-mathematics/yices2/metadata.xml
new file mode 100644
index 000000000000..0b8f70011239
--- /dev/null
+++ b/sci-mathematics/yices2/metadata.xml
@@ -0,0 +1,26 @@
+<?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>
+    Yices 2 is an SMT solver that decides the satisfiability of formulas
+    containing uninterpreted function symbols with equality, real and integer
+    arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both
+    linear and nonlinear arithmetic. Yices 2 can process input written in the
+    SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively,
+    you can write specifications using Yices 2's own specification language,
+    which includes tuples and scalar types. You can also use Yices 2 as a
+    library in your software.
+  </longdescription>
+  <use>
+    <flag name="mcsat">Enable support for MCSAT</flag>
+  </use>
+  <upstream>
+    <bugs-to>https://github.com/SRI-CSL/yices2/issues/</bugs-to>
+    <remote-id type="github">SRI-CSL/yices2</remote-id>
+  </upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/yices2/yices2-2.6.4.ebuild b/sci-mathematics/yices2/yices2-2.6.4.ebuild
new file mode 100644
index 000000000000..8fcf3fcb619b
--- /dev/null
+++ b/sci-mathematics/yices2/yices2-2.6.4.ebuild
@@ -0,0 +1,47 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit autotools
+
+DESCRIPTION="SMT Solver supporting SMT-LIB and Yices specification language"
+HOMEPAGE="https://github.com/SRI-CSL/yices2/"
+SRC_URI="https://github.com/SRI-CSL/${PN}/archive/Yices-${PV}.tar.gz"
+S="${WORKDIR}"/${PN}-Yices-${PV}
+
+LICENSE="GPL-3+"
+SLOT="0/${PV}"
+KEYWORDS="~amd64 ~x86"
+IUSE="+mcsat"
+
+RDEPEND="
+	dev-libs/gmp:=
+	mcsat? (
+		sci-mathematics/libpoly:=
+		sci-mathematics/cudd:=
+	)
+"
+DEPEND="${RDEPEND}"
+
+DOCS=( FAQ.md README.md )
+
+src_prepare() {
+	default
+
+	eautoreconf
+}
+
+src_configure() {
+	econf $(use_enable mcsat)
+}
+
+src_compile() {
+	emake STRIP=echo
+}
+
+src_install() {
+	default
+
+	doman doc/*.1
+}