Trait rsmt2::parse::ModelParser

pub trait ModelParser<Ident, Type, Value, Input>: Copy {
    fn parse_value(
        self, 
        i: Input, 
        id: &Ident, 
        args: &[(Ident, Type)], 
        out: &Type
    ) -> SmtRes<Value>;
}

Can parse models. Used for get-model.

For more information refer to the module-level documentation.

Required methods

fn parse_value(
    self,
    i: Input,
    id: &Ident,
    args: &[(Ident, Type)],
    out: &Type
) -> SmtRes<Value>

Parses a value in the context of a get-model command.

When rsmt2 parses a value for some symbol id in a model, it will call this function so that it knows what to construct the value with. Remember that in a model, values are usually presented as

(define-fun <symbol> ( (<arg> <arg_sort>) ... ) <out_sort> <value>)

This function’s purpose is to parse <value> and construct an actual Value, given all the information preceeding the <value> token. So, parameter

• i is the “Text input”, the actual value token tree (<value>);
• id is the symbol (symbol) we’re parsing the value of;
• args is id’s “input signature” ((<arg> <arg_sort>) ...);
• out is id’s output sort (<out_sort>).

Loading content...

Implementors

impl<'a> ModelParser<String, String, Cst, &'a str> for Parser

fn parse_value(
    self,
    input: &'a str,
    _: &String,
    _: &[(String, String)],
    _: &String
) -> SmtRes<Cst>

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

fn parse_value(
    self,
    input: &'a str,
    name: &Ident,
    inputs: &[(Ident, Type)],
    output: &Type
) -> SmtRes<Value>

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

fn parse_value(
    self,
    input: &'a mut SmtParser<Br>,
    name: &Ident,
    inputs: &[(Ident, Type)],
    output: &Type
) -> SmtRes<Value>

Loading content...