Crate rsmt2 [−] [src]

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

See CHANGES.md for the list of changes.

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. Print traits are in the to_smt module, while the parse traits are in the parse module.

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

`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 workflow is introduced below on a simple example. We first define a few helper types we will use later for the expression type.

/// Operators. Just implements `Display`, never manipulated directly by the
/// solver.
#[derive(Copy, Clone)]
pub enum Op {
  Add, Sub, Mul, Conj, Disj, Eql, Ge, Gt, Lt, Le,
}
impl ::std::fmt::Display for Op {
  fn fmt(& self, w: & mut ::std::fmt::Formatter) -> ::std::fmt::Result {
    w.write_str(
      match * self {
        Op::Add => "+",
        Op::Sub => "-",
        Op::Mul => "*",
        Op::Conj => "and",
        Op::Disj => "or",
        Op::Eql => "=",
        Op::Ge => ">=",
        Op::Gt => ">",
        Op::Lt => "<",
        Op::Le => "<=",
      }
    )
  }
}


/// A constant.
#[derive(Clone, Copy)]
pub enum Cst {
  /// Boolean constant.
  B(bool),
  /// Integer constant.
  I(isize),
}
impl ::std::fmt::Display for Cst {
  fn fmt(& self, w: & mut ::std::fmt::Formatter) -> ::std::fmt::Result {
    match * self {
      Cst::B(b) => write!(w, "{}", b),
      Cst::I(i) if i >= 0 => write!(w, "{}", i),
      Cst::I(i) => write!(w, "(- {})", - i),
    }
  }
}
impl From<bool> for Cst {
  fn from(b: bool) -> Self {
    Cst::B(b)
  }
}
impl From<isize> for Cst {
  fn from(i: isize) -> Self {
    Cst::I(i)
  }
}

These types are defined in the simple_example module, and will be imported from there in the rest of the explanation. We then define the expression type, and make it implement the Expr2Smt trait that writes it as an SMT-LIB 2 expression in a writer.

Print functions

Since the structure for S-expressions is provided by 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).

All user-provided printing functions take some information. That way, users can pass some information to, say, assert that can modify printing. This is typically used when dealing with transition systems to perform "print-time unrolling". See the example module if you're interested; the example below will not use print-time information.

extern crate rsmt2 ;

use rsmt2::to_smt::Expr2Smt ;
use rsmt2::SmtRes ;
use rsmt2::example::simple::{ Op, Cst } ;

/// An example of expression.
pub enum Expr {
  /// A constant.
  C(Cst),
  /// Variable.
  V(String),
  /// Operator application.
  O( Op, Vec<Expr> ),
}
impl Expr {
  pub fn cst<C: Into<Cst>>(c: C) -> Self {
    Expr::C( c.into() )
  }
}
impl Expr2Smt<()> for Expr {
  fn expr_to_smt2<Writer>(
    & self, w: & mut Writer, _: ()
  ) -> SmtRes<()>
  where Writer: ::std::io::Write {
    let mut stack = vec![ (false, vec![self], false) ] ;
    while let Some((space, mut to_write, closing_paren)) = stack.pop() {
      if let Some(next) = to_write.pop() {
        if space {
          write!(w, " ") ?
        }
        // We have something to print, push the rest back.
        stack.push((space, to_write, closing_paren)) ;
        match * next {
          Expr::C(cst) => write!(w, "{}", cst) ?,
          Expr::V(ref var) => write!(w, "{}", var) ?,
          Expr::O(op, ref sub_terms) => {
            write!(w, "({}", op) ? ;
            stack.push((true, sub_terms.iter().rev().collect(), true))
          },
        }
      } else {
        // No more things to write at this level.
        if closing_paren {
          write!(w, ")") ?
        }
      }
    }
    Ok(())
  }
}

For convenience, all the ...2Smt traits are implemented for & str. This is useful for testing and maybe very simple application. Here, we won't implement Sym2Smt or Sort2Smt and rely on & str for symbols and sorts. Using a solver then boils down to creating a solver Kid representing the process itself, and then (here) a PlainSolver that's just a wrapper around the Kid proving functions from the Solver trait.

extern crate rsmt2 ;

use rsmt2::solver ;
use rsmt2::{ Kid, Solver } ;
use rsmt2::example::simple::{ Op, Cst, Expr } ;

let conf = ::rsmt2::conf::z3() ;

let mut kid = Kid::new(conf).expect(
  "could not spawn solver kid"
) ;

{

  let mut solver = solver(& mut kid, ()).expect(
    "could not create solver from kid"
  ) ;

  let v_1 = "v_1".to_string() ;
  let v_2 = "v_2".to_string() ;

  solver.declare_const( & v_1, & "Bool" ).expect(
    "while declaring v_1"
  ) ;
  solver.declare_const( & v_2, & "Int" ).expect(
    "while declaring v_2"
  ) ;

  let expr = Expr::O(
    Op::Disj, vec![
      Expr::O(
        Op::Ge, vec![ Expr::cst(-7), Expr::V( v_2.clone() ) ]
      ),
      Expr::V( v_1.clone() )
    ]
  ) ;

  solver.assert( & expr ).expect(
    "while asserting an expression"
  ) ;

  if solver.check_sat().expect("during check sat") {
    ()
  } else {
    panic!("expected sat, got unsat")
  }

}

Note the unit parameter that we passed to the solver function: solver(& mut kid, ()). This is actually the parser the solver should use when it needs to parse values, symbols, types... In the example above, we only asked for the satisfiability of the assertions. If we had asked for a model, the compiler would have complained by saying that our parser () does not implement the right parsing traits.

The parser

This example will only use get_model, which only requires IdentParser and ValueParser. In most cases, an empty parser struct with the right implementations should be enough.

extern crate rsmt2 ;

use rsmt2::SmtRes ;
use rsmt2::parse::{ IdentParser, ValueParser } ;
use rsmt2::example::simple::Cst ;

/// Empty parser structure, we will not maintain any context.
#[derive(Clone, Copy)]
pub struct Parser ;
impl<'a> IdentParser<String, String, & 'a str> for Parser {
  fn parse_ident(self, input: & 'a str) -> SmtRes<String> {
    Ok( input.to_string() )
  }
  fn parse_type(self, input: & 'a str) -> SmtRes<String> {
    match input {
      "Int" => Ok( "Int".into() ),
      "Bool" => Ok( "Bool".into() ),
      sort => bail!("unexpected sort `{}`", sort),
    }
  }
}
impl<'a> ValueParser<Cst, & 'a str> for Parser {
  fn parse_value(self, input: & 'a str) -> SmtRes<Cst> {
    match input.trim() {
      "true" => Ok( Cst::B(true) ),
      "false" => Ok( Cst::B(false) ),
      int => {
        use std::str::FromStr ;
        let s = int.trim() ;
        if let Ok(res) = isize::from_str(s) {
          return Ok( Cst::I(res) )
        } else if s.len() >= 4 {
          if & s[0 .. 1] == "("
          && & s[s.len() - 1 ..] == ")" {
            let s = & s[1 .. s.len() - 1].trim() ;
            if & s[0 .. 1] == "-" {
              let s = & s[1..].trim() ;
              if let Ok(res) = isize::from_str(s) {
                return Ok( Cst::I(- res) )
              }
            }
          }
        }
        bail!("unexpected value `{}`", int)
      },
    }
  }
}

As a side note, it would have been simpler to implement ValueParser with a & mut SmtParser, as it provides the parsers we needed.

use rsmt2::SmtRes ;
use rsmt2::parse::{ SmtParser, IdentParser, ValueParser } ;
use rsmt2::example::simple::Cst ;


#[derive(Clone, Copy)]
struct Parser ;
impl<'a, Br> ValueParser< Cst, & 'a mut SmtParser<Br> > for Parser
where Br: ::std::io::BufRead {
  fn parse_value(self, input: & 'a mut SmtParser<Br>) -> SmtRes<Cst> {
    use std::str::FromStr ;
    if let Some(b) = input.try_bool() ? {
      Ok( Cst::B(b) )
    } else if let Some(int) = input.try_int(
      |int, pos| match isize::from_str(int) {
        Ok(int) => if pos { Ok(int) } else { Ok(- int) },
        Err(e) => Err(e),
      }
    ) ? {
      Ok( Cst::I(int) )
    } else {
      input.fail_with("unexpected value")
    }
  }
}

Anyway, once we pass Parser to the solver creation function, and all conditions are met to ask the solver for a model.

extern crate rsmt2 ;

use rsmt2::{ solver, SmtRes, Kid, Solver } ;
use rsmt2::conf::z3 ;
use rsmt2::example::simple::{
  Cst, Op, Expr, Parser
} ;

let conf = z3() ;

let mut kid = Kid::new(conf).expect(
  "could not spawn solver kid"
) ;

{

  let mut solver = solver(& mut kid, Parser).expect(
    "could not create solver from kid"
  ) ;

  let v_1 = "v_1".to_string() ;
  let v_2 = "v_2".to_string() ;

  solver.declare_const( & v_1, & "Bool" ).expect(
    "while declaring v_1"
  ) ;
  solver.declare_const( & v_2, & "Int" ).expect(
    "while declaring v_2"
  ) ;

  let expr = Expr::O(
    Op::Disj, vec![
      Expr::O(
        Op::Ge, vec![ Expr::cst(-7), Expr::V( v_2.clone() ) ]
      ),
      Expr::V( v_1.clone() )
    ]
  ) ;

  solver.assert( & expr ).expect(
    "while asserting an expression"
  ) ;

  if solver.check_sat().expect("during check sat") {

    let model = solver.get_model_const().expect(
      "while getting model"
    ) ;

    let mut okay = false ;
    for (ident, typ, value) in model {
      if ident == v_1 {
        assert_eq!( typ, "Bool" ) ;
        match value {
          Cst::B(true) => okay = true,
          Cst::B(false) => (),
          Cst::I(int) => panic!(
            "value for v_1 is `{}`, expected boolean", int
          ),
        }
      } else if ident == v_2 {
        assert_eq!( typ, "Int" ) ;
        match value {
          Cst::I(i) if -7 >= i => okay = true,
          Cst::I(_) => (),
          Cst::B(b) => panic!(
            "value for v_2 is `{}`, expected isize", b
          ),
        }
      }
    }

    if ! okay {
      panic!("got sat, but model is spurious")
    }

  } else {
    panic!("expected sat, got unsat")
  }

}

Reexports

pub use errors::SmtRes;

Modules

actlit	Activation literal type and helpers.
conf	Solver configuration, contains backend solver specific info.
errors	Errors of this library.
example	A simple example of using `rsmt2`.
parse	SMT Lib 2 result parsers.
to_smt	Traits your types must implement so that `rsmt2` can use them.

Structs

Kid	A solver `Child`.
PlainSolver	Plain solver, as opposed to `TeeSolver` which logs IOs.
TeeSolver	Wrapper around a `PlainSolver` logging IOs to a file.

Crate rsmt2 [−] [src]

`async` versus `sync`

Workflow

Print functions

The parser

Reexports

Modules

Structs

Enums

Traits

Functions