Added feature to analyze matching loop with selected end-node

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

@@ -24,6 +24,7 @@ pub enum Filter {
     ShowLongestPath(NodeIndex),
     SelectNthMatchingLoop(usize),
     ShowMatchingLoopSubgraph,
+    AnalyzeMatchingLoopWithEndNode(NodeIndex),
 }
 
 impl Display for Filter {
@@ -75,6 +76,7 @@ impl Display for Filter {
             Self::ShowMatchingLoopSubgraph => {
                 write!(f, "Showing all potential matching loops")
             }
+            Self::AnalyzeMatchingLoopWithEndNode(node) => write!(f, "Analyzing potential matching loop with end-node {}", node.index()),
         }
     }
 }
@@ -102,6 +104,7 @@ impl Filter {
             Filter::ShowLongestPath(nidx) => return FilterOutput::LongestPath(graph.show_longest_path_through(nidx)),
             Filter::SelectNthMatchingLoop(n) => return FilterOutput::MatchingLoopGraph(graph.show_nth_matching_loop(n, parser)),
             Filter::ShowMatchingLoopSubgraph => graph.show_matching_loop_subgraph(),
+            Filter::AnalyzeMatchingLoopWithEndNode(endnode) => return FilterOutput::MatchingLoopGraph(graph.analyze_matching_loop_with_endnode(endnode, parser)),
         }
         FilterOutput::None
     }

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

@@ -47,6 +47,9 @@ pub fn node_actions(props: &NodeActionsProps) -> Html {
     let show_longest_path = callback_from(Box::new(|inst: &InstInfo| {
         Filter::ShowLongestPath(inst.node_index)
     }));
+    let analyze_matching_loop_with_endnode = callback_from(Box::new(|inst: &InstInfo| {
+        Filter::AnalyzeMatchingLoopWithEndNode(inst.node_index)
+    }));
     html! {
     <>
         <h4>{"You have selected some nodes. Here are possible actions (applied to all selected nodes):"}</h4>
@@ -71,6 +74,9 @@ pub fn node_actions(props: &NodeActionsProps) -> Html {
         <div>
             <button onclick={show_longest_path}>{"Show longest path through last selected node"}</button>
         </div>
+        <div>
+            <button onclick={analyze_matching_loop_with_endnode}>{"Analyze matching loop with endnode being the last selected node"}</button>
+        </div>
     </>
     }
 }

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

@@ -312,12 +312,12 @@ fn selected_nodes_info(
                 <ul>
                     <li><h4>{"Instantiation number: "}</h4><p>{format!("{}", selected_inst.inst_idx)}</p></li>
                     <li><h4>{"Cost: "}</h4><p>{"Calculated "}{selected_inst.cost}{z3_gen}</p></li>
-                    <li><h4>{"Instantiated formula: "}</h4><p>{&selected_inst.formula}</p></li>
+                    <li><h4>{"Instantiated formula: "}</h4><p style="overflow: auto;">{&selected_inst.formula}</p></li>
                     <li>{get_ul("Blamed terms: ", &selected_inst.blamed_terms)}</li>
                     <li>{get_ul("Bound terms: ", &selected_inst.bound_terms)}</li>
                     <li>{get_ul("Yield terms: ", &selected_inst.yields_terms)}</li>
                     <li>{get_ul("Equality explanations: ", &selected_inst.equality_expls)}</li>
-                    <li><h4>{"Resulting term: "}</h4><p>{if let Some(ref val) = selected_inst.resulting_term {val.to_string()} else { String::new() }}</p></li>
+                    <li><h4>{"Resulting term: "}</h4><p style="overflow: auto;">{if let Some(ref val) = selected_inst.resulting_term {val.to_string()} else { String::new() }}</p></li>
                 </ul>
             </details>
         }})
@@ -353,12 +353,12 @@ fn selected_edges_info(
                 {match selected_edge.edge_data {
                     BlameKind::Term { .. } => html! {
                         <div>
-                        <h4>{"Blame term: "}</h4><p>{selected_edge.blame_term.clone()}</p>
+                        <h4>{"Blame term: "}</h4><p style="overflow: auto;">{selected_edge.blame_term.clone()}</p>
                         </div>
                     },
                     BlameKind::Equality { .. } => html! {
                         <div>
-                        <h4>{"Equality: "}</h4><p>{selected_edge.blame_term.clone()}</p>
+                        <h4>{"Equality: "}</h4><p style="overflow: auto;">{selected_edge.blame_term.clone()}</p>
                         </div>
                     },
                     _ => html! {}

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

@@ -531,6 +531,22 @@ impl InstGraph {
         nr_matching_loop_end_nodes
     }
 
+    pub fn analyze_matching_loop_with_endnode(&mut self, endnode: NodeIndex, p: &mut Z3Parser) -> Graph<String, InstOrEquality> {
+        if let Some(idx) = self.matching_loop_end_nodes.iter().position(|&nx| {
+            if let Some(node) = self.matching_loop_subgraph.node_weight(nx) {
+                endnode == node.orig_graph_idx
+            } else {
+                false
+            }
+        }) {
+            log!(format!("Analyzing matching loop with endnode {}", endnode.index()));
+            self.show_nth_matching_loop(idx, p)
+        } else {
+            log!(format!("Not analyzing matching loop with endnode {}", endnode.index()));
+            Graph::new()
+        }
+    }
+
     pub fn show_nth_matching_loop(&mut self, n: usize, p: &mut Z3Parser) -> Graph<String, InstOrEquality> {
         self.reset_visibility_to(false);
         // relies on the fact that we have previously sorted self.matching_loop_end_nodes by max_depth in descending order in