19 releases (11 breaking)

Uses old Rust 2015

0.12.1 Jul 25, 2023
0.11.2 Aug 24, 2021
0.11.1 Jul 21, 2021
0.10.0 Mar 23, 2021
0.1.0 Dec 28, 2015

#61 in Algorithms

Download history 1137/week @ 2024-03-13 1215/week @ 2024-03-20 944/week @ 2024-03-27 1503/week @ 2024-04-03 949/week @ 2024-04-10 1110/week @ 2024-04-17 1380/week @ 2024-04-24 1071/week @ 2024-05-01 863/week @ 2024-05-08 1764/week @ 2024-05-15 1148/week @ 2024-05-22 1164/week @ 2024-05-29 989/week @ 2024-06-05 1237/week @ 2024-06-12 1102/week @ 2024-06-19 812/week @ 2024-06-26

4,281 downloads per month
Used in 13 crates (11 directly)

MIT license

20MB
428K SLoC

C++ 371K SLoC // 0.1% comments Python 16K SLoC // 0.3% comments C# 12K SLoC // 0.4% comments Java 10K SLoC // 0.4% comments Rust 6.5K SLoC // 0.0% comments C 5.5K SLoC // 0.2% comments TypeScript 4.5K SLoC // 0.2% comments OCaml 3K SLoC // 0.4% comments Jupyter Notebooks 383 SLoC // 0.3% comments D 364 SLoC // 0.1% comments Visual Studio Project 136 SLoC Visual Studio Solution 124 SLoC Batch 85 SLoC Shell 45 SLoC // 0.2% comments JavaScript 36 SLoC // 0.1% comments

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 Cargo.toml like so:

[dependencies]
z3 = "0.12"

Note: This library has a dependency on Z3. You will either need to have the Z3 dependency already installed, or you can statically link to our build of Z3 like so:

[dependencies]
z3 = {version="0.12", features = ["static-link-z3"]}

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