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.
Editing
- Syntax highlighting for VIM.
- Syntax highlighting mode TextMate and Sublime.
- Emacs mode to edit and run SMT-LIB 2 scripts.
Parsing
- An ANTLR grammar of SMT-LIB 2.6 scripts.
- 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.0 scripts implemented in Flex and Bison and C99.
- A Haskell library for parsing and printing SMT-LIB 2 scripts.
- An SWI-Prolog parser for SMT-LIB 2.6 scripts.
- An OCaml parser for SMT-LIB 2.0 scripts (not maintained).
Language Servers
- Dolmen, an LSP server SMT-LIB 2.6.
Debugging
- ddSMT, a delta-debugger (input minimizer) for SMT-LIB-compliant solvers.
Interfaces
- Nsolv, a front-end that allows multiple SMT-LIB 2 compliant solvers to be executed in parallel.
- rsmt2, a generic Rust library to interact with SMT-LIB 2 compliant solvers running in a separate system process.
- SBV, a tool to express properties of Haskell programs and prove them using SMT solvers via an SMT-LIB interface.
- SMT Kit, a C++11 library for many-sorted logics targeting quantifier-free SMT-LIB 2.0 formulas.
- SMTpp, an OCaml tool operating both as a source-to-source transformer and analyzer for SMT-LIB 2.0.
- pySMT, a Python library for manipulating and solving SMT formulas using SMT-LIB 2-compliant solvers.