Module rsmt2::parse [−][src]
Expand description
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 |
SymParser | Solver::get_unsat_core |
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
SMT-LIB 2.0 parser.
Traits
Can parse expressions. Used for Solver::get_values
.
Can parse identifiers and types. Used for Solver::get_model
.
Can parse models. Used for Solver::get_model
.
Can parse proofs. Currenly unused.
Can parse symbols.
Can parse values. Used for Solver::get_values
.
Type Definitions
Alias for the underlying parser.