From 3b41519a3589ef74c7a8308a7d17ab36999da34a Mon Sep 17 00:00:00 2001 From: ojyrkinen Date: Sat, 22 Jun 2024 10:43:40 +0300 Subject: [PATCH] Bug fixes --- axiom-profiler-GUI/src/results/node_info.rs | 4 +-- axiom-profiler-GUI/src/results/svg_result.rs | 9 +++++- smt-log-parser/src/analysis/graph/raw.rs | 6 ++-- smt-log-parser/src/items.rs | 1 + smt-log-parser/src/parsers/z3/z3parser.rs | 29 ++++++++++++++++++-- 5 files changed, 41 insertions(+), 8 deletions(-) diff --git a/axiom-profiler-GUI/src/results/node_info.rs b/axiom-profiler-GUI/src/results/node_info.rs index aa4b091e..14c4aa4d 100644 --- a/axiom-profiler-GUI/src/results/node_info.rs +++ b/axiom-profiler-GUI/src/results/node_info.rs @@ -416,8 +416,8 @@ impl<'a, 'b> EdgeInfo<'a, 'b> { (!forward).then_some("Reverse ").unwrap_or_default() ), VisibleEdgeKind::Direct(_, EdgeKind::ProofStep) => "Proof Step".to_string(), - VisibleEdgeKind::Direct(_, EdgeKind::Decision(true)) => "Assign true".to_string(), - VisibleEdgeKind::Direct(_, EdgeKind::Decision(false)) => "Assign false".to_string(), + VisibleEdgeKind::Direct(_, EdgeKind::Decision { assigned_to, .. }) => format!("Assign {}", assigned_to), + // VisibleEdgeKind::Direct(_, EdgeKind::Decision(false)) => "Assign false".to_string(), VisibleEdgeKind::Direct(_, EdgeKind::BacktrackDecision) => "Backtrack".to_string(), VisibleEdgeKind::YieldBlame { trigger_term, .. } => { format!("Yield/Blame trigger #{trigger_term}") diff --git a/axiom-profiler-GUI/src/results/svg_result.rs b/axiom-profiler-GUI/src/results/svg_result.rs index e25b3be0..c3f3a06d 100644 --- a/axiom-profiler-GUI/src/results/svg_result.rs +++ b/axiom-profiler-GUI/src/results/svg_result.rs @@ -379,8 +379,15 @@ impl Component for SVGResult { } _ => "normal", }; + let label = match inst_graph.raw[fg[edge_data.target()].idx].kind() { + NodeKind::Decision(dec_idx) => { + let search_path = rc_parser.parser.borrow()[*dec_idx].search_path; + format!("label={}", search_path) + }, + _ => "".to_string(), + }; format!( - "id=edge_{} tooltip=\"{tooltip}\" style={style} class={class} arrowhead={arrowhead}", + "id=edge_{} tooltip=\"{tooltip}\" style={style} class={class} arrowhead={arrowhead} {label}", // For edges the `id` is the `VisibleEdgeIndex` from the VisibleGraph! edge_data.id().index(), ) diff --git a/smt-log-parser/src/analysis/graph/raw.rs b/smt-log-parser/src/analysis/graph/raw.rs index fa26822b..378d73fd 100644 --- a/smt-log-parser/src/analysis/graph/raw.rs +++ b/smt-log-parser/src/analysis/graph/raw.rs @@ -189,7 +189,7 @@ impl RawInstGraph { let current_lvl = dec.lvl; let pred_lvl = parser[idx].lvl; if let Some(prev_decision) = dec.prev_decision { - self_.add_edge(prev_decision, idx, EdgeKind::Decision(parser[prev_decision].assignment)); + self_.add_edge(prev_decision, idx, EdgeKind::Decision {assigned_to: parser[prev_decision].assignment }); // match current_lvl < pred_lvl { // true => self_.add_edge(prev_decision, idx, EdgeKind::BacktrackDecision), // false => self_.add_edge(prev_decision, idx, EdgeKind::Decision(parser[prev_decision].assignment)), @@ -517,7 +517,9 @@ pub enum EdgeKind { forward: bool, }, ProofStep, - Decision(bool), + Decision { + assigned_to: bool, + }, BacktrackDecision, } diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs index d9ad42b1..51260b7d 100644 --- a/smt-log-parser/src/items.rs +++ b/smt-log-parser/src/items.rs @@ -724,6 +724,7 @@ pub struct Decision { pub clause_propagations: Vec<(TermIdx, bool)>, pub prev_decision: Option, pub backtracked_from: Vec, + pub search_path: usize, } impl std::fmt::Display for Decision { diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index 86326da4..713d64ea 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/smt-log-parser/src/parsers/z3/z3parser.rs @@ -38,6 +38,7 @@ pub struct Z3Parser { current_cdcl_lvl: usize, current_decision: Option, detected_conflict: bool, + search_path: usize, pub strings: StringTable, } @@ -59,6 +60,7 @@ impl Default for Z3Parser { current_cdcl_lvl: 0, current_decision: None, detected_conflict: false, + search_path: 0, strings, } } @@ -686,6 +688,7 @@ impl Z3LogParser for Z3Parser { if let Some(prev_dec) = d.prev_decision { dec = prev_dec } else { + self.current_decision = None; break } } @@ -713,6 +716,7 @@ impl Z3LogParser for Z3Parser { clause_propagations: Default::default(), prev_decision: self.current_decision, backtracked_from: Default::default(), + search_path: self.search_path, }; self.decision_assigns.raw.try_reserve(1)?; let dec_idx = self.decision_assigns.push_and_get_key(dec.clone()); @@ -720,9 +724,27 @@ impl Z3LogParser for Z3Parser { log!(format!("Created {} with idx {}", dec, dec_idx)) }, "clause" => { - let current_dec = self.decision_assigns.get_mut(self.current_decision.unwrap()).unwrap(); - current_dec.clause_propagations.push((result, assignment)); - log!(format!("\t Updated dec idx {} to {}", self.current_decision.unwrap(), current_dec)) + // let current_dec = self.decision_assigns.get_mut(self.current_decision.unwrap()).unwrap(); + if let Some(current_dec_idx) = self.current_decision { + let current_dec = self.decision_assigns.get_mut(current_dec_idx).unwrap(); + current_dec.clause_propagations.push((result, assignment)); + log!(format!("\t Updated dec idx {} to {}", self.current_decision.unwrap(), current_dec)) + } + // } else { + // let dec = Decision { + // result, + // assignment, + // lvl: self.current_cdcl_lvl, + // results_in_conflict: false, + // clause_propagations: vec![(result, assignment)], + // prev_decision: None, + // backtracked_from: Default::default(), + // search_path: self.search_path, + // }; + // self.decision_assigns.raw.try_reserve(1)?; + // let dec_idx = self.decision_assigns.push_and_get_key(dec.clone()); + // self.current_decision = Some(dec_idx); + // } }, _ => () } @@ -732,6 +754,7 @@ impl Z3LogParser for Z3Parser { fn conflict<'a>(&mut self, mut _l: impl Iterator) -> Result<()> { self.detected_conflict = true; + self.search_path += 1; if let Some(dec) = self.current_decision { self.decision_assigns.get_mut(dec).unwrap().results_in_conflict = true; }