Struct z3tracer::model::Model [−][src]
pub struct Model { /* fields omitted */ }
Expand description
Main state of the Z3 tracer.
Implementations
Build a new Z3 tracer.
Experimental. Use Model::default()
instead if possible.
Process some input.
All instantiations in the model.
Number of Z3 logs that were processed.
The current scope in the model.
Construct a max-heap of the (most) instantiated quantified terms.
The QIs seen as explaining the successive conflicts.
Retrieve a particular term, including metadata.
Display a term given by id.