added subcommand to track statistics of a z3 log file

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

@@ -141,7 +141,15 @@ impl Filter {
                 let nodes_of_nth_matching_loop = graph
                     .raw
                     .node_indices()
-                    .filter(|nx| graph.raw[*nx].part_of_ml.contains(&n))
+                    .flat_map(|nx| {
+                        let node = &graph.raw[nx];
+                        match *node.kind() {
+                            NodeKind::Instantiation(iidx) => {
+                                node.part_of_ml.contains(&n).then_some(iidx)
+                            }
+                            _ => None,
+                        }
+                    })
                     .collect::<fxhash::FxHashSet<_>>();
                 let relevant_non_qi_nodes: Vec<_> = Dfs::new(&*graph.raw.graph, nth_ml_endnode.0)
                     .iter(graph.raw.rev())

axiom-profiler-GUI/src/utils/lookup.rs

@@ -76,7 +76,7 @@ pub type StringLookupZ3 = StringLookup<FxHashMap<Kind, Entry>>;
 impl StringLookupZ3 {
     pub fn init(parser: &Z3Parser) -> Self {
         let mut lookup = Self::new();
-        for (idx, instantiation) in parser.instantiations() {
+        for (idx, instantiation) in parser.instantiations().iter_enumerated() {
             let match_ = &parser[instantiation.match_];
             if let Some(quant) = match_.kind.quant_idx() {
                 let name = match &parser[quant].kind {

smt-log-parser/src/analysis/dependencies.rs

@@ -0,0 +1,103 @@
+use std::{cmp::Ordering, ops::Deref};
+
+use fxhash::FxHashSet;
+
+use crate::{items::QuantIdx, FxHashMap, TiVec, Z3Parser};
+
+use super::InstGraph;
+
+#[derive(Clone)]
+pub struct QuantifierAnalysis(TiVec<QuantIdx, QuantifierInfo>);
+
+#[derive(Default, Clone)]
+pub struct QuantifierInfo {
+    /// How much total cost did this quantifier accrue from individual
+    /// instantiations.
+    pub costs: f64,
+    /// How many times does an instantiation of this quantifier depend on an
+    /// instantiation of the other quantifier.
+    pub direct_deps: FxHashMap<QuantIdx, u32>,
+}
+
+type TransQuantAnalaysis = TiVec<QuantIdx, FxHashSet<QuantIdx>>;
+
+impl Deref for QuantifierAnalysis {
+    type Target = TiVec<QuantIdx, QuantifierInfo>;
+    fn deref(&self) -> &Self::Target {
+        &self.0
+    }
+}
+
+impl QuantifierAnalysis {
+    /// Calculate the analysis. Make sure that you have run
+    /// `initialise_inst_succs_and_preds` on the `inst_graph`!
+    pub fn new(parser: &Z3Parser, inst_graph: &InstGraph) -> Self {
+        let mut self_ = Self(
+            parser
+                .quantifiers
+                .iter()
+                .map(|_| QuantifierInfo::default())
+                .collect(),
+        );
+        for (iidx, inst) in parser.insts.insts.iter_enumerated() {
+            let match_ = &parser.insts[inst.match_];
+            let Some(qidx) = match_.kind.quant_idx() else {
+                continue;
+            };
+            let qinfo = &mut self_.0[qidx];
+            let ginst = &inst_graph.raw[iidx];
+            qinfo.costs += ginst.cost;
+            for &parent_iidx in &ginst.inst_parents.nodes {
+                let parent_inst = &parser.insts[parent_iidx];
+                let parent_match_ = &parser.insts[parent_inst.match_];
+                let Some(parent_qidx) = parent_match_.kind.quant_idx() else {
+                    continue;
+                };
+                *qinfo.direct_deps.entry(parent_qidx).or_default() += 1;
+            }
+        }
+        self_
+    }
+
+    pub fn total_costs(&self) -> f64 {
+        self.iter().map(|info| info.costs).sum()
+    }
+
+    pub fn calculate_transitive(&self, mut steps: Option<u32>) -> TransQuantAnalaysis {
+        let mut initial = self
+            .iter()
+            .map(|info| info.direct_deps.keys().copied().collect())
+            .collect();
+        while !steps.is_some_and(|steps| steps == 0) {
+            if !self.calculate_transitive_one(&mut initial) {
+                break;
+            }
+            if let Some(steps) = &mut steps {
+                *steps -= 1;
+            }
+        }
+        initial
+    }
+    fn calculate_transitive_one(&self, analysis: &mut TransQuantAnalaysis) -> bool {
+        let mut changed = false;
+        for (idx, info) in self.iter_enumerated() {
+            for &ddep in info.direct_deps.keys() {
+                let (curr, ddep) = match idx.cmp(&ddep) {
+                    Ordering::Less => {
+                        let (left, right) = analysis.split_at_mut(ddep);
+                        (&mut left[idx], right.first().unwrap())
+                    }
+                    Ordering::Greater => {
+                        let (left, right) = analysis.split_at_mut(idx);
+                        (right.first_mut().unwrap(), &left[ddep])
+                    }
+                    Ordering::Equal => continue,
+                };
+                let old_len = curr.len();
+                curr.extend(ddep);
+                changed |= old_len != curr.len();
+            }
+        }
+        changed
+    }
+}

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

@@ -1,5 +1,3 @@
-use std::collections::HashSet;
-
 use petgraph::Direction;
 
 use crate::{
@@ -37,9 +35,7 @@ impl<C: NextInstsInitialiser<FORWARD>, const FORWARD: bool> Initialiser<FORWARD,
         }
     }
     fn base(&mut self, _node: &Node, _parser: &Z3Parser) -> Self::Value {
-        NextInsts {
-            nodes: HashSet::default(),
-        }
+        NextInsts::default()
     }
     fn assign(&mut self, node: &mut Node, value: Self::Value) {
         if FORWARD {
@@ -68,54 +64,30 @@ impl<C: NextInstsInitialiser<FORWARD>, const FORWARD: bool> TransferInitialiser<
     }
     fn add(&mut self, node: &mut Node, value: Self::Value) {
         if FORWARD {
-            node.inst_parents = NextInsts {
-                nodes: node
-                    .inst_parents
-                    .nodes
-                    .iter()
-                    .cloned()
-                    .chain(value.nodes.iter().cloned())
-                    .collect(),
-            };
+            node.inst_parents.nodes.extend(value.nodes);
         } else {
-            node.inst_children = NextInsts {
-                nodes: node
-                    .inst_children
-                    .nodes
-                    .iter()
-                    .cloned()
-                    .chain(value.nodes.iter().cloned())
-                    .collect(),
-            };
+            node.inst_children.nodes.extend(value.nodes);
         }
     }
 }
 
 pub struct DefaultNextInsts<const FORWARD: bool>;
 impl<const FORWARD: bool> NextInstsInitialiser<FORWARD> for DefaultNextInsts<FORWARD> {
     fn base(&mut self, _node: &Node, _parser: &Z3Parser) -> NextInsts {
-        NextInsts {
-            nodes: HashSet::default(),
-        }
-    }
-    type Observed = NextInsts;
-    fn observe(&mut self, node: &Node, _parser: &Z3Parser) -> Self::Observed {
-        if FORWARD {
-            node.inst_parents.clone()
-        } else {
-            node.inst_children.clone()
-        }
+        NextInsts::default()
     }
+    type Observed = ();
+    fn observe(&mut self, _node: &Node, _parser: &Z3Parser) -> Self::Observed {}
     fn transfer(
         &mut self,
         node: &Node,
-        from_idx: RawNodeIndex,
+        _from_idx: RawNodeIndex,
         _idx: usize,
         _incoming: &[Self::Observed],
     ) -> NextInsts {
-        let value = match node.kind() {
-            NodeKind::Instantiation(_) => NextInsts {
-                nodes: std::iter::once(from_idx).collect(),
+        match *node.kind() {
+            NodeKind::Instantiation(iidx) => NextInsts {
+                nodes: std::iter::once(iidx).collect(),
             },
             _ => {
                 if FORWARD {
@@ -124,7 +96,6 @@ impl<const FORWARD: bool> NextInstsInitialiser<FORWARD> for DefaultNextInsts<FOR
                     node.inst_children.clone()
                 }
             }
-        };
-        value
+        }
     }
 }

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

@@ -313,7 +313,7 @@ pub struct Depth {
 #[derive(Debug, Clone, Default)]
 pub struct NextInsts {
     /// What are the immediate next instantiation nodes
-    pub nodes: FxHashSet<RawNodeIndex>,
+    pub nodes: FxHashSet<InstIdx>,
 }
 
 impl Node {
@@ -325,12 +325,8 @@ impl Node {
             bwd_depth: Depth::default(),
             subgraph: None,
             kind,
-            inst_parents: NextInsts {
-                nodes: FxHashSet::default(),
-            },
-            inst_children: NextInsts {
-                nodes: FxHashSet::default(),
-            },
+            inst_parents: NextInsts::default(),
+            inst_children: NextInsts::default(),
             part_of_ml: FxHashSet::default(),
         }
     }

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

@@ -15,7 +15,7 @@ use crate::{
 
 use super::{
     analysis::matching_loop::MIN_MATCHING_LOOP_LENGTH,
-    raw::{EdgeKind, Node, NodeKind},
+    raw::{EdgeKind, IndexesInstGraph, Node, NodeKind},
     InstGraph, RawEdgeIndex, RawNodeIndex,
 };
 
@@ -126,7 +126,8 @@ impl InstGraph {
         for (i, node) in self.raw.graph.node_weights().enumerate() {
             let from = node_index_map[i];
             if from != NodeIndex::end() {
-                for next_inst in node.inst_children.nodes.clone() {
+                for &next_inst in &node.inst_children.nodes {
+                    let next_inst = next_inst.index(&self.raw);
                     let to = node_index_map[next_inst.0.index()];
                     if to != NodeIndex::end() {
                         graph.add_edge(

smt-log-parser/src/analysis/misc.rs

@@ -0,0 +1,68 @@
+use crate::{items::QuantIdx, TiVec, Z3Parser};
+
+pub struct LogInfo {
+    pub match_: MatchesInfo,
+    pub inst: InstsInfo,
+    pub quants: QuantsInfo,
+}
+
+#[derive(Default)]
+/// Counts of different match-line kinds. Essentially how many instantiations
+/// were from each of the different categories.
+pub struct MatchesInfo {
+    pub mbqi: u64,
+    pub theory_solving: u64,
+    pub axioms: u64,
+    pub quantifiers: u64,
+}
+
+#[derive(Default)]
+/// Counts of different instantiation stats.
+pub struct InstsInfo {
+    pub enodes: u64,
+    pub geqs: u64,
+    pub treqs: u64,
+    pub insts: u64,
+}
+
+impl InstsInfo {
+    pub fn total(&self) -> u64 {
+        self.enodes + self.geqs + self.treqs + self.insts
+    }
+}
+
+/// How many times each quantifier was instantiated
+pub struct QuantsInfo(pub TiVec<QuantIdx, u64>);
+
+impl LogInfo {
+    pub fn new(parser: &Z3Parser) -> Self {
+        let mut quants = QuantsInfo(parser.quantifiers.iter().map(|_| 0).collect());
+        let mut match_ = MatchesInfo::default();
+        for inst in parser.instantiations().iter() {
+            let match_i = &parser[inst.match_];
+            if let Some(qidx) = match_i.kind.quant_idx() {
+                quants.0[qidx] += 1;
+            }
+            use crate::items::MatchKind::*;
+            match &match_i.kind {
+                MBQI { .. } => match_.mbqi += 1,
+                TheorySolving { .. } => match_.theory_solving += 1,
+                Axiom { .. } => match_.axioms += 1,
+                Quantifier { .. } => match_.quantifiers += 1,
+            }
+        }
+
+        let inst = InstsInfo {
+            insts: parser.insts.insts.len() as u64,
+            enodes: parser.egraph.enodes.len() as u64,
+            geqs: parser.egraph.equalities.given.len() as u64,
+            treqs: parser.egraph.equalities.transitive.len() as u64,
+        };
+
+        Self {
+            match_,
+            inst,
+            quants,
+        }
+    }
+}

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

@@ -1,3 +1,7 @@
+mod dependencies;
 mod graph;
+mod misc;
 
+pub use dependencies::*;
 pub use graph::*;
+pub use misc::*;

smt-log-parser/src/cmd/args.rs

@@ -16,13 +16,22 @@ pub enum Commands {
         logfile: std::path::PathBuf,
 
         /// Depth of dependencies to lookup
-        #[arg(short, long, default_value_t = 1)]
-        depth: u32,
+        #[arg(short, long, default_value = "0")]
+        depth: Option<u32>,
 
         /// Whether to pretty print the output results
         #[arg(short, long, default_value_t = false)]
         pretty_print: bool,
     },
+    #[cfg(feature = "analysis")]
+    /// Print out statistics for the SMT solver
+    Stats {
+        /// The path to the smt log file
+        logfile: std::path::PathBuf,
+        /// how many of the most instantiated axioms to print
+        #[arg(short)]
+        k: Option<usize>,
+    },
     /// Tests the parser and analysis, printing out timing information
     Test {
         /// The paths to the smt log files