Facebook releases Rust-SMT-LIB-API

An API that can be used to expose an SMT-LIB compliant SMT solver to a developer tool written in Rust. 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.


Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s