Struct SmtParser 

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

SMT-LIB 2.0 parser.

Implementations

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

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

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

impl<R: BufRead> SmtParser<R>

pub fn new(input: R) -> Self

Creates an SMT parser.

pub fn swap(&mut self, nu_input: &mut R)

Swaps the input source.

pub fn buff(&self) -> &str

Immutable access to the buffer.

pub fn buff_rest(&self) -> &str

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

pub fn cursor(&self) -> usize

The current position in the buffer.

pub 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(), "" ) ;

pub fn clear(&mut self)

Clears the buffer up to the current position.

pub fn print(&self, pref: &str)

Prints itself, for debugging.

pub 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 ) ;

pub 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") ) ;

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

Parses a tag or fails.

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

pub 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.

pub 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" ) ;

pub 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" )

pub 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.

pub fn prompt(&mut self) -> SmtRes<()>

Parses the annoying CVC4 prompt. Can’t fail.

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

Generates a failure at the current position.

pub 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"
) ;

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

Parses a boolean or fails.

pub 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             # Not followed by a '.'
        | '(' '-' usize ')'
usize ::= '0' | [1-9][0-9]*

Examples

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) ;
println!("666") ;
assert_eq!( parser.try_int(to_int).expect("int"), Some(666) ) ;
assert_eq!(
    parser.buff_rest(), " (- 11) false; comment\n"
) ;

println!("- 11") ;
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") ;

println!("31") ;
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 ) ;

let txt = " 7.0 " ;
println!("{}", txt) ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_int(to_int).expect("int"), None ) ;
assert_eq!(
    parser.buff_rest(), " 7.0 "
) ;

let txt = " 00 " ;
println!("{}", txt) ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_int(to_int).expect("int"), None ) ;
assert_eq!(
    parser.buff_rest(), " 00 "
) ;

pub 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 '.' usize ')' | 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 = "\
    0.0 666.0 7.42 (- 11.0) 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((0, 1)) ) ;
assert_eq!(
    parser.buff_rest(), " 666.0 7.42 (- 11.0) false; comment\n"
) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), Some((666, 1)) ) ;
assert_eq!(
    parser.buff_rest(), " 7.42 (- 11.0) false; comment\n"
) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), Some((742, 100)) ) ;
assert_eq!(
    parser.buff_rest(), " (- 11.0) 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))) ) ;

let txt = " 7 " ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), None ) ;
assert_eq!(
    parser.buff_rest(), " 7 "
) ;

let txt = " (- 7) " ;
let mut parser = SmtParser::of_str(txt) ;
assert_eq!( parser.try_rat(to_rat).expect("rat"), None ) ;
assert_eq!(
    parser.buff_rest(), " (- 7) "
) ;

pub 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())
) ;

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

Parses success.

pub fn try_error(&mut self) -> SmtRes<()>

Parses an error.

Returns Ok(()) if no error was parsed, an error otherwise.

Examples

use rsmt2::parse::{ IdentParser, ValueParser } ;
use rsmt2::SmtRes ;
let txt = "\
    ( error \"huge panic\" )
" ;
let mut parser = SmtParser::of_str(txt) ;
if let Err(e) = parser.try_error() {
    assert_eq! { & format!("{}", e), "solver error: \"huge panic\"" }
} else {
    panic!("expected error, got nothing :(")
}

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

Parses the result of a check-sat.

Returns None if the solver reported unknown.

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

Tries to parse a reserved actlit id.

pub 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> ModelParser<Ident, Type, Value, &'a mut Self>,

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

pub fn get_model<Ident, Value, Type, Parser>( &mut self, prune_actlits: bool, parser: Parser, ) -> SmtRes<Vec<(Ident, Vec<(Ident, Type)>, Type, Value)>>

where Parser: for<'a> IdentParser<Ident, Type, &'a mut Self> + for<'a> ModelParser<Ident, Type, Value, &'a mut Self>,

Parses the result of a get-model.

pub fn get_values<Val, Info: Clone, Expr, Parser>( &mut self, parser: Parser, info: Info, ) -> SmtRes<Vec<(Expr, Val)>>

where Parser: for<'a> ValueParser<Val, &'a mut Self> + for<'a> ExprParser<Expr, Info, &'a mut Self>,

Parses the result of a get-value.

Trait Implementations

impl<'a, Expr, Info, T, Br> ExprParser<Expr, Info, &'a mut SmtParser<Br>> for T

where T: ExprParser<Expr, Info, &'a str>, Br: BufRead,

fn parse_expr(self, input: &'a mut SmtParser<Br>, info: Info) -> SmtRes<Expr>

impl<'a, Proof, T, Br> ProofParser<Proof, &'a mut SmtParser<Br>> for T

where T: ProofParser<Proof, &'a str>, Br: BufRead,

fn parse_proof(self, input: &'a mut SmtParser<Br>) -> SmtRes<Proof>

impl<'a, Value, T, Br> ValueParser<Value, &'a mut SmtParser<Br>> for T

where T: ValueParser<Value, &'a str>, Br: BufRead,

fn parse_value(self, input: &'a mut SmtParser<Br>) -> SmtRes<Value>

Parses a plain value.