Module isla_axiomatic::axiomatic::model [−][src]
This module defines utilites for parsing and interpreting the models returned by Z3 when invoked on the command line.
Structs
| Model | 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 |