Struct z3tracer::model::Model

pub struct Model { /* fields omitted */ }

Main state of the Z3 tracer.

Implementations

impl Model

pub fn new(config: ModelConfig) -> Self

Build a new Z3 tracer. Experimental. Use Model::default() instead if possible.

pub fn process<R>(&mut self, path_name: Option<String>, input: R) -> Result<()> where
    R: BufRead, 

Process some input.

pub fn terms(&self) -> &BTreeMap<Ident, TermData>

All terms in the model.

pub fn instantiations(&self) -> &BTreeMap<QiKey, QuantInstantiation>

All instantiations in the model.

pub fn processed_logs(&self) -> usize

Number of Z3 logs that were processed.

pub fn scopes(&self) -> &Vec<Scope>

All (finalized) scopes in the model.

pub fn current_scope(&self) -> &Scope

The current scope in the model.

pub fn most_instantiated_terms(&self) -> BinaryHeap<(usize, Ident)>

Construct a max-heap of the (most) instantiated quantified terms.

pub fn conflicts(&self) -> impl Iterator<Item = &Conflict>

The QIs seen as explaining the successive conflicts.

pub fn term(&self, id: &Ident) -> RawResult<&Term>

Retrieve a particular term.

pub fn term_data(&self, id: &Ident) -> RawResult<&TermData>

Retrieve a particular term, including metadata.

pub fn id_to_sexp(
    &self,
    venv: &BTreeMap<u64, Symbol>,
    id: &Ident
) -> RawResult<String>

Display a term given by id.

pub fn term_to_sexp(
    &self,
    venv: &BTreeMap<u64, Symbol>,
    term: &Term
) -> RawResult<String>

Display a term by id.

Trait Implementations

impl Debug for Model

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Model

fn default() -> Model

Returns the “default value” for a type.

impl LogVisitor for &mut Model

fn add_term(&mut self, ident: Ident, term: Term) -> RawResult<()>

fn add_instantiation(&mut self, key: QiKey, frame: QiFrame) -> RawResult<()>

fn start_instance(&mut self, key: QiKey, instance: QiInstance) -> RawResult<()>

fn end_instance(&mut self) -> RawResult<()>

fn add_equality(&mut self, id: Ident, eq: Equality) -> RawResult<()>

fn attach_meaning(&mut self, id: Ident, m: Meaning) -> RawResult<()>

fn attach_var_names(&mut self, id: Ident, names: Vec<VarName>) -> RawResult<()>

fn attach_enode(&mut self, id: Ident, _generation: u64) -> RawResult<()>

fn tool_version(&mut self, _s1: String, _s2: String) -> RawResult<()>

fn begin_check(&mut self, _i: u64) -> RawResult<()>

fn assign(&mut self, lit: Literal, _s: String) -> RawResult<()>

fn conflict(&mut self, lits: Vec<Literal>, _s: String) -> RawResult<()>

fn push(&mut self, level: u64) -> RawResult<()>

fn pop(&mut self, num: u64, current_level: u64) -> RawResult<()>

fn resolve_lit(&mut self, _i: u64, lit: Literal) -> RawResult<()>

fn resolve_process(&mut self, lit: Literal) -> RawResult<()>