sci-mathematics / stp

Simple Theorem Prover, an efficient SMT solver for bitvectors

Official package sites : https://github.com/stp/stp/ · https://stp.github.io/ ·

STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

v2.3.4 :: 0/2.3.4 :: gentoo

Modified
License
GPL-2+ MIT
Keywords
~amd64 ~x86
USE flags
cryptominisat debug python test

v2.3.3-r3 :: 0/2.3.3 :: gentoo

Modified
License
GPL-2+ MIT
Keywords
~amd64 ~x86
USE flags
cryptominisat debug python test

General

cryptominisat
Enable sci-mathematics/cryptominisat support
debug
Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces
python
Enable building the Python interface
test
Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)

python_single_target

python3_10
Build for Python 3.10 only
python3_11
Build for Python 3.11 only
python3_12
Build for Python 3.12 only
python3_13
Build for Python 3.13 only

dev-db / sqlite : SQL database engine

dev-lang / python : Freethreading (no-GIL) version of Python programming language

dev-libs / boost : Boost Libraries for C++

dev-libs / icu : International Components for Unicode

sci-mathematics / cryptominisat : Advanced SAT solver with C++ and command-line interfaces

sci-mathematics / minisat : Small yet efficient SAT solver with reference paper

sys-libs / zlib : Standard (de)compression library

dev-db / sqlite : SQL database engine

dev-lang / python : Freethreading (no-GIL) version of Python programming language

dev-libs / boost : Boost Libraries for C++

dev-libs / icu : International Components for Unicode

sci-mathematics / cryptominisat : Advanced SAT solver with C++ and command-line interfaces

sci-mathematics / minisat : Small yet efficient SAT solver with reference paper

sys-libs / zlib : Standard (de)compression library

895770
sci-mathematics/stp-2.3.3-r2 help2man: can't get `--help' info from /var/tmp/portage/sci-mathematics/stp-2.3.3-r2/work/stp-2.3.3_build/stp
942340
sci-mathematics/stp-2.3.4 fails tests: 9 - StrengthReduction_TestTests-gtest (Subprocess aborted)
Repository mirror & CI · gentoo
Merge updates from master
Michał Górny · gentoo
Rename dev-python/{OutputCheck → outputcheck}
Signed-off-by: Michał Górny <mgorny@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: build tweaks
Closes: https://bugs.gentoo.org/880135 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: bump to 2.3.4
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: enable py3.12 compat
Closes: https://bugs.gentoo.org/929798 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: update PYTHON_COMPAT; add help2man to BDEPEND
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: patch - include cstdint
Closes: https://bugs.gentoo.org/895096 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Maciej Barć · gentoo
sci-mathematics/stp: rename patches
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
David Seifert · gentoo
*/*: remove py3.8 from PYTHON_COMPAT
Signed-off-by: David Seifert <soap@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: do not run C API tests
Closes: https://bugs.gentoo.org/879325 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: compile python modules
Closes: https://bugs.gentoo.org/864124 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: filter LTO (ODR)
Closes: https://bugs.gentoo.org/863263 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/stp: multiple fixes
- add missing test submodules - add optional cryptominisat dependency (USE=dependency) - add the Gentoo Mathematics Project to co-maintainers - change python to optional dependency (USE=python) - install PDF documentation - patch CMakeLists.txt to fix CFLAGS - patch stp.py to fix python module Closes: https://bugs.gentoo.org/759457 Package-Manager: Portage-3.0.28, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Maciej Barć · gentoo
sci-mathematics/stp: dev-libs -> sci-mathematics
Signed-off-by: Maciej Barć <xgqt@gentoo.org>