diff --git a/axiom-profiler-GUI/src/configuration/data.rs b/axiom-profiler-GUI/src/configuration/data.rs index ff7e02aa..bdd3e8d3 100644 --- a/axiom-profiler-GUI/src/configuration/data.rs +++ b/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), } } } diff --git a/axiom-profiler-GUI/src/configuration/page.rs b/axiom-profiler-GUI/src/configuration/page.rs index 1c1891c3..944fff79 100644 --- a/axiom-profiler-GUI/src/configuration/page.rs +++ b/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,6 +129,19 @@ 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! {

{"Configuration flags"}

@@ -136,6 +149,7 @@ pub fn Flags(props: &FlagsProps) -> Html { {debug} {replace_symbols} {ast_depth_limit} + {summary_weighing}
} diff --git a/axiom-profiler-GUI/src/screen/file/summary.rs b/axiom-profiler-GUI/src/screen/file/summary.rs index a58669c2..3e5dc091 100644 --- a/axiom-profiler-GUI/src/screen/file/summary.rs +++ b/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, pub term_display: Rc, 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! {
{ format!("{q}") }
}; (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! {
{ format!("{q}") }
}; (left, right) }).collect::>(); - html! { + html! { } }).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! {
{ format!("{q}") }
}; (left, right) }).collect::>(); - html! { + html! { } }).unwrap_or_default() @@ -251,17 +255,17 @@ fn format_to_html(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, -) -> Vec<(Cow<'a, str>, Option, T)> { + quants: impl Iterator, +) -> Vec<(Cow<'a, str>, Option, 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::>(); if REVERSE { diff --git a/smt-log-parser/src/util.rs b/smt-log-parser/src/util.rs index a42c7523..8010c47f 100644 --- a/smt-log-parser/src/util.rs +++ b/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 {