Improve performance of analyses which skip disabled nodes (#96)

* Improve performance of analyses which skip disabled nodes

* Add average weighing

axiom-profiler-GUI/src/configuration/data.rs

@@ -2,7 +2,7 @@ use fxhash::FxHashMap;
 use smt_log_parser::{
     display_with::{DisplayConfiguration, SymbolReplacement},
     formatter::TermDisplayContext,
-    NonMaxU32,
+    F64Ord, NonMaxU32,
 };
 
 use crate::screen::homepage::FileInfo;
@@ -47,6 +47,7 @@ impl ConfigurationProvider {
 pub struct Configuration {
     pub display: DisplayConfiguration,
     pub term_display: TermDisplayContextFiles,
+    pub avg_weighing: F64Ord,
 }
 impl Configuration {
     pub const fn default_display() -> DisplayConfiguration {
@@ -69,6 +70,7 @@ impl Default for Configuration {
         Self {
             display: Self::default_display(),
             term_display: TermDisplayContextFiles::default(),
+            avg_weighing: F64Ord(1.0),
         }
     }
 }

axiom-profiler-GUI/src/configuration/page.rs

@@ -1,6 +1,6 @@
 use std::rc::Rc;
 
-use smt_log_parser::{display_with::SymbolReplacement, NonMaxU32};
+use smt_log_parser::{display_with::SymbolReplacement, F64Ord, NonMaxU32};
 use wasm_bindgen::JsCast;
 use yew::{
     function_component, use_context, use_effect_with_deps, Callback, Event, Html, Properties,
@@ -129,13 +129,27 @@ pub fn Flags(props: &FlagsProps) -> Html {
     );
     use_effect_with_deps(move |deps| effect(deps), deps);
 
+    let (summary_weighing, effect, deps) = flag_widget!(
+        cfg,
+        default,
+        avg_weighing,
+        "Average weighing",
+        "When sorting by average, how much weight should be given to the total count. Currently only affects quantifier sorting on the summary screen. A weight of 0% means sorting exactly by the average, while N% means that anything with < N% of the total will be heavily down-ranked.", |
+        if F64Ord(0.0) => "0%",
+        if F64Ord(1.0) => "1%",
+        if F64Ord(10.0) => "10%",
+        if F64Ord(100.0) => "100%",
+    );
+    use_effect_with_deps(move |deps| effect(deps), deps);
+
     yew::html! {
         <div class="flags-page"><div class="flags-content">
             <h1>{"Configuration flags"}</h1>
             <button onclick={reset}>{"Reset configuration"}</button>
             {debug}
             {replace_symbols}
             {ast_depth_limit}
+            {summary_weighing}
             <TermDisplayFlag cfg={cfg.clone()} file={props.file.clone()} />
         </div></div>
     }

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

@@ -52,6 +52,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
         analysis: props.analysis.clone(),
         term_display: term_display.clone(),
         config: cfg.config.display,
+        avg_weighing: cfg.config.avg_weighing.0,
     };
 
     let graph = props.analysis.clone().map(|analysis| {
@@ -68,6 +69,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 />
@@ -82,6 +84,7 @@ pub struct SummaryPropsInner {
     pub analysis: Option<RcAnalysis>,
     pub term_display: Rc<TermDisplayContext>,
     pub config: DisplayConfiguration,
+    pub avg_weighing: f64,
 }
 
 impl SummaryPropsInner {
@@ -138,13 +141,13 @@ pub fn MostQuants(props: &SummaryPropsInner) -> Html {
     let summary = &props.parser.summary;
     let colours = &props.parser.colour_map;
 
-    let quants = summary.log_info.quants_iter();
-    let quants = quants_ordered::<_, true>(&parser, colours, quants);
+    let quants = summary.log_info.quants_iter().map(|(q, c)| (q, (), c));
+    let quants = quants_ordered::<(), _, true>(&parser, colours, quants);
     let quants = quants
         .iter()
         .take(DISPLAY_TOP_N)
         .take_while(|(.., c)| *c > 0);
-    let quants = quants.map(|(q, hue, c)| {
+    let quants = quants.map(|(q, hue, (), c)| {
         let left = format_to_html(*c);
         let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
         (left, right)
@@ -158,24 +161,63 @@ 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 offset = log_info.match_.quantifiers as f64 * props.avg_weighing / 100.;
 
-        let costs = analysis.quants.quants_costs().map(|(q, c)| (q, F64Ord(c)));
-        let costs = quants_ordered::<_, true>(&parser, colours, costs);
+        let costs = analysis.quants.quants_costs().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, 0.0, F64Ord(0.0))
+            } else {
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
+            }
+        });
+        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 costs = costs.map(|(q, hue, c, _)| {
+            let left = html!{{ format!("{c:.1}") }};
             let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
             (left, right)
         }).collect::<Vec<_>>();
-        html! {<Detail title="Most expensive quantifiers" hover="The quantifiers upon which the most instantiations depend.">
+        html! {<Detail title="Average cost" hover="The quantifiers upon which the most instantiations causally depend. See average weighing flag.">
             <TreeList elements={costs} />
         </Detail>}
     }).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 offset = log_info.match_.quantifiers as f64 * props.avg_weighing / 100.;
+
+        let mults = analysis.quants.quants_children().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, 0.0, F64Ord(0.0))
+            } else {
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
+            }
+        });
+        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!("{c:.1}") }};
+            let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+            (left, right)
+        }).collect::<Vec<_>>();
+        html! {<Detail title="Average multiplicativity" hover="The quantifiers which the highest multiplicative factor, i.e. those that on average directly cause N other instantiations. See average weighing flag.">
+            <TreeList elements={mults} />
+        </Detail>}
+    }).unwrap_or_default()
+}
+
 #[function_component]
 pub fn CostLemmas(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {
@@ -213,17 +255,17 @@ fn format_to_html<F: ToFormattedString>(f: F) -> Html {
     html! {{ f.to_formatted_string(&Locale::en) }}
 }
 
-fn quants_ordered<'a, T: Ord + Copy + Debug, const REVERSE: bool>(
+fn quants_ordered<'a, D, T: Ord + Copy + Debug, const REVERSE: bool>(
     parser: &'a Z3Parser,
     colour_map: &QuantIdxToColourMap,
-    quants: impl Iterator<Item = (QuantIdx, T)>,
-) -> Vec<(Cow<'a, str>, Option<f64>, T)> {
+    quants: impl Iterator<Item = (QuantIdx, D, T)>,
+) -> Vec<(Cow<'a, str>, Option<f64>, D, T)> {
     let mut quants = quants
-        .filter_map(|(q, c)| {
+        .filter_map(|(q, d, c)| {
             let name = parser[q].kind.name(&parser.strings)?;
             let hue = colour_map.get_rbg_hue(Some(q));
             // log::info!("{name}: {hue:?} | {c:?}");
-            Some((name, hue, c))
+            Some((name, hue, d, c))
         })
         .collect::<Vec<_>>();
     if REVERSE {

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);