This crate provides a generic high-level API for interacting with SMT solvers. The aim of this interface is to be solver-agnostic (i.e. the user can switch between back-end SMT solvers by modifying a single line of code) and to mimic the SMT-LIB standard commands as closely as possible. Currently, Z3 is supported as a back-end. See links below for more information on SMT-LIB and Z3. See tests/test.rs for examples of how to use the interface.
- Rust-SMT-LIB-API requires the latest nightly build of Z3
- Follow the install instructions on the Z3 website (see below)
- Download or clone Rust-SMT-LIB-API
- cd to the root directory of Rust-SMT-LIB-API and run: cargo test
Rust-SMT-LIB-API is MIT licensed, as found in the LICENSE file.