Improved node info in CDCL graph

viperproject · Jun 23, 2024 · 6e5deaf · 6e5deaf
1 parent 3b41519
commit 6e5deaf
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 4 deletions.
diff --git a/axiom-profiler-GUI/src/results/node_info.rs b/axiom-profiler-GUI/src/results/node_info.rs
@@ -214,7 +214,8 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
         Some(
             dec.clause_propagations
                 .iter()
-                .map(|(cl, val)| format!("{} → {}", cl.with(self.ctxt), val))
+                // .map(|(cl, val)| format!("{} → {}", cl.with(self.ctxt), val))
+                .map(|prop| format!("{} → {} on path {}", prop.clause.with(self.ctxt), prop.value, prop.search_path))
                 .collect(),
         )
     }

diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs
@@ -721,15 +721,26 @@ pub struct Decision {
     pub assignment: bool,
     pub lvl: usize,
     pub results_in_conflict: bool,
-    pub clause_propagations: Vec<(TermIdx, bool)>,
+    // pub clause_propagations: Vec<(TermIdx, bool)>,
+    pub clause_propagations: Vec<Propagation>,
     pub prev_decision: Option<DecisionIdx>,
     pub backtracked_from: Vec<DecisionIdx>,
     pub search_path: usize,
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone)]
+pub struct Propagation {
+    pub clause: TermIdx,
+    pub value: bool,
+    pub search_path: usize,
+}
+
 impl std::fmt::Display for Decision {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        let propagations = self.clause_propagations.iter().map(|(tidx, val)| format!("{} to {}", val, tidx.0)).collect::<Vec<String>>().join(", ");
+        // let propagations = self.clause_propagations.iter().map(|(tidx, val)| format!("{} to {}", val, tidx.0)).collect::<Vec<String>>().join(", ");
+        let propagations = self.clause_propagations.iter().map(|propagation| format!("{} to {} on path {}", propagation.value, propagation.clause.0, propagation.search_path)).collect::<Vec<String>>().join(", ");
         let prev_decision = if let Some(prev_decision) = self.prev_decision { format!("{}", prev_decision.0) } else { "".to_string() }; 
         match self.assignment {
             true => write!(f, "[assign] {} decision axiom at lvl {}, propagating values {} with prev dec {}", self.result.0, self.lvl, propagations, prev_decision),

diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
@@ -727,7 +727,8 @@ impl Z3LogParser for Z3Parser {
                 // 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));
+                    // current_dec.clause_propagations.push((result, assignment));
+                    current_dec.clause_propagations.push(Propagation { clause: result, value: assignment, search_path: self.search_path });
                     log!(format!("\t Updated dec idx {} to {}", self.current_decision.unwrap(), current_dec))
                 }
                 // } else {