fn get_dependency_graph()

in z3tracer/src/main.rs [95:197]

• 92 lines of code
• 26 McCabe index (conditional complexity)

fn get_dependency_graph(
    model: &Model,
    with_conflicts: bool,
    keep_only_user_instantiations: Option<&str>,
    merge_conflicts_in_graphs: bool,
) -> petgraph::Graph<String, String> {
    // Define nodes as the names of QIs (e.g. the names of quantified expressions in the source code).
    let nodes = model
        .instantiations()
        .iter()
        .filter_map(|(k, _)| {
            if model.key2name(k).is_some() {
                model.key2name(k)
            } else {
                None
            }
        })
        .collect::<HashSet<_>>();

    // Define weighted edges (counting dependencies in the original graph of QIs).
    let edges = {
        let mut map = HashMap::new();
        for (k, qi) in model.instantiations() {
            if let Some(name) = model.key2name(k) {
                let deps = map.entry(name).or_insert_with(HashMultiSet::new);
                for qik in &qi.qi_deps {
                    if let Some(n) = model.key2name(&qik.key) {
                        deps.insert(n);
                    }
                }
            }
        }
        map
    };

    // Translate the graph into `petgraph` for drawing purposes.
    let mut graph = Graph::<String, String>::new();

    let mut pg_nodes = HashMap::new();
    for node in &nodes {
        if let Some(prefix) = keep_only_user_instantiations {
            if !node.starts_with(prefix) {
                continue;
            }
        }
        let n = graph.add_node(node.to_string());
        pg_nodes.insert(node.to_string(), n);
    }

    for (n, d) in edges.iter() {
        if let Some(n) = pg_nodes.get(n) {
            for m in d.distinct_elements() {
                let c = d.count_of(m);
                if let Some(m) = pg_nodes.get(m) {
                    graph.add_edge(*n, *m, c.to_string());
                }
            }
        }
    }

    if with_conflicts {
        if merge_conflicts_in_graphs {
            // Adding one node for all conflicts.
            let n0 = graph.add_node("all conflicts".into());
            let mut outgoing = HashMultiSet::new();
            for c in model.conflicts() {
                for d in &c.qi_deps {
                    if let Some(m) = model.key2name(&d.key) {
                        outgoing.insert(m)
                    }
                }
            }
            for m in outgoing.distinct_elements() {
                let c = outgoing.count_of(m);
                if let Some(m) = pg_nodes.get(m) {
                    graph.add_edge(n0, *m, c.to_string());
                }
            }
        } else {
            // Adding conflicts separately (with multiplicities as weights)
            for c in model.conflicts() {
                let mut outgoing = HashMultiSet::new();
                for d in &c.qi_deps {
                    if let Some(m) = model.key2name(&d.key) {
                        outgoing.insert(m)
                    }
                }
                if outgoing.is_empty() {
                    // Skip dependency-less conflicts.
                    continue;
                }
                let n = graph.add_node(format!("conflict@{}", c.timestamp));
                for m in outgoing.distinct_elements() {
                    let c = outgoing.count_of(m);
                    if let Some(m) = pg_nodes.get(m) {
                        graph.add_edge(n, *m, c.to_string());
                    }
                }
            }
        }
    }
    graph
}