### 6 releases

0.2.2 | Aug 2, 2024 |
---|---|

0.2.1 | Sep 5, 2023 |

0.2.0 | Aug 15, 2023 |

0.1.2 | Jun 1, 2023 |

0.1.0 | Jan 27, 2023 |

#**106** in Algorithms

**581** downloads per month

Used in **2** crates

**MIT/Apache**

55KB

1.5K
SLoC

## About

is a crate for interacting with an SMT solver subprocess. This crate
provides APIs for`easy-smt`

- building up expressions and assertions using the SMT-LIB 2 language,
- querying an SMT solver for solutions to those assertions,
- and inspecting the solver's results.

works with any solver, as long as the solver has an interactive REPL
mode. You just tell `easy-smt`

how to spawn the subprocess.`easy-smt`

## Example

`use` `easy_smt``::``{`ContextBuilder`,` Response`}``;`
`fn` `main``(``)`` ``->` `std``::``io``::``Result``<``(``)``>` `{`
`//` Create a new context, backed by a Z3 subprocess.
`let` `mut` ctx `=` `ContextBuilder``::`new`(``)`
`.``solver``(``"`z3`"``,` `[``"`-smt2`"``,` `"`-in`"``]``)`
`.``build``(``)``?``;`
`//` Declare `x` and `y` variables that are bitvectors of width 32.
`let` bv32 `=` ctx`.``bit_vec_sort``(`ctx`.``numeral``(``32``)``)``;`
`let` x `=` ctx`.``declare_const``(``"`x`"``,` bv32`)``?``;`
`let` y `=` ctx`.``declare_const``(``"`y`"``,` bv32`)``?``;`
`//` Assert that `x * y = 18`.
ctx`.``assert``(`ctx`.``eq``(`
ctx`.``bvmul``(`x`,` y`)``,`
ctx`.``binary``(``32``,` `18``)``,`
`)``)``?``;`
`//` And assert that neither `x` nor `y` is 1.
ctx`.``assert``(`ctx`.``not``(`ctx`.``eq``(`x`,` ctx`.``binary``(``32``,` `1``)``)``)``)``?``;`
ctx`.``assert``(`ctx`.``not``(`ctx`.``eq``(`y`,` ctx`.``binary``(``32``,` `1``)``)``)``)``?``;`
`//` Check whether the assertions are satisfiable. They should be in this example.
`assert_eq!``(`ctx`.``check``(``)``?``,` `Response``::`Sat`)``;`
`//` Print the solution!
`let` solution `=` ctx`.``get_value``(``vec!``[`x`,` y`]``)``?``;`
`for` `(`variable`,` value`)` `in` solution `{`
`println!``(``"``{}` = `{}``"``,` ctx`.``display``(`variable`)``,` ctx`.``display``(`value`)``)``;`
`}`
`//` There are many solutions, but the one I get from Z3 is:
`//`
`//` x = #x10000012
`//` y = #x38000001
`//`
`//` Solvers are great at finding edge cases and surprising-to-humans results! In
`//` this case, I would have naively expected something like `x = 2, y = 9` or
`//` `x = 3, y = 6`, but the solver found a solution where the multiplication
`//` wraps around. Neat!
`Ok``(``(``)``)`
`}`

## Debugging

### Displaying S-Expressions

Want to display an S-Expression that you've built up to make sure it is what you
expect? You can use the

method:`easy_smt ::`

`Context`display

`::``use` `easy_smt``::`ContextBuilder`;`
`let` ctx `=` `ContextBuilder``::`new`(``)``.``build``(``)``.``unwrap``(``)``;`
`let` my_s_expr `=` ctx`.``list``(``vec!``[`
ctx`.``atom``(``"`hi`"``)``,`
ctx`.``atom``(``"`hello`"``)``,`
ctx`.``numeral``(``42``)``,`
`]``)``;`
`let` string `=` `format!``(``"``{}``"``,` ctx`.``display``(`my_s_expr`)``)``;`
`assert_eq!``(`string`,` `"`(hi hello 42)`"``)``;`

### Logging Solver Interactions

Need to debug exactly what is being sent to and received from the underlying
solver?

uses the `easy-smt`

crate and logs all communication with the
solver at the `log`

log level.`TRACE`

For example, you can use

to see the log messages. Initialize the
logger at the start of `env_logger`

:`main`

`fn` `main``(``)`` ``{`
`env_logger``::`init`(``)``;`
`//` ...
`}`

And then run your program with the

environment
variable set to see the `RUST_LOG``=``"`easy_smt=trace`"`

logs:`TRACE`

`$`` RUST_LOG=``"`easy_smt=trace`"` cargo run` --`example sudoku
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (set-option :print-success true)
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (set-option :produce-models true)
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (set-option :produce-unsat-cores true)
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (declare-fun cell_0_0 () `Int`)
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (assert (and (`>` cell_0_0 0) `(``<=` `cell_0_0`` 9``)`))
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (declare-fun cell_0_1 () `Int`)
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] -``>` (assert (and (`>` cell_0_1 0) `(``<=` `cell_0_1`` 9``)`))
`[2023-01-09T23:41:05Z`` TRACE easy_smt::solver] ``<``-` success
`...`

### Replaying Solver Interactions

You can save all commands that are being sent to the solver to a file that you can replay without needing to dynamically rebuild your expressions, assertions, and commands.

`use` `easy_smt``::`ContextBuilder`;`
`fn` `main``(``)`` ``->` `std``::``io``::``Result``<``(``)``>` `{`
`let` ctx `=` `ContextBuilder``::`new`(``)`
`//` Everything needed to replay the solver session will be written
`//` to `replay.smt2`.
`.``replay_file``(``Some``(``std``::``fs``::``File``::`create`(``"`replay.smt2`"``)``?``)``)`
`.``solver``(``"`z3`"``,` `[``"`-smt2`"``,` `"`-in`"``]``)`
`.``build``(``)``?``;`
`//` ...
`Ok``(``(``)``)`
`}`

## Inspiration

Inspired by the

haskell package.`simple-smt`

#### Dependencies

~640KB