SMT Solvers
The table below summarizes some of the features of the many available SMT solvers. The column "SMT-LIB" indicates compatibility with the SMT-LIB language; many systems marked 'yes' may support only older versions of SMT-LIB, or offer only partial support for the language. The column "CVC" indicates support for the CVC language. The column "DIMACS" indicates support for the DIMACS format.
Projects differ not only in features and performance, but also in the viability of the surrounding community, its ongoing interest in a project, and its ability to contribute documentation, fixes, tests and enhancements. Based on these measures, it appears that the most vibrant, well-organized projects are OpenSMT, STP and CVC4.
| Platform | Features | Notes | |||||||
|---|---|---|---|---|---|---|---|---|---|
| Name | OS | License | SMT-LIB | CVC | DIMACS | Built-in theories | API | SMT-COMP | |
| ABsolver | Linux | CPL | v1.2 | No | Yes | linear arithmetic, non-linear arithmetic | C++ | no | DPLL-based |
| Alt-Ergo | Linux, Mac OS, Windows | CeCILL-C | partial v1.2 and v2.0 | No | No | empty theory, linear integer and rational arithmetic, non-linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers | OCaml | 2008 | Polymorphic first-order input language à la ML, SAT-solver based, combines Shostak-like and Nelson-Oppen like approaches for reasoning modulo theories |
| Barcelogic | Linux | Proprietary | v1.2 | empty theory, difference logic | C++ | 2009 | DPLL-based, congruence closure | ||
| Beaver | Linux, Windows | BSD | v1.2 | No | No | bitvectors | OCaml | 2009 | SAT-solver based |
| Boolector | Linux | GPLv3 | v1.2 | No | No | bitvectors, arrays | C | 2009 | SAT-solver based |
| CVC3 | Linux | BSD | v1.2 | Yes | empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers | C/C++ | 2010 | proof output to HOL | |
| CVC4 | Linux, Mac OS | BSD | Yes | Yes | rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols | 2010 | version 1.0 released Dec. 2012 | ||
| Decision Procedure Toolkit (DPT) | Linux | Apache | No | OCaml | no | DPLL-based | |||
| iSAT | Linux | Proprietary | No | non-linear arithmetic | no | DPLL-based | |||
| MathSAT | Linux | Proprietary | Yes | Yes | empty theory, linear arithmetic, bitvectors, arrays | C/C++, Python, Java | 2010 | DPLL-based | |
| MiniSmt | Linux | LGPL | partial v2.0 | non-linear arithmetic | 2010 | Yices-based | |||
| OpenSMT | Linux, Mac OS, Windows | GPLv3 | partial v2.0 | Yes | empty theory, differences, linear arithmetic, bitvectors | C++ | 2011 | lazy SMT Solver | |
| SatEEn | ? | Proprietary | v1.2 | linear arithmetic, difference logic | none | 2009 | |||
| SMT-RAT | Linux, Mac OS | GPLv3 | v2.0 | No | No | linear arithmetic, nonlinear arithmetic | C++ | no | Toolbox offering theory solver modules for the development of SMT solvers for nonlinear real arithmetic (NRA). Example embedding in OpenSMT available. |
| SONOLAR | Linux, Windows | Proprietary | partial v2.0 | bitvectors | C | 2010 | SAT-solver based | ||
| Spear | Linux, Mac OS, Windows | Proprietary | v1.2 | bitvectors | 2008 | ||||
| STP | Linux, OpenBSD, Windows, Mac OS | MIT | partial v2.0 | Yes | No | bitvectors, arrays | C, C++, Python, OCaml, Java | 2011 | SAT-solver based |
| SWORD | Linux | Proprietary | v1.2 | bitvectors | 2009 | ||||
| UCLID | Linux | BSD | No | No | No | empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.) | no | SAT-solver based, written in Moscow ML. Input language is SMV model checker. Well-documented! | |
| veriT | Linux | BSD | partial v2.0 | empty theory, difference logic | C/C++ | 2010 | SAT-solver based | ||
| Yices | Linux, Mac OS, Windows | Proprietary | v1.2 | 2009 | |||||
| Z3 | Linux, Mac OS, Windows, FreeBSD | MSR-LA | v2.0 | Yes | empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers | C/C++, .NET, OCaml, Python, Java | 2011 | Source code is available online | |
Read more about this topic: Satisfiability Modulo Theories