diff options
Diffstat (limited to 'academic/yices2/README')
| -rw-r--r-- | academic/yices2/README | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/academic/yices2/README b/academic/yices2/README new file mode 100644 index 0000000000..65774f7f8c --- /dev/null +++ b/academic/yices2/README @@ -0,0 +1,14 @@ + 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. |