Module rsmt2::parse [−][src]
SMT Lib 2 result parsers.
Depending on the commands you plan to use, your parser will need to implement
for | |
---|---|
IdentParser | Solver::get_model |
ModelParser | Solver::get_model |
ValueParser | Solver::get_model |
ExprParser | Solver::get_values |
ProofParser | currently unused |
You can choose the kind of input you want to parse, between
& [u8]
, e.g. fornom
,& str
, e.g. forregex
,& mut SmtParser
,rmst2
’s own 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.
Parsing: &str
(and &[u8]
)
Here is a first example where we defined a value parser that only recognizes booleans, to
showcase ValueParser
and Solver::get_values
. Expr
essions
are represented as strings, and Val
ues are booleans.
use rsmt2::{SmtConf, SmtRes, Solver, parse::ValueParser, parse::ExprParser}; pub type Expr = String; pub type Val = bool; #[derive(Clone, Copy)] pub struct Parser; // Value parser implementation for `&'a str` input. impl<'a> ValueParser<Val, &'a str> for Parser { fn parse_value(self, input: &'a str) -> SmtRes<Val> { // When parsing `&str` or `&[u8]`, the input is the actual value. match input { "true" => Ok(true), "false" => Ok(false), s => Err(format!("unsupported value `{}`", s).into()), } } } impl<'a> ExprParser<Expr, (), &'a str> for Parser { fn parse_expr(self, input: &'a str, _: ()) -> SmtRes<Expr> { // When parsing `&str` or `&[u8]`, the input is the actual expression. Here we're not // constructing some complex expression, we just want to turn the `&str` into a // `String`. Ok(input.into()) } } let mut solver = SmtConf::default_z3().spawn(Parser).unwrap(); solver.declare_const("a", "Bool").unwrap(); solver.declare_const("b", "Bool").unwrap(); solver.assert("(and a (not b))").unwrap(); let is_sat = solver.check_sat().unwrap(); assert!(is_sat); let values = solver.get_values(&["a", "b", "(and a (not b))"]).unwrap(); assert_eq!( &format!("{:?}", values), r#"[("a", true), ("b", false), ("(and a (not b))", true)]"# ); let mut values = values.into_iter(); assert_eq!( values.next(), Some(("a".to_string(), true)) ); assert_eq!( values.next(), Some(("b".to_string(), false)) ); assert_eq!( values.next(), Some(("(and a (not b))".to_string(), true)) );
Here is a second example where we implement ModelParser
and IdentParser
. We must provide
parsing functions for identifiers, types and values.
use rsmt2::parse::{ IdentParser, ModelParser }; use rsmt2::SmtRes; let txt = "\ ( model (define-fun a () Int (- 17)) ) "; let mut parser = SmtParser::of_str(txt); struct Parser; impl<'a, 'b> ModelParser< String, String, String, & 'a str > for & 'b Parser { fn parse_value( self, input: & 'a str, _: & String, _: & [ (String, String) ], _: & String, ) -> 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()) ] )
Parsing: SmtParser
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
SmtParser::try_int
and SmtParser::try_sym
.
use rsmt2::parse::{ IdentParser, ModelParser }; 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> ModelParser< String, String, String, & 'a mut SmtParser<Br> > for & 'b Parser { fn parse_value( self, input: & 'a mut SmtParser<Br>, _: & String, _: & [ (String, String) ], _: & String, ) -> 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 |
IdentParser | Can parse identifiers and types. Used for |
ModelParser | Can parse models. Used for |
ProofParser | Can parse proofs. Currenly unused. |
ValueParser | Can parse values. Used for |
Type Definitions
RSmtParser | Alias for the underlying parser. |