sci-mathematics/opensmt: drop old 2.5.2

Signed-off-by: Maciej Barć <xgqt@gentoo.org>
This commit is contained in:
Maciej Barć
2025-11-21 20:11:51 +01:00
parent c68a719fb2
commit d0a5277940
4 changed files with 0 additions and 158 deletions

View File

@@ -1,2 +1 @@
DIST opensmt-2.5.2.tar.gz 1935650 BLAKE2B 85cd171d56591d2f1162a41ff8a425fc818238a2820aab0f75cc75ece8898c5e7de1478aeab93e8905a1aedad85a6df03062fefaad69bea043dce1f3f3d531f5 SHA512 c22d17d3aee33a3360f8ea552c82151eafdef7cc89e6750d34b4ff2a011675a5a5f04a7cb68ff984dd6a5332b2f180fb8abc529e64c3970aba6b7eb60408f198
DIST opensmt-2.7.0.gh.tar.gz 1532323 BLAKE2B 5d51d4919adbdd6be38348524820a05804ccd05f2caf637cc238fd220f88fec6926098d7905ddf3e00c6874286cee788301b98b9b71bf9c7e3ae5d80d4e1dd2d SHA512 15b87a9a9a9b55f63086ea10f6da75d8f8e86e71b46aff36efb28a49abb293a28e5e71a8d0e52d347112b8d4b3c045c884dbb1179f148e4da9a72e25f445001f

View File

@@ -1,8 +0,0 @@
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.3)
+cmake_minimum_required(VERSION 3.20)
if (POLICY CMP0074) # Policy 0074 has been introduced in CMake 3.12, so we need a check, otherwise older version would give an error
cmake_policy(SET CMP0074 NEW)

View File

@@ -1,68 +0,0 @@
From f30e983f876df3bd34571f9d554b3ebe226dd4bd Mon Sep 17 00:00:00 2001
From: Kostadin Shishmanov <kocelfc@tutanota.com>
Date: Tue, 7 Nov 2023 16:38:39 +0200
Subject: [PATCH] Add include <algorithm> to fix building with gcc 14
Gentoo bug:
https://bugs.gentoo.org/916855
Upstream PR:
https://github.com/usi-verification-and-security/opensmt/pull/653
Signed-off-by: Kostadin Shishmanov <kocelfc@tutanota.com>
---
src/logics/Logic.cc | 1 +
src/pterms/PtStore.cc | 1 +
src/simplifiers/BoolRewriting.cc | 1 +
src/tsolvers/egraph/EnodeStore.cc | 2 ++
4 files changed, 5 insertions(+)
diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc
index 2619df1fd..84b04d515 100644
--- a/src/logics/Logic.cc
+++ b/src/logics/Logic.cc
@@ -21,6 +21,7 @@
#include <queue>
#include <set>
#include <sstream>
+#include <algorithm>
using namespace std;
diff --git a/src/pterms/PtStore.cc b/src/pterms/PtStore.cc
index 377642947..63c6f56f3 100644
--- a/src/pterms/PtStore.cc
+++ b/src/pterms/PtStore.cc
@@ -29,6 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#include "OsmtApiException.h"
#include <sstream>
+#include <algorithm>
const int PtStore::ptstore_vec_idx = 1;
const int PtStore::ptstore_buf_idx = 2;
diff --git a/src/simplifiers/BoolRewriting.cc b/src/simplifiers/BoolRewriting.cc
index e2aa52b2c..196a642c4 100644
--- a/src/simplifiers/BoolRewriting.cc
+++ b/src/simplifiers/BoolRewriting.cc
@@ -5,6 +5,7 @@
#include "BoolRewriting.h"
#include "Logic.h"
#include <unordered_set>
+#include <algorithm>
// Replace subtrees consisting only of ands / ors with a single and / or term.
// Search a maximal section of the tree consisting solely of ands / ors. The
diff --git a/src/tsolvers/egraph/EnodeStore.cc b/src/tsolvers/egraph/EnodeStore.cc
index 2bed3302b..de2216410 100644
--- a/src/tsolvers/egraph/EnodeStore.cc
+++ b/src/tsolvers/egraph/EnodeStore.cc
@@ -28,6 +28,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#include "Symbol.h"
#include "Logic.h"
+#include <algorithm>
+
EnodeStore::EnodeStore(Logic& l)
: logic(l)
, ea(1024*1024)

View File

@@ -1,81 +0,0 @@
# Copyright 1999-2025 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
inherit cmake
DESCRIPTION="Compact and open-source SMT-solver written in C++"
HOMEPAGE="http://verify.inf.usi.ch/opensmt/
https://github.com/usi-verification-and-security/opensmt/"
if [[ "${PV}" == *9999* ]] ; then
inherit git-r3
EGIT_REPO_URI="https://github.com/usi-verification-and-security/${PN}"
else
SRC_URI="https://github.com/usi-verification-and-security/${PN}/archive/v${PV}.tar.gz
-> ${P}.tar.gz"
KEYWORDS="~amd64 ~x86"
fi
LICENSE="MIT"
SLOT="0/${PV}"
IUSE="debug libedit +readline test"
REQUIRED_USE="?? ( libedit readline )"
RESTRICT="!test? ( test )"
RDEPEND="
dev-libs/gmp:=[cxx]
readline? ( sys-libs/readline:= )
libedit? ( dev-libs/libedit:= )
"
DEPEND="
${RDEPEND}
"
BDEPEND="
app-alternatives/yacc
app-alternatives/lex
test? ( dev-cpp/gtest )
"
PATCHES=(
"${FILESDIR}/opensmt-2.5.2-cmake_minimum.patch"
"${FILESDIR}/opensmt-2.5.2-gcc-14.patch"
)
src_prepare() {
cmake_src_prepare
echo "add_subdirectory(unit)" > "${S}"/test/CMakeLists.txt || die
}
src_configure() {
local CMAKE_BUILD_TYPE
if use debug ; then
CMAKE_BUILD_TYPE=Debug
else
CMAKE_BUILD_TYPE=Release
fi
local -a mycmakeargs=(
-DPACKAGE_TESTS=$(usex test)
-DUSE_READLINE=$(usex readline)
)
if use readline || use libedit ; then
mycmakeargs+=( -DENABLE_LINE_EDITING=ON )
fi
cmake_src_configure
}
src_install() {
cmake_src_install
if use elibc_glibc ; then
dolib.so "${ED}"/usr/lib/libopensmt.so*
rm "${ED}"/usr/lib/libopensmt.so* || die
fi
rm "${ED}"/usr/lib/libopensmt.a || die
}