Summary
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.
Versions
v3.2.4 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cryptominisat examples gmp minisat picosat python test
v3.2.3 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64 ~x86
- USE flags
- cryptominisat examples gmp minisat picosat python test
USE flags
General
- cryptominisat
- Enable support for sci-mathematics/cryptominisat
- examples
- Install examples, usually source code
- gmp
- Add support for dev-libs/gmp (GNU MP library)
- minisat
- Enable support for sci-mathematics/minisat
- picosat
- Enable support for sci-mathematics/picosat
- python
- Add optional support/bindings for the Python language
- 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
Dependencies
dev-lang / python : Freethreading (no-GIL) version of Python programming language
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
sci-mathematics / btor2tools : Generic parser and tools for the BTOR2 format
sci-mathematics / cryptominisat : Advanced SAT solver with C++ and command-line interfaces
sci-mathematics / minisat : Small yet efficient SAT solver with reference paper
sci-mathematics / picosat : SAT solver with proof and core support
Runtime Dependencies
dev-lang / python : Freethreading (no-GIL) version of Python programming language
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
sci-mathematics / btor2tools : Generic parser and tools for the BTOR2 format
sci-mathematics / cryptominisat : Advanced SAT solver with C++ and command-line interfaces
sci-mathematics / minisat : Small yet efficient SAT solver with reference paper
sci-mathematics / picosat : SAT solver with proof and core support
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/boolector: bump to 3.2.4
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/boolector: fix install on musl
Closes: https://bugs.gentoo.org/928977 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/boolector: drop old 3.2.2_p20220110
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/boolector: bump to 3.2.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/boolector: H -> COMMIT
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/boolector: fix build to not require static libs
Bug: https://bugs.gentoo.org/890700 Bug: https://bugs.gentoo.org/890698 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/boolector: new package; add 3.2.2_p20220110
Signed-off-by: Maciej Barć <xgqt@gentoo.org>