Trait rsmt2::parse::IdentParser

pub trait IdentParser<Ident, Type, Input>: Copy {
    fn parse_ident(self, i: Input) -> SmtRes<Ident>;
    fn parse_type(self, i: Input) -> SmtRes<Type>;
}

Can parse identifiers and types. Used for Solver::get_model.

For more information refer to the module-level documentation.

Required methods

fn parse_ident(self, i: Input) -> SmtRes<Ident>

Parses an identifier.

fn parse_type(self, i: Input) -> SmtRes<Type>

Parses a type.

Implementations on Foreign Types

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>

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

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>

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

Implementors

impl<'a> IdentParser<String, String, &'a str> for Parser

impl<'a, Ident, Type, T> IdentParser<Ident, Type, &'a str> for T where
    T: IdentParser<Ident, Type, &'a [u8]>, 

impl<'a, Ident, Type, T, Br> IdentParser<Ident, Type, &'a mut SmtParser<Br>> for T where
    T: IdentParser<Ident, Type, &'a str>,
    Br: BufRead,