Improve performance of analyses which skip disabled nodes

axiom-profiler-GUI/src/screen/file/summary.rs

@@ -68,6 +68,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
             <Metrics ..inner.clone() />
             <MostQuants ..inner.clone() />
             <CostQuants ..inner.clone() />
+            <MultQuants ..inner.clone() />
         </DetailContainer><DetailContainer>
             <CostLemmas ..inner.clone() />
             <CostCdcl ..inner />
@@ -158,15 +159,23 @@ pub fn MostQuants(props: &SummaryPropsInner) -> Html {
 #[function_component]
 pub fn CostQuants(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {
+        let log_info = &props.parser.summary.log_info;
         let parser = props.parser.parser.borrow();
         let analysis = analysis.borrow();
         let colours = &props.parser.colour_map;
 
-        let costs = analysis.quants.quants_costs().map(|(q, c)| (q, F64Ord(c)));
+        let costs = analysis.quants.quants_costs().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, F64Ord(0.0))
+            } else {
+                (q, F64Ord(c / qis as f64))
+            }
+        });
         let costs = quants_ordered::<_, true>(&parser, colours, costs);
         let costs = costs.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
         let costs = costs.map(|(q, hue, c)| {
-            let left = format_to_html(c.0 as u64);
+            let left = html!{{ format!("{:.1}", c.0) }};
             let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
             (left, right)
         }).collect::<Vec<_>>();
@@ -176,6 +185,35 @@ pub fn CostQuants(props: &SummaryPropsInner) -> Html {
     }).unwrap_or_default()
 }
 
+#[function_component]
+pub fn MultQuants(props: &SummaryPropsInner) -> Html {
+    props.analysis.as_ref().map(|analysis| {
+        let log_info = &props.parser.summary.log_info;
+        let parser = props.parser.parser.borrow();
+        let analysis = analysis.borrow();
+        let colours = &props.parser.colour_map;
+
+        let mults = analysis.quants.quants_children().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, F64Ord(0.0))
+            } else {
+                (q, F64Ord(c / qis as f64))
+            }
+        });
+        let mults = quants_ordered::<_, true>(&parser, colours, mults);
+        let mults = mults.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
+        let mults = mults.map(|(q, hue, c)| {
+            let left = html!{{ format!("{:.1}", c.0) }};
+            let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+            (left, right)
+        }).collect::<Vec<_>>();
+        html! {<Detail title="Multiplicative quantifiers" hover="The quantifiers which the highest multiplicative factor, i.e. those that on average directly cause N other instantiations.">
+            <TreeList elements={mults} />
+        </Detail>}
+    }).unwrap_or_default()
+}
+
 #[function_component]
 pub fn CostLemmas(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {

axiom-profiler-GUI/src/screen/inst_graph/filter/add_filter.rs

@@ -116,7 +116,7 @@ impl AddFilter<'_> {
             mk_filter(
                 &nodes,
                 |&(n, _, _)| {
-                    raw.neighbors_directed(n, Direction::Outgoing)
+                    raw.neighbors_directed(n, Direction::Outgoing, &self.graph.analysis.reach)
                         .count_hidden()
                         > 0
                 },
@@ -125,7 +125,7 @@ impl AddFilter<'_> {
             mk_filter(
                 &nodes,
                 |&(n, _, _)| {
-                    raw.neighbors_directed(n, Direction::Incoming)
+                    raw.neighbors_directed(n, Direction::Incoming, &self.graph.analysis.reach)
                         .count_hidden()
                         > 0
                 },

axiom-profiler-GUI/src/screen/inst_graph/filter/apply.rs

@@ -51,7 +51,10 @@ impl Filter {
             }
             MaxBranching(n) => graph.keep_first_n_children(n),
             ShowNeighbours(nidx, direction) => {
-                let nodes: Vec<_> = graph.raw.neighbors_directed(nidx, direction).collect();
+                let nodes: Vec<_> = graph
+                    .raw
+                    .neighbors_directed(nidx, direction, &graph.analysis.reach)
+                    .collect();
                 let modified = graph.raw.set_visibility_many(false, nodes.iter().copied());
                 select = Some(nodes);
                 modified

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

@@ -17,6 +17,9 @@ pub struct QuantPatInfo {
     /// How much total cost did this quantifier + pattern accrue from individual
     /// instantiations.
     pub costs: f64,
+    /// How many other instantiations of other quantifiers is this quantifier
+    /// _directly_ responsible for.
+    pub children: f64,
     /// How many times does an instantiation of this quantifier depend on an
     /// instantiation of the other quantifier.
     pub direct_deps: Vec<DirectDep>,
@@ -49,6 +52,16 @@ impl QuantifierAnalysis {
             let ginst = &inst_graph.raw[data.iidx];
             qinfo.costs += ginst.cost;
 
+            for &child in ginst.children.insts.iter() {
+                let cq = parser.get_inst(child).match_.kind.quant_idx();
+                if cq.is_some_and(|q| q == qpat.quant) {
+                    // Skip self references.
+                    continue;
+                }
+                let parents = inst_graph.raw[child].parents.insts.len() as f64;
+                qinfo.children += 1.0 / parents;
+            }
+
             let pat = parser.get_pattern(qpat);
             let subpats = pat.map(|p| parser[p].child_ids.len()).unwrap_or_default();
             for (i, blame) in data.match_.pattern_matches().enumerate() {
@@ -97,6 +110,13 @@ impl QuantifierAnalysis {
             .map(|(quant, data)| (quant, data.iter_enumerated().map(|(_, d)| d.costs).sum()))
     }
 
+    pub fn quants_children(&self) -> impl Iterator<Item = (QuantIdx, f64)> + '_ {
+        self.0
+             .0
+            .iter_enumerated()
+            .map(|(quant, data)| (quant, data.iter_enumerated().map(|(_, d)| d.children).sum()))
+    }
+
     pub fn calculate_transitive(&self, mut steps: Option<u32>) -> TransQuantAnalaysis {
         let mut initial: TiVec<QuantIdx, _> =
             (0..self.0 .0.len()).map(|_| FxHashSet::default()).collect();

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

@@ -14,20 +14,22 @@ use mem_dbg::{MemDbg, MemSize};
 
 use matching_loop::MlData;
 
-use crate::{F64Ord, Result, Z3Parser};
+use crate::{F64Ord, Result, TiVec, Z3Parser};
 
 use self::{
     cost::{DefaultCost, ProofCost},
     depth::DefaultDepth,
     next_nodes::NextInstsInit,
     proof::ProofInitialiser,
+    reconnect::{BwdReachableAnalysis, ReachNonDisabled},
 };
 
 use super::{raw::RawInstGraph, InstGraph, RawNodeIndex};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Default)]
 pub struct Analysis {
+    pub reach: TiVec<RawNodeIndex, ReachNonDisabled>,
     // Highest to lowest
     pub cost: OrderingAnalysis,
     // Most to least
@@ -89,6 +91,7 @@ impl Analysis {
         // Alloc `fwd_depth_min` vector
         let fwd_depth_min = cost.duplicate()?;
         Ok(Self {
+            reach: Default::default(),
             cost,
             children,
             fwd_depth_min,
@@ -107,6 +110,9 @@ impl InstGraph {
     }
 
     pub fn initialise_default(&mut self, parser: &Z3Parser) {
+        let mut reach = BwdReachableAnalysis::<ReachNonDisabled>::default();
+        self.analysis.reach = self.topo_analysis(&mut reach);
+
         self.initialise_transfer(DefaultCost, parser);
         self.initialise_transfer(ProofCost, parser);
         self.initialise_collect(DefaultDepth::<true>, parser);

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

@@ -1,5 +1,8 @@
 use std::collections::hash_map::Entry;
 
+#[cfg(feature = "mem_dbg")]
+use mem_dbg::{MemDbg, MemSize};
+
 use fxhash::FxHashSet;
 
 use crate::{
@@ -9,10 +12,52 @@ use crate::{
 
 use super::run::TopoAnalysis;
 
-pub struct BwdReachableVisAnalysis;
+pub trait ReachKind: Copy + core::fmt::Debug + From<bool> + Into<bool> {
+    fn current(node: &Node) -> Self;
+    fn value(self) -> bool {
+        self.into()
+    }
+}
+
+macro_rules! reach_kind {
+    ($name:ident($node:ident => $e:expr)) => {
+        #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+        #[cfg_attr(feature = "mem_dbg", copy_type)]
+        #[derive(Debug, Clone, Copy)]
+        pub struct $name(bool);
+        impl ReachKind for $name {
+            fn current($node: &Node) -> Self {
+                Self($e)
+            }
+        }
+        impl From<bool> for $name {
+            fn from(b: bool) -> Self {
+                Self(b)
+            }
+        }
+        impl From<$name> for bool {
+            fn from(b: $name) -> bool {
+                b.0
+            }
+        }
+    };
+}
+
+reach_kind!(ReachVisible(node => node.visible()));
+reach_kind!(ReachNonDisabled(node => !node.disabled()));
 
-impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
-    type Value = bool;
+/// If `VIS` is true, then it checks if a visible node is reachable from this
+/// one, otherwise it checks if any non-disabled node is reachable.
+#[derive(Clone, Copy)]
+pub struct BwdReachableAnalysis<Kind: ReachKind>(core::marker::PhantomData<Kind>);
+impl<Kind: ReachKind> Default for BwdReachableAnalysis<Kind> {
+    fn default() -> Self {
+        Self(Default::default())
+    }
+}
+
+impl<Kind: ReachKind> TopoAnalysis<false, false> for BwdReachableAnalysis<Kind> {
+    type Value = Kind;
 
     fn collect<'a, 'n, T: Iterator<Item = (RawNodeIndex, &'n Self::Value)>>(
         &mut self,
@@ -24,11 +69,9 @@ impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
     where
         Self::Value: 'n,
     {
-        if node.visible() {
-            true
-        } else {
-            from_all().any(|(_, &b)| b)
-        }
+        let curr = Kind::current(node).value();
+        let reach = curr || from_all().any(|(_, &b)| b.value());
+        reach.into()
     }
 }
 
@@ -42,7 +85,7 @@ impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
 ///
 /// The `to` is implicit in the index which we used to reach the
 /// `TopoAnalysis::Value`.
-pub struct ReconnectAnalysis(pub TiVec<RawNodeIndex, bool>);
+pub struct ReconnectAnalysis(pub TiVec<RawNodeIndex, ReachVisible>);
 
 #[derive(Debug, Default)]
 pub struct ReconnectData {
@@ -164,7 +207,7 @@ impl TopoAnalysis<true, false> for ReconnectAnalysis {
         Self::Value: 'n,
     {
         let mut data = Self::Value::default();
-        if !self.0[cidx] {
+        if !self.0[cidx].value() {
             return data;
         }
 

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

@@ -10,6 +10,8 @@ use crate::{
     TiVec, Z3Parser,
 };
 
+use super::reconnect::ReachNonDisabled;
+
 // FIXME: `ID` makes the implementations unique, but is not a great solution.
 /// FORWARD: Do a forward or reverse topological walk?
 pub trait Initialiser<const FORWARD: bool, const ID: u8> {
@@ -75,9 +77,10 @@ impl RawInstGraph {
         &self,
         curr: RawNodeIndex,
         dir: Direction,
+        reach: &TiVec<RawNodeIndex, ReachNonDisabled>,
     ) -> impl Iterator<Item = RawNodeIndex> + '_ {
         if SKIP_DISABLED {
-            either::Either::Left(self.neighbors_directed(curr, dir))
+            either::Either::Left(self.neighbors_directed(curr, dir, reach))
         } else {
             either::Either::Right(self.graph.neighbors_directed(curr.0, dir).map(RawNodeIndex))
         }
@@ -119,7 +122,7 @@ impl InstGraph {
                 } else {
                     let from_all = || {
                         self.raw
-                            .neighbors_directed_::<SKIP_DISABLED>(curr, dir)
+                            .neighbors_directed_::<SKIP_DISABLED>(curr, dir, &self.analysis.reach)
                             .map(|i| {
                                 let data = &data[i];
                                 // Safety: The data is initialised as the graph is a DAG
@@ -175,7 +178,11 @@ impl InstGraph {
             let for_each = |idx: RawNodeIndex| {
                 let from_all = || {
                     self.raw
-                        .neighbors_directed_::<SKIP_DISABLED>(idx, I::direction())
+                        .neighbors_directed_::<SKIP_DISABLED>(
+                            idx,
+                            I::direction(),
+                            &self.analysis.reach,
+                        )
                         .map(|i| &self.raw[i])
                 };
                 let value = initialiser.collect(&self.raw.graph[idx.0], from_all);
@@ -209,11 +216,14 @@ impl InstGraph {
             let for_each = |idx: RawNodeIndex| {
                 let incoming: Vec<_> = self
                     .raw
-                    .neighbors_directed(idx, I::direction())
+                    .neighbors_directed(idx, I::direction(), &self.analysis.reach)
                     .map(|i| initialiser.observe(&self.raw[i], parser))
                     .collect();
                 let mut i = 0;
-                let mut neighbors = self.raw.neighbors_directed(idx, I::direction()).detach();
+                let mut neighbors = self
+                    .raw
+                    .neighbors_directed(idx, I::direction(), &self.analysis.reach)
+                    .detach();
                 while let Some(neighbor) = neighbors.next(&self.raw) {
                     let transfer = initialiser.transfer(&self.raw.graph[idx.0], idx, i, &incoming);
                     initialiser.add(&mut self.raw[neighbor], transfer);