fn main()

in z3tracer/src/main.rs [199:376]

• 161 lines of code
• 19 McCabe index (conditional complexity)

fn main() {
    let mut options = Options::from_args();
    if options.plot_all {
        options.plot_instantiations = true;
        options.plot_user_instantiations = true;
        options.plot_scopes = true;
        options.plot_conflicts = true;
        options.plot_user_conflicts = true;
        options.plot_instantiation_graph = true;
        options.plot_instantiation_graph_with_conflicts = true;
    }
    for input in &options.inputs {
        let file_name = input.to_str().unwrap().to_string();
        eprintln!("Processing {}", file_name);
        let model = process_file(options.config.clone(), &input).unwrap();
        eprintln!("Done processing {}", file_name);
        eprintln!("Terms: {}", model.terms().len());
        eprintln!("Instantiations: {}", model.instantiations().len());

        if !options.plot_instantiations
            && !options.plot_user_instantiations
            && !options.plot_scopes
            && !options.plot_conflicts
            && !options.plot_user_conflicts
            && !options.plot_instantiation_graph
            && !options.plot_instantiation_graph_with_conflicts
        {
            continue;
        }

        let instantiations = get_instantiations(&model);
        let user_instantiations = instantiations
            .clone()
            .into_iter()
            .filter(|(n, _)| n.starts_with(&options.user_instantiation_prefix))
            .collect::<Vec<_>>();
        let conflicts = model
            .conflicts()
            .map(|c| {
                (
                    c.timestamp,
                    c.qi_deps
                        .iter()
                        .map(|k| model.key2name(&k.key).unwrap_or_else(|| "??".to_string()))
                        .collect::<BTreeSet<_>>(),
                )
            })
            .collect::<Vec<_>>();

        if options.plot_instantiations {
            let path = std::path::PathBuf::from(file_name.clone() + ".qis.png");
            eprintln!(
                "Writing instantiation charts to {}",
                path.to_str().unwrap_or("")
            );
            let backend = BitMapBackend::new(&path, (1000, 800));
            let root = backend.into_drawing_area();
            plot_instantiations(
                root,
                &instantiations,
                "Top Quantifiers Instantiations",
                options.keep_top_instantiations,
            )
            .unwrap();
        }

        if options.plot_user_instantiations {
            let path = std::path::PathBuf::from(file_name.clone() + ".user_qis.png");
            eprintln!(
                "Writing user instantiation charts to {}",
                path.to_str().unwrap_or("")
            );
            let backend = BitMapBackend::new(&path, (1000, 800));
            let root = backend.into_drawing_area();
            plot_instantiations(
                root,
                &user_instantiations,
                "Top User Quantifiers Instantiations",
                options.keep_top_instantiations,
            )
            .unwrap();
        }

        if options.plot_scopes {
            let path = std::path::PathBuf::from(file_name.clone() + ".scopes.png");
            eprintln!("Writing scope charts to {}", path.to_str().unwrap_or(""));

            let scopes = model
                .scopes()
                .iter()
                .map(|s| (s.timestamp, s.level))
                .collect::<Vec<(usize, u64)>>();
            let backend = BitMapBackend::new(&path, (1000, 800));
            let root = backend.into_drawing_area();
            plot_scopes(root, &scopes, "Backtracking levels").unwrap();
        }

        if options.plot_conflicts {
            let path = std::path::PathBuf::from(file_name.clone() + ".conflicts.png");
            eprintln!("Writing conflict charts to {}", path.to_str().unwrap_or(""));

            let backend = BitMapBackend::new(&path, (1000, 800));
            let root = backend.into_drawing_area();
            plot_instantiations_with_conflicts(
                root,
                &instantiations,
                "Top Quantifiers Instantiations + Conflicts",
                options.keep_top_instantiations,
                &conflicts,
            )
            .unwrap();
        }

        if options.plot_user_conflicts {
            let path = std::path::PathBuf::from(file_name.clone() + ".user_conflicts.png");
            eprintln!(
                "Writing user conflict charts to {}",
                path.to_str().unwrap_or("")
            );

            let backend = BitMapBackend::new(&path, (1000, 800));
            let root = backend.into_drawing_area();
            plot_instantiations_with_conflicts(
                root,
                &user_instantiations,
                "Top User Quantifiers Instantiations + Conflicts",
                options.keep_top_instantiations,
                &conflicts,
            )
            .unwrap();
        }

        let keep_only_user_instantiations = if options.keep_only_user_instantiations_in_graphs {
            Some(options.user_instantiation_prefix.as_str())
        } else {
            None
        };

        if options.plot_instantiation_graph {
            let path = std::path::PathBuf::from(file_name.clone() + ".qis_graph.dot");
            eprintln!(
                "Writing dependency graph to {}",
                path.to_str().unwrap_or("")
            );

            let g = get_dependency_graph(&model, false, keep_only_user_instantiations, false);
            let mut f = std::fs::File::create(path.clone()).unwrap();
            writeln!(f, "{}", petgraph::dot::Dot::new(&g)).unwrap();

            std::process::Command::new("dot")
                .args(&["-O", "-Tpng", path.to_str().unwrap()])
                .status()
                .expect("Error running `dot` (is graphviz installed?)");
        }

        if options.plot_instantiation_graph_with_conflicts {
            let path = std::path::PathBuf::from(file_name.clone() + ".qis_and_conflicts_graph.dot");
            eprintln!(
                "Writing dependency graph with conflicts to {}",
                path.to_str().unwrap_or("")
            );

            let g = get_dependency_graph(
                &model,
                true,
                keep_only_user_instantiations,
                options.merge_conflicts_in_graphs,
            );
            let mut f = std::fs::File::create(path.clone()).unwrap();
            writeln!(f, "{}", petgraph::dot::Dot::new(&g)).unwrap();

            std::process::Command::new("dot")
                .args(&["-O", "-Tpng", path.to_str().unwrap()])
                .status()
                .expect("Error running `dot` (is graphviz installed?)");
        }
    }
}