#smt-solver #smt #bindings

boolector

Safe high-level bindings for the Boolector SMT solver

9 releases

0.4.3 Apr 5, 2022
0.4.2 Jan 7, 2021
0.4.1 Aug 31, 2020
0.4.0 Jul 27, 2020
0.1.1 Sep 16, 2019

#1024 in Algorithms

Download history 30/week @ 2024-11-16 43/week @ 2024-11-23 23/week @ 2024-11-30 33/week @ 2024-12-07 41/week @ 2024-12-14 5/week @ 2024-12-21 3/week @ 2024-12-28 20/week @ 2025-01-04 70/week @ 2025-01-11 104/week @ 2025-01-18 34/week @ 2025-01-25 46/week @ 2025-02-01 32/week @ 2025-02-08 35/week @ 2025-02-15 46/week @ 2025-02-22 89/week @ 2025-03-01

208 downloads per month
Used in 4 crates

MIT license

115KB
1.5K SLoC

boolector

crates.io License

Safe high-level bindings for the Boolector SMT solver, version 3.2.2.

Installation

This crate is on crates.io, so you can simply add it as a dependency in your Cargo.toml:

[dependencies]
boolector = "0.4.3"

This crate relies on the boolector-sys crate, so you will need to follow its directions for installation as well. In particular, you can either:

  • compile and install Boolector 3.2.2 on your system as a shared library; or
  • activate the vendor-lgl feature on this crate, which will automatically build a static Boolector and link to it. E.g.,
    [dependencies]
    boolector = { version = "0.4.3", features = ["vendor-lgl"] }
    

For more details, see the boolector-sys README.

Documentation

Full documentation, including examples, can be found at https://docs.rs/boolector.

Caveats

These bindings are not necessarily complete; there may be some features present in boolector-sys which are not directly exposed here, e.g., uninterpreted functions (boolector_uf()). Contributions are welcome.

This crate currently requires Rust 1.41+.

Dependencies

~4.5MB
~111K SLoC