#smt #solver #z3

bin+lib z3tracer

Parser for Z3 tracing logs

14 releases (breaking)

0.11.1 Jun 9, 2021
0.10.0 Apr 13, 2021
0.7.0 Mar 24, 2021

#36 in Science

Download history 24/week @ 2021-02-26 39/week @ 2021-03-05 104/week @ 2021-03-12 69/week @ 2021-03-19 96/week @ 2021-03-26 87/week @ 2021-04-02 1496/week @ 2021-04-09 1222/week @ 2021-04-16 1768/week @ 2021-04-23 1754/week @ 2021-04-30 2435/week @ 2021-05-07 1512/week @ 2021-05-14 1795/week @ 2021-05-21 1085/week @ 2021-05-28 1529/week @ 2021-06-04 1588/week @ 2021-06-11

4,855 downloads per month

MIT/Apache

6MB
7K SLoC

z3tracer

z3tracer on crates.io Documentation License License

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.

Contributing

See the CONTRIBUTING file for how to help out.

License

This project is available under the terms of either the Apache 2.0 license or the MIT license.

Dependencies

~4.5–9.5MB
~117K SLoC