9 releases
0.2.0 | May 2, 2024 |
---|---|
0.1.8 | Dec 26, 2023 |
0.1.7 | Nov 15, 2023 |
0.1.6 | Jan 16, 2023 |
0.1.1 | Dec 30, 2022 |
#524 in Algorithms
290KB
5K
SLoC
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, 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(())
}
Dependencies
~3–15MB
~168K SLoC