Crate rsmt2 [−] [src]
A wrapper around an SMT Lib 2(.5)-compliant SMT solver.
Solvers run in a separate process and communication is achieved via system pipes.
This library does not have a structure for S-expressions. It should be provided by the user, as well as the relevant printing and parsing functions.
async
versus sync
The functions corresponding to SMT Lib 2 queries come in two flavors, asynchronous and synchronous.
Synchronous means that the query is printed on the solver's stdin, and the result is parsed right away. Users get control back whenever the solver is done working and parsing is done. In other words, synchronous queries are blocking.
Asynchronous means that after the query is printed and control is given back
to the user. To retrieve the result, users must call the relevant parse_...
function. For instance, parse_sat
for check_sat
.
In other words, asynchronous queries are non-blocking. Not that parse_...
functions are blocking though.
The example below uses synchronous queries.
Workflow
The worflow is introduced below on a running example. It uses a structure for S-expressions representing the unrolling of some predicates over discrete time-steps.
N.B. this example is very naïve and should not be used as is.
S-expressions are defined as follows:
/// Under the hood a symbol is a string. type Sym = String ; /// A variable wraps a symbol. #[derive(Debug,Clone,PartialEq)] enum Var { /// Variable constant in time (Non-Stateful Var: SVar). NSVar(Sym), /// State variable in the current step. SVar0(Sym), /// State variable in the next step. SVar1(Sym), } /// A constant. #[derive(Debug,Clone,PartialEq)] enum Const { /// Boolean constant. BConst(bool), /// Integer constant. IConst(usize), /// Rational constant. RConst(usize,usize), } /// An S-expression. #[derive(Debug,Clone,PartialEq)] enum SExpr { /// A variable. Id(Var), /// A constant. Val(Const), /// An application of function symbol. App(Sym, Vec<SExpr>), }
We then use Offset
to specify what the index of the current and next step
are:
/// An offset gives the index of current and next step. #[derive(Debug,Clone,Copy,PartialEq)] struct Offset(usize, usize) ; /// A symbol is a variable and an offset. #[derive(Debug,Clone,PartialEq)] struct Symbol<'a, 'b>(& 'a Var, & 'b Offset) ; /// An unrolled SExpr. #[derive(Debug,Clone,PartialEq)] struct Unrolled<'a, 'b>(& 'a SExpr, & 'b Offset) ;
Print functions
Since the structure for S-expressions is provided by the users, they also need to provide functions to print it in SMT Lib 2.
To use all SMT Lib 2 commands in a type-safe manner, the library requires printers over
- sorts:
Sort2Smt
trait (e.g. fordeclare-fun
), - symbols:
Sym2Smt
trait (e.g. fordeclare-fun
), - expressions:
Expr2Smt
trait (e.g. forassert
).
The last two are parameterized by a Type for the information at print time. Commands using the user's structure for printing are enriched with a field to pass information down to the printer.
For convenience, all these traits are implemented for & str
. This is useful
for testing and maybe very simple application.
In our example, printing a symbol / an expression requires an offset. The idea
is that Symbol
(Unrolled
) will implement Sym2Smt
(Expr2Smt
). For sorts
we will use & str
for simplicity.
We begin by writing printing functions taking an offset for our structure, as well as simple helper funtions:
#[macro_use] extern crate rsmt2 ; use std::io::Write ; use rsmt2::* ; use Var::* ; use Const::* ; use SExpr::* ; impl Var { pub fn nsvar(s: & str) -> Self { NSVar(s.to_string()) } pub fn svar0(s: & str) -> Self { SVar0(s.to_string()) } pub fn svar1(s: & str) -> Self { SVar1(s.to_string()) } /// Given an offset, a variable can be printed in SMT Lib 2. #[inline(always)] pub fn to_smt2(& self, writer: & mut Write, off: & Offset) -> Res<()> { smt_cast_io!( "writing a variable" => match * self { NSVar(ref sym) => write!(writer, "|{}|", sym), /// SVar at 0, we use the index of the current step. SVar0(ref sym) => write!(writer, "|{}@{}|", sym, off.0), /// SVar at 1, we use the index of the next step. SVar1(ref sym) => write!(writer, "|{}@{}|", sym, off.1), } ) } /// Given an offset, a variable can become a Symbol. pub fn to_sym<'a, 'b>(& 'a self, off: & 'b Offset) -> Symbol<'a, 'b> { Symbol(self, off) } } impl Const { /// A constant can be printed in SMT Lib 2. #[inline(always)] pub fn to_smt2(& self, writer: & mut Write) -> Res<()> { smt_cast_io!( "writing a constant" => match * self { BConst(ref b) => write!(writer, "{}", b), IConst(ref i) => write!(writer, "{}", i), RConst(ref num, ref den) => write!(writer, "(/ {} {})", num, den), } ) } } impl SExpr { pub fn app(sym: & str, args: Vec<SExpr>) -> Self { App(sym.to_string(), args) } /// Given an offset, an S-expression can be printed in SMT Lib 2. pub fn to_smt2(& self, writer: & mut Write, off: & Offset) -> Res<()> { match * self { Id(ref var) => var.to_smt2(writer, off).chain_err( || "while writing an identifier" ), Val(ref cst) => cst.to_smt2(writer).chain_err( || "while writing a plain value" ), App(ref sym, ref args) => { smtry_io!( "writing an application (symbol)" => write!(writer, "({}", sym) ) ; for ref arg in args { smtry_io!( "writing an application (args)" => write!(writer, " ") ; arg.to_smt2(writer, off) ) } ; smt_cast_io!( "writing an application (trailer)" => write!(writer, ")") ) } } } /// Given an offset, an S-expression can be unrolled. pub fn unroll<'a, 'b>(& 'a self, off: & 'b Offset) -> Unrolled<'a,'b> { Unrolled(self, off) } }
It is now easy to implement Sym2Smt
and Expr2Smt
:
/// A symbol can be printed in SMT Lib 2. impl<'a, 'b> Sym2Smt<()> for Symbol<'a,'b> { fn sym_to_smt2(& self, writer: & mut Write, _: & ()) -> Res<()> { self.0.to_smt2(writer, self.1) } } /// An unrolled SExpr can be printed in SMT Lib 2. impl<'a, 'b> Expr2Smt<()> for Unrolled<'a,'b> { fn expr_to_smt2(& self, writer: & mut Write, _: & ()) -> Res<()> { self.0.to_smt2(writer, self.1) } }
Before writing the parsers...
...we can actually already test our structure. To create a solver, one must
give an implementation of ParseSmt2
. But we can define a dummy parser as long
as we don't actually need to parse anything specific to our structure.
That is, as long as we only use the check-sat
and check-sat-assuming
queries. On the other hand, we will not be able to call, say, get-model
for
now because then we would need to provide a parser for symbols and values.
So, we define a dummy parser for now and perform a check-sat
:
// Parser library. #[macro_use] extern crate nom ; #[macro_use] extern crate rsmt2 ; use nom::IResult ; /// Dummy parser. struct Parser ; impl ParseSmt2 for Parser { type Ident = Var ; type Value = Const ; type Expr = SExpr ; type Proof = () ; type I = () ; fn parse_ident<'a>( & self, array: & 'a [u8] ) -> IResult<& 'a [u8], Var> { panic!("not implemented") } fn parse_value<'a>( & self, array: & 'a [u8] ) -> IResult<& 'a [u8], Const> { panic!("not implemented") } fn parse_expr<'a>( & self, array: & 'a [u8], _: & () ) -> IResult<& 'a [u8], SExpr> { panic!("not implemented") } fn parse_proof<'a>( & self, _: & 'a [u8] ) -> IResult<& 'a [u8], ()> { panic!("not implemented") } } /// Convenience macro. macro_rules! smtry { ($e:expr, failwith $( $msg:expr ),+) => ( match $e { Ok(something) => something, Err(e) => panic!( $($msg),+ , e) } ) ; } fn main() { use rsmt2::* ; let conf = SolverConf::z3() ; let mut kid = match Kid::mk(conf) { Ok(kid) => kid, Err(e) => panic!("Could not spawn solver kid: {:?}", e) } ; { let mut solver = smtry!( solver(& mut kid, Parser), failwith "could not create solver: {:?}" ) ; let nsv = Var::nsvar("non stateful var") ; let s_nsv = Id(nsv.clone()) ; let sv_0 = Var::svar0("stateful var") ; let s_sv_0 = Id(sv_0.clone()) ; let app2 = SExpr::app("not", vec![ s_sv_0.clone() ]) ; let app1 = SExpr::app("and", vec![ s_nsv.clone(), app2.clone() ]) ; let offset1 = Offset(0,1) ; let sym = nsv.to_sym(& offset1) ; smtry!( solver.declare_fun(& sym, &[], & "bool", & ()), failwith "declaration failed: {:?}" ) ; let sym = sv_0.to_sym(& offset1) ; smtry!( solver.declare_fun(& sym, &[], & "bool", & ()), failwith "declaration failed: {:?}" ) ; let expr = app1.unroll(& offset1) ; smtry!( solver.assert(& expr, & ()), failwith "assert failed: {:?}" ) ; match smtry!( solver.check_sat(), failwith "error in checksat: {:?}" ) { true => (), false => panic!("expected sat, got unsat"), } } smtry!( kid.kill(), failwith "error while killing solver: {:?}" ) ; }
Parsing
This library uses the nom
parser combinator library. Users can
use whatever they want as long as they implement the ParseSmt2
trait.
Note that there is no reason a priori for the structures returned by the
parsers to be the same as the one used for printing. In our running example,
parsing a variable with an offset of 6
(in a get-values
for example) as
an SExpr
is ambiguous. Is 6
the index of the current or next step? What's
the other index?
For this simple example however, we will use the same structures. Despite the fact that it makes little sense.
Unfortunately writing the code as a (tested) documentation comment does not
work currently. The nom
macros recurse quite deeply and the thread for the
test overflows its stack. I do not know how to fix this. Please contact me if
you do.
The implementation of the parser, as well as an example using get-model
and
get-values
are written as a private test/example directly in the source. You
can view it here.
Modules
internals |
Internal traits used to build solvers. |
Macros
smt_cast_io |
Wraps errors (if any) into |
smtry_io |
Wraps errors (if any) into |
Structs
Error |
The Error type. |
Kid |
A solver |
PlainSolver |
Plain solver, as opposed to |
SolverConf |
Configuration and solver specific info. |
TeeSolver |
Wrapper around a |
Enums
ErrorKind |
The kind of an error. |
Logic |
SMT Lib 2 logics. |
SolverStyle |
Solver styles. |
Traits
Expr2Smt |
An expression printable in the SMT Lib 2 standard given some info. |
ParseSmt2 |
Parsers on the user's structure. |
Query |
Prints queries. |
QueryExpr |
Queries with expr printing. |
QueryExprInfo |
Queries with expr printing and related print/parse information. |
QueryIdent |
Queries with ident printing. |
ResExt |
Additional methods for |
Solver |
Provides SMT-LIB commands that are not queries. |
Sort2Smt |
A sort printable in the SMT Lib 2 standard. |
Sym2Smt |
A symbol printable in the SMT Lib 2 standard given some info. |
Functions
solver |
Creates a solver from a kid. |
Type Definitions
ConfItem |
A configuration item is either a keyword or unsupported. |
Res |
Convenient wrapper around |