Crate z3tracer[−][src]
This crate provides an experimental parser for Z3 tracing logs obtained by passing
trace=true proof=true
.
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. |