First attempt for matching loop detection

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

@@ -20,6 +20,7 @@ pub enum Filter {
     VisitSubTreeWithRoot(NodeIndex, bool),
     MaxDepth(usize),
     ShowLongestPath(NodeIndex),
+    ShowMatchingLoops,
 }
 
 impl Display for Filter {
@@ -46,6 +47,7 @@ impl Display for Filter {
             },
             Self::MaxDepth(depth) => write!(f, "Show nodes up to depth {}", depth),
             Self::ShowLongestPath(node) => write!(f, "Showing longest path through node {}", node.index()),
+            Self::ShowMatchingLoops => write!(f, "Showing matching loops (experimental)"),
         }
     }
 }
@@ -68,6 +70,7 @@ impl Filter {
             Filter::VisitSourceTree(nidx, retain) => graph.visit_ancestors(nidx, retain),
             Filter::MaxDepth(depth) => graph.retain_nodes(|node: &NodeData| node.min_depth.unwrap() <= depth),
             Filter::ShowLongestPath(nidx) => return Some(graph.show_longest_path_through(nidx)),
+            Filter::ShowMatchingLoops => graph.show_matching_loops(), 
         }
         None
     }
@@ -111,6 +114,10 @@ pub fn graph_filter(props: &GraphFilterProps) -> Html {
         let callback = props.add_filters.clone();
         Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth.value)]))
     };
+    let show_matching_loops = {
+        let callback = props.add_filters.clone();
+        Callback::from(move |_| callback.emit(vec![Filter::ShowMatchingLoops]))
+    };
     html! {
         <div>
             <h2>{"Add (optional) filters:"}</h2>
@@ -158,6 +165,10 @@ pub fn graph_filter(props: &GraphFilterProps) -> Html {
                 />
                 <button onclick={add_max_depth_filter}>{"Add"}</button>
             </div>
+            <div>
+                <label for="matching_loops">{"Show matching loops"}</label>
+                <button onclick={show_matching_loops} id="matching_loops">{"Add"}</button>
+            </div>
             {if selected_insts.len() > 0 {
                 html! {
                     <NodeActions selected_nodes={selected_insts} action={props.add_filters.clone()} />

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

@@ -140,7 +140,7 @@ impl Component for SVGResult {
             }
             Msg::ResetGraph => {
                 log::debug!("Resetting graph");
-                self.inst_graph.reset();
+                self.inst_graph.reset_visibility_to(true);
                 false
             }
             Msg::RenderGraph(UserPermission { permission }) => {

smt-log-parser/src/parsers/z3/inst_graph.rs

@@ -1,4 +1,4 @@
-use fxhash::FxHashMap;
+use fxhash::{FxHashMap, FxHashSet};
 use gloo_console::log;
 use petgraph::graph::{Edge, NodeIndex};
 use petgraph::stable_graph::StableGraph;
@@ -17,6 +17,8 @@ use crate::items::{BlamedTermItem, InstIdx, QuantIdx, TermIdx, DepType, Dependen
 
 use super::z3parser::Z3Parser;
 
+const MATCHING_LOOP_LOWER_BOUND: usize = 3;
+
 #[derive(Clone, Copy, Default)]
 pub struct NodeData {
     pub line_nr: usize,
@@ -99,6 +101,7 @@ pub struct InstGraph {
     cost_ranked_node_indices: Vec<NodeIndex>,
     branching_ranked_node_indices: Vec<NodeIndex>,
     tr_closure: Vec<RoaringBitmap>,
+    non_theory_quants: FxHashSet<QuantIdx>,
 }
 
 enum InstOrder {
@@ -394,9 +397,74 @@ impl InstGraph {
     //     }
     // }
 
-    pub fn reset(&mut self) {
+    pub fn show_matching_loops(&mut self) {
+        let mut matching_loops: Vec<Vec<NodeIndex>> = Vec::new();
+        for quant in self.non_theory_quants.clone() {
+            // log!(format!("Processing quant {}", quant));
+            self.reset_visibility_to(true);
+            self.retain_nodes(|node: &NodeData| !node.is_theory_inst && node.quant_idx == quant);
+            self.retain_visible_nodes_and_reconnect();
+            let mut subgraph_of_quant: Graph<NodeData, EdgeData> = Graph::from(self.visible_graph.clone());
+            let longest_path = Self::find_longest_path(&mut subgraph_of_quant);
+            matching_loops.push(longest_path);
+        }
+        self.reset_visibility_to(false);
+        for matching_loop in matching_loops {
+            if matching_loop.len() >= MATCHING_LOOP_LOWER_BOUND {
+                for node in matching_loop {
+                    // log!(format!("Node {} is part of a matching loop", node.index()));
+                    self.orig_graph[node].visible = true;
+                }
+            }
+        }
+    }
+
+    fn find_longest_path(graph: &mut Graph<NodeData, EdgeData>) -> Vec<NodeIndex> {
+        // traverse this subtree in topological order to compute longest distances from node
+        let mut topo = Topo::new(&*graph);
+        while let Some(nx) = topo.next(&*graph) {
+            let parents = graph.neighbors_directed(nx, Incoming); 
+            let max_parent_depth = parents
+                .map(|nx| graph.node_weight(nx).unwrap().max_depth)
+                .max(); 
+            if let Some(depth) = max_parent_depth {
+                // log!(format!("Computing depth {} for node {}", depth + 1, nx.index()));
+                graph[nx].max_depth = depth + 1;
+            } else {
+                graph[nx].max_depth = 0;
+                // log!(format!("Computing depth {} for node {}", 0, nx.index()));
+            }
+        }
+        let furthest_away_node_idx = graph 
+            .node_indices()
+            .max_by(|node_a, node_b| graph.node_weight(*node_a).unwrap().max_depth.cmp(&graph.node_weight(*node_b).unwrap().max_depth))
+            .unwrap();
+        // log!(format!("Furthest away node is {}", furthest_away_node_idx.index()));
+        // backtrack a longest path from furthest away node in subgraph until we reach a root 
+        let mut longest_path: Vec<NodeIndex> = Vec::new();
+        let mut visitor: Vec<NodeIndex>= Vec::new();
+        visitor.push(furthest_away_node_idx);
+        while let Some(curr) = visitor.pop() {
+            // log!(format!("Backtracking. Currently at node {}", curr.index()));
+            longest_path.push(graph.node_weight(curr).unwrap().orig_graph_idx);
+            let curr_distance = graph.node_weight(curr).unwrap().max_depth;
+            let pred = graph 
+                .neighbors_directed(curr, Incoming)
+                .filter(|pred| { 
+                    let pred_distance = graph.node_weight(*pred).unwrap().max_depth; 
+                    pred_distance == curr_distance - 1 
+                })
+                .last();
+            if let Some(node) = pred {
+                visitor.push(node);
+            }
+        }
+        longest_path
+    }
+
+    pub fn reset_visibility_to(&mut self, visibility: bool) {
         for node in self.orig_graph.node_weights_mut() {
-            node.visible = true;
+            node.visible = visibility;
         }
     }
 
@@ -536,6 +604,10 @@ impl InstGraph {
                     max_depth: 0,
                     topo_ord: 0,
                 });
+                if !dep.quant_discovered {
+                    self.non_theory_quants.insert(quant_idx);
+                    // log!(format!("Inserting quant {} into non_theory_quants", quant_idx));
+                }
             }
         }
         // then add all edges between nodes