Trait rsmt2::parse::ModelParser
source · [−]pub trait ModelParser<Ident, Type, Value, Input>: Copy {
fn parse_value(
self,
i: Input,
id: &Ident,
args: &[(Ident, Type)],
out: &Type
) -> SmtRes<Value>;
}
Expand description
Can parse models. Used for Solver::get_model
.
For more information refer to the module-level documentation.
Required Methods
sourcefn parse_value(
self,
i: Input,
id: &Ident,
args: &[(Ident, Type)],
out: &Type
) -> SmtRes<Value>
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
isid
’s “input signature” ((<arg> <arg_sort>) ...
);out
isid
’s output sort (<out_sort>
).