#smt-solver #smt #low-level #ffi #bitwuzla

sys bitwuzla-sys

Low-level bindings for the Bitwuzla SMT solver

3 unstable releases

0.2.0 Jul 26, 2022
0.1.1 Nov 25, 2021
0.1.0 Nov 25, 2021

#1426 in Algorithms

Download history 12/week @ 2023-12-18 1/week @ 2024-02-12 34/week @ 2024-02-19 40/week @ 2024-02-26 18/week @ 2024-03-04 28/week @ 2024-03-11 1/week @ 2024-03-18 35/week @ 2024-04-01

66 downloads per month

MIT license

4MB
115K SLoC

C 80K SLoC // 0.1% comments C++ 31K SLoC // 0.0% comments Rust 1.5K SLoC Cython 1K SLoC // 0.5% comments Python 813 SLoC // 0.2% comments Shell 527 SLoC // 0.3% comments

crates.io docs.rs

bitwuzla-sys

This Rust crate provides low-level bindings for the Bitwuzla SMT solver.

Installation

Using shared bitwuzla library

Compile bitwuzla as a shared library and install it. Then add this crate to your Cargo.toml:

[dependencies]
bitwuzla-sys = "0.2"

Using vendored static bitwuzla library

This is possible on UNIX-like targets only. Add this crate to your Cargo.toml with the vendor-cadical feature enabled:

[dependencies]
bitwuzla-sys = { version = "0.2", features = ["vendor-cadical"] }

Enabling vendor-cadical will automatically build a static bitwuzla library and link against it. Currently this uses the CaDiCaL SAT solver.

In order for the build to succeed, you'll need to install some tools on your build host; for a Debian-based distribution build-essential, cmake, curl, and git should be sufficient.

License

This crate is licensed under the MIT license.

Dependencies