:sccache 1
:dep prover-lab = { path = "../.." }
:dep z3tracer = "0.8.0"

use prover_lab::z3log::*;

let model = process_file("/tmp/mvp.z3log")?;

// Compute top instantiated terms and retrieve the "timestamps" at which instantiations occur for each of the top terms.
let instantiation_times = compute_instantiation_times(&model);

plot_instantiations(&instantiation_times, "Top 10 Quantifiers Instantiations", 10)

let user_instantiation_times = instantiation_times.clone().into_iter()
                  .filter(|(n, _)| n.starts_with("outputbpl")).collect::<Vec<_>>();
plot_instantiations(&user_instantiation_times, "Top 10 User Quantifiers Instantiations", 10)