Utilities and Tools
The page contains a set of utilities and tools to work with the SMT-LIB 2 format.
Note: Most of the utilities tools below have been developed by third parties and are provided here as a convenience to the community. Appearance on this page does not imply an endorsement of their full conformance to the SMT-LIB standard. Please contact each utility's authors directly for questions, bug reports, or other requests.
- A minimal syntax highlighting mode for VIM.
- jSMTLIB, a suite of Java tools for parsing and type-checking SMT-LIB 2 scripts, and translating them to the input languages of some non-SMT-LIB-conforming solvers.
- An open source generic lexer and parser for SMT-LIB 2 scripts implemented in Flex and Bison and C99
- An OCaml parser for SMT-LIB 2.0 scripts.
- ddSMT, a delta-debugger (input minimizer) for SMT-LIB-compliant solvers.
- Delta SMT, another delta-debugger for SMT-LIB-compliant solvers [Webpage].
- A Haskell library for parsing and printing SMT-LIB 2 scripts.
- SBV, a tool to express properties of Haskell programs and prove them using SMT solvers via an SMT-LIB interface.
- Nsolv, a front-end that allows multiple SMT-LIB compliant solvers to be executed in parallel.
- SMT Kit, a C++11 library for many-sorted logics targeting quantifier-free SMT-LIB 2.0 formulas.
- SMTpp, a tool operating both as a source-to-source transformer and analyzer for SMT-LIB.