Expand description
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. This means that to use a solver, it needs to be available as a binary in your path. For the moment, only z3 is officially supported, although there is experimental support for cvc4 and yices 2.
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.
Note on 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 withSmtConf::models
. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.
Since solver run as system processes on the end-user’s system, it is hard to make any assumption
regarding the command that will run a particular solver. For this reason you should make sure
you allow your users to pass command that specifies how to run a given solver.You can take a
look at the custom_cmd
example for guidance.
Note that the command for each solver can be passed through environment variables, see
- the
conf
module for general information, conf::Z3_ENV_VAR
,conf::CVC4_ENV_VAR
,conf::YICES_2_ENV_VAR
, and- the
conf::SmtConf::z3_or_env
,conf::SmtConf::cvc4_or_env
, andconf::SmtConf::yices_2_or_env
constructors.
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.
This is typically done by creating an SmtConf
solver configuration. This
configuration lets rsmt2 know which solver you plan on using, as well as override the command
used to launch it or activate model production.
let parser = ();
use rsmt2::SmtConf;
let conf = SmtConf::default_z3();
let mut solver = conf.spawn(parser).unwrap();
let is_sat = solver.check_sat().unwrap();
assert!(is_sat)
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_z3(())?;
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 calls to
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 Solver::define_fun
.
use rsmt2::{ Solver, SmtRes };
use rsmt2::parse::{ IdentParser, ModelParser };
#[derive(Clone, Copy)]
struct Parser;
impl<'a> IdentParser<String, String, & 'a str> for Parser {
// Idents ~~~~~~~^^^^^^ ^^^^^^ ^^^^^^^^~~~~ Input
// Types ~~~~~~~~~~~~|
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> ModelParser<String, String, String, & 'a str> for Parser {
// Idents ~~~~~~~^^^^^^ ^^^^^^ ^^^^^^ ^^^^^^^^~~~~ Input
// Types ~~~~~~~~| |~~~~~ Values
fn parse_value(
self, input: & 'a str,
ident: & String, params: & [ (String, String) ], typ: & String,
) -> SmtRes<String> {
Ok(input.into())
}
}
let mut solver = Solver::default_z3(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 on Solver
,
users can issue the check-sat command, work on something else, and get the result later on.
The print_check_sat...
Solver
functions return a
FutureCheckSat
required by the parse_check_sat...
Solver
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 Solver::push
and Solver::pop
that’s more limited but more efficient.
Custom data structures
Examples in the examples
module discusses in detail how to use rsmt2 with a
custom data structure. This includes implementing the print traits and writing a
more evolved parser. Examples are only visible if the examples
features is active.
Print-Time Information Passing
The print_time
example in examples
showcases print-time
information-passing. 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 asSolver::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 print_time
in
examples
.
Asynchronous check-sat-s
See the asynch
module and Solver::async_check_sat_or_unk
.
Re-exports
Modules
Activation literal type and helpers.
This modules handles asynchronous interactions with the solver.
Solver configuration, contains backend-solver-specific info.
Errors.
A few examples of using rsmt2.
Promises for future results on ongoing computations.
SMT-LIB 2 result parsers.
Common rsmt2 type and helpers.
Traits your types must implement so that rsmt2 can use them.
Structs
Solver providing most of the SMT-LIB 2.5 commands.
Enums
SMT-LIB 2 logics, used with Solver::set_logic
.