Increase timeout for ML search and add subgraph ML filter opt

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

@@ -6,4 +6,4 @@ mod signature;
 pub use node::*;
 pub use signature::*;
 
-pub const MIN_MATCHING_LOOP_LENGTH: usize = 3;
+pub const MIN_MATCHING_LOOP_LENGTH: u32 = 6;

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

@@ -4,7 +4,7 @@ use crate::{
     analysis::{
         analysis::MlEndNodes, raw::NodeKind, visible::VisibleEdge, InstGraph, RawNodeIndex,
     },
-    items::{InstIdx, TermIdx, TimeRange},
+    items::{GraphIdx, InstIdx, TermIdx, TimeRange},
     Z3Parser,
 };
 
@@ -56,23 +56,34 @@ impl InstGraph {
     }
 
     fn has_n_overlapping_stacks(
+        &self,
         parser: &Z3Parser,
         i: impl Iterator<Item = InstIdx>,
-        n: usize,
+        n: u32,
     ) -> bool {
-        let mut frames: Vec<_> = i.map(|inst| parser[parser[inst].frame].active).collect();
+        let mut frames: Vec<_> = i
+            .map(|inst| {
+                (
+                    self.raw[inst].subgraph.map(|s| s.0),
+                    parser[parser[inst].frame].active,
+                )
+            })
+            .collect();
         frames.sort_unstable();
-        let mut frame_stack = Vec::<TimeRange>::new();
-        for frame in frames {
+        let mut frame_stack = Vec::<(GraphIdx, TimeRange)>::new();
+        for (subgraph, frame) in frames {
+            let Some(subgraph) = subgraph else {
+                continue;
+            };
             while let Some(last) = frame_stack.last() {
-                if last.sorted_overlap(&frame) {
+                if subgraph == last.0 && last.1.sorted_overlap(&frame) {
                     break;
                 } else {
                     frame_stack.pop();
                 }
             }
-            frame_stack.push(frame);
-            if frame_stack.len() >= n {
+            frame_stack.push((subgraph, frame));
+            if frame_stack.len() >= n as usize {
                 return true;
             }
         }
@@ -88,7 +99,7 @@ impl InstGraph {
         let mut signatures: Vec<_> = signatures
             .into_iter()
             .filter_map(|(sig, insts)| {
-                Self::has_n_overlapping_stacks(
+                self.has_n_overlapping_stacks(
                     parser,
                     insts.iter().copied(),
                     MIN_MATCHING_LOOP_LENGTH,
@@ -109,13 +120,15 @@ impl InstGraph {
                 .set_visibility_many(false, insts.iter().copied().map(to_raw));
             let mut single_quant_subgraph = self.to_visible_opt();
 
-            let (leaves, nodes) =
-                single_quant_subgraph.collect_nodes_in_long_paths(MIN_MATCHING_LOOP_LENGTH);
+            let max_depths =
+                single_quant_subgraph.compute_longest_distances_from_roots(self, parser);
+            let (leaves, nodes) = single_quant_subgraph
+                .collect_nodes_in_long_paths(&max_depths, MIN_MATCHING_LOOP_LENGTH);
             let mut leaves: Vec<_> = leaves.collect();
             if leaves.is_empty() {
                 continue;
             }
-            leaves.sort_unstable_by_key(|(len, idx)| (usize::MAX - *len, *idx));
+            leaves.sort_unstable_by_key(|(len, idx)| (u32::MAX - *len, *idx));
             long_path_leaves.push((sig, leaves));
             long_path_nodes.extend(nodes);
         }

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

@@ -21,7 +21,7 @@ use self::{
 
 use super::{raw::Node, InstGraph, RawNodeIndex};
 
-pub type MlEndNodes = Vec<(MlSignature, Vec<(usize, RawNodeIndex)>)>;
+pub type MlEndNodes = Vec<(MlSignature, Vec<(u32, RawNodeIndex)>)>;
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Default)]

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

@@ -10,7 +10,7 @@ use petgraph::{
 use crate::{
     graph_idx,
     items::{ENodeIdx, EqGivenIdx},
-    NonMaxU32,
+    NonMaxU32, TiVec, Z3Parser,
 };
 
 use super::{
@@ -58,7 +58,6 @@ impl InstGraph {
                 idx,
                 hidden_parents: hidden_parents as u32,
                 hidden_children: hidden_children as u32,
-                max_depth: 0,
             };
             graph.add_node(v_node);
         }
@@ -109,7 +108,6 @@ impl InstGraph {
                     idx,
                     hidden_parents: hidden_parents as u32,
                     hidden_children: hidden_children as u32,
-                    max_depth: 0,
                 }
             })
         };
@@ -172,7 +170,6 @@ impl InstGraph {
                     .iter()
                     .filter(|&n| self.raw[*n].hidden())
                     .count() as u32,
-                max_depth: 0,
             };
             node_index_map[i] = graph.add_node(nw);
         }
@@ -369,22 +366,22 @@ impl VisibleInstGraph {
     /// Collect all nodes that are part of a path of at least `min_length`
     /// nodes. Additionally, returns a list of all of the leaves of these long
     /// paths along with their max depth.
-    pub(crate) fn collect_nodes_in_long_paths(
-        &mut self,
-        min_length: usize,
+    pub(crate) fn collect_nodes_in_long_paths<'a>(
+        &'a mut self,
+        max_depths: &'a TiVec<VisibleNodeIndex, u32>,
+        min_length: u32,
     ) -> (
-        impl Iterator<Item = (usize, RawNodeIndex)> + '_,
-        impl Iterator<Item = RawNodeIndex> + '_,
+        impl Iterator<Item = (u32, RawNodeIndex)> + 'a,
+        impl Iterator<Item = RawNodeIndex> + 'a,
     ) {
         // traverse this subtree in topological order to compute longest distances from root nodes
-        Self::compute_longest_distances_from_roots(self);
         let long_path_leaves: Vec<_> = self
             .graph
             .node_indices()
             // only want to keep end nodes of longest paths, i.e., nodes without any children
             .filter(|nx| self.graph.neighbors(*nx).next().is_none())
             // only want to show matching loops of length at least 3, hence only keep nodes with depth at least 2
-            .filter(|nx| self.graph[*nx].max_depth >= min_length - 1)
+            .filter(|nx| max_depths[VisibleNodeIndex(*nx)] >= min_length - 1)
             .collect();
         // Walk backwards from leaves to collect all nodes
         let rev_graph = Reversed(&self.graph);
@@ -393,18 +390,45 @@ impl VisibleInstGraph {
 
         let long_path_leaves = long_path_leaves
             .into_iter()
-            .map(|nx| (self.graph[nx].max_depth, self.graph[nx].idx));
+            .map(|nx| (max_depths[VisibleNodeIndex(nx)], self.graph[nx].idx));
         let long_path_nodes = dfs.iter(rev_graph).map(|nx| self.graph[nx].idx);
         (long_path_leaves, long_path_nodes)
     }
 
-    pub fn compute_longest_distances_from_roots(&mut self) {
+    pub fn compute_longest_distances_from_roots(
+        &self,
+        graph: &InstGraph,
+        parser: &Z3Parser,
+    ) -> TiVec<VisibleNodeIndex, u32> {
+        let mut ast_sizes: TiVec<VisibleNodeIndex, u32> =
+            self.graph.node_indices().map(|_| u32::MAX).collect();
+        let mut max_depths: TiVec<VisibleNodeIndex, u32> =
+            self.graph.node_indices().map(|_| 0).collect();
         let mut topo = Topo::new(&self.graph);
         while let Some(nx) = topo.next(&self.graph) {
+            let ast_size = graph.raw[self.graph[nx].idx]
+                .kind()
+                .inst()
+                .map(|inst| {
+                    let bound_terms = parser[parser[inst].match_]
+                        .kind
+                        .bound_terms(|e| parser[e].owner, |t| t);
+                    bound_terms
+                        .iter()
+                        .map(|&tidx| parser.ast_size(tidx).unwrap())
+                        .sum()
+                })
+                .unwrap_or_default();
+            ast_sizes[VisibleNodeIndex(nx)] = ast_size;
+
             let parents = self.graph.neighbors_directed(nx, Incoming);
-            let max_parent_depth = parents.map(|nx| self.graph[nx].max_depth + 1).max();
-            self.graph[nx].max_depth = max_parent_depth.unwrap_or_default();
+            let max_parent_depth = parents
+                .map(VisibleNodeIndex)
+                .filter_map(|nx| (ast_size >= ast_sizes[nx]).then_some(max_depths[nx] + 1))
+                .max();
+            max_depths[VisibleNodeIndex(nx)] = max_parent_depth.unwrap_or_default();
         }
+        max_depths
     }
 }
 
@@ -436,7 +460,6 @@ pub struct VisibleNode {
     pub idx: RawNodeIndex,
     pub hidden_parents: u32,
     pub hidden_children: u32,
-    pub max_depth: usize,
 }
 
 #[derive(Clone, PartialEq, Eq, Hash)]

smt-log-parser/tests/parse_logs.rs

@@ -93,21 +93,33 @@ fn parse_all_logs() {
                 mem_limit / mb,
             );
             ALLOCATOR.set_limit(mem_limit as usize).unwrap();
+
+            let now = Instant::now();
             let mut inst_graph = InstGraph::new(&parser).unwrap();
+            assert!(
+                now.elapsed() < timeout,
+                "Constructing inst graph took longer than timeout"
+            );
+
             inst_graph.search_matching_loops(&mut parser);
             let elapsed = now.elapsed();
+
             max_analysis_ovhd = f64::max(
                 max_analysis_ovhd,
                 (ALLOCATOR.allocated() as u64 - middle_alloc) as f64 / parse_bytes as f64,
             );
             println!(
-                "Finished analysis in {elapsed:?} ({} kB/ms). {} nodes. Memory use {} MB / {} MB:",
+                "Finished analysis in {elapsed:?} ({} kB/ms). {} nodes, {} mls. Memory use {} MB / {} MB:",
                 parse_bytes_kb / elapsed.as_millis() as u64,
                 inst_graph.raw.graph.node_count(),
+                inst_graph.analysis.matching_loop_end_nodes.as_ref().map(|ml| ml.len()).unwrap_or_default(),
                 ALLOCATOR.allocated() / mb as usize,
                 ALLOCATOR.limit() / mb as usize,
             );
-            assert!(elapsed < timeout, "Analysis took longer than timeout");
+            assert!(
+                elapsed < 10 * timeout,
+                "ML search took longer than 10*timeout"
+            );
             inst_graph.mem_dbg(DbgFlags::default()).ok();
             println!();
             println!("===");