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. Each backend is behind a feature flag, so for example to use the Z3 binary backend install smtlib by running

cargo add smtlib --features z3

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(())
}

Re-exports

• pub use terms::Sort;
• 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.
• 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

• AsyncSolver
  The AsyncSolver type is the primary entrypoint to interaction with the solver. Checking for validity of a set of assertions requires:
• 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:

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.