Summary
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.
Versions
v2.6.4-r1 :: 0/2.6.4 :: gentoo
- Modified
- License
- GPL-3+
- Keywords
- ~amd64 ~x86
- USE flags
- mcsat
USE flags
General
- mcsat
- Enable support for MCSAT
Dependencies
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
sci-mathematics / cudd : Colorado University binary Decision Diagram library
sci-mathematics / libpoly : C library for manipulating polynomials
Runtime Dependencies
dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers
sci-mathematics / cudd : Colorado University binary Decision Diagram library
sci-mathematics / libpoly : C library for manipulating polynomials
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/yices2: do not install static libs
Closes: https://bugs.gentoo.org/890758 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/yices2: new package; add 2.6.4
Signed-off-by: Maciej Barć <xgqt@gentoo.org>