Skip to content

Commit

Permalink
Fixed crashing behaviour when interpreting qvar's
Browse files Browse the repository at this point in the history
  • Loading branch information
oskari1 committed Dec 12, 2023
1 parent 6d17902 commit 0356a26
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 10 deletions.
10 changes: 6 additions & 4 deletions axiom-profiler-GUI/src/results/graph/graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ use yew::prelude::*;
use yew::{function_component, html, use_node_ref, Html};
use petgraph::graph::NodeIndex;

const NODE_SHAPE: &str = "polygon";

#[derive(Properties, PartialEq, Default)]
pub struct GraphProps {
pub svg_text: AttrValue,
Expand Down Expand Up @@ -73,7 +75,7 @@ pub fn graph(props: &GraphProps) -> Html {
for i in 0..nodes.length() {
let node = nodes.item(i).unwrap();
let ellipse = node
.query_selector("ellipse")
.query_selector(NODE_SHAPE)
.expect("Failed to select ellipse")
.unwrap();
let _ = ellipse.set_attribute("stroke-width", "1");
Expand Down Expand Up @@ -106,7 +108,7 @@ pub fn graph(props: &GraphProps) -> Html {
// extract node_index from node to construct callback that emits it
let node = descendant_nodes.item(i).unwrap();
let ellipse = node
.query_selector("ellipse")
.query_selector(NODE_SHAPE)
.expect("Failed to select title element")
.unwrap();
let node_index = node.id().strip_prefix("node").unwrap().parse::<usize>().unwrap();
Expand Down Expand Up @@ -231,7 +233,7 @@ pub fn graph(props: &GraphProps) -> Html {
let node = nodes.item(i).unwrap();
let node_index = NodeIndex::new(node.id().strip_prefix("node").unwrap().parse::<usize>().unwrap());
let ellipse = node
.query_selector("ellipse")
.query_selector(NODE_SHAPE)
.expect("Failed to select ellipse")
.unwrap();
if selected_nodes.contains(&node_index) {
Expand All @@ -253,7 +255,7 @@ pub fn graph(props: &GraphProps) -> Html {
for i in 0..nodes.length() {
let node = nodes.item(i).unwrap();
let ellipse = node
.query_selector("ellipse")
.query_selector(NODE_SHAPE)
.expect("Failed to select ellipse")
.unwrap();
let _ = ellipse.set_attribute("stroke-width", "1");
Expand Down
18 changes: 13 additions & 5 deletions axiom-profiler-GUI/src/results/svg_result.rs
Original file line number Diff line number Diff line change
Expand Up @@ -188,16 +188,24 @@ impl Component for SVGResult {
}
),
&|_, (_, node_data)| {
format!("id={} label=\"{}\" style=filled shape=oval fillcolor=\"{}\" fontcolor=black gradientangle=90",
format!("id={} label=\"{}\" style=filled shape={} fillcolor=\"{}\" fontcolor=black gradientangle=90",
format!("node{}", node_data.orig_graph_idx.index()),
node_data.orig_graph_idx.index(),
// match (self.inst_graph.node_has_filtered_children(node_data.orig_graph_idx),
// self.inst_graph.node_has_filtered_parents(node_data.orig_graph_idx)) {
// (false, false) => format!("{}", self.colour_map.get(&node_data.quant_idx, 0.7)),
// (false, true) => format!("{}:{}", self.colour_map.get(&node_data.quant_idx, 1.0), self.colour_map.get(&node_data.quant_idx, 0.1)),
// (true, false) => format!("{}:{}", self.colour_map.get(&node_data.quant_idx, 0.1), self.colour_map.get(&node_data.quant_idx, 1.0)),
// (true, true) => format!("{}", self.colour_map.get(&node_data.quant_idx, 0.3)),
// },
match (self.inst_graph.node_has_filtered_children(node_data.orig_graph_idx),
self.inst_graph.node_has_filtered_parents(node_data.orig_graph_idx)) {
(false, false) => format!("{}", self.colour_map.get(&node_data.quant_idx, 0.7)),
(false, true) => format!("{}:{}", self.colour_map.get(&node_data.quant_idx, 1.0), self.colour_map.get(&node_data.quant_idx, 0.1)),
(true, false) => format!("{}:{}", self.colour_map.get(&node_data.quant_idx, 0.1), self.colour_map.get(&node_data.quant_idx, 1.0)),
(true, true) => format!("{}", self.colour_map.get(&node_data.quant_idx, 0.3)),
(false, false) => "box",
(false, true) => "house",
(true, false) => "invhouse",
(true, true) => "diamond",
},
self.colour_map.get(&node_data.quant_idx, 0.4),
)
},
)
Expand Down
8 changes: 7 additions & 1 deletion smt-log-parser/src/items.rs
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,13 @@ impl Term {
let kind = match self.kind {
TermKind::Var(qvar) if ctxt.quant.is_some() => {
match ctxt.quant.unwrap().vars.as_ref().unwrap() {
VarNames::NameAndType(vars) => vars[qvar].0.clone(),
VarNames::NameAndType(vars) => {
if let Some(var_name) = vars.get(qvar) {
var_name.0.clone()
} else {
format!("{}", self.kind)
}
},
_ => format!("{}", self.kind),
}
},
Expand Down

0 comments on commit 0356a26

Please sign in to comment.