#ffi #smt #satisfiability #solver

sys z3-sys

Low-level bindings for the Z3 SMT solver from Microsoft Research

10 releases (6 breaking)

0.7.0 Jul 21, 2021
0.6.3 Oct 29, 2020
0.6.2 Jun 29, 2020
0.5.0 Aug 29, 2019
0.1.0 Dec 28, 2015

#130 in Math

Download history 973/week @ 2021-04-08 931/week @ 2021-04-15 609/week @ 2021-04-22 722/week @ 2021-04-29 1257/week @ 2021-05-06 846/week @ 2021-05-13 1487/week @ 2021-05-20 879/week @ 2021-05-27 1069/week @ 2021-06-03 822/week @ 2021-06-10 1145/week @ 2021-06-17 1042/week @ 2021-06-24 713/week @ 2021-07-01 1281/week @ 2021-07-08 2198/week @ 2021-07-15 931/week @ 2021-07-22

4,652 downloads per month
Used in 17 crates (6 directly)

MIT license

300KB
2K SLoC

z3-sys

Low-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-sys/

Installation

This crate works with Cargo and is on crates.io. Add it to your Cargo.toml like so:

[dependencies]
z3-sys = "0.7.0"

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–1.4MB
~30K SLoC