Struct rsmt2::parse::SmtParser [−][src]
pub struct SmtParser<R> { /* fields omitted */ }
Expand description
SMT-LIB 2.0 parser.
Implementations
Immutable access to the part of the buffer that’s not been parsed yet.
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(), "" );
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 );
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") );
Parses a tag or fails.
Returns ()
exactly when Self::try_tag
returns true
, and an error otherwise.
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.
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" );
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" )
Parses a sequence of things potentially separated by whitespaces and/or comments.
Returns ()
exactly when Self::try_tags
returns true
, and an error otherwise.
Generates a failure at the current position.
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"
);
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 "
);
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) "
);
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())
);
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 :(")
}
Parses the result of a check-sat.
Returns None
if the solver reported unknown
.
Tries to parse a reserved actlit id.
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>,
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>,
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>,
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>,
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, Expr, Info, T, Br> ExprParser<Expr, Info, &'a mut SmtParser<Br>> for T where
T: ExprParser<Expr, Info, &'a str>,
Br: BufRead,
impl<'a, Expr, Info, T, Br> ExprParser<Expr, Info, &'a mut SmtParser<Br>> for T where
T: ExprParser<Expr, Info, &'a str>,
Br: BufRead,
Parses an expression given some info.
Parses an identifier.
Parses a type.
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
Parses an identifier.
Parses a type.
Parses an identifier.
Parses a type.
impl<'a, Ident, Type, Value, T, Br> ModelParser<Ident, Type, Value, &'a mut SmtParser<Br>> for T where
T: ModelParser<Ident, Type, Value, &'a str>,
Br: BufRead,
impl<'a, Ident, Type, Value, T, Br> ModelParser<Ident, Type, Value, &'a mut SmtParser<Br>> for T where
T: ModelParser<Ident, Type, Value, &'a str>,
Br: BufRead,
impl<'a, Proof, T, Br> ProofParser<Proof, &'a mut SmtParser<Br>> for T where
T: ProofParser<Proof, &'a str>,
Br: BufRead,
impl<'a, Proof, T, Br> ProofParser<Proof, &'a mut SmtParser<Br>> for T where
T: ProofParser<Proof, &'a str>,
Br: BufRead,
Parses a proof.
Pull some bytes from this source into the specified buffer, returning how many bytes were read. Read more
Like read
, except that it reads into a slice of buffers. Read more
can_vector
)Determines if this Read
er has an efficient read_vectored
implementation. Read more
read_initializer
)Determines if this Read
er can work with buffers of uninitialized
memory. Read more
Read all bytes until EOF in this source, placing them into buf
. Read more
Read all bytes until EOF in this source, appending them to buf
. Read more
Read the exact number of bytes required to fill buf
. Read more
Creates a “by reference” adapter for this instance of Read
. Read more
Creates an adapter which will chain this stream with another. Read more
Parses a plain value.
Parses a plain value.
impl<'a, Value, T, Br> ValueParser<Value, &'a mut SmtParser<Br>> for T where
T: ValueParser<Value, &'a str>,
Br: BufRead,
impl<'a, Value, T, Br> ValueParser<Value, &'a mut SmtParser<Br>> for T where
T: ValueParser<Value, &'a str>,
Br: BufRead,
Parses a plain value.
Auto Trait Implementations
impl<R> RefUnwindSafe for SmtParser<R> where
R: RefUnwindSafe,
impl<R> UnwindSafe for SmtParser<R> where
R: UnwindSafe,
Blanket Implementations
Mutably borrows from an owned value. Read more
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
Parses an identifier.
Parses a type.
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
T: IdentParser<Ident, Type, &'a str>,
Br: BufRead,
Parses an identifier.
Parses a type.