# [−][src]Crate rsmt2_zz

A wrapper around SMT Lib 2(.5)-compliant SMT solvers.

See `CHANGES.md`

for the list of changes.

If you use this library consider contacting us on the repository so that we can add your project to the readme.

# Description

In rsmt2, solvers run in a separate process and communication is achieved *via* system pipes.
For the moment, only z3 is officially supported. If you would like `rsmt2`

to support
other solvers, please open an issue on the repository.

**NB**: most of the tests and documentation examples in this crate will not work unless you have
z3 in your path under the name `z3`

.

This library does **not** have a structure for S-expressions. It must be provided by the user,
as well as the relevant printing and parsing functions. Printing-related traits are discussed in
the `print`

module, and parsing-related traits are in the `parse`

module.

# Supported Backend Solvers

This crate supports the following solvers:

- z3: full support
- cvc4: full support in theory, but only partially tested. Note that
`get-value`

is known to crash some versions of CVC4. - yices 2: full support in theory, but only partially tested. Command
`get-model`

will only work on Yices 2 >`2.6.1`

, and needs to be activated in SmtConf with`conf.models()`

. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.

# Very basic example

String types already implement `rsmt2`

's SMT-printing traits. It's not a scalable approach, but
it's useful for testing and explaining things. Let's create a solver first.

fn do_smt_stuff() -> ::rsmt2::SmtRes<()> { let parser = () ; use rsmt2::SmtConf ; let solver = SmtConf::z3().spawn(parser) ? ; // Alternatively use rsmt2::Solver ; let _solver = Solver::new(SmtConf::z3(), parser) ? ; // Another alternative, using the default configuration let _solver = Solver::default(parser) ? ; Ok(()) } do_smt_stuff().unwrap()

Notice that all three functions spawning a solver take a parser used to parse identifiers,
values and/or expressions. `rsmt2`

parses everything else (keywords and such), and lets users
handle the important parts. See the `parse`

module documentation for more details.

Our current parser `()`

is enough for this example. We can even perform `check-sat`

s since,
unlike `get-model`

for instance, it does not require any user-data-structure-specific parsing.
Let's declare a few symbols and perform a check-sat.

use rsmt2::Solver ; let mut solver = Solver::default(()) ? ; solver.declare_const("n", "Int") ? ; // ^^^^^^^^^^^^^~~~ same as `declare-fun` for a nullary symbol solver.declare_const("m", "Int") ? ; solver.assert("(= (+ (* n n) (* m m)) 7)") ? ; let is_sat = solver.check_sat() ? ; assert! { ! is_sat }

We already knew there's no pair of integers the sum of the squares of which is equal to `7`

, but
now we **proved** it.

# Parsing things

If we want to be able to retrieve models, we need a parser that can parse two things:
identifiers, types and values. That is, we need a parser that implements
`IdentParser`

(identifiers and types) and `ModelParser`

(values). The previous parser `()`

doesn't, so `solver.get_model()`

won't even compile.

There's different ways to implement these traits, discussed in the `parse`

module
documentation. Let us be lazy and just have rsmt2 do the work for us. Note the (unnecessary) use
of `define_fun`

.

use rsmt2::{ Solver, SmtRes } ; use rsmt2::parse::{ IdentParser, ModelParser } ; #[derive(Clone, Copy)] struct Parser ; // Types ~~~~~~~~~~~~vvvvvv impl<'a> IdentParser<String, String, & 'a str> for Parser { // Idents ~~~~~~~~~^^^^^^ ^^^^^^^^~~~~ Input fn parse_ident(self, input: & 'a str) -> SmtRes<String> { Ok(input.into()) } fn parse_type(self, input: & 'a str) -> SmtRes<String> { Ok(input.into()) } } // Types ~~~~~~~~~~~~~~~~~~vvvvvv vvvvvv~~~~~~~~~~~~~~ Values impl<'a> ModelParser<String, String, String, & 'a str> for Parser { // Idents ~~~~~~~~~^^^^^^ ^^^^^^^^~~~~ Input fn parse_value( self, input: & 'a str, ident: & String, params: & [ (String, String) ], typ: & String, ) -> SmtRes<String> { Ok(input.into()) } } let mut solver = Solver::default(Parser) ? ; solver.define_fun( "sq", & [ ("n", "Int") ], "Int", "(* n n)" // fn sq (n: Int) -> Int { n * n } ) ? ; solver.declare_const("n", "Int") ? ; solver.declare_const("m", "Int") ? ; solver.assert("(= (+ (sq n) (sq m)) 29)") ? ; solver.assert("(and (< n 5) (> n 0) (> m 0))") ? ; let is_sat = solver.check_sat() ? ; assert! { is_sat } let mut model = solver.get_model() ? ; model.sort() ; // Order might vary, sorting for assert below. assert_eq! { model, vec![ ("m".into(), vec![], "Int".into(), "5".into()), ("n".into(), vec![], "Int".into(), "2".into()), ] }

# Asynchronous check-sats.

The check-sat command above is blocking, in that the caller cannot do anything until the backend
solver answers. Using the `print_check_sat...`

and `parse_check_sat...`

functions, users can
issue the check-sat command, work on something else, and get the result later on.

The `print_check_sat...`

functions return a `FutureCheckSat`

required by the
`parse_check_sat...`

functions to guarantee statically that the parse request makes sense.
`FutureCheckSat`

is equivalent to unit and exists only at compile time.

Rewriting the previous example in an asynchronous fashion yields (omitting most of the unmodified code):

solver.define_fun( "sq", & [ ("n", "Int") ], "Int", "(* n n)" ) ? ; solver.declare_const("n", "Int") ? ; solver.declare_const("m", "Int") ? ; solver.assert("(= (+ (sq n) (sq m)) 29)") ? ; solver.assert("(and (< n 5) (> n 0) (> m 0))") ? ; let my_check_sat = solver.print_check_sat() ? ; // Solver is working, we can do other things. let is_sat = solver.parse_check_sat(my_check_sat) ? ; assert! { is_sat }

# Other SMT-LIB 2 commands

Refer to `Solver`

's documentation for the complete list of SMT-LIB 2 commands.

# Activation literals

Module `actlit`

discusses rsmt2's API for *activation literals*, a alternative to
`push`

/`pop`

that's more limited but more efficient.

# Custom data structures

Module `example::simple`

's documentation discusses in detail how to use rsmt2 with
a custom data structure. This includes implementing the print traits and writing a
more evolved parser.

# Print-time information

Module `example::print_time`

's documentation showcases print-time information.
Proper documentation is somewhat lacking as it is a rather advanced topic, and no one asked for
more details about it.

Print-time information is the reason for

- the
`Info`

type parameter in the`...2Smt`

traits, - all the
`..._with`

solver functions, such as`assert_with`

.

Users can call these functions to pass information down to their own printers as commands are
written on the solver's input. The typical use-case is *print-time unrolling* when working with
transition systems. Given a transition relation `T`

over a current and next state `s[0]`

and
`s[1]`

, *unrolling* consists in creating a sequence of states `s[0]`

, `s[1]`

, `s[2]`

, ... such
that `T(s[0], s[1]) and T(s[1], s[2]) and ...`

. Such a sequence is called a *trace*.

Say the state `s`

is some variables `(x, y)`

and the transition relation is `T(s[0], s[1]) = (x[1] == x[0] + 1) && (y[1] == 2 * y[0])`

. Then in SMT-LIB, unrolling `T`

twice looks like

```
(define-fun trans ( (x_0 Int) (y_0 Int) (x_1 Int) (y_1 Int) ) Bool
(and (= x_1 (+ x_0 1)) (= y_1 (* 2 y_0)) )
)
(declare-fun x_0 () Int)
(declare-fun y_0 () Int)
(declare-fun x_1 () Int)
(declare-fun y_1 () Int)
(assert (trans x_0 y_0 x_1 y_1))
(declare-fun x_2 () Int)
(declare-fun y_2 () Int)
(assert (trans x_1 y_1 x_2 y_2))
```

In a model-checker, at each point of the unrolling one wants to (conditionally) assert terms about a state, or a pair of succeeding states, but never more. Also, the "same" term will typically be asserted for many different states / pair of states.

Notice that if we want to assert `P(s) = x > 0`

for `s[0]`

and `s[1]`

, then in theory we have to
create two terms `x_0 > 0`

and `x_1 > 0`

. By extension, these are called *unrollings* of `P`

.
Now, these terms can end up being pretty big, and memory can become a problem, even with
hashconsing.

Creating a different term for each unrolling of `P`

, asserting it, and then (usually) discarding
them right away is not practical time- and memory-wise. It is better if the term structure has a
notion of "current `x`

" (`x_0`

) and "next `x`

" (`x_1`

), and to decide how to print them *at
print-time* by passing an *offset* that's essentially an integer. It represents the offset for
the "current" state.

So, from the term `x_1 > x_0`

for instance, passing an offset of `3`

to the printer would cause
`x_0`

to be printed as `x_3`

and `x_1`

as `x_4`

. Without creating anything, just from the
original term.

This is the workflow showcased (but only partially explained) by
`example::print_time`

.

## Re-exports

`pub use crate::errors::SmtRes;` |

## Modules

actlit | Activation literal type and helpers. |

errors | Errors. |

example | A few examples of using rsmt2. |

future | Promises for future results on ongoing computations. |

parse | SMT Lib 2 result parsers. |

Traits your types must implement so that |

## Structs

SmtConf | Configuration and solver specific info. |

Solver | Solver providing most of the SMT-LIB 2.5 commands. |

## Enums

Logic | SMT Lib 2 logics. |

SmtStyle | Solver styles. |