Crate rsmt2

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. for declare-fun),
• symbols: Sym2Smt trait (e.g. for declare-fun),
• expressions: Expr2Smt trait (e.g. for assert).

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 IoErrors and (not-early-)returns the first error, if any.
smtry_io	Wraps errors (if any) into IoErrors and early-returns.

Structs

Error	The Error type.
Kid	A solver Child.
PlainSolver	Plain solver, as opposed to TeeSolver which logs IOs.
SolverConf	Configuration and solver specific info.
TeeSolver	Wrapper around a PlainSolver logging IOs to a file.

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 Result, for easy interaction with this crate.
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 std::Result.