Module rsmt2::parse

SMT Lib 2 result parsers.

Depending on the commands you plan to use, your parser will need to implement

	for
IdentParser	get-model
ValueParser	get-model and get-value
ExprParser	get-value
ProofParser	currently unused

You can choose the kind of input you want to parse, between

• & [u8], e.g. for nom,
• & str, e.g. for regex,
• & mut SmtParser, rmst2's internal parser which provides simple helpers to parse s-expressions.

The first two are safe in that your parsers will be called on the tokens they are supposed to parse and nothing else.

use rsmt2::parse::{ IdentParser, ValueParser } ;
use rsmt2::SmtRes ;
let txt = "\
  ( model (define-fun a () Int (- 17)) )
" ;
let mut parser = SmtParser::of_str(txt) ;

struct Parser ;
impl<'a, 'b> ValueParser<String, & 'a str> for & 'b Parser {
  fn parse_value(self, input: & 'a str) -> SmtRes<String> {
    Ok(input.into())
  }
}
impl<'a, 'b> IdentParser<String, String, & 'a str> for & 'b Parser {
  fn parse_ident(self, input: & 'a str) -> SmtRes<String> {
    Ok(input.into())
  }
  fn parse_type(self, input: & 'a str) -> SmtRes<String> {
    Ok(input.into())
  }
}

let model = parser.get_model_const( false, & Parser ).expect("model") ;
assert_eq!( model, vec![ ("a".into(), "Int".into(), "(- 17)".into()) ] )

But a parser taking SmtParser as input is "unsafe" in the sense that it has access to the whole input. Note that SmtParser provides helper parsing functions such as try_int and try_sym.

use rsmt2::parse::{ IdentParser, ValueParser } ;
use rsmt2::errors::SmtRes ;
let txt = "\
  ( model (define-fun a () Int (- 17)) )
" ;
let mut parser = SmtParser::of_str(txt) ;

struct Parser ;
impl<'a, 'b, Br: ::std::io::BufRead> ValueParser<
  String, & 'a mut SmtParser<Br>
> for & 'b Parser {
  fn parse_value(self, input: & 'a mut SmtParser<Br>) -> SmtRes<String> {
    input.tag("(- 17))") ? ; Ok( "-17".into() )
    //               ^~~~~ eating more input than we should...
  }
}
impl<'a, 'b, Br: ::std::io::BufRead> IdentParser<
  String, String, & 'a mut SmtParser<Br>
> for & 'b Parser {
  fn parse_ident(self, input: & 'a mut SmtParser<Br>) -> SmtRes<String> {
    input.tag("a") ? ; Ok( "a".into() )
  }
  fn parse_type(self, input: & 'a mut SmtParser<Br>) -> SmtRes<String> {
    input.tag("Int") ? ; Ok( "Int".into() )
  }
}

use rsmt2::errors::ErrorKind ;
match * parser.get_model_const( false, & Parser ).unwrap_err().kind() {
  ErrorKind::ParseError(ref msg, ref token) => {
    assert_eq!(
      msg, "expected `(` opening define-fun or `)` closing model"
    ) ;
    assert_eq!(token, "eof")
  },
  ref error => panic!("unexpected error: {}", error)
}

Structs

SmtParser

SMT-LIB 2.0 parser.

Traits

ExprParser	Can parse expressions. Used for get_value.
IdentParser	Can parse identifiers and types. Used for get_model.
ProofParser	Can parse proofs. Currenly unused.
ValueParser	Can parse values. Used for get-model and get-value.