smtlib

A high-level API for interacting with SMT solvers

If you are looking for more control and less ergonomics, take a look at the low-level crate smtlib-lowlevel for construct SMT-LIB code and talking directly with SMT solvers.

Background

Satisfiability modulo theories (SMT) is the problem of determining whether or not a mathematical formula is satisfiable. SMT solvers (such as Z3 and cvc5) are programs to automate this process. These are fantastic tools which are very powerful and can solve complex problems efficiently.

To communicate with the solvers, the SMT-LIB specification has been made to standardize the input/output language to all of the solvers.

Writing this format by-hand (or "programmatically by-hand") can at times be tedious and error prone. Even more so is interpreting the result produced by the solvers.

Thus the goal of smtlib (and smtlib-lowlevel) is to provide ergonomic API's for communicating with the solvers, independent of the concrete solver.

Usage

The primary way to use smtlib is by constructing a smtlib::Solver. A solver takes as argument a smtlib::Backend. To see which backends are provided with the library check out the smtlib::backend module. Some backend is behind a feature flag, so for example to use the Z3 statically backend install smtlib by running cargo add smtlib -F z3-static, but otherwise add it by running:

cargo add smtlib

Now you can go ahead and use the library in your project.

use smtlib::{backend::Z3Binary, Int, SatResultWithModel, Solver, Sort};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Initialize the solver with the Z3 backend. The "z3" string refers the
    // to location of the already installed `z3` binary. In this case, the
    // binary is in the path.
    let mut solver = Solver::new(Z3Binary::new("z3")?)?;

    // Declare two new variables
    let x = Int::from_name("x");
    let y = Int::from_name("y");

    // Assert some constraints. This tells the solver that these expressions
    // must be true, so any solution will satisfy these.
    solver.assert(x._eq(y + 25))?;
    solver.assert(x._eq(204))?;
    // The constraints are thus:
    // - x == y + 25
    // - x == 204
    // Note that we use `a._eq(b)` rather than `a == b`, since we want to
    // express the mathematical relation of `a` and `b`, while `a == b` checks
    // that the two **expressions** are structurally the same.

    // Check for validity
    match solver.check_sat_with_model()? {
        SatResultWithModel::Sat(model) => {
            // Since it is valid, we can extract the possible values of the
            // variables using a model
            println!("x = {}", model.eval(x).unwrap());
            println!("y = {}", model.eval(y).unwrap());
        }
        SatResultWithModel::Unsat => println!("No valid solutions found!"),
        SatResultWithModel::Unknown => println!("Satisfaction remains unknown..."),
    }

    Ok(())
}