This Rust crate provides low-level bindings for the Boolector SMT solver, version 3.2.2.

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

[dependencies]
boolector-sys = "0.7.2"

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

[dependencies]
boolector-sys = { version = "0.7.2", features = ["vendor-lgl"] }

Enabling vendor-lgl will automatically build a static boolector library and link against it. Currently this uses the Lingeling 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.

This crate is licensed under the MIT license.