### 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 |

#**387** in Algorithms

**44** downloads per month

**MIT/Apache**

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

(and `smtlib`

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

## Usage

The primary way to use

is by constructing a `smtlib`

. A solver takes as argument a `smtlib ::`Solver

`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–14MB

~149K SLoC