Trait rsmt2::ParseSmt2 [−] [src]

pub trait ParseSmt2 {
    type Ident: Debug;
    type Value: Debug;
    type Expr: Debug;
    type Proof: Debug;
    type I;
    fn parse_ident<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Ident>;
    fn parse_value<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Value>;
    fn parse_expr<'a>(&self,
                      _: &'a [u8],
                      _: &Self::I)
                      -> IResult<&'a [u8], Self::Expr>;
    fn parse_proof<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Proof>;
}

Parsers on the user's structure.

Not all of them are necessary depending on the queries wanted. See each method for details.

Associated Types

`type Ident: Debug`

Type of identifiers in the user's structure.

`type Value: Debug`

Type of values in the user's structure.

`type Expr: Debug`

Type of expressions in the user's structure.

`type Proof: Debug`

Type of proofs in the user's structure.

`type I`

Type of the info passed when parsing expressions.

Required Methods

`fn parse_ident<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Ident>`

Parses an ident from self, viewed as a reader.

Required by

get-assignment
get-model
get-unsat-assumptions
get-unsat-core

`fn parse_value<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Value>`

Parses a value from self, viewed as a reader.

Required by

get-value
get-assignment
get-model

`fn parse_expr<'a>(&self, _: &'a [u8], _: &Self::I) -> IResult<&'a [u8], Self::Expr>`

Parses an expression from self, viewed as a reader.

Required by

get_assertions

`fn parse_proof<'a>(&self, _: &'a [u8]) -> IResult<&'a [u8], Self::Proof>`

Parses a proof from self, viewed as a reader.

Required by

get_proof

Implementors

impl ParseSmt2 for ()