Struct isla_axiomatic::axiomatic::model::Model

pub struct Model<'s, 'ev, B> { /* fields omitted */ }

A model, as parsed from the SMT solver output, contains a list of function declarations (which can have arity 0 for constants) for each declare-const and declare-fun in the model. A model can also be parameterised by a set of events. The two lifetime parameters correspond to the underlying smtlib model 's and the events 'ev.

Implementations

impl<'s, 'ev, B: BV> Model<'s, 'ev, B>

pub fn parse(events: &[&'ev str], model: &'s str) -> Option<Self>

Parse a model from a string of the form (model (define-fun …) (define-fun …) …)

pub fn interpret(
    &mut self,
    f: &str,
    args: &[SexpVal<'ev, B>]
) -> Result<SexpVal<'ev, B>, InterpretError>

Interprets a function in the model

pub fn interpret_rel(
    &mut self,
    rel: &str,
    events: &[&'ev str]
) -> Result<Vec<(&'ev str, &'ev str)>, InterpretError>

Inteprets a relation (an Event * Event -> Bool function) over a set of events. Note that all events in this set must have been used to parameterise the model in Model::parse.

pub fn interpret_bits(&mut self, val: &Val<B>) -> Result<B, InterpretError>

Interpret either a bitvector symbol in the model, or just return the bitvector directory if the val is concrete