diff --git a/axiom-profiler-GUI/src/lib.rs b/axiom-profiler-GUI/src/lib.rs index 89224005..742fca24 100644 --- a/axiom-profiler-GUI/src/lib.rs +++ b/axiom-profiler-GUI/src/lib.rs @@ -1,3 +1,5 @@ +use std::cell::RefCell; + use gloo_file::{callbacks::FileReader, FileList}; use results::svg_result::SVGResult; use smt_log_parser::parsers::z3::z3parser::Z3Parser; @@ -172,10 +174,10 @@ enum Route { Test, } -pub struct RcParser(std::rc::Rc); +pub struct RcParser(std::rc::Rc>); impl std::ops::Deref for RcParser { - type Target = Z3Parser; + type Target = RefCell; fn deref(&self) -> &Self::Target { &self.0 @@ -196,9 +198,6 @@ impl PartialEq for RcParser { impl RcParser { fn new(parser: Z3Parser) -> Self { - Self(std::rc::Rc::new(parser)) - } - pub(crate) fn as_ptr(&self) -> *const Z3Parser { - std::rc::Rc::as_ptr(&self.0) + Self(std::rc::Rc::new(RefCell::new(parser))) } } diff --git a/axiom-profiler-GUI/src/results/filters/filter_chain.rs b/axiom-profiler-GUI/src/results/filters/filter_chain.rs index 8158d92c..346c516e 100644 --- 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; @@ -15,6 +15,7 @@ pub enum Msg { pub struct FilterChain { filter_chain: Vec, prev_filter_chain: Vec, + add_filters: Callback>, } const DEFAULT_FILTER_CHAIN: &[Filter] = &[ @@ -27,7 +28,6 @@ pub struct FilterChainProps { pub apply_filter: Callback, pub reset_graph: Callback<()>, pub render_graph: Callback, - pub dependency: *const smt_log_parser::Z3Parser, pub weak_link: WeakComponentLink, } @@ -36,6 +36,7 @@ impl yew::html::Component for FilterChain { type Properties = FilterChainProps; fn create(ctx: &Context) -> Self { + log!("Creating FilterChain component"); ctx.props() .weak_link .borrow_mut() @@ -46,9 +47,11 @@ impl yew::html::Component for FilterChain { } ctx.props().render_graph.emit(UserPermission::default()); let prev_filter_chain = filter_chain.clone(); + let add_filters = ctx.link().callback(Msg::AddFilters); Self { filter_chain, prev_filter_chain, + add_filters, } } @@ -62,7 +65,8 @@ impl yew::html::Component for FilterChain { ctx.props().apply_filter.emit(filter); } ctx.props().render_graph.emit(UserPermission::default()); - true + // true + false } Msg::RemoveNthFilter(n) => { log!("Removing filter", n); @@ -111,12 +115,10 @@ impl yew::html::Component for FilterChain { .collect(); let reset_filters = ctx.link().callback(|_| Msg::ResetFilters); - let add_filters = ctx.link().callback(Msg::AddFilters); html!( <> -

{"Filter chain:"}

{for filter_chain} diff --git a/axiom-profiler-GUI/src/results/filters/graph_filters.rs b/axiom-profiler-GUI/src/results/filters/graph_filters.rs index 6e8f7cc5..d757d066 100644 --- a/axiom-profiler-GUI/src/results/filters/graph_filters.rs +++ b/axiom-profiler-GUI/src/results/filters/graph_filters.rs @@ -1,9 +1,10 @@ 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 gloo::console::log; use petgraph::{stable_graph::NodeIndex, Direction}; use smt_log_parser::{ items::QuantIdx, - parsers::z3::inst_graph::{InstGraph, InstInfo, NodeData}, + parsers::z3::inst_graph::{InstGraph, InstInfo, NodeData}, Z3Parser, }; use std::fmt::Display; use yew::prelude::*; @@ -21,7 +22,8 @@ pub enum Filter { VisitSubTreeWithRoot(NodeIndex, bool), MaxDepth(usize), ShowLongestPath(NodeIndex), - ShowMatchingLoops, + SelectNthMatchingLoop(usize), + ShowMatchingLoopSubgraph, } impl Display for Filter { @@ -61,147 +63,187 @@ impl Display for Filter { Self::ShowLongestPath(node) => { write!(f, "Showing longest path through node {}", node.index()) } - Self::ShowMatchingLoops => write!(f, "Showing matching loops"), + Self::SelectNthMatchingLoop(n) => { + let ordinal = match n { + 0 => "".to_string(), + 1 => "2nd".to_string(), + 2 => "3rd".to_string(), + n => (n+1).to_string() + "th", + }; + write!(f, "Showing {} longest matching loop", ordinal) + } + Self::ShowMatchingLoopSubgraph => { + write!(f, "Showing all potential matching loops") + } } } } +pub enum FilterOutput { + LongestPath(Vec), + MatchingLoopGeneralizedTerms(Vec), + None +} + impl Filter { - pub fn apply(self: Filter, graph: &mut InstGraph) -> Option> { + pub fn apply(self: Filter, graph: &mut InstGraph, parser: &mut Z3Parser) -> FilterOutput { match self { - Filter::MaxNodeIdx(max) => graph - .retain_nodes(|node: &NodeData| node.orig_graph_idx.index() <= max), - Filter::IgnoreTheorySolving => { - graph.retain_nodes(|node: &NodeData| !node.is_theory_inst) - } - Filter::IgnoreQuantifier(qidx) => { - graph.retain_nodes(|node: &NodeData| node.mkind.quant_idx() != qidx) - } - Filter::IgnoreAllButQuantifier(qidx) => { - graph.retain_nodes(|node: &NodeData| node.mkind.quant_idx() == qidx) - } + Filter::MaxNodeIdx(max) => graph.retain_nodes(|node: &NodeData| node.orig_graph_idx.index() <= max), + Filter::IgnoreTheorySolving => graph.retain_nodes(|node: &NodeData| !node.is_theory_inst), + Filter::IgnoreQuantifier(qidx) => graph.retain_nodes(|node: &NodeData| node.mkind.quant_idx() != qidx), + Filter::IgnoreAllButQuantifier(qidx) => graph.retain_nodes(|node: &NodeData| node.mkind.quant_idx() == qidx), Filter::MaxInsts(n) => graph.keep_n_most_costly(n), Filter::MaxBranching(n) => graph.keep_n_most_branching(n), Filter::ShowNeighbours(nidx, direction) => graph.show_neighbours(nidx, direction), Filter::VisitSubTreeWithRoot(nidx, retain) => graph.visit_descendants(nidx, retain), Filter::VisitSourceTree(nidx, retain) => graph.visit_ancestors(nidx, retain), - Filter::MaxDepth(depth) => { - 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::MaxDepth(depth) => graph.retain_nodes(|node: &NodeData| node.min_depth.unwrap() <= depth), + Filter::ShowLongestPath(nidx) => return FilterOutput::LongestPath(graph.show_longest_path_through(nidx)), + Filter::SelectNthMatchingLoop(n) => return FilterOutput::MatchingLoopGeneralizedTerms(graph.show_nth_matching_loop(n, parser)), + Filter::ShowMatchingLoopSubgraph => graph.show_matching_loop_subgraph(), } - None + FilterOutput::None } } +pub struct GraphFilters { + max_node_idx: usize, + max_instantiations: usize, + max_branching: usize, + max_depth: usize, + selected_insts: Vec, + _selected_insts_listener: ContextHandle>, +} + #[derive(Properties, PartialEq)] -pub struct GraphFilterProps { +pub struct GraphFiltersProps { pub add_filters: Callback>, - 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::>().expect("no ctx found"); +pub enum Msg { + SetMaxNodeIdx(usize), + SetMaxInsts(usize), + SetMaxBranching(usize), + SetMaxDepth(usize), + SelectedInstsUpdated(Vec), +} - 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! { -
-

{"Add (optional) filters:"}

-
- - -
-
- - -
-
- - -
-
- - -
-
- - -
+impl Component for GraphFilters { + type Message = Msg; + type Properties = GraphFiltersProps; + + fn update(&mut self, _ctx: &Context, 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::SelectedInstsUpdated(selected_insts) => { + self.selected_insts = selected_insts; + true + } + } + } + + fn create(ctx: &Context) -> Self { + log!("Creating GraphFilters component"); + let (selected_insts, _selected_insts_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, + selected_insts, + _selected_insts_listener, + } + } + fn view(&self, ctx: &Context) -> 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)])) + }; + html! {
- - +

{"Add (optional) filters:"}

+
+ + +
+
+ + +
+
+ + +
+
+ + +
+
+ + +
+ {if !self.selected_insts.is_empty() { + html! { + + } + } else { + html! {} + }}
- {if !selected_insts.is_empty() { - html! { - - } - } else { - html! {} - }} - // - // -
- + } } -} +} \ No newline at end of file diff --git a/axiom-profiler-GUI/src/results/graph_info.rs b/axiom-profiler-GUI/src/results/graph_info.rs index 34b75332..769da609 100644 --- a/axiom-profiler-GUI/src/results/graph_info.rs +++ b/axiom-profiler-GUI/src/results/graph_info.rs @@ -3,10 +3,15 @@ use gloo::console::log; use indexmap::map::IndexMap; use material_yew::WeakComponentLink; use petgraph::graph::{EdgeIndex, NodeIndex}; +use smt_log_parser::parsers::z3::inst_graph::EdgeType; use smt_log_parser::{ items::BlameKind, - parsers::z3::inst_graph::{EdgeInfo, InstInfo}, + parsers::z3::{ + inst_graph::{EdgeInfo, InstInfo}, + z3parser::Z3Parser, + }, }; +use std::rc::Rc; use web_sys::HtmlElement; use yew::prelude::*; @@ -20,6 +25,7 @@ pub struct GraphInfo { selected_edges: IndexMap, selected_edges_ref: NodeRef, ignore_term_ids: bool, + generalized_terms: Vec, } pub enum Msg { @@ -30,6 +36,7 @@ pub enum Msg { SelectNodes(Vec), DeselectAll, ToggleIgnoreTermIds, + ShowGeneralizedTerms(Vec), } #[derive(Properties, PartialEq)] @@ -60,6 +67,7 @@ impl Component for GraphInfo { selected_edges: IndexMap::new(), selected_edges_ref: NodeRef::default(), ignore_term_ids: true, + generalized_terms: Vec::new(), } } @@ -181,6 +189,10 @@ impl Component for GraphInfo { } true } + Msg::ShowGeneralizedTerms(terms) => { + self.generalized_terms = terms; + true + } } } @@ -231,6 +243,9 @@ impl Component for GraphInfo { let on_node_select = ctx.link().callback(Msg::UserSelectedNode); let on_edge_select = ctx.link().callback(Msg::UserSelectedEdge); let deselect_all = ctx.link().callback(|_| Msg::DeselectAll); + let generalized_terms = self.generalized_terms.iter().map(|term| html! { +
  • {term}
    • + }); html! { <> >()} /> -
    +
    +
    + + +

    {"Information about selected nodes:"}

    >()} on_click={on_node_click} /> @@ -249,9 +268,9 @@ impl Component for GraphInfo {
    >()} on_click={on_edge_click} />
    +

    {"Information about displayed matching loop:"}

    - - +
      {for generalized_terms}
    diff --git a/axiom-profiler-GUI/src/results/svg_result.rs b/axiom-profiler-GUI/src/results/svg_result.rs index cf00a7ab..12cfc71f 100644 --- a/axiom-profiler-GUI/src/results/svg_result.rs +++ b/axiom-profiler-GUI/src/results/svg_result.rs @@ -1,6 +1,6 @@ use crate::{ - results::graph_info::{GraphInfo, Msg as GraphInfoMsg}, - RcParser, + results::{graph_info::{GraphInfo, Msg as GraphInfoMsg}, filters::graph_filters::FilterOutput}, + RcParser, utils::indexer::Indexer, }; use self::colours::HSVColour; @@ -17,7 +17,13 @@ use petgraph::dot::{Config, Dot}; use petgraph::graph::{EdgeIndex, NodeIndex}; use smt_log_parser::{ items::{BlameKind, MatchKind}, - parsers::z3::inst_graph::{EdgeInfo, EdgeType, InstGraph, InstInfo, VisibleGraphInfo}, + parsers::{ + z3::{ + inst_graph::{EdgeInfo, EdgeType, InstGraph, InstInfo, VisibleGraphInfo}, + z3parser::Z3Parser, + }, + LogParser, + }, }; use std::num::NonZeroUsize; use viz_js::VizInstance; @@ -37,6 +43,9 @@ pub enum Msg { GetUserPermission, WorkerOutput(super::worker::WorkerOutput), UpdateSelectedNodes(Vec), + SearchMatchingLoops, + SelectNthMatchingLoop(usize), + ShowMatchingLoopSubgraph, } #[derive(Default)] @@ -68,6 +77,8 @@ pub struct SVGResult { get_node_info: Callback<(NodeIndex, bool, RcParser), InstInfo>, get_edge_info: Callback<(EdgeIndex, bool, RcParser), EdgeInfo>, selected_insts: Vec, + searched_matching_loops: bool, + matching_loop_count: usize, } #[derive(Properties, PartialEq)] @@ -82,19 +93,19 @@ impl Component for SVGResult { fn create(ctx: &Context) -> Self { log::debug!("Creating SVGResult component"); let parser = RcParser::clone(&ctx.props().parser); - let inst_graph = InstGraph::from(&parser); - let (quant_count, non_quant_insts) = parser.quant_count_incl_theory_solving(); + let inst_graph = InstGraph::from(&parser.borrow()); + let (quant_count, non_quant_insts) = parser.borrow().quant_count_incl_theory_solving(); let colour_map = QuantIdxToColourMap::from(quant_count, non_quant_insts); let get_node_info = Callback::from({ let node_info_map = inst_graph.get_node_info_map(); move |(node, ignore_ids, parser): (NodeIndex, bool, RcParser)| { - node_info_map.get_instantiation_info(node.index(), &parser, ignore_ids) + node_info_map.get_instantiation_info(node.index(), &parser.borrow(), ignore_ids) } }); let get_edge_info = Callback::from({ let edge_info_map = inst_graph.get_edge_info_map(); move |(edge, ignore_ids, parser): (EdgeIndex, bool, RcParser)| { - edge_info_map.get_edge_info(edge, &parser, ignore_ids) + edge_info_map.get_edge_info(edge, &parser.borrow(), ignore_ids) } }); Self { @@ -113,6 +124,8 @@ impl Component for SVGResult { get_node_info, get_edge_info, selected_insts: Vec::new(), + searched_matching_loops: false, + matching_loop_count: 0, } } @@ -121,17 +134,48 @@ impl Component for SVGResult { Msg::WorkerOutput(_out) => false, Msg::ApplyFilter(filter) => { log::debug!("Applying filter {}", filter); - if let Some(ref path) = filter.apply(&mut self.inst_graph) { - self.insts_info_link - .borrow() - .clone() - .unwrap() - .send_message(GraphInfoMsg::SelectNodes(path.clone())); - false - } else { - false + match filter.apply(&mut self.inst_graph, &mut self.parser.borrow_mut()) { + FilterOutput::LongestPath(path) => { + self.insts_info_link + .borrow() + .clone() + .unwrap() + .send_message(GraphInfoMsg::SelectNodes(path)); + false + } + FilterOutput::MatchingLoopGeneralizedTerms(gen_terms) => { + self.insts_info_link + .borrow() + .clone() + .unwrap() + .send_message(GraphInfoMsg::ShowGeneralizedTerms(gen_terms)); + false + } + FilterOutput::None => false } } + Msg::SearchMatchingLoops => { + self.matching_loop_count = self.inst_graph.search_matching_loops(); + self.searched_matching_loops = true; + ctx.link().send_message(Msg::SelectNthMatchingLoop(0)); + true + } + Msg::SelectNthMatchingLoop(n) => { + self.filter_chain_link + .borrow() + .clone() + .unwrap() + .send_message(FilterChainMsg::AddFilters(vec![Filter::SelectNthMatchingLoop(n)])); + false + } + Msg::ShowMatchingLoopSubgraph => { + self.filter_chain_link + .borrow() + .clone() + .unwrap() + .send_message(FilterChainMsg::AddFilters(vec![Filter::ShowMatchingLoopSubgraph])); + false + } Msg::ResetGraph => { log::debug!("Resetting graph"); self.inst_graph.reset_visibility_to(true); @@ -332,13 +376,28 @@ impl Component for SVGResult { html! { <>
    + {if !self.searched_matching_loops { + html! { + + } + } else { + html! { + <> + + + + } + }} > context={self.selected_insts.clone()}> >> {async_graph_and_filter_chain_warning} diff --git a/axiom-profiler-GUI/src/utils/indexer.rs b/axiom-profiler-GUI/src/utils/indexer.rs new file mode 100644 index 00000000..ef309aa7 --- /dev/null +++ b/axiom-profiler-GUI/src/utils/indexer.rs @@ -0,0 +1,90 @@ +use yew::prelude::*; + +#[derive(Properties, PartialEq)] +pub struct IndexerProps { + pub label: AttrValue, + pub index_consumer: Callback, + pub max: usize, +} + +pub struct Indexer { + index: usize, +} + +pub enum Msg { + Decrement, + Increment, + SetToMin, + SetToMax, +} + +impl Component for Indexer { + type Message = Msg; + + type Properties = IndexerProps; + + fn create(_ctx: &Context) -> Self { + Self { + index: 0, + } + } + + fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { + match msg { + Msg::Decrement => { + let old_index = self.index; + self.index = self.index.saturating_sub(1); + if old_index != self.index { + ctx.props().index_consumer.emit(self.index); + true + } else { + false + } + } + Msg::Increment => { + if self.index + 1 <= ctx.props().max { + self.index = self.index.saturating_add(1); + ctx.props().index_consumer.emit(self.index); + true + } else { + false + } + } + Msg::SetToMin => { + let old_index = self.index; + self.index = 0; + if old_index != self.index { + ctx.props().index_consumer.emit(self.index); + true + } else { + false + } + } + Msg::SetToMax => { + let old_index = self.index; + self.index = ctx.props().max; + if old_index != self.index { + ctx.props().index_consumer.emit(self.index); + true + } else { + false + } + } + } + } + + fn view(&self, ctx: &Context) -> Html { + html! { +
    +

    {ctx.props().label.to_string()}

    +
    + + + {format!("{}/{}", self.index + 1, ctx.props().max + 1) } + + +
    +
    + } + } +} \ No newline at end of file diff --git a/axiom-profiler-GUI/src/utils/input_state.rs b/axiom-profiler-GUI/src/utils/input_state.rs deleted file mode 100644 index 7f2eb39b..00000000 --- a/axiom-profiler-GUI/src/utils/input_state.rs +++ /dev/null @@ -1,120 +0,0 @@ -use wasm_bindgen::{JsCast, UnwrapThrowExt}; -use web_sys::HtmlInputElement; -use yew::prelude::*; - -pub enum InputAction { - SetValueTo(usize), -} - -#[derive(Clone, Debug, PartialEq)] -pub struct InputValue { - pub value: usize, -} - -impl Default for InputValue { - fn default() -> Self { - Self { value: usize::MAX } - } -} - -impl From for InputValue { - fn from(value: usize) -> Self { - Self { value } - } -} - -impl Reducible for InputValue { - type Action = InputAction; - - fn reduce(self: std::rc::Rc, action: Self::Action) -> std::rc::Rc { - match action { - InputAction::SetValueTo(value) => Self { value }.into(), - } - } -} - -#[derive(Properties, PartialEq)] -pub struct UsizeInputProps { - pub label: AttrValue, - pub dependency: *const smt_log_parser::Z3Parser, - pub input_value: UseReducerHandle, - pub default_value: usize, - pub placeholder: AttrValue, -} - -/// Function component for input fields that accept usize -/// Must specify label: AttrValue, dependency: AttrValue, input_value: UseReducerHandle -/// Resets the value whenever the dependency changes -#[function_component(UsizeInput)] -pub fn integer_input(props: &UsizeInputProps) -> Html { - let input_value = props.input_value.clone(); - let input_ref = use_node_ref(); - - let set_value = { - let input_value = input_value.clone(); - let default_value = props.default_value; - move |input_event: Event| { - let target: HtmlInputElement = input_event - .target() - .unwrap_throw() - .dyn_into() - .unwrap_throw(); - match target.value().to_string().parse::() { - Ok(value) => { - log::debug!("Setting the value to {}", value); - input_value.dispatch(InputAction::SetValueTo(value)); - } - Err(_) => { - input_value.dispatch(InputAction::SetValueTo(default_value)); - } - } - } - }; - - let set_value_on_enter = Callback::from({ - let set_value = set_value.clone(); - move |key_event: KeyboardEvent| { - if key_event.key() == "Enter" { - let event: Event = key_event.clone().into(); - set_value(event); - } - } - }); - - let set_value_on_blur = Callback::from({ - let set_value = set_value.clone(); - move |blur_event: FocusEvent| { - let event: Event = blur_event.clone().into(); - set_value(event); - } - }); - - { - // Whenever dependency changes, need to reset the state - let dep = props.dependency; - let input_value = input_value.clone(); - let input_ref = input_ref.clone(); - let default_value = props.default_value; - use_effect_with_deps( - { - let input_value = input_value.clone(); - move |_| { - input_value.dispatch(InputAction::SetValueTo(default_value)); - let input = input_ref - .cast::() - .expect("div_ref not attached to div element"); - input.set_value(""); - } - }, - dep, - ); - } - let placeholder = props.placeholder.to_string(); - - html! { - <> - - - - } -} diff --git a/axiom-profiler-GUI/src/utils/mod.rs b/axiom-profiler-GUI/src/utils/mod.rs index 716bddac..0caa51b1 100644 --- 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; +pub mod indexer; \ No newline at end of file diff --git a/axiom-profiler-GUI/src/utils/select_dropdown.rs b/axiom-profiler-GUI/src/utils/select_dropdown.rs deleted file mode 100644 index 5ccf28a9..00000000 --- a/axiom-profiler-GUI/src/utils/select_dropdown.rs +++ /dev/null @@ -1,38 +0,0 @@ -use yew::prelude::*; - -#[derive(Properties, PartialEq)] -pub struct SelectDropDownProps where { - pub label: AttrValue, - pub options: Vec, - pub selected_option: UseStateHandle, -} - -#[function_component(SelectDropDown)] -pub fn select_dropdown(props: &SelectDropDownProps) -> Html { - let options = props.options.iter().enumerate().map(|(idx, option)| html! { - - }); - - // let change_selected_option = Callback::from({ - // let selected_option = props.selected_option.clone(); - // move |event: Event| { - // if let Some(target) = event.target() { - // if let Ok(select) = target.dyn_into::() { - // let selected_value = select.value().to_string(); - // log::debug!("Selected: {selected_value}"); - // } - // } - // } - // }); - - html! { -
    - - // - // -
    - } -} \ No newline at end of file diff --git a/axiom-profiler-GUI/src/utils/usize_input.rs b/axiom-profiler-GUI/src/utils/usize_input.rs new file mode 100644 index 00000000..f9c3da88 --- /dev/null +++ b/axiom-profiler-GUI/src/utils/usize_input.rs @@ -0,0 +1,77 @@ +use wasm_bindgen::{JsCast, UnwrapThrowExt}; +use web_sys::HtmlInputElement; +use yew::prelude::*; + +#[derive(Properties, PartialEq)] +pub struct UsizeInputProps { + pub label: AttrValue, + pub placeholder: AttrValue, + pub set_value: Callback, +} + +#[function_component(UsizeInput)] +pub fn integer_input(props: &UsizeInputProps) -> Html { + let input_ref = use_node_ref(); + let set_value_to = { + let set_value = props.set_value.clone(); + move |input_event: Event| { + let target: HtmlInputElement = input_event + .target() + .unwrap_throw() + .dyn_into() + .unwrap_throw(); + if let Ok(value) = target.value().to_string().parse::() { + log::debug!("Setting the value to {}", value); + set_value.emit(value); + } + } + }; + + let set_value_on_enter = Callback::from({ + let set_value = set_value_to.clone(); + move |key_event: KeyboardEvent| { + if key_event.key() == "Enter" { + let event: Event = key_event.clone().into(); + set_value(event); + } + } + }); + + let set_value_on_blur = Callback::from({ + let set_value = set_value_to.clone(); + move |blur_event: FocusEvent| { + let event: Event = blur_event.clone().into(); + set_value(event); + } + }); + + // { + // // Whenever dependency changes, need to reset the state + // let dep = props.dependency; + // let input_value = input_value.clone(); + // let input_ref = input_ref.clone(); + // let default_value = props.default_value; + // use_effect_with_deps( + // { + // let input_value = input_value.clone(); + // move |_| { + // input_value.dispatch(InputAction::SetValueTo(default_value)); + // let input = input_ref + // .cast::() + // .expect("div_ref not attached to div element"); + // input.set_value(""); + // } + // }, + // dep, + // ); + // } + let placeholder = props.placeholder.to_string(); + + html! { + <> + + + + } +} + diff --git a/smt-log-parser/Cargo.toml b/smt-log-parser/Cargo.toml index 3a692c94..434f8a96 100644 --- a/smt-log-parser/Cargo.toml +++ b/smt-log-parser/Cargo.toml @@ -6,12 +6,9 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -regex = "1" futures = "0.3" serde = { version = "1.0.183", features = ["derive"] } -serde_json = "1.0.105" petgraph = "0.6.4" -implicit-clone = "0.4.1" wasm-timer = "0.2" semver = "1.0" typed-index-collections = { version = "3.1", features = ["serde"] } @@ -19,7 +16,6 @@ fxhash = "0.2" duplicate = "1.0" gloo-console = "0.3.0" roaring = "0.10" -itertools = "0.12.0" lasso = { version = "0.7", features = ["serialize"] } [dev-dependencies] diff --git a/smt-log-parser/src/display_with.rs b/smt-log-parser/src/display_with.rs index 03126700..a68ac7eb 100644 --- a/smt-log-parser/src/display_with.rs +++ b/smt-log-parser/src/display_with.rs @@ -255,9 +255,15 @@ impl<'a: 'b, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a Term ) -> fmt::Result { data.with_children(&self.child_ids, |data| { if ctxt.display_term_ids { - let namespace = &ctxt.parser.strings[self.id.namespace]; - let id = self.id.id.map(|id| (u32::from(id) - 1).to_string()).unwrap_or_default(); - write!(f, "[{namespace}#{id}]")?; + match self.id { + None => write!(f, "[synthetic]")?, + Some(id) => { + let namespace = &ctxt.parser.strings[id.namespace]; + let id = id.id.map(|id| (u32::from(id) - 1).to_string()).unwrap_or_default(); + write!(f, "[{namespace}#{id}]")? + } + } + } if let Some(meaning) = ctxt.parser.meaning(data.term) { write!(f, "{}", meaning.with_data(ctxt, data))?; @@ -283,6 +289,7 @@ impl<'a, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a TermKind } TermKind::ProofOrApp(poa) => write!(f, "{}", poa.with_data(ctxt, data)), TermKind::Quant(idx) => write!(f, "{}", ctxt.parser[*idx].with_data(ctxt, data)), + TermKind::GeneralizedPrimitive => write!(f, "_"), } } } diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs index 432c6830..60249ad4 100644 --- a/smt-log-parser/src/items.rs +++ b/smt-log-parser/src/items.rs @@ -45,22 +45,23 @@ idx!(ENodeIdx, "e{}"); idx!(MatchIdx, "m{}"); /// A Z3 term and associated data. -#[derive(Debug, Serialize, Deserialize)] +#[derive(Debug, Serialize, Deserialize,PartialEq, Eq, Hash, Clone)] pub struct Term { - pub id: TermId, + pub id: Option, pub kind: TermKind, // Reduces memory usage compared to a Vec pub child_ids: Box<[TermIdx]>, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Copy, PartialEq, Eq, Hash)] pub enum TermKind { Var(usize), ProofOrApp(ProofOrApp), Quant(QuantIdx), + GeneralizedPrimitive, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Copy, PartialEq, Eq, Hash)] pub struct ProofOrApp { pub is_proof: bool, pub name: IString, @@ -87,7 +88,7 @@ impl TermKind { } } -#[derive(Debug, Serialize, Deserialize, PartialEq, Eq)] +#[derive(Debug, Serialize, Deserialize, PartialEq, Eq, Clone, Copy, Hash)] pub struct Meaning { /// The theory in which the value should be interpreted (e.g. `bv`) pub theory: IString, @@ -331,7 +332,7 @@ impl fmt::Display for Fingerprint { } /// Represents an ID string of the form `name#id` or `name#`. -#[derive(Debug, Clone, Copy, Serialize, Deserialize, Default, Hash)] +#[derive(Debug, Clone, Copy, Serialize, Deserialize, Default, Hash, PartialEq, Eq)] pub struct TermId { pub namespace: IString, pub id: Option, diff --git a/smt-log-parser/src/main.rs b/smt-log-parser/src/main.rs index 0be68fe0..0b89d806 100644 --- a/smt-log-parser/src/main.rs +++ b/smt-log-parser/src/main.rs @@ -6,12 +6,7 @@ use wasm_timer::Instant; fn main() { let args: Vec = env::args().collect(); - let settings = get_settings(); - let filenames = if args.len() < 2 { - Cow::Owned(vec![settings.file]) - } else { - Cow::Borrowed(&args[1..]) - }; + let filenames = &args[1..]; for path in &*filenames { let path = std::path::Path::new(path); @@ -50,39 +45,3 @@ fn main() { // println!("Done, run took {} seconds.", elapsed_time.as_secs_f32()); } } - -/// Parsing settings. -#[derive(Default, Clone, Debug, Deserialize)] -pub struct Settings { - // not all settings currently work - /// Name of file to parse. - pub file: String, - /// Whether to consider terms with reused IDs as separate from previous terms with the same ID. Does not work yet. - pub reuses: bool, - /// Print contents of parser to standard output item by item. - pub verbose: bool, - /// Whether to print all text/json files (Dot and SVG will always be generated regardless of this setting) - pub save_all_data: bool, - /// Select a sort type (by line number, cost, depth, etc.) - /// Does not work yet. - /// ## TODO - /// Replace with an enum - pub sort_by: String, - /// Stop parsing after a certain amount of time. Does not work yet. - pub timeout: f32, - /// Parse only up to a certain number of lines. Does not work yet. - pub line_limit: usize, - // add settings for: - // - number of instantiations to display in final visualization. -} - -/// settings file -const SETTINGS: &str = "settings.json"; - -/// Read settings from `SETTINGS` json file, saving them to a `Settings` struct -pub fn get_settings() -> Settings { - std::fs::read_to_string(SETTINGS) - .ok() - .map(|s| serde_json::from_str(&s).unwrap()) - .unwrap_or_default() -} diff --git a/smt-log-parser/src/parsers/z3/inst_graph.rs b/smt-log-parser/src/parsers/z3/inst_graph.rs index 38491f2e..a4ef44fa 100644 --- a/smt-log-parser/src/parsers/z3/inst_graph.rs +++ b/smt-log-parser/src/parsers/z3/inst_graph.rs @@ -1,6 +1,5 @@ use fxhash::{FxHashSet, FxHashMap}; use gloo_console::log; -use itertools::Itertools; use petgraph::graph::NodeIndex; use petgraph::stable_graph::StableGraph; use petgraph::visit::{Bfs, IntoEdgeReferences, Topo, IntoEdges}; @@ -12,11 +11,13 @@ use petgraph::{ use petgraph::{Direction, Graph}; use roaring::bitmap::RoaringBitmap; use std::fmt; +use std::iter::zip; use typed_index_collections::TiVec; use crate::display_with::{DisplayCtxt, DisplayWithCtxt}; -use crate::items::{BlameKind, ENodeIdx, Fingerprint, InstIdx, MatchKind}; +use crate::items::{BlameKind, ENodeIdx, Fingerprint, InstIdx, MatchKind, Term, TermIdx, QuantIdx, TermKind}; +use super::terms::Terms; use super::z3parser::Z3Parser; const MIN_MATCHING_LOOP_LENGTH: usize = 3; @@ -140,6 +141,9 @@ pub struct InstGraph { cost_ranked_node_indices: Vec, branching_ranked_node_indices: Vec, tr_closure: Vec, + matching_loop_subgraph: Graph, + matching_loop_end_nodes: Vec, // these are sorted by maximal depth in descending order + generalized_terms: TiVec>>, } enum InstOrder { @@ -154,6 +158,30 @@ pub struct VisibleGraphInfo { pub edge_count_decreased: bool, } +impl Terms { + pub fn generalize(&mut self, t1: TermIdx, t2: TermIdx) -> TermIdx { + if t1 == t2 { + // if terms are equal, no need to generalize + t1 + } else if let TermKind::GeneralizedPrimitive = self[t1].kind { + // if t1 is already generalized, no need to generalize further + t1 + } else if let TermKind::GeneralizedPrimitive = self[t2].kind { + // if t2 is already generalized, no need to generalize further + t2 + } else if self.meaning(t1) == self.meaning(t2) && self[t1].kind == self[t2].kind { + // if neither term is generalized, check the meanings and kinds and recurse over children + let a = self[t1].child_ids.clone(); + let b = self[t2].child_ids.clone(); + let children = zip(Vec::from(a), Vec::from(b)).map(|(c1, c2)| self.generalize(c1, c2)).collect(); + self.new_synthetic_term(self[t1].kind, children, self.meaning(t1).copied()) + } else { + // if meanings or kinds don't match up, need to generalize + self.new_synthetic_term(crate::items::TermKind::GeneralizedPrimitive, vec![], None) + } + } +} + impl InstGraph { pub fn from(parser: &Z3Parser) -> Self { let mut inst_graph = Self::default(); @@ -427,7 +455,7 @@ impl InstGraph { // } // } - pub fn show_matching_loops(&mut self) { + pub fn search_matching_loops(&mut self) -> usize { let quants: FxHashSet<_> = self .orig_graph .node_weights() @@ -455,10 +483,126 @@ impl InstGraph { self.orig_graph[node].visible = true; } } + self.retain_visible_nodes_and_reconnect(); + self.matching_loop_subgraph = self.visible_graph.clone(); + // for displaying the nth longest matching loop later on, we want to compute the end nodes of all the matching loops + // and sort them by max-depth in descending order + Self::compute_longest_distances_from_roots(&mut self.matching_loop_subgraph); + // compute end-nodes of matching loops + self.matching_loop_end_nodes = self.matching_loop_subgraph + .node_indices() + // only keep end-points of matching loops, i.e., nodes without any children in the matching loop subgraph + .filter(|nx| self.matching_loop_subgraph.neighbors_directed(*nx, Outgoing).count() == 0) + .collect(); + // sort the matching loop end-nodes by the max-depth + self.matching_loop_end_nodes.sort_unstable_by(|node_a, node_b| { + let max_depth_node_a = self.matching_loop_subgraph.node_weight(*node_a).unwrap().max_depth; + let max_depth_node_b = self.matching_loop_subgraph.node_weight(*node_b).unwrap().max_depth; + if max_depth_node_a < max_depth_node_b { + std::cmp::Ordering::Greater + } else { + std::cmp::Ordering::Less + } + }); + // return the total number of potential matching loops + let nr_matching_loop_end_nodes = self.matching_loop_end_nodes.len(); + self.generalized_terms.resize(nr_matching_loop_end_nodes, None); + nr_matching_loop_end_nodes } - fn find_longest_paths(graph: &mut Graph) -> FxHashSet { - // traverse this subtree in topological order to compute longest distances from node + pub fn show_nth_matching_loop(&mut self, n: usize, p: &mut Z3Parser) -> Vec { + self.reset_visibility_to(false); + // relies on the fact that we have previously sorted self.matching_loop_end_nodes by max_depth in descending order in + // search_matching_loops + let end_node_of_nth_matching_loop = self.matching_loop_end_nodes.get(n); + if let Some(&node) = end_node_of_nth_matching_loop { + // start a reverse-DFS from node and mark all the nodes as visible along the way + // during the reverse-DFS collect information needed to compute the generalized terms later on + // we abstract the edges over the from- and to-quantifiers as well as the trigger, i.e., + // two edges (a,b) and (c,d) are the same abstract edge iff + // - a and c correspond to an instantiation of the same quantifier + // - and b and d correspond to an instantiation of the same quantifier + // - and b and d used the same trigger + let mut abstract_edge_blame_terms: FxHashMap<(QuantIdx, QuantIdx, TermIdx), Vec> = FxHashMap::default(); + let mut dfs = Dfs::new(petgraph::visit::Reversed(&self.matching_loop_subgraph), node); + while let Some(nx) = dfs.next(petgraph::visit::Reversed(&self.matching_loop_subgraph)) { + let orig_index = self.matching_loop_subgraph.node_weight(nx).unwrap().orig_graph_idx; + self.orig_graph[orig_index].visible = true; + // add all direct dependencies which have BlameKind::Term to the correct bin in abstract_edges + // such that later on we can generalize over each all edges in a matching loop that have + // identical from- and to-quantifiers + // (*) + // avoid unnecessary recomputation if we have already computed the generalized terms + if let None = &self.generalized_terms[n] { + log!(format!("Computation I for matching loop #{}", n)); + if let Some(to_quant) = self.matching_loop_subgraph.node_weight(nx).unwrap().mkind.quant_idx() { + for incoming_edge in self.matching_loop_subgraph.edges_directed(nx, Incoming) { + let from = incoming_edge.source(); + if let Some(from_quant) = self.matching_loop_subgraph.node_weight(from).unwrap().mkind.quant_idx() { + if let Some(blame_term) = incoming_edge.weight().blame_term_idx() { + let blame_term_idx = p[blame_term].owner; + if let Some(trigger) = self.matching_loop_subgraph.node_weight(nx).unwrap().mkind.pattern() { + if let Some(blame_terms) = abstract_edge_blame_terms.get_mut(&(from_quant, to_quant, trigger)) { + blame_terms.push(blame_term_idx); + } else { + abstract_edge_blame_terms.insert((from_quant, to_quant, trigger), vec![blame_term_idx]); + } + } + } + } + } + } + } + } + if let Some(generalized_terms) = &self.generalized_terms[n] { + // check if we have already computed the generalized terms for the n-th matching loop + generalized_terms.clone() + } else { + log!(format!("Computation II for matching loop #{}", n)); + // if not, compute the generalized terms for each bucket in abstract_edge_blame_terms + let mut generalized_terms: Vec = Vec::new(); + for blame_terms in abstract_edge_blame_terms.values() { + // let generalized_term = blame_terms.iter().reduce(|&t1, &t2| generalize(t1, t2, p)).unwrap(); + if let Some(t1) = blame_terms.get(0) { + let mut gen_term = *t1; + for &t2 in &blame_terms[1..] { + gen_term = p.terms.generalize(gen_term, t2); + // let ctxt = DisplayCtxt { + // parser: p, + // display_term_ids: false, + // display_quantifier_name: false, + // use_mathematical_symbols: true, + // }; + // log!(format!("Generalized term {} and {}", gen_term.with(&ctxt), t2.with(&ctxt))); + } + let ctxt = DisplayCtxt { + parser: p, + display_term_ids: false, + display_quantifier_name: false, + use_mathematical_symbols: true, + }; + let pretty_gen_term = gen_term.with(&ctxt).to_string(); + generalized_terms.push(pretty_gen_term); + } + } + self.generalized_terms[n] = Some(generalized_terms.clone()); + generalized_terms + } + // after generalizing over the terms for each abstract edge, store the key-value pair (n, MatchingLoopInfo) in the + // InstGraph such that we don't need to recompute the generalization => can check if the value is already in the map at (*) + } else { + Vec::new() + } + } + + pub fn show_matching_loop_subgraph(&mut self) { + self.reset_visibility_to(false); + for node in self.matching_loop_subgraph.node_weights() { + self.orig_graph[node.orig_graph_idx].visible = true; + } + } + + fn compute_longest_distances_from_roots(graph: &mut Graph) { let mut topo = Topo::new(&*graph); while let Some(nx) = topo.next(&*graph) { let parents = graph.neighbors_directed(nx, Incoming); @@ -471,20 +615,21 @@ impl InstGraph { graph[nx].max_depth = 0; } } - let furthest_away_nodes = graph + } + + fn find_longest_paths(graph: &mut Graph) -> FxHashSet { + // traverse this subtree in topological order to compute longest distances from root nodes + Self::compute_longest_distances_from_roots(graph); + let furthest_away_end_nodes = graph .node_indices() + // only want to keep end nodes of longest paths, i.e., nodes without any children + .filter(|nx| graph.neighbors_directed(*nx, Outgoing).count() == 0) // only want to show matching loops of length at least 3, hence only keep nodes with depth at least 2 - .filter(|nx| graph.node_weight(*nx).unwrap().max_depth >= MIN_MATCHING_LOOP_LENGTH - 1) - .max_set_by(|node_a, node_b| { - graph - .node_weight(*node_a) - .unwrap() - .max_depth - .cmp(&graph.node_weight(*node_b).unwrap().max_depth) - }); + .filter(|nx| graph.node_weight(*nx).unwrap().max_depth >= MIN_MATCHING_LOOP_LENGTH - 1) + .collect(); // backtrack longest paths from furthest away nodes in subgraph until we reach a root let mut matching_loop_nodes: FxHashSet = FxHashSet::default(); - let mut visitor: Vec = furthest_away_nodes; + let mut visitor: Vec = furthest_away_end_nodes; let mut visited: FxHashSet<_> = FxHashSet::default(); while let Some(curr) = visitor.pop() { matching_loop_nodes.insert(graph.node_weight(curr).unwrap().orig_graph_idx); diff --git a/smt-log-parser/src/parsers/z3/terms.rs b/smt-log-parser/src/parsers/z3/terms.rs index 357a064e..72cb3c95 100644 --- a/smt-log-parser/src/parsers/z3/terms.rs +++ b/smt-log-parser/src/parsers/z3/terms.rs @@ -3,14 +3,17 @@ use typed_index_collections::TiVec; use crate::{ Error, Result, - items::{Term, TermId, TermIdToIdxMap, TermIdx, StringTable, Meaning, QuantIdx} + items::{StringTable, Term, TermId, TermIdToIdxMap, TermIdx, TermKind, Meaning, QuantIdx} }; #[derive(Debug)] pub struct Terms { term_id_map: TermIdToIdxMap, terms: TiVec, - meanings: FxHashMap + meanings: FxHashMap, + parsed_terms: Option, + + synthetic_terms: FxHashMap<(Term, Option), TermIdx>, } impl Terms { @@ -19,13 +22,19 @@ impl Terms { term_id_map: TermIdToIdxMap::new(strings), terms: TiVec::new(), meanings: FxHashMap::default(), + parsed_terms: None, + + synthetic_terms: FxHashMap::default(), } } - pub(super) fn new_term(&mut self, id: TermId, term: Term) -> Result { + pub(super) fn new_term(&mut self, term: Term) -> Result { self.terms.raw.try_reserve(1)?; + let id = term.id; let idx = self.terms.push_and_get_key(term); - self.term_id_map.register_term(id, idx)?; + if let Some(id) = id { + self.term_id_map.register_term(id, idx)?; + } Ok(idx) } @@ -59,6 +68,26 @@ impl Terms { }; Ok(()) } + + pub(super) fn end_of_file(&mut self) { + self.parsed_terms = Some(self.terms.next_key()); + } + + pub(super) fn new_synthetic_term(&mut self, kind: TermKind, children: Vec, meaning: Option) -> TermIdx { + let term = Term { + id: None, + kind, + child_ids: children.into_boxed_slice(), + }; + let term = self.synthetic_terms.entry((term, meaning)); + *term.or_insert_with_key(|(term, meaning)| { + let term = self.terms.push_and_get_key(term.clone()); + if let Some(meaning) = meaning { + self.meanings.insert(term, *meaning); + } + term + }) + } } impl std::ops::Index for Terms { diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index b53f1ed7..64f3f548 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/smt-log-parser/src/parsers/z3/z3parser.rs @@ -217,11 +217,11 @@ impl Z3LogParser for Z3Parser { assert!(!child_ids.is_empty()); let qidx = self.quantifiers.next_key(); let term = Term { - id: full_id, + id: Some(full_id), kind: TermKind::Quant(qidx), child_ids, }; - let tidx = self.terms.new_term(full_id, term)?; + let tidx = self.terms.new_term(term)?; let q = Quantifier { num_vars, kind: quant_name, @@ -246,11 +246,11 @@ impl Z3LogParser for Z3Parser { // Return if there is unexpectedly more data Self::expect_completed(l)?; let term = Term { - id: full_id, + id: Some(full_id), kind, child_ids: Default::default(), }; - self.terms.new_term(full_id, term)?; + self.terms.new_term(term)?; Ok(()) } @@ -268,11 +268,11 @@ impl Z3LogParser for Z3Parser { // TODO: add rewrite, monotonicity cases let child_ids = self.gobble_children(l)?; let term = Term { - id: full_id, + id: Some(full_id), kind, child_ids, }; - self.terms.new_term(full_id, term)?; + self.terms.new_term(term)?; Ok(()) } @@ -525,6 +525,7 @@ impl Z3LogParser for Z3Parser { } fn eof(&mut self) { + self.terms.end_of_file(); // TODO: this shouldn't be done here. self.compute_costs(); } diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs index ddb6346a..ad0cf6cb 100644 --- a/smt-log-parser/tests/parse_logs.rs +++ b/smt-log-parser/tests/parse_logs.rs @@ -34,7 +34,7 @@ fn parse_all_logs() { // Some memory usage is still left over from previous loop iterations, so we'll need to subtract that. let start_mem = memory_stats::memory_stats().unwrap().physical_mem as u64; // TODO: optimize memory usage and reduce `max_mem`. - let max_mem = start_mem + 2 * file_size + 1024*1024*1024; + let max_mem = start_mem + 2 * file_size + 1024 * 1024 * 1024; let now = Instant::now(); parser.process_check_every(Duration::from_millis(100), |_, _| {