Crate z3tracer

This crate provides an experimental parser for Z3 tracing logs obtained by passing trace=true proof=true.

let mut model = z3tracer::Model::default();
let input = br#"
[mk-app] #0 a
[mk-app] #1 + #0 #0
[eof]
"#;
model.process(None, &input[1..])?;
assert_eq!(model.terms().len(), 2);

More information about Z3 tracing logs can be found in the documentation of the project Axiom Profiler.

Re-exports

pub use error::Error;

pub use error::Result;

pub use model::Model;

pub use model::ModelConfig;

Modules

error	Error management.
model	Main analyzer module.
parser	Parsing of Z3 logs.
syntax	Terms and data structures found in Z3 logs.