35 lines
1.8 KiB
Markdown
35 lines
1.8 KiB
Markdown
+++
|
|
date = 2024-02-02T04:14:54-08:00
|
|
draft = false
|
|
title = 'Z3'
|
|
subtitle = 'Theorem Prover'
|
|
links = [
|
|
{ title = "Homepage", url = "https://github.com/Z3Prover/z3", icon = 'fa-solid fa-home' },
|
|
{ title = "Source Code", url = "https://github.com/Z3Prover/z3", icon = 'fa-brands fa-github' },
|
|
{ title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
|
|
]
|
|
applications = ['SMT Solver', 'Theorem Prover']
|
|
developers = ['Microsoft Research']
|
|
licenses = ['MIT']
|
|
inputs = ['SMTLIB2', 'DIMACS']
|
|
interfaces = ['CLI', 'Python', 'Rust', 'C', 'C++', 'Java', '.NET', 'Online']
|
|
maintenance = ['Actively Maintained']
|
|
# techniques = ['CDCL']
|
|
publications = ['deMoura2008']
|
|
+++
|
|
|
|
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
|
|
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.
|
|
|
|
## APIs and Bindings
|
|
Z3 is available through several interfaces, making it a convenient option to build into a project.
|
|
|
|
- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
|
|
- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)
|
|
- **.NET API:** [Z3 .NET Namespace Reference](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
|
|
- **Java API:** [Z3 Java API Reference](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
|
|
- **Python bindings:** [z3-solver PyPI package](https://pypi.org/project/z3-solver/) ([Documentation](https://z3prover.github.io/api/html/z3.html))
|
|
- **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3)
|
|
|
|
|