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>
&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 ()