Wrote basic code for term generalisation and refactored graph_filters.rs

viperproject · Dec 22, 2023 · c7b7b2f · c7b7b2f
1 parent 64a982a
commit c7b7b2f
Show file tree

Hide file tree

Showing 9 changed files with 330 additions and 116 deletions.
diff --git a/axiom-profiler-GUI/src/results/filters/filter_chain.rs b/axiom-profiler-GUI/src/results/filters/filter_chain.rs
@@ -1,5 +1,5 @@
 use super::super::svg_result::{UserPermission, DEFAULT_NODE_COUNT};
-use super::graph_filters::{Filter, GraphFilter};
+use super::graph_filters::{Filter, GraphFilters};
 use gloo::console::log;
 use yew::prelude::*;
 // use gloo_console::log;
@@ -114,7 +114,7 @@ impl yew::html::Component for FilterChain {
         let add_filters = ctx.link().callback(Msg::AddFilters);
         html!(
             <>
-                <GraphFilter
+                <GraphFilters
                     add_filters={add_filters.clone()}
                     dependency={ctx.props().dependency}
                 />

diff --git a/axiom-profiler-GUI/src/results/filters/graph_filters.rs b/axiom-profiler-GUI/src/results/filters/graph_filters.rs
@@ -1,5 +1,5 @@
 use super::node_actions::NodeActions;
-use crate::utils::input_state::{InputValue, UsizeInput};
+use crate::{utils::usize_input::UsizeInput, results::svg_result::DEFAULT_NODE_COUNT};
 use petgraph::{stable_graph::NodeIndex, Direction};
 use smt_log_parser::{
     items::QuantIdx,
@@ -21,7 +21,7 @@ pub enum Filter {
     VisitSubTreeWithRoot(NodeIndex, bool),
     MaxDepth(usize),
     ShowLongestPath(NodeIndex),
-    ShowMatchingLoops,
+    AnalyzeMatchingLoops(usize),
 }
 
 impl Display for Filter {
@@ -61,7 +61,7 @@ impl Display for Filter {
             Self::ShowLongestPath(node) => {
                 write!(f, "Showing longest path through node {}", node.index())
             }
-            Self::ShowMatchingLoops => write!(f, "Showing matching loops"),
+            Self::AnalyzeMatchingLoops(loop_count) => write!(f, "Showing the {} longest matching loops", loop_count),
         }
     }
 }
@@ -89,7 +89,7 @@ impl Filter {
                 graph.retain_nodes(|node: &NodeData| node.min_depth.unwrap() <= depth)
             }
             Filter::ShowLongestPath(nidx) => return Some(graph.show_longest_path_through(nidx)),
-            Filter::ShowMatchingLoops => graph.show_matching_loops(),
+            Filter::AnalyzeMatchingLoops(n) => graph.show_n_longest_matching_loops(n),
         }
         None
     }
@@ -101,107 +101,181 @@ pub struct GraphFilterProps {
     pub dependency: *const smt_log_parser::Z3Parser,
 }
 
-#[function_component(GraphFilter)]
-pub fn graph_filter(props: &GraphFilterProps) -> Html {
-    let max_node_idx = use_reducer(InputValue::default);
-    let max_instantiations = use_reducer(InputValue::default);
-    let max_branching = use_reducer(InputValue::default);
-    let max_depth = use_reducer(InputValue::default);
-    let selected_insts = use_context::<Vec<InstInfo>>().expect("no ctx found");
+pub struct GraphFilters {
+    max_node_idx: usize,
+    max_instantiations: usize,
+    max_branching: usize,
+    max_depth: usize,
+    max_matching_loops: usize,
+    selected_insts: Vec<InstInfo>,
+    context_listener: ContextHandle<Vec<InstInfo>>,
+    // add additional bool field to store whether matching loops have 
+    // already been analyzed 
+    // analyzed_matching_loops
+    // in that case, display additional filters such as 
+    // show n longest matching loops where n =
+}
 
-    let add_max_line_nr_filter = {
-        let max_node_idx = max_node_idx.clone();
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::MaxNodeIdx(max_node_idx.value)]))
-    };
-    let add_theory_filter = {
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::IgnoreTheorySolving]))
-    };
-    let add_max_insts_filter = {
-        let max_instantiations = max_instantiations.clone();
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::MaxInsts(max_instantiations.value)]))
-    };
-    let add_max_branching_filter = {
-        let max_branching = max_branching.clone();
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::MaxBranching(max_branching.value)]))
-    };
-    let add_max_depth_filter = {
-        let max_depth = max_depth.clone();
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth.value)]))
-    };
-    let show_matching_loops = {
-        let callback = props.add_filters.clone();
-        Callback::from(move |_| callback.emit(vec![Filter::ShowMatchingLoops]))
-    };
-    html! {
-        <div>
-            <h2>{"Add (optional) filters:"}</h2>
-            <div>
-                <UsizeInput
-                    label={"Only show nodes up to index "}
-                    dependency={props.dependency}
-                    input_value={max_node_idx}
-                    default_value={usize::MAX}
-                    placeholder={""}
-                />
-                <button onclick={add_max_line_nr_filter}>{"Add"}</button>
-            </div>
-            <div>
-                <label for="theory_button">{"Ignore theory-solving instantiations"}</label>
-                <button onclick={add_theory_filter} id="theory_button">{"Add"}</button>
-            </div>
-            <div>
-                <UsizeInput
-                    label={"Render the n most expensive instantiations where n = "}
-                    dependency={props.dependency}
-                    input_value={max_instantiations}
-                    default_value={super::super::svg_result::DEFAULT_NODE_COUNT}
-                    placeholder={""}
-                />
-                <button onclick={add_max_insts_filter}>{"Add"}</button>
-            </div>
-            <div>
-                <UsizeInput
-                    label={"Render the n instantiations with most children where n = "}
-                    dependency={props.dependency}
-                    input_value={max_branching}
-                    default_value={usize::MAX}
-                    placeholder={""}
-                />
-                <button onclick={add_max_branching_filter}>{"Add"}</button>
-            </div>
-            <div>
-                <UsizeInput
-                    label={"Render up to depth "}
-                    dependency={props.dependency}
-                    input_value={max_depth}
-                    default_value={usize::MAX}
-                    placeholder={""}
-                />
-                <button onclick={add_max_depth_filter}>{"Add"}</button>
-            </div>
+#[derive(Properties, PartialEq)]
+pub struct GraphFiltersProps {
+    pub add_filters: Callback<Vec<Filter>>,
+    pub dependency: *const smt_log_parser::Z3Parser,
+}
+
+pub enum Msg {
+    SetMaxNodeIdx(usize),
+    SetMaxInsts(usize),
+    SetMaxBranching(usize),
+    SetMaxDepth(usize),
+    SetMaxMatchingLoops(usize),
+    SelectedInstsUpdated(Vec<InstInfo>)
+}
+
+impl Component for GraphFilters {
+    type Message = Msg;
+    type Properties = GraphFiltersProps;
+
+    fn update(&mut self, ctx: &Context<Self>, msg: Self::Message) -> bool {
+        match msg {
+            Msg::SetMaxNodeIdx(to) => {
+                self.max_node_idx = to;
+                true
+            }
+            Msg::SetMaxInsts(to) => {
+                self.max_instantiations = to;
+                true
+            }
+            Msg::SetMaxBranching(to) => {
+                self.max_branching = to;
+                true
+            }
+            Msg::SetMaxDepth(to) => {
+                self.max_depth = to;
+                true
+            }
+            Msg::SetMaxMatchingLoops(to) => {
+                self.max_matching_loops = to;
+                true
+            }
+            Msg::SelectedInstsUpdated(selected_insts) => {
+                self.selected_insts = selected_insts;
+                true
+            }
+        }
+    }
+
+    fn create(ctx: &Context<Self>) -> Self {
+        let (selected_insts, context_listener) = ctx
+            .link()
+            .context(ctx.link().callback(Msg::SelectedInstsUpdated))
+            .expect("No context provided");
+        Self {
+            max_node_idx: usize::MAX,
+            max_instantiations: DEFAULT_NODE_COUNT,
+            max_branching: usize::MAX,
+            max_depth: usize::MAX,
+            max_matching_loops: 1,
+            selected_insts,
+            context_listener,
+        }
+    }
+    fn view(&self, ctx: &Context<Self>) -> Html {
+        let add_max_line_nr_filter = {
+            let callback = ctx.props().add_filters.clone();
+            let max_node_idx = self.max_node_idx;
+            Callback::from(move |_| callback.emit(vec![Filter::MaxNodeIdx(max_node_idx)]))
+        };
+        let add_theory_filter = {
+            let callback = ctx.props().add_filters.clone();
+            Callback::from(move |_| callback.emit(vec![Filter::IgnoreTheorySolving]))
+        };
+        let add_max_insts_filter = {
+            let callback = ctx.props().add_filters.clone();
+            let max_instantiations = self.max_instantiations;
+            Callback::from(move |_| callback.emit(vec![Filter::MaxInsts(max_instantiations)]))
+        };
+        let add_max_branching_filter = {
+            let callback = ctx.props().add_filters.clone();
+            let max_branching = self.max_branching;
+            Callback::from(move |_| callback.emit(vec![Filter::MaxBranching(max_branching)]))
+        };
+        let add_max_depth_filter = {
+            let callback = ctx.props().add_filters.clone();
+            let max_depth = self.max_depth;
+            Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth)]))
+        };
+        let analyze_matching_loops = {
+            let callback = ctx.props().add_filters.clone();
+            let max_matching_loops = self.max_matching_loops;
+            Callback::from(move |_| callback.emit(vec![Filter::AnalyzeMatchingLoops(max_matching_loops)]))
+        };
+        html! {
             <div>
-                <label for="matching_loops">{"Show matching loops"}</label>
-                <button onclick={show_matching_loops} id="matching_loops">{"Add"}</button>
+                <h2>{"Add (optional) filters:"}</h2>
+                <div>
+                    // pass a WeakComponentLink here as prop such that the UsizeInput can directly update the 
+                    // fields in the GraphFilters struct
+                    <UsizeInput
+                        label={"Only show nodes up to index "}
+                        placeholder={""}
+                        set_value={ctx.link().callback(Msg::SetMaxNodeIdx)}
+                    />
+                    <button onclick={add_max_line_nr_filter}>{"Add"}</button>
+                </div>
+                <div>
+                    <label for="theory_button">{"Ignore theory-solving instantiations"}</label>
+                    <button onclick={add_theory_filter} id="theory_button">{"Add"}</button>
+                </div>
+                <div>
+                    <UsizeInput
+                        label={"Render the n most expensive instantiations where n = "}
+                        placeholder={""}
+                        set_value={ctx.link().callback(Msg::SetMaxInsts)}
+                    />
+                    <button onclick={add_max_insts_filter}>{"Add"}</button>
+                </div>
+                <div>
+                    <UsizeInput
+                        label={"Render the n instantiations with most children where n = "}
+                        placeholder={""}
+                        set_value={ctx.link().callback(Msg::SetMaxBranching)}
+                    />
+                    <button onclick={add_max_branching_filter}>{"Add"}</button>
+                </div>
+                <div>
+                    <UsizeInput
+                        label={"Render up to depth "}
+                        placeholder={""}
+                        set_value={ctx.link().callback(Msg::SetMaxDepth)}
+                    />
+                    <button onclick={add_max_depth_filter}>{"Add"}</button>
+                </div>
+                // <div>
+                //     <label for="matching_loops">{"Show matching loops"}</label>
+                //     <button onclick={show_matching_loops} id="matching_loops">{"Add"}</button>
+                // </div>
+                <div>
+                    <UsizeInput
+                        label={"Analyze the n longest matching loops where n = "}
+                        placeholder={"1"}
+                        set_value={ctx.link().callback(Msg::SetMaxMatchingLoops)}
+                    />
+                    <button onclick={analyze_matching_loops}>{"Add"}</button>
+                </div>
+                {if !self.selected_insts.is_empty() {
+                    html! {
+                        <NodeActions selected_nodes={self.selected_insts.clone()} action={ctx.props().add_filters.clone()} />
+                    }
+                } else {
+                    html! {}
+                }}
+                // <SelectDropDown
+                //     label={"Select a layout engine:"}
+                //     options={layout_engines}
+                //     selected_option={layout_engine}
+                // />
+                // <button onclick={update_settings}>{"Render graph"}</button>
             </div>
-            {if !selected_insts.is_empty() {
-                html! {
-                    <NodeActions selected_nodes={selected_insts} action={props.add_filters.clone()} />
-                }
-            } else {
-                html! {}
-            }}
-            // <SelectDropDown
-            //     label={"Select a layout engine:"}
-            //     options={layout_engines}
-            //     selected_option={layout_engine}
-            // />
-            // <button onclick={update_settings}>{"Render graph"}</button>
-        </div>
-
+        }
     }
-}
+}
diff --git a/axiom-profiler-GUI/src/utils/mod.rs b/axiom-profiler-GUI/src/utils/mod.rs
@@ -1,2 +1,3 @@
 pub mod input_state;
 pub mod toggle_switch;
+pub mod usize_input;