Crate rsmt2 [−] [src]

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.

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-sats 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 ValueParser (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, ValueParser } ;

#[derive(Clone, Copy)]
struct Parser ;

  //       Types ~~~~~~~~~~~~vvvvvv
impl<'a> IdentParser<String, String, & 'a str> for Parser {
  // Identifiers ~~~~^^^^^^          ^^^^^^^^~~~~ 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())
  }
}

impl<'a> ValueParser<String, & 'a str> for Parser {
  // Values ~~~~~~~~~^^^^^^  ^^^^^^^^~~~~ Input
  fn parse_value(self, input: & 'a str) -> 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 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.
print	Traits your types must implement so that `rsmt2` can use them.

Structs

SmtConf	Configuration and solver specific info.
Solver	Solver providing most of the SMT-LIB 2.5 commands.

Enums

Logic

SMT Lib 2 logics.