Crate smtlib

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::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, Storage, prelude::*};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let st = Storage::new();

    // 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(&st, Z3Binary::new("z3")?)?;

    // Declare two new variables
    let x = Int::new_const(&st, "x");
    let y = Int::new_const(&st, "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(())
}

Re-exports

pub use terms::Sorted;

pub use smtlib_lowlevel as lowlevel;

pub use theories::core::*;

pub use theories::fixed_size_bit_vectors::*;

pub use theories::ints::*;

pub use theories::reals::*;

Modules

backend

Backends are concrete solvers which can be communicated with using the SMT-LIB language.

funs

Function declarations.

prelude

The prelude module contains the most commonly used types and traits in smtlib. It is recommended to import this module when using smtlib.

sorts

SMT sorts.

terms

Terms are the building blocks for constructing the mathematical expressions used in assertions with Solver.

theories

Theories in SMT-LIB are definitions of sorts and in general functions present in the logics.

Structs

Model

A Model contains the values of all named constants returned through Solver::check_sat_with_model or by calling Solver::get_model.

Solver

The Solver type is the primary entrypoint to interaction with the solver. Checking for validity of a set of assertions requires:

Storage

Enums

Error

An error that occurred during any stage of using smtlib.

Logic

Logics allow specifictation of which (sub-)logic should be used by a solver.

SatResult

The satisfiability result produced by a solver

SatResultWithModel

The satisfiability result produced by a solver, where the Sat variant carries the satisfying model as well.

Traits

Backend

The Backend trait is used to interact with SMT solver using the SMT-LIB language.

Logger