This repository contains high-level and low-level Rust bindings for the Z3 solver.

The z3 crate provides high-level bindings to the Z3 solver. It is built on top of, and wraps, the z3-sys crate. This is the crate you'll want to use 99% of the time.

The z3-sys crate provides the raw, unsafe, low-level C API that Z3 exposes.

The z3-src crate contains the Z3 source distribution and logic to handle vendored builds.

Starting with version 0.20.0, z3-rs aims to track the latest Z3 release and stay up-to-date with API changes.

Function and opaque structure FFI bindings were generated and committed sometime around Z3 4.8.12 and updated ad-hoc, but enum bindings were re-generated via bindgen on every build. This let the enums track whatever Z3 version was linked, giving broad 4.8.12–4.16.0 support. The cost was that new high-level Z3 APIs could not easily be defined without feature-gating, and were often omitted entirely.

Both functions and enums are tracked in version control (z3-sys/src/generated/functions.rs and z3-sys/src/generated/enums.rs). There is by default no dynamic bindgen step on every build. The minimum supported upstream Z3 version is 4.16.0.

FFI bindings can be regenerated for new Z3 versions by running cargo xtask gen-bindings.

Users who wish to generate FFI bindings at build-time for their system's Z3 can build with the bindgen feature enabled; note though that while the low-level bindings may work, the high-level bindings will not be able to link against (old) versions of z3 that do not export the necessary symbols.

The first scenario where it makes sense to use z3-sys directly is when some Z3 feature isn't wrapped into high-level bindings in the z3 crate yet. In this case, it is worth filing an issue and discussing its implementation in the z3 crate, but you can get at the raw, underlying features via the z3-sys crate in the meantime.

The only other time to use z3-sys directly would be if you are writing your own custom high-level API for Z3, instead of using the z3 crate.