Fix remaining issues

smt-log-parser/src/items/cdcl.rs

@@ -16,10 +16,19 @@ pub struct Cdcl {
 }
 
 impl Cdcl {
+    /// Creates the `Root` node of the CDCL tree. Should only be used once.
+    pub fn root(frame: StackIdx) -> Self {
+        Self {
+            kind: CdclKind::Root,
+            frame,
+            propagates: Vec::new(),
+        }
+    }
+
     /// Creates a `Empty` node in the CDCL tree.
-    pub fn new_empty(frame: StackIdx) -> Self {
+    pub fn new_empty(parent: CdclIdx, frame: StackIdx) -> Self {
         Self {
-            kind: CdclKind::Empty,
+            kind: CdclKind::Empty(parent),
             frame,
             propagates: Vec::new(),
         }
@@ -54,9 +63,12 @@ impl Cdcl {
 #[derive(Debug, Clone)]
 pub enum CdclKind {
     /// Represents an empty node. Used as the root of the CDCL tree (in which
-    /// the solver may already propagate some facts) and when assignments are
-    /// propagated at a higher stack frame than the current decision.
-    Empty,
+    /// the solver may already propagate some facts).
+    Root,
+    /// Same as `Root` but used when assignments are propagated at a different
+    /// stack frame than the current decision. The frame of the current decision
+    /// may have been popped, thus this points to where it should be slotted in.
+    Empty(CdclIdx),
     /// The branching decision z3 took, it "arbitrarily" decided that this
     /// clause has this boolean value.
     Decision(Assignment),

smt-log-parser/src/items/stack.rs

@@ -85,6 +85,10 @@ impl TimeRangeStatus {
     pub fn is_ended(self) -> bool {
         matches!(self, Self::Ended)
     }
+
+    pub fn is_active_or_global(self) -> bool {
+        matches!(self, Self::Active | Self::Global)
+    }
 }
 
 impl fmt::Display for TimeRange {

smt-log-parser/src/parsers/z3/stack.rs

@@ -117,7 +117,7 @@ pub struct CdclTree {
 impl Default for CdclTree {
     fn default() -> Self {
         let mut cdcl = TiVec::default();
-        cdcl.push(Cdcl::new_empty(Stack::ZERO_FRAME));
+        cdcl.push(Cdcl::root(Stack::ZERO_FRAME));
         Self {
             cdcl,
             conflict: None,
@@ -128,7 +128,8 @@ impl Default for CdclTree {
 impl CdclTree {
     pub fn new_decision(&mut self, assign: Assignment, frame: StackIdx) -> Result<CdclIdx> {
         debug_assert!(self.conflict.is_none());
-        debug_assert!(!self.cdcl.last().is_some_and(|cdcl| cdcl.frame == frame));
+        // Not always true:
+        // debug_assert_ne!(self.cdcl.last().unwrap().frame, frame, "{:?}", self.cdcl.last().unwrap());
 
         let cdcl = Cdcl::new_decision(assign, frame);
         self.cdcl.raw.try_reserve(1)?;
@@ -142,11 +143,7 @@ impl CdclTree {
     }
 
     pub fn backtrack(&mut self, stack: &Stack) -> Result<CdclIdx> {
-        let active = |i: &CdclIdx| {
-            let status = stack[self[*i].frame].active.status();
-            status.is_active() || status.is_global()
-        };
-        let backtrack = self.curr_to_root().find(active).unwrap();
+        let backtrack = self.last_active(stack);
         // Not always true:
         // debug_assert_eq!(self[backtrack].frame, stack.active_frame());
 
@@ -157,11 +154,13 @@ impl CdclTree {
         Ok(self.cdcl.push_and_get_key(cdcl))
     }
 
-    pub fn new_propagate(&mut self, assign: Assignment, frame: StackIdx) -> Result<()> {
+    pub fn new_propagate(&mut self, assign: Assignment, stack: &Stack) -> Result<()> {
         debug_assert!(self.conflict.is_none());
+        let frame = stack.active_frame();
         let mut last = self.cdcl.last_mut().unwrap();
         if last.frame != frame {
-            let empty = Cdcl::new_empty(frame);
+            let parent = self.last_active(stack);
+            let empty = Cdcl::new_empty(parent, frame);
             self.cdcl.raw.try_reserve(1)?;
             let new = self.cdcl.push_and_get_key(empty);
             last = &mut self.cdcl[new];
@@ -175,6 +174,11 @@ impl CdclTree {
         self.conflict.is_some()
     }
 
+    fn last_active(&self, stack: &Stack) -> CdclIdx {
+        let active = |i: &CdclIdx| stack[self[*i].frame].active.status().is_active_or_global();
+        self.curr_to_root().find(active).unwrap()
+    }
+
     fn curr_to_root(&self) -> impl Iterator<Item = CdclIdx> + '_ {
         let mut curr = self.cdcl.last_key();
         core::iter::from_fn(move || {

smt-log-parser/src/parsers/z3/z3parser.rs

@@ -880,8 +880,7 @@ impl Z3LogParser for Z3Parser {
                     .ok_or(E::UnexpectedNewline)?;
                 debug_assert_eq!(assign.value, value);
 
-                let frame = self.stack.active_frame();
-                self.cdcl.new_propagate(assign, frame)?;
+                self.cdcl.new_propagate(assign, &self.stack)?;
                 Ok(())
             }
             "justification" => {
@@ -940,11 +939,11 @@ impl Z3LogParser for Z3Parser {
         // Return if there is unexpectedly more data
         Self::expect_completed(l)?;
 
-        let from_cdcl = matches!(self.comm.prev().last_line_kind, LineKind::Conflict);
-        debug_assert_eq!(from_cdcl, self.cdcl.has_conflict());
-        let from_cdcl = self.stack.pop_frames(num, scope, from_cdcl)?;
+        let conflict = matches!(self.comm.prev().last_line_kind, LineKind::Conflict);
+        debug_assert_eq!(conflict, self.cdcl.has_conflict());
+        let from_cdcl = self.stack.pop_frames(num, scope, conflict)?;
         self.events.new_pop(num, from_cdcl)?;
-        if from_cdcl {
+        if conflict {
             self.cdcl.backtrack(&self.stack)?;
         }
         Ok(())

smt-log-parser/tests/parse_logs.rs

@@ -68,12 +68,9 @@ fn parse_all_logs() {
             let elapsed = now.elapsed();
             let mut parser = parser.take_parser();
 
-            max_parse_ovhd = f64::max(
-                max_parse_ovhd,
-                (ALLOCATOR.allocated() as u64 - start_alloc) as f64 / parse_bytes as f64,
-            );
             let parse_bytes_kb = parse_bytes / 1024;
             let mem_size = parser.mem_size(SizeFlags::default());
+            max_parse_ovhd = f64::max(max_parse_ovhd, mem_size as f64 / parse_bytes as f64);
             println!(
                 "Finished parsing in {elapsed:?} ({} kB/ms). Memory use {} MB / {} MB (real {} MB):",
                 parse_bytes_kb / elapsed.as_millis() as u64,
@@ -84,8 +81,8 @@ fn parse_all_logs() {
             parser.mem_dbg(DbgFlags::default()).ok();
             // TODO: decrease this
             assert!(
-                mem_size as u64 <= parse_bytes * 3 / 2,
-                "Parser takes up more memory than 3/2 * file size!"
+                mem_size as u64 <= parse_bytes * 2,
+                "Parser takes up more memory than 2 * file size!"
             );
 
             let middle_alloc = ALLOCATOR.allocated() as u64;
@@ -115,11 +112,8 @@ fn parse_all_logs() {
             let elapsed_ml = now.elapsed();
             let elapsed = elapsed_ig + elapsed_ml;
 
-            max_analysis_ovhd = f64::max(
-                max_analysis_ovhd,
-                (ALLOCATOR.allocated() as u64 - middle_alloc) as f64 / parse_bytes as f64,
-            );
             let mem_size = inst_graph.mem_size(SizeFlags::default());
+            max_analysis_ovhd = f64::max(max_analysis_ovhd, mem_size as f64 / parse_bytes as f64);
             let (sure_mls, maybe_mls) = inst_graph.found_matching_loops().unwrap();
             println!(
                 "Finished analysis in {elapsed:?} ({} kB/ms). {} nodes, {sure_mls}+{maybe_mls} mls. Memory use {} MB / {} MB:",