Rust-SMT-LIB-API

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.

Installing z3

• Rust-SMT-LIB-API requires the latest nightly build of Z3
• Follow the install instructions on the Z3 website (see below)

Building

• Download or clone Rust-SMT-LIB-API
• cd to the root directory of Rust-SMT-LIB-API and run: cargo test

Additional links

• SMT-LIB standard and documentation.
• Z3 SMT solver.

License

Rust-SMT-LIB-API is MIT licensed, as found in the LICENSE file.