#smt-solver #solver #smt #satisfiability

sys z3-sys

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

13 releases (7 breaking)

0.8.1 Jul 25, 2023
0.7.1 Aug 24, 2021
0.7.0 Jul 21, 2021
0.6.3 Oct 29, 2020
0.1.0 Dec 28, 2015

#2378 in Algorithms

Download history 1196/week @ 2024-07-21 1505/week @ 2024-07-28 1194/week @ 2024-08-04 1406/week @ 2024-08-11 1362/week @ 2024-08-18 1247/week @ 2024-08-25 1640/week @ 2024-09-01 1773/week @ 2024-09-08 1845/week @ 2024-09-15 2374/week @ 2024-09-22 1634/week @ 2024-09-29 1712/week @ 2024-10-06 1495/week @ 2024-10-13 1781/week @ 2024-10-20 1605/week @ 2024-10-27 1452/week @ 2024-11-03

6,519 downloads per month
Used in 33 crates (8 directly)

MIT license

20MB
424K 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 C 5.5K SLoC // 0.2% comments TypeScript 4.5K SLoC // 0.2% comments OCaml 3K SLoC // 0.4% comments Rust 2K SLoC // 0.0% comments Jupyter Notebooks 384 SLoC // 0.3% comments D 365 SLoC // 0.1% comments Visual Studio Project 137 SLoC Visual Studio Solution 125 SLoC Batch 86 SLoC Shell 46 SLoC // 0.2% comments JavaScript 37 SLoC // 0.1% comments

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.8"

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.
  • If the feature static-link-z3 is enabled, the z3.h of the built Z3 will be used.
  • Alternatively, the path to the desired z3.h can be specified via the environment variable Z3_SYS_Z3_HEADER. I.e., running:
$ Z3_SYS_Z3_HEADER="/path/to/my/z3.h" cargo build

in your project will use /path/to/my/z3.h instead.

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