Clean up explanation code

axiom-profiler-GUI/src/results/filters.rs

@@ -1,10 +1,10 @@
 use petgraph::{
     visit::{Dfs, Walker},
-    Direction, Graph,
+    Direction,
 };
 use smt_log_parser::{
     analysis::{
-        analysis::matching_loop::{MLGraphEdge, MLGraphNode},
+        analysis::matching_loop::MlExplanation,
         raw::{IndexesInstGraph, Node, NodeKind, RawInstGraph},
         InstGraph, RawNodeIndex,
     },
@@ -222,7 +222,7 @@ impl Filter {
 pub enum FilterOutput {
     LongestPath(Vec<RawNodeIndex>),
     MatchingLoopGeneralizedTerms(Vec<String>),
-    MatchingLoopGraph(Graph<MLGraphNode, MLGraphEdge>),
+    MatchingLoopGraph(Option<MlExplanation>),
     None,
 }
 

axiom-profiler-GUI/src/results/svg_result.rs

@@ -20,11 +20,10 @@ use palette::{encoding::Srgb, white_point::D65, FromColor, Hsluv, Hsv, LuvHue};
 use petgraph::{
     dot::{Config, Dot},
     visit::EdgeRef,
-    Graph,
 };
 use smt_log_parser::{
     analysis::{
-        analysis::matching_loop::{MLGraphEdge, MLGraphNode},
+        analysis::matching_loop::{MLGraphNode, MlExplanation},
         raw::NodeKind,
         visible::VisibleInstGraph,
         InstGraph, RawNodeIndex, VisibleEdgeIndex,
@@ -69,7 +68,7 @@ pub enum Msg {
     ResetGraph,
     UserPermission(WarningChoice),
     WorkerOutput(super::worker::WorkerOutput),
-    RenderMLGraph(Graph<MLGraphNode, MLGraphEdge>),
+    RenderMLGraph(Option<MlExplanation>),
     // UpdateSelectedNodes(Vec<RawNodeIndex>),
     // SearchMatchingLoops,
     // SelectNthMatchingLoop(usize),
@@ -508,7 +507,9 @@ impl Component for SVGResult {
                 true
             }
             Msg::RenderMLGraph(graph) => {
-                let _filtered_graph = &graph;
+                let Some(graph) = graph else {
+                    return false;
+                };
                 let cfg = ctx.link().get_configuration().unwrap();
                 let mut ctxt = DisplayCtxt {
                     parser: &parser.borrow(),
@@ -535,7 +536,7 @@ impl Component for SVGResult {
                     "digraph {{\n{}\n{:?}\n}}",
                     settings.join("\n"),
                     Dot::with_attr_getters(
-                        &graph,
+                        &*graph.graph,
                         &[
                             Config::EdgeNoLabel,
                             Config::NodeNoLabel,

smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs

@@ -1,28 +1,25 @@
 use fxhash::FxHashSet;
-use petgraph::graph::NodeIndex;
 
 use crate::{
     analysis::{
         analysis::{MlEndNodes, TopoAnalysis},
         raw::Node,
         InstGraph, RawNodeIndex,
     },
-    items::{Blame, EqualityExpl, InstIdx},
+    items::{Blame, InstIdx, TermIdx},
     parsers::z3::synthetic::SynthIdx,
-    FxHashMap, Graph, Z3Parser,
+    FxHashMap, Z3Parser,
 };
 
-use super::{MLGraphEdge, MLGraphNode, MlSignature};
+use super::{MlExplanation, MlSignature};
 
 pub struct MlOutput {
-    ml_leaves: MlEndNodes,
+    pub(super) ml_leaves: MlEndNodes,
     pub ml_nodes: FxHashSet<InstIdx>,
-    node_to_ml: FxHashMap<InstIdx, MlNodeInfo>,
+    pub(super) node_to_ml: FxHashMap<InstIdx, MlNodeInfo>,
     topo: FxHashMap<InstIdx, FxHashSet<InstIdx>>,
 }
 
-type InstGraphNodes = (NodeIndex, Vec<(NodeIndex, Vec<NodeIndex>)>);
-
 impl MlOutput {
     pub fn leaves(&self) -> impl Iterator<Item = &(MlSignature, Vec<(u32, InstIdx)>)> + '_ {
         self.ml_leaves
@@ -33,123 +30,26 @@ impl MlOutput {
     pub fn others_between(&self, iidx: InstIdx) -> FxHashSet<InstIdx> {
         let node = &self.node_to_ml[&iidx];
         let mut others_between = self.topo[&iidx].clone();
-        for above in &node.tree_above {
-            for above_all in &self.topo[above] {
+        for above in node.tree_above() {
+            for above_all in &self.topo[&above] {
                 others_between.remove(above_all);
             }
         }
         assert!(others_between.contains(&iidx));
         others_between
     }
 
-    pub fn ml_graphs(&self, parser: &mut Z3Parser) -> Vec<Graph<MLGraphNode, MLGraphEdge>> {
+    pub fn ml_graphs(&self, parser: &mut Z3Parser) -> Vec<MlExplanation> {
         self.leaves()
             .map(|(_sig, leaves)| {
-                let mut graph = Graph::with_capacity(0, 0);
-
                 let iidx = leaves[0].1;
-                let leaf = &self.node_to_ml[&iidx];
-                let others_between = self.others_between(iidx);
-                let insts_map: FxHashMap<_, _> = others_between
-                    .into_iter()
-                    .map(|iidx| (iidx, self.add_inst(parser, &mut graph, iidx)))
-                    .collect();
-                let root = insts_map[&iidx].0;
-
-                for (iidx, idata) in insts_map.iter() {
-                    self.add_dependencies(&*parser, &mut graph, *iidx, idata, |get_iidx| {
-                        if leaf.tree_above.contains(&get_iidx) {
-                            Some((root, true))
-                        } else {
-                            insts_map.get(&get_iidx).map(|(node, _)| (*node, false))
-                        }
-                    });
-                }
 
-                graph
+                let mut expl = MlExplanation::new();
+                expl.explain_leaf(self, parser, iidx);
+                expl
             })
             .collect()
     }
-
-    fn add_inst(
-        &self,
-        parser: &mut Z3Parser,
-        graph: &mut Graph<MLGraphNode, MLGraphEdge>,
-        iidx: InstIdx,
-    ) -> InstGraphNodes {
-        let inst = &self.node_to_ml[&iidx];
-        let sig = self.ml_leaves[inst.ml_sig].0.clone();
-        let gen_pat = parser
-            .synth_terms
-            .generalise_pattern(&parser.terms, sig.pattern)
-            .unwrap();
-        let node = MLGraphNode::QI(sig, gen_pat);
-        let node = graph.add_node(node);
-        let generalisation = inst
-            .generalisation
-            .iter()
-            .map(|gen| {
-                let enode = graph.add_node(MLGraphNode::ENode(gen.enode));
-                let mut last_node = enode;
-                let equalities: Vec<_> = gen
-                    .equalities
-                    .iter()
-                    .map(|&(from, to)| {
-                        let equality = graph.add_node(MLGraphNode::Equality(from, to));
-                        graph.add_edge(last_node, equality, MLGraphEdge::BlameRewrite);
-                        last_node = equality;
-                        equality
-                    })
-                    .collect();
-                graph.add_edge(last_node, node, MLGraphEdge::Blame);
-                (enode, equalities)
-            })
-            .collect();
-        (node, generalisation)
-    }
-
-    fn add_dependencies(
-        &self,
-        parser: &Z3Parser,
-        graph: &mut Graph<MLGraphNode, MLGraphEdge>,
-        iidx: InstIdx,
-        idata: &InstGraphNodes,
-        insts_map: impl Fn(InstIdx) -> Option<(NodeIndex, bool)>,
-    ) {
-        let inst = &parser[iidx];
-        let match_ = &parser[inst.match_];
-        for (i, tm) in match_.trigger_matches().enumerate() {
-            let curr_idata = &idata.1[i];
-
-            let tm_enode = tm.enode();
-            let blame = &parser[tm_enode];
-            if let Some(created_by) = blame.created_by {
-                if let Some((created_by, rec)) = insts_map(created_by) {
-                    graph.add_edge(created_by, curr_idata.0, MLGraphEdge::Yield(rec));
-                }
-            }
-
-            for (i, eq) in tm
-                .equalities()
-                .filter(|&eq| parser[eq].given_len > 0)
-                .enumerate()
-            {
-                parser.egraph.walk_trans(eq, |given, _| {
-                    let EqualityExpl::Literal { eq, .. } = &parser[given] else {
-                        return;
-                    };
-                    let eq = &parser[*eq];
-                    if let Some((created_by, rec)) = eq.created_by.and_then(&insts_map) {
-                        graph.add_edge(created_by, curr_idata.1[i], MLGraphEdge::YieldEq(rec));
-                    }
-                    // else {
-                    //     let fixed = graph.add_node(MLGraphNode::FixedEquality(eq.owner));
-                    //     graph.add_edge(fixed, curr_idata.1[i], MLGraphEdge::FixedEquality);
-                    // }
-                });
-            }
-        }
-    }
 }
 
 pub struct MlAnalysis<'a> {
@@ -218,10 +118,13 @@ impl<'a> MlAnalysis<'a> {
         data: &MlNodeInfo,
         ml_nodes: &mut FxHashSet<InstIdx>,
     ) {
-        for &reachable in &data.tree_above {
-            if ml_nodes.insert(reachable) {
-                let data = &node_to_ml[&reachable];
-                Self::walk_tree(node_to_ml, data, ml_nodes);
+        let mut stack = vec![data];
+        while let Some(data) = stack.pop() {
+            for reachable in data.tree_above() {
+                if ml_nodes.insert(reachable) {
+                    let data = &node_to_ml[&reachable];
+                    stack.push(data);
+                }
             }
         }
     }
@@ -232,18 +135,18 @@ pub struct MlNodeInfo {
     pub is_root: bool,
     pub ml_sig: usize,
     pub ast_size: u32,
-    pub tree_above: FxHashSet<InstIdx>,
+    pub tree_above: Vec<InstIdx>,
     pub max_depth: u32,
-    pub generalisation: Vec<GeneralisedBlame>,
+    pub generalisation: Vec<GeneralisedBlame<SynthIdx>>,
 }
 
 #[derive(Debug)]
-pub struct GeneralisedBlame {
-    pub enode: SynthIdx,
-    pub equalities: Vec<(SynthIdx, SynthIdx)>,
+pub struct GeneralisedBlame<Idx> {
+    pub enode: Idx,
+    pub equalities: Vec<(Idx, Idx)>,
 }
 
-impl GeneralisedBlame {
+impl<T: From<TermIdx>> GeneralisedBlame<T> {
     pub fn new(parser: &Z3Parser, blame: Blame<'_>) -> Self {
         let enode = parser[blame.enode()].owner.into();
         let equalities = blame
@@ -260,41 +163,61 @@ impl GeneralisedBlame {
             .collect();
         Self { enode, equalities }
     }
-
-    pub fn generalise(&mut self, other: &Self, parser: &mut Z3Parser) {
-        self.enode = parser
+}
+impl GeneralisedBlame<SynthIdx> {
+    pub fn generalise(&self, curr: GeneralisedBlame<TermIdx>, parser: &mut Z3Parser) -> Self {
+        let enode = parser
             .synth_terms
-            .generalise(&parser.terms, vec![self.enode, other.enode])
+            .generalise(&parser.terms, self.enode, curr.enode)
             .unwrap();
-        assert_eq!(self.equalities.len(), other.equalities.len());
-        for (self_eq, other_eq) in self.equalities.iter_mut().zip(other.equalities.iter()) {
-            self_eq.0 = parser
-                .synth_terms
-                .generalise(&parser.terms, vec![self_eq.0, other_eq.0])
-                .unwrap();
-            self_eq.1 = parser
-                .synth_terms
-                .generalise(&parser.terms, vec![self_eq.1, other_eq.1])
-                .unwrap();
-        }
+        assert_eq!(self.equalities.len(), curr.equalities.len());
+        let equalities = self
+            .equalities
+            .iter()
+            .zip(curr.equalities.iter())
+            .map(|(self_eq, other_eq)| {
+                let from = parser
+                    .synth_terms
+                    .generalise(&parser.terms, self_eq.0, other_eq.0)
+                    .unwrap();
+                let to = parser
+                    .synth_terms
+                    .generalise(&parser.terms, self_eq.1, other_eq.1)
+                    .unwrap();
+                (from, to)
+            })
+            .collect();
+        Self { enode, equalities }
     }
 }
 
 impl MlNodeInfo {
-    pub fn new(parser: &Z3Parser, iidx: InstIdx, ml_sig: usize) -> Self {
+    pub fn generalisation<T: From<TermIdx>>(
+        parser: &Z3Parser,
+        iidx: InstIdx,
+    ) -> impl Iterator<Item = GeneralisedBlame<T>> + '_ {
         let generalisation = parser[parser[iidx].match_].trigger_matches();
-        let generalisation = generalisation
-            .map(|blame| GeneralisedBlame::new(parser, blame))
-            .collect();
+        generalisation.map(|blame| GeneralisedBlame::new(parser, blame))
+    }
+
+    pub fn new(parser: &Z3Parser, iidx: InstIdx, ml_sig: usize) -> Self {
         Self {
             is_root: true,
             ml_sig,
             ast_size: parser.inst_ast_size(iidx),
-            tree_above: FxHashSet::default(),
+            tree_above: Default::default(),
             max_depth: 0,
-            generalisation,
+            generalisation: Vec::new(),
         }
     }
+
+    pub fn tree_above(&self) -> impl Iterator<Item = InstIdx> + '_ {
+        // TODO: handle when `tree_above.len() > 1`
+        self.tree_above.first().copied().into_iter()
+    }
+    pub fn tree_above_contains(&self, iidx: InstIdx) -> bool {
+        self.tree_above().any(|i| i == iidx)
+    }
 }
 
 impl TopoAnalysis<true, false> for MlAnalysis<'_> {
@@ -327,20 +250,29 @@ impl TopoAnalysis<true, false> for MlAnalysis<'_> {
             if prev_info.ml_sig == curr_info.ml_sig && prev_info.ast_size <= curr_info.ast_size {
                 prev_info.is_root = false;
                 curr_info.max_depth = curr_info.max_depth.max(prev_info.max_depth + 1);
-                curr_info.tree_above.insert(prev_iidx);
-                let gen = curr_info
-                    .generalisation
-                    .iter_mut()
-                    .zip(prev_info.generalisation.iter());
-                for (curr_gen, prev_gen) in gen {
-                    curr_gen.generalise(prev_gen, self.parser);
-                }
+                curr_info.tree_above.push(prev_iidx);
                 false
             } else {
                 true
             }
         });
 
+        curr_info
+            .tree_above
+            .sort_unstable_by_key(|&pidx| (u32::MAX - self.node_to_ml[&pidx].max_depth, pidx));
+        let generalisation = if let Some(pidx) = curr_info.tree_above().next() {
+            let gen: Vec<_> = MlNodeInfo::generalisation(self.parser, iidx).collect();
+            self.node_to_ml[&pidx]
+                .generalisation
+                .iter()
+                .zip(gen)
+                .map(|(prev_gen, curr_gen)| prev_gen.generalise(curr_gen, self.parser))
+                .collect()
+        } else {
+            MlNodeInfo::generalisation(self.parser, iidx).collect()
+        };
+        curr_info.generalisation = generalisation;
+
         self.node_to_ml.insert(iidx, curr_info);
         self_info.insert(iidx);
         self_info