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| {
@@ -83,6 +84,7 @@ pub struct SummaryPropsInner {
     pub analysis: Option<RcAnalysis>,
     pub term_display: Rc<TermDisplayContext>,
     pub config: DisplayConfiguration,
+    pub avg_weighing: f64,
 }
 
 impl SummaryPropsInner {
@@ -139,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)
@@ -163,23 +165,24 @@ pub fn CostQuants(props: &SummaryPropsInner) -> Html {
         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)| {
             let qis = log_info.quant_insts(q);
             if qis == 0 {
-                (q, F64Ord(0.0))
+                (q, 0.0, F64Ord(0.0))
             } else {
-                (q, F64Ord(c / qis as f64))
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
             }
         });
-        let costs = quants_ordered::<_, true>(&parser, colours, costs);
+        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 = html!{{ format!("{:.1}", c.0) }};
+        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()
@@ -192,23 +195,24 @@ pub fn MultQuants(props: &SummaryPropsInner) -> Html {
         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, F64Ord(0.0))
+                (q, 0.0, F64Ord(0.0))
             } else {
-                (q, F64Ord(c / qis as f64))
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
             }
         });
-        let mults = quants_ordered::<_, true>(&parser, colours, mults);
+        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 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="Multiplicative quantifiers" hover="The quantifiers which the highest multiplicative factor, i.e. those that on average directly cause N other instantiations.">
+        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()
@@ -251,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 {

smt-log-parser/src/util.rs

@@ -1,5 +1,11 @@
-#[derive(Debug, Clone, Copy, PartialEq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone, Copy)]
 pub struct F64Ord(pub f64);
+impl std::cmp::PartialEq for F64Ord {
+    fn eq(&self, other: &Self) -> bool {
+        self.0.total_cmp(&other.0).is_eq()
+    }
+}
 impl std::cmp::Eq for F64Ord {}
 impl std::cmp::PartialOrd for F64Ord {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {