Skip to content

Commit

Permalink
Bug fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@oskari1
oskari1 committed Jun 22, 2024
1 parent a0d9538 commit 3b41519
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 8 deletions.
4 changes: 2 additions & 2 deletions axiom-profiler-GUI/src/results/node_info.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}")
Expand Down
9 changes: 8 additions & 1 deletion axiom-profiler-GUI/src/results/svg_result.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
)
Expand Down
6 changes: 4 additions & 2 deletions smt-log-parser/src/analysis/graph/raw.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)),
Expand Down Expand Up @@ -517,7 +517,9 @@ pub enum EdgeKind {
forward: bool,
},
ProofStep,
Decision(bool),
Decision {
assigned_to: bool,
},
BacktrackDecision,
}

Expand Down
1 change: 1 addition & 0 deletions smt-log-parser/src/items.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -724,6 +724,7 @@ pub struct Decision {
pub clause_propagations: Vec<(TermIdx, bool)>,
pub prev_decision: Option<DecisionIdx>,
pub backtracked_from: Vec<DecisionIdx>,
pub search_path: usize,
}

impl std::fmt::Display for Decision {
Expand Down
29 changes: 26 additions & 3 deletions smt-log-parser/src/parsers/z3/z3parser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ pub struct Z3Parser {
current_cdcl_lvl: usize,
current_decision: Option<DecisionIdx>,
detected_conflict: bool,
search_path: usize,

pub strings: StringTable,
}
Expand All @@ -59,6 +60,7 @@ impl Default for Z3Parser {
current_cdcl_lvl: 0,
current_decision: None,
detected_conflict: false,
search_path: 0,
strings,
}
}
Expand Down Expand Up @@ -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
}
}
Expand Down Expand Up @@ -713,16 +716,35 @@ 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());
self.current_decision = Some(dec_idx);
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);
// }
},
_ => ()
}
Expand All @@ -732,6 +754,7 @@ impl Z3LogParser for Z3Parser {

fn conflict<'a>(&mut self, mut _l: impl Iterator<Item = &'a str>) -> 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;
}
Expand Down

0 comments on commit 3b41519

Please sign in to comment.