Pat-Lafon/z3.rs

Rust bindings for the Z3 solver.

z3 and z3-sys

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

z3

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.

z3-sys

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

When should I use z3-sys instead of z3?

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.

Release Process

1. Make a version bump commit
   1. Bump version for the relevant crate in Cargo.toml
   2. Update version in examples/READMEs
2. Create a git tag for the commit
   1. i.e. git tag z3-v0.10.0
3. Push the changes
   1. git push
   2. git push --tags
4. Publish on crates.io
   1. cargo publish