mirror of
https://github.com/Ponce/slackbuilds
synced 2024-11-29 13:00:32 +01:00
15 lines
653 B
Text
15 lines
653 B
Text
|
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.
|
||
|
|
|
||
|
|
|
||
|
|
If you want to enable non-linear real and integer arithmetic
|
||
|
|
set MCSAT=yes, this requires libpoly and libcudd.
|