Struct rsmt2::parse::SmtParser

pub struct SmtParser<R> { /* 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.

See also Self::tag, Self::tag_info and Self::tags.

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 Self::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 Self::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 Self::try_tags returns true, and an error otherwise.

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<'me, F, T, Err>(&'me mut self, f: F) -> SmtRes<Option<T>>where
    F: FnOnce(&'me 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\n\n'something' () parens\" )
";
let mut parser = SmtParser::of_str(txt);
if let Err(e) = parser.try_error() {
    assert_eq! { & format!("{}", e), "solver error: \"huge panic\n\n'something' () parens\"" }
} 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_unsat_core<Sym, Parser>(&mut self, parser: Parser) -> SmtRes<Vec<Sym>>where
    Parser: for<'a> SymParser<Sym, &'a mut Self>,

Parses the result of a get-unsat-core.

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

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.

pub fn get_interpolant<Expr, Info, Parser>(
    &mut self,
    parser: Parser,
    info: Info
) -> SmtRes<Expr>where
    Parser: for<'a> ExprParser<Expr, Info, &'a mut Self>,

Parses the result of a get-interpolant.

Trait Implementations

impl<'a, Br> ExprParser<&'a str, (), &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

fn parse_expr(self, input: &'a mut SmtParser<Br>, _info: ()) -> SmtRes<&'a str>

Parses an expression given some info.

impl<'a, Expr, Info, T, Br> ExprParser<Expr, Info, &'a mut SmtParser<Br>> for Twhere
    T: ExprParser<Expr, Info, &'a str>,
    Br: BufRead,

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

Parses an expression given some info.

impl<'a, Br> ExprParser<String, (), &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

fn parse_expr(self, input: &'a mut SmtParser<Br>, _info: ()) -> SmtRes<String>

Parses an expression given some info.

impl<'a, Br> IdentParser<&'a str, &'a str, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses an identifier.

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

Parses a type.

impl<'a, Br> IdentParser<String, String, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses an identifier.

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

Parses a type.

impl<'a, Br> ModelParser<&'a str, &'a str, &'a str, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

fn parse_value(
    self,
    input: &'a mut SmtParser<Br>,
    _name: &&'a str,
    _inputs: &[(&'a str, &'a str)],
    _output: &&'a str
) -> SmtRes<&'a str>

Parses a value in the context of a get-model command.

impl<'a, Br> ModelParser<String, String, String, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

fn parse_value(
    self,
    input: &'a mut SmtParser<Br>,
    _name: &String,
    _inputs: &[(String, String)],
    _output: &String
) -> SmtRes<String>

Parses a value in the context of a get-model command.

impl<'a, Proof, T, Br> ProofParser<Proof, &'a mut SmtParser<Br>> for Twhere
    T: ProofParser<Proof, &'a str>,
    Br: BufRead,

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

Parses a proof.

impl<R: Read> Read for SmtParser<R>

fn read(&mut self, buf: &mut [u8]) -> Result<usize>

Pull some bytes from this source into the specified buffer, returning how many bytes were read.

fn read_vectored(&mut self, bufs: &mut [IoSliceMut<'_>]) -> Result<usize, Error>

Like read, except that it reads into a slice of buffers.

fn is_read_vectored(&self) -> bool

🔬This is a nightly-only experimental API. (can_vector)

Determines if this Reader has an efficient read_vectored implementation.

fn read_to_end(&mut self, buf: &mut Vec<u8, Global>) -> Result<usize, Error>

Read all bytes until EOF in this source, placing them into buf.

fn read_to_string(&mut self, buf: &mut String) -> Result<usize, Error>

Read all bytes until EOF in this source, appending them to buf.

fn read_exact(&mut self, buf: &mut [u8]) -> Result<(), Error>

Read the exact number of bytes required to fill buf.

fn read_buf(&mut self, buf: BorrowedCursor<'_>) -> Result<(), Error>

🔬This is a nightly-only experimental API. (read_buf)

Pull some bytes from this source into the specified buffer.

fn read_buf_exact(&mut self, cursor: BorrowedCursor<'_>) -> Result<(), Error>

🔬This is a nightly-only experimental API. (read_buf)

Read the exact number of bytes required to fill cursor.

fn by_ref(&mut self) -> &mut Self

Creates a “by reference” adaptor for this instance of Read.

fn bytes(self) -> Bytes<Self>

Transforms this Read instance to an Iterator over its bytes.

fn chain<R>(self, next: R) -> Chain<Self, R>where
    R: Read,

Creates an adapter which will chain this stream with another.

fn take(self, limit: u64) -> Take<Self>

Creates an adapter which will read at most limit bytes from it.

impl<'a, Br> SymParser<&'a str, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses a symbol.

impl<'a, Br> SymParser<String, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses a symbol.

impl<'a, Sym, T, Br> SymParser<Sym, &'a mut SmtParser<Br>> for Twhere
    T: SymParser<Sym, &'a str>,
    Br: BufRead,

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

Parses a symbol.

impl<'a, Br> ValueParser<&'a str, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses a plain value.

impl<'a, Br> ValueParser<String, &'a mut SmtParser<Br>> for ()where
    Br: BufRead,

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

Parses a plain value.

impl<'a, Value, T, Br> ValueParser<Value, &'a mut SmtParser<Br>> for Twhere
    T: ValueParser<Value, &'a str>,
    Br: BufRead,

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

Parses a plain value.