Crate z3tracer

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

Currently, this library only supports Z3 v4.8.9

use z3tracer::{Model, syntax::{Ident, Term}};
let mut model = 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);
assert!(matches!(model.term(&Ident::from_str("#1")?)?, Term::App { .. }));
assert_eq!(model.id_to_sexp(&BTreeMap::new(), &Ident::from_str("#1").unwrap()).unwrap(), "(+ a a)");

See also in the repository for more complex examples using Jupyter notebooks.

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.
lexer	Tokenization of Z3 logs.
model	Main analyzer module.
parser	Parsing of Z3 logs.
syntax	Terms and data structures found in Z3 logs.