Summary
OpenSMT2 is an SMT solver written in C++. It supports reading files in SMT-LIB2 format and the theories QF_UF, QF_RDL, QF_IDL, QF_LRA, QF_LIA, QF_UFLRA, QF_UFLIA and QF_AX. The system also provides an API; the distribution includes a minimal example how to use the API.
Versions
v2.5.2 :: 0/2.5.2 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- debug libedit readline test
USE flags
General
- 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
- libedit
- Use the libedit library (replacement for readline)
- readline
- Enable support for libreadline, a GNU line-editing library that almost everyone wants
- test
- Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)
Dependencies
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
Runtime Dependencies
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
Bugs
- 928095
- sci-mathematics/opensmt-2.5.2 fails to compile: Polynomial.h:183:15: error: no declaration matches long unsigned int PolynomialT<VarType>::size() const
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: fix libdir on glibc only
Closes: https://bugs.gentoo.org/924977 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/opensmt: sys-devel/bison -> app-alternatives/yacc
All of these will be using app-alternatives/yacc anyway as they're not unsetting YACC or LEX, so make the dep reflect reality. (Included both YACC and LEX out of conservatism.) Signed-off-by: Sam James <sam@gentoo.org> - Sam James · gentoo
sci-mathematics/opensmt: sys-devel/flex -> app-alternatives/lex
All of these will be using app-alternatives/lex anyway as they're not unsetting YACC or LEX, so make the dep reflect reality. (Included both YACC and LEX out of conservatism.) Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Kostadin Shishmanov · gentoo
sci-mathematics/opensmt: fix build with gcc 14
Closes: https://bugs.gentoo.org/916855 Signed-off-by: Kostadin Shishmanov <kocelfc@tutanota.com> Closes: https://github.com/gentoo/gentoo/pull/33708 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: drop old 2.5.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: fix .so install
Closes: https://bugs.gentoo.org/912314 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: bump to 2.5.2
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/opensmt: drop old 2.5.0
Closes: https://bugs.gentoo.org/894728 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: bump to 2.5.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/opensmt: drop old 2.4.3-r2
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: bump to 2.5.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: require gmp with USE=cxx
Closes: https://bugs.gentoo.org/904272 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: fix build on musl
Bug: https://github.com/usi-verification-and-security/opensmt/pull/590 Closes: https://bugs.gentoo.org/890794 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/opensmt: drop old 2.4.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: prevent fetching googletest
Closes: https://bugs.gentoo.org/890722 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/opensmt: do not install static libs
Closes: https://bugs.gentoo.org/890724 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/opensmt: new package; add 2.4.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org>