This crate provides an experimental parser for Z3 tracing logs obtained by passing
trace=true proof=true.
rust
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.
See the CONTRIBUTING file for how to help out.
This project is available under the terms of either the Apache 2.0 license or the MIT license.