Low-level rust bindings to the Z3 SMT solver
Licensed under the MIT license.
See https://github.com/Z3Prover/z3 for details on Z3.
The API is fully documented with examples: https://docs.rs/z3-sys/
This crate works with Cargo and is on
crates.io.
Add it to your Cargo.toml
like so:
[dependencies]
z3-sys = "0.8"
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.
Note: This crate requires a z3.h
during build time.
- By default, the crate will look for a
z3.h
in standard/system include paths. TheZ3_SYS_Z3_HEADER
environment variable can also be used to customize this. - Enabling the
bundled
feature will cause the bundled copy ofz3.h
to be used. TheZ3_SYS_Z3_HEADER
environment variable can also be used to customize this. - Enabling the
vcpkg
feature will cause the copy ofz3.h
provided by that version to be used. In this case, there is no override via the environment variable.
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.
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.