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. for nom,
& str, e.g. for regex,
& 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. Expressions are represented as strings, and Values 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)
}