Struct rsmt2::parse::SmtParser

pub struct SmtParser<R: BufRead> { /* fields omitted */ }

SMT-LIB 2.0 parser.

Methods

impl<'a> SmtParser<BufReader<&'a [u8]>>

fn of_str(s: &'a str) -> Self

Constructor from a string, mostly for doc/test purposes.

impl<R: BufRead> SmtParser<R>

fn new(input: R) -> Self

Creates an smt parser.

fn buff(&self) -> &str

Immutable access to the buffer.

fn buff_rest(&self) -> &str

Immutable access to the part of the buffer that's not been parsed yet.

fn cursor(&self) -> usize

The current position in the buffer.

fn get_sexpr(&mut self) -> SmtRes<&str>

Returns the next s-expression and positions the cursor directly after it.

An s-expression is an ident, a constant with no parens (42, false, etc.), or something between (nested) parens.

let txt = "\
  token  ; a comment\n\n next_token ; more comments\n\
  (+ |quoted ident, ; a comment\n parens don't count)| 7)42 false\
" ;
let mut parser = SmtParser::of_str(txt) ;

assert_eq!( parser.get_sexpr().unwrap(), "token" ) ;
assert_eq!( parser.buff_rest(), "  ; a comment\n" ) ;

assert_eq!( parser.get_sexpr().unwrap(), "next_token" ) ;
assert_eq!( parser.buff_rest(), " ; more comments\n" ) ;

assert_eq!(
  parser.get_sexpr().unwrap(),
  "(+ |quoted ident, ; a comment\n parens don't count)| 7)"
) ;
assert_eq!( parser.buff_rest(), "42 false" ) ;

assert_eq!( parser.get_sexpr().unwrap(), "42" ) ;
assert_eq!( parser.buff_rest(), " false" ) ;

assert_eq!( parser.get_sexpr().unwrap(), "false" ) ;
assert_eq!( parser.buff_rest(), "" ) ;

fn clear(&mut self)

Clears the buffer up to the current position.

fn print(&self, pref: &str)

Prints itself, for debugging.

fn spc_cmt(&mut self)

Parses some spaces or some comments.

Parsing a tag or loading an s-expression fetches new lines, this does not.

let txt = "  token  ; a comment\n\n next token ; last comment" ;
let mut parser = SmtParser::of_str(txt) ;

parser.spc_cmt() ;
assert_eq!( parser.buff_rest(), "" ) ;
assert_eq!( parser.buff(), "" ) ;

assert!( parser.try_tag("token").expect("token") ) ;
assert_eq!( parser.buff_rest(), "  ; a comment\n" ) ;
assert_eq!( parser.buff(), "  token  ; a comment\n" ) ;

parser.spc_cmt() ;
assert_eq!( parser.buff_rest(), "" ) ;
assert_eq!( parser.buff(), "  token  ; a comment\n" ) ;

assert!( parser.try_tag("next token").expect("token") ) ;
assert_eq!( parser.buff_rest(), " ; last comment" ) ;
assert_eq!( parser.buff(), txt ) ;

parser.spc_cmt() ;
assert_eq!( parser.buff_rest(), "" ) ;
assert_eq!( parser.buff(), txt ) ;

fn try_tag(&mut self, tag: &str) -> SmtRes<bool>

Tries to parse a tag, true if successful. Parse whitespaces and comments if any before the token.

If this function returns false, then the cursor is at the first non-whitespace non-commented character after the original cursor position.

let txt = "\
  a tag is anything  |(>_<)|  ; a comment\n\n next token ; last comment\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert!( parser.try_tag("a tag is anything").expect("tag") ) ;
assert_eq!( parser.buff_rest(), "  |(>_<)|  ; a comment\n" ) ;
assert!( ! parser.try_tag("not the token").expect("tag") ) ;
assert_eq!( parser.buff_rest(), "|(>_<)|  ; a comment\n" ) ;
assert!( parser.try_tag("|(>_<)|").expect("tag") ) ;
assert!( ! parser.try_tag("not the next token").expect("tag") ) ;
assert_eq!( parser.buff_rest(), "next token ; last comment" ) ;
assert!( parser.try_tag("next token").expect("tag") ) ;

fn tag(&mut self, tag: &str) -> SmtRes<()>

Parses a tag or fails.

Returns () exactly when try_tag returns true, and an error otherwise.

fn tag_info(&mut self, tag: &str, err_msg: &str) -> SmtRes<()>

Parses a tag or fails, appends err_msg at the end of the error message.

Returns () exactly when try_tag returns true, and an error otherwise.

fn try_word(&mut self, word: &str) -> SmtRes<bool>

Parses a tag followed by a whitespace, a paren or a comment.

If this function returns false, then the cursor is at the first non-whitespace non-commented character after the original cursor position.

let txt = "\
  a word is anything  |(>_<)|  last; comment\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert!( parser.try_word("a word is").expect("word") ) ;
assert_eq!( parser.buff_rest(), " anything  |(>_<)|  last; comment" ) ;
assert!( ! parser.try_word("a").expect("word") ) ;
assert_eq!( parser.buff_rest(), "anything  |(>_<)|  last; comment" ) ;
assert!( ! parser.try_word("any").expect("word") ) ;
assert_eq!( parser.buff_rest(), "anything  |(>_<)|  last; comment" ) ;
assert!( ! parser.try_word("anythin").expect("word") ) ;
assert_eq!( parser.buff_rest(), "anything  |(>_<)|  last; comment" ) ;
assert!( parser.try_word("anything").expect("word") ) ;
assert_eq!( parser.buff_rest(), "  |(>_<)|  last; comment" ) ;
assert!( parser.try_word("|").expect("word") ) ;
assert_eq!( parser.buff_rest(), "(>_<)|  last; comment" ) ;
assert!( parser.try_tag("(").expect("tag") ) ;
assert_eq!( parser.buff_rest(), ">_<)|  last; comment" ) ;
assert!( parser.try_word(">_<").expect("word") ) ;
assert_eq!( parser.buff_rest(), ")|  last; comment" ) ;
assert!( parser.try_tag(")").expect("tag") ) ;
assert_eq!( parser.buff_rest(), "|  last; comment" ) ;
assert!( parser.try_word("|").expect("word") ) ;
assert_eq!( parser.buff_rest(), "  last; comment" ) ;
assert!( parser.try_word("last").expect("word") ) ;
assert_eq!( parser.buff_rest(), "; comment" ) ;

fn try_tags<'a, Tags, S>(&mut self, tags: &'a Tags) -> SmtRes<bool> where
    &'a Tags: IntoIterator<Item = S>,
    S: AsRef<str>, 

Tries to parse a sequence of things potentially separated by whitespaces and/or comments.

If this function returns false, then the cursor is at the first non-whitespace non-commented character after the original cursor position.

let txt = "\
  a tag is anything  |(>_<)|  ; a comment\n\n next token ; last comment\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert!(
  parser.try_tags(
     &[ "a", "tag", "is anything", "|", "(", ">_<", ")", "|" ]
  ).expect("tags")
) ;
assert_eq!( parser.buff_rest(), "  ; a comment\n" ) ;
assert!(
  ! parser.try_tags(
    & [ "next", "token", "something else?" ]
  ).expect("tags")
) ;
assert_eq!( parser.buff_rest(), "next token ; last comment" )

fn tags<'a, Tags, S>(&mut self, tags: &'a Tags) -> SmtRes<()> where
    &'a Tags: IntoIterator<Item = S>,
    S: AsRef<str>, 

Parses a sequence of things potentially separated by whitespaces and/or comments.

Returns () exactly when try_tags returns true, and an error otherwise.

fn fail_with<T, Str: Into<String>>(&mut self, msg: Str) -> SmtRes<T>

Generates a failure at the current position.

fn try_bool(&mut self) -> SmtRes<Option<bool>>

Tries to parse a boolean.

let txt = "\
  true fls  true_ly_bad_ident false; comment\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_bool().expect("bool"), Some(true) ) ;
assert_eq!(
  parser.buff_rest(), " fls  true_ly_bad_ident false; comment"
) ;
assert_eq!( parser.try_bool().expect("bool"), None ) ;
assert_eq!(
  parser.buff_rest(), "fls  true_ly_bad_ident false; comment"
) ;
parser.tag("fls").expect("tag") ;
assert_eq!( parser.try_bool().expect("bool"), None ) ;
assert_eq!(
  parser.buff_rest(), "true_ly_bad_ident false; comment"
) ;
parser.tag("true_ly_bad_ident").expect("tag") ;
assert_eq!( parser.try_bool().expect("bool"), Some(false) ) ;
assert_eq!(
  parser.buff_rest(), "; comment"
) ;

fn bool(&mut self) -> SmtRes<bool>

Parses a boolean or fails.

fn try_int<F, T, Err>(&mut self, f: F) -> SmtRes<Option<T>> where
    F: FnOnce(&str, bool) -> Result<T, Err>,
    Err: Display, 

Tries to parses an integer.

Parameters of the input function:

• the absolute value of the integer parsed,
• positiveness flag: true iff the integer is positive.

NB: input function f cannot return the input string in any way. Doing so will not borrow-check and is completely unsafe as the parser can and in general will discard what's in its buffer once it's parsed.

Only recognizes integers of the form

int   ::= usize
        | '(' '-' usize ')'
usize ::= [0-9][0-9]*

use std::str::FromStr ;
fn to_int(
  input: & str, positive: bool
) -> Result<isize, <isize as FromStr>::Err> {
  isize::from_str(input).map(
    |num| if positive { num } else { - num }
  )
}
let txt = "\
  666 (- 11) false; comment\n(+ 31) (= tru)\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_int(to_int).expect("int"), Some(666) ) ;
assert_eq!(
  parser.buff_rest(), " (- 11) false; comment\n"
) ;
assert_eq!( parser.try_int(to_int).expect("int"), Some(- 11) ) ;
assert_eq!(
  parser.buff_rest(), " false; comment\n"
) ;
assert_eq!( parser.try_int(to_int).expect("int"), None ) ;
parser.tag("false").expect("tag") ;
assert_eq!( parser.try_int(to_int).expect("int"), Some(31) ) ;
assert_eq!(
  parser.buff_rest(), " (= tru)"
) ;
assert_eq!( parser.try_int(to_int).expect("int"), None ) ;

fn try_rat<F, T, Err>(&mut self, f: F) -> SmtRes<Option<T>> where
    F: Fn(&str, &str, bool) -> Result<T, Err>,
    Err: Display, 

Tries to parses a rational (called Real in SMT-LIB).

Parameters of the input function:

• numerator of the rational parsed (> 0),
• denominator of the rational parsed (> 0),
• positiveness flag: true iff the rational is positive.

Only recognizes integers of the form

rat   ::= '(' '/' udec udec ')'
        | '(' '-' '(' '/' udec udec ')' ')'
        | idec
idec  ::= '(' '-' udec ')' | udec
udec  ::= usize | usize.0
usize ::= [0-9][0-9]*

NB: input function f cannot return the input strings in any way. Doing so will not borrow-check and is completely unsafe as the parser can and in general will discard what's in its buffer once it's parsed.

use std::str::FromStr ;
fn to_rat(
  num: & str, den: & str, positive: bool
) -> Result<(isize, usize), String> {
  let num = isize::from_str(num).map(
    |num| if positive { num } else { - num }
  ).map_err(|e| format!("{}", e)) ? ;
  let den = usize::from_str(den).map_err(|e| format!("{}", e)) ? ;
  Ok((num, den))
}
let txt = "\
  666 (- 11) false; comment\n(/ 31 27) (- (/ 63 0)) (= tru)\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), Some((666, 1)) ) ;
assert_eq!(
  parser.buff_rest(), " (- 11) false; comment\n"
) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), Some((- 11, 1)) ) ;
assert_eq!(
  parser.buff_rest(), " false; comment\n"
) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), None ) ;
parser.tag("false").expect("tag") ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), Some((31, 27)) ) ;
assert_eq!(
  parser.buff_rest(), " (- (/ 63 0)) (= tru)"
) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), (Some((- 63, 0))) ) ;

fn try_sym<F, T, Err>(&mut self, f: F) -> SmtRes<Option<T>> where
    F: FnOnce(&str) -> Result<T, Err>,
    Err: Display, 

Tries to parse a symbol.

Quoted symbols (anything but | surrounded by |) are passed with the surrounding |.

NB: input function f cannot return the input string in any way. Doing so will not borrow-check and is completely unsafe as the parser can and in general will discard what's in its buffer once it's parsed.

fn sym(input: & str) -> Result<String, String> {
  Ok( input.into() )
}
let txt = "\
  ident (- 11) +~stuff; comment\n |some stuff \n [{}!+)(}|\
" ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_sym(sym).expect("sym"), Some("ident".into()) ) ;
assert_eq!(
  parser.buff_rest(), " (- 11) +~stuff; comment\n"
) ;
assert_eq!( parser.try_sym(sym).expect("sym"), None ) ;
assert_eq!(
  parser.buff_rest(), "(- 11) +~stuff; comment\n"
) ;
parser.tag("(- 11)").expect("tag") ;
assert_eq!( parser.try_sym(sym).expect("sym"), Some("+~stuff".into()) ) ;
assert_eq!(
  parser.buff_rest(), "; comment\n"
) ;
assert_eq!(
  parser.try_sym(sym).expect("sym"),
  Some("|some stuff \n [{}!+)(}|".into())
) ;

fn success(&mut self) -> SmtRes<()>

Parses success.

fn check_sat(&mut self) -> SmtRes<Option<bool>>

Parses the result of a check-sat.

fn try_actlit_id(&mut self) -> SmtRes<bool>

Tries to parse a reserved actlit id.

fn get_model_const<Ident, Value, Type, Parser>(
    &mut self,
    prune_actlits: bool,
    parser: Parser
) -> SmtRes<Vec<(Ident, Type, Value)>> where
    Parser: for<'a> IdentParser<Ident, Type, &'a mut Self> + for<'a> ValueParser<Value, &'a mut Self>, 

Parses the result of a get-model where all symbols are nullary.

fn get_model<Ident, Value, Type, Parser>(
    &mut self,
    prune_actlits: bool,
    parser: Parser
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
    Parser: for<'a> IdentParser<Ident, Type, &'a mut Self> + for<'a> ValueParser<Value, &'a mut Self>, 

Parses the result of a get-model.

fn get_values<Value, Info: Clone, Expr, Parser>(
    &mut self,
    parser: Parser,
    info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
    Parser: for<'a> ValueParser<Value, &'a mut Self> + for<'a> ExprParser<Expr, Info, &'a mut Self>, 

Parses the result of a get-value.