Crate z3tracer[−][src]

Expand description

This crate provides an experimental parser and analyzer for detailed log files produced by Z3.

To obtain a file z3.log, pass the options trace=true and proof=true on the command line of Z3 (for instance, z3 trace=true proof=true file.smt2). For large problems, you may choose to limit the size of the log file by interrupting z3 with ^C or by setting a shorter timeout. Passing only trace=true is also possible but it will prevent any dependency analysis (see below).

While parsing the logs, a “model” of the logs is constructed to record most operations, as well as the syntactic terms under each #NUM notation:

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

Besides, the library will attempt to reconstruct the following information:

Quantifier Instantiations (QIs), that is, which quantified formulas were instantiated by Z3 and why;
The successive backtracking levels during SMT solving;
SAT/SMT conflicts and their causal dependencies in terms of QIs;
Causal dependencies between QIs.