At a Glance
| Applications | SMT Solver Theorem Prover SAT Solver |
| Developers | Microsoft Research |
| Inputs | SMTLIB2 DIMACS |
| Interfaces | CLI Python Rust C C++ Java .NET Online |
| Licenses | MIT |
| Maintenance | Actively Maintained |
Description
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings
This tool is available through the following interfaces:
- C API: Z3 C API Reference
- C++ API: Z3 C++ Namespace Reference
- .NET API: Z3 .NET Namespace Reference
- Java API: Z3 Java API Reference
- Python bindings: z3-solver PyPI package (Documentation)
- Rust bindings: z3 crate on crates.io
Publications
- Z3: An Efficient SMT Solver (March 2008) by de Moura, Leonardo et. al. | Appears in TACAS 2008 | Published by Springer, Berlin, Heidelberg | 10.1007/978-3-540-78800-3_24