21 releases (12 breaking)
new 0.13.1 | Jul 11, 2025 |
---|---|
0.12.1 | Jul 25, 2023 |
0.11.2 | Aug 24, 2021 |
0.11.1 | Jul 21, 2021 |
0.1.0 | Dec 28, 2015 |
#46 in Algorithms
8,875 downloads per month
Used in 26 crates
(19 directly)
525KB
7K
SLoC
z3
High-level rust bindings to the Z3 SMT solver
Licensed under the MIT license.
See https://github.com/Z3Prover/z3 for details on Z3.
Documentation
The API is fully documented with examples: https://docs.rs/z3/
Installation
This crate works with Cargo and is on
crates.io.
Add it to your project with cargo add
:
$ cargo add z3
Finding Z3 Libraries
Note: This library has a dependency on Z3.
There are 3 ways for this crate to currently find Z3:
- By default, it will look for a system-installed copy of Z3.
On Linux, this would be via the package manager. On macOS, this
might be via Homebrew (
brew install z3
). - Enabling the
bundled
feature will usecmake
to build a locally bundled copy of Z3. This copy is provided via a git submodule within the repository. - Enabling the
vcpkg
feature will usevcpkg
to build and install a copy of Z3 which is then used. - Enabling the
gh-release
feature will download a pre-compiled copy of Z3 from the GitHub release page for the current platform, if available. You may specify the version of Z3 to download via theZ3_SYS_Z3_VERSION
environment variable.
This might look like:
[dependencies]
z3 = {version="0", features = ["bundled"]}
or:
[dependencies]
z3 = {version="0", features = ["vcpkg"]}
Support and Maintenance
I am developing this library largely on my own so far. I am able to offer support and maintenance, but would very much appreciate donations via Patreon. I can also provide commercial support, so feel free to contact me.
Contribution
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, shall be dual licensed as above, without any additional terms or conditions.
Dependencies
~0.4–4MB
~75K SLoC