在解析日志的同时，将构建一个日志“模型”，以记录大多数操作，以及每个#NUM符号下的句法术语

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)");

此外，库将尝试重建以下信息

• 量词实例化（QIs），即Z3实例化了哪些量化公式以及原因；

• SMT求解过程中的连续回溯级别；

• SAT/SMT冲突及其在QIs方面的因果关系；

• QIs之间的因果关系。

提供了一个基于库的工具z3tracer，用于从命令行处理日志文件z3.log并生成图表。

有关使用Jupyter笔记本的更多示例，请参阅存储库。

目前，此库仅支持Z3 v4.8.9。

有关Z3跟踪日志的更多信息，请参阅项目Axiom Profiler的文档。

贡献

查看CONTRIBUTING文件了解如何提供帮助。

许可证

该项目可以在以下许可证的条款下使用：Apache 2.0许可证或MIT许可证。