From 44f3e858d286aa5641077dab14a078dc9d2b158f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Fri, 15 Nov 2024 15:38:16 +0100
Subject: [PATCH] Update mem_dbg and fix related bugs

---
 axiom-profiler-GUI/Cargo.toml                 |   2 +-
 smt-log-parser/Cargo.toml                     |   2 +-
 smt-log-parser/src/analysis/dependencies.rs   |   2 +-
 .../graph/analysis/matching_loop/mod.rs       |   4 +-
 .../graph/analysis/matching_loop/node.rs      |   5 +
 .../graph/analysis/matching_loop/search.rs    |   2 +-
 .../graph/analysis/matching_loop/signature.rs |   3 +-
 smt-log-parser/src/analysis/graph/raw.rs      |  11 +-
 smt-log-parser/src/analysis/graph/visible.rs  |   2 +-
 smt-log-parser/src/display_with.rs            |   8 +-
 smt-log-parser/src/items/enode.rs             |   3 +-
 smt-log-parser/src/items/equality.rs          |   2 +
 smt-log-parser/src/items/idx.rs               |   1 +
 smt-log-parser/src/items/inst.rs              |   5 +-
 smt-log-parser/src/items/proof.rs             |   1 +
 smt-log-parser/src/items/stack.rs             |   2 +
 smt-log-parser/src/items/term.rs              |   2 +
 smt-log-parser/src/lib.rs                     |   4 +-
 smt-log-parser/src/mem_dbg/impl.rs            | 103 +++++++++---------
 smt-log-parser/src/mem_dbg/mod.rs             |  21 ++++
 smt-log-parser/src/mem_dbg/utils.rs           |   4 +
 smt-log-parser/src/parsers/z3/egraph.rs       |   2 +-
 smt-log-parser/src/parsers/z3/inter_line.rs   |   3 +
 smt-log-parser/src/parsers/z3/stm2.rs         |   2 +
 smt-log-parser/src/parsers/z3/synthetic.rs    |   2 +
 25 files changed, 130 insertions(+), 68 deletions(-)

diff --git a/axiom-profiler-GUI/Cargo.toml b/axiom-profiler-GUI/Cargo.toml
index a5917db1..6ab98726 100644
--- a/axiom-profiler-GUI/Cargo.toml
+++ b/axiom-profiler-GUI/Cargo.toml
@@ -39,7 +39,7 @@ wasm-timer = "0.2"
 gloo-timers = { version = "0.3.0", features = ["futures"] }
 semver = "1.0"
 nucleo-matcher = "0.3.1"
-mem_dbg = { version = "0.1.8", features = ["std", "derive"], default-features = false }
+mem_dbg = { version = "0.2.4", features = ["std", "derive"], default-features = false }
 duplicate = "1.0"
 
 # For random colour generation
diff --git a/smt-log-parser/Cargo.toml b/smt-log-parser/Cargo.toml
index 398a14b6..c5515046 100644
--- a/smt-log-parser/Cargo.toml
+++ b/smt-log-parser/Cargo.toml
@@ -18,7 +18,7 @@ num = "0.4"
 futures = "0.3"
 semver = "1.0"
 wasm-timer = "0.2"
-mem_dbg = { version = "0.1.8", features = ["std", "derive"], default-features = false, optional = true }
+mem_dbg = { version = "0.2.4", features = ["std", "derive"], default-features = false, optional = true }
 # Analysis
 petgraph = "0.6.4"
 roaring = "0.10"
diff --git a/smt-log-parser/src/analysis/dependencies.rs b/smt-log-parser/src/analysis/dependencies.rs
index 9956ba0c..fd4b4dee 100644
--- a/smt-log-parser/src/analysis/dependencies.rs
+++ b/smt-log-parser/src/analysis/dependencies.rs
@@ -45,7 +45,7 @@ impl QuantifierAnalysis {
             let qinfo = &mut self_.0[qidx];
             let ginst = &inst_graph.raw[iidx];
             qinfo.costs += ginst.cost;
-            for &parent_iidx in &ginst.inst_parents.nodes {
+            for &parent_iidx in ginst.inst_parents.nodes.iter() {
                 let parent_inst = &parser.insts[parent_iidx];
                 let parent_match_ = &parser.insts[parent_inst.match_];
                 let Some(parent_qidx) = parent_match_.kind.quant_idx() else {
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
index 3d04ddc8..5115f4b2 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
@@ -11,7 +11,7 @@ pub use signature::*;
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
-use crate::{idx, items::InstIdx, Graph, TiVec};
+use crate::{idx, items::InstIdx, BoxSlice, Graph, TiVec};
 
 pub const MIN_MATCHING_LOOP_LENGTH: u32 = 6;
 
@@ -29,7 +29,7 @@ pub struct MlData {
 pub struct MatchingLoop {
     pub sig: MlSigIdx,
     pub leaves: MlLeaves,
-    pub members: Box<[InstIdx]>,
+    pub members: BoxSlice<InstIdx>,
     pub graph: Option<(GenIdx, Option<MlExplanation>)>,
 }
 pub type MlExplanation = Graph<MLGraphNode, MLGraphEdge>;
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
index f46a7a96..5f171f23 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
@@ -2,6 +2,10 @@ use crate::{items::TermIdx, parsers::z3::synthetic::SynthIdx};
 
 use super::MlSignature;
 
+#[cfg(feature = "mem_dbg")]
+use mem_dbg::{MemDbg, MemSize};
+
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Eq, Hash, PartialEq)]
 pub enum MLGraphNode {
     QI(MlSignature),
@@ -11,6 +15,7 @@ pub enum MLGraphNode {
     RecurringEquality(SynthIdx, SynthIdx, Option<bool>),
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Eq, Hash, PartialEq)]
 pub enum MLGraphEdge {
     Blame(usize),
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
index d5653f3e..5cdac3e8 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
@@ -40,7 +40,7 @@ impl InstGraph {
         let mls = ml_data.matching_loops.len();
         for (i, ml) in ml_data.matching_loops.iter().enumerate() {
             let mut last = None;
-            for &member in &ml.members {
+            for &member in ml.members.iter() {
                 self.raw[member].part_of_ml.insert(i);
                 if let Some(last) = last.replace(member) {
                     for between in MlOutput::others_between(&topo, member, last) {
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
index b582e464..41746d52 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
@@ -26,7 +26,8 @@ pub struct MlSignature {
 /// Instantiation chains which all depend on a single term will have the same
 /// `InstParent`.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub enum InstParent {
     Quant(QuantIdx),
     Const(ENodeIdx),
diff --git a/smt-log-parser/src/analysis/graph/raw.rs b/smt-log-parser/src/analysis/graph/raw.rs
index f9d634b5..fbdb9381 100644
--- a/smt-log-parser/src/analysis/graph/raw.rs
+++ b/smt-log-parser/src/analysis/graph/raw.rs
@@ -3,7 +3,6 @@ use std::{
     ops::{Index, IndexMut},
 };
 
-use fxhash::FxHashSet;
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 use petgraph::{
@@ -18,7 +17,7 @@ use crate::{
         ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx, StackIdx,
         TransitiveExplSegmentKind,
     },
-    DiGraph, FxHashMap, NonMaxU32, Result, Z3Parser,
+    DiGraph, FxHashMap, FxHashSet, NonMaxU32, Result, Z3Parser,
 };
 
 graph_idx!(raw_idx, RawNodeIndex, RawEdgeIndex, RawIx);
@@ -250,6 +249,7 @@ impl GraphStats {
     }
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone)]
 pub struct Node {
     state: NodeState,
@@ -260,9 +260,10 @@ pub struct Node {
     kind: NodeKind,
     pub inst_parents: NextInsts,
     pub inst_children: NextInsts,
-    pub part_of_ml: fxhash::FxHashSet<usize>,
+    pub part_of_ml: FxHashSet<usize>,
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum NodeState {
     Disabled,
@@ -270,6 +271,7 @@ pub enum NodeState {
     Visible,
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Copy, Default)]
 pub struct Depth {
     /// What is the shortest path to a root/leaf
@@ -278,6 +280,7 @@ pub struct Depth {
     pub max: u32,
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Default)]
 pub struct NextInsts {
     /// What are the immediate next instantiation nodes
@@ -327,6 +330,7 @@ impl Node {
     }
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Copy)]
 pub enum NodeKind {
     /// Corresponds to `ENodeIdx`.
@@ -401,6 +405,7 @@ impl NodeKind {
     }
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Clone, Copy)]
 pub enum EdgeKind {
     /// Instantiation -> ENode
diff --git a/smt-log-parser/src/analysis/graph/visible.rs b/smt-log-parser/src/analysis/graph/visible.rs
index 5e0060a5..f2077af9 100644
--- a/smt-log-parser/src/analysis/graph/visible.rs
+++ b/smt-log-parser/src/analysis/graph/visible.rs
@@ -180,7 +180,7 @@ impl InstGraph {
             if from == NodeIndex::end() {
                 continue;
             }
-            for &next_inst in &node.inst_children.nodes {
+            for &next_inst in node.inst_children.nodes.iter() {
                 let next_inst = next_inst.index(&self.raw);
                 let to = node_index_map[next_inst.0.index()];
                 if to == NodeIndex::end() {
diff --git a/smt-log-parser/src/display_with.rs b/smt-log-parser/src/display_with.rs
index 21289af4..10fca4ff 100644
--- a/smt-log-parser/src/display_with.rs
+++ b/smt-log-parser/src/display_with.rs
@@ -166,6 +166,12 @@ impl DisplayConfiguration {
         #[cfg(not(feature = "display_html"))]
         return false;
     }
+    pub fn font_tag(&self) -> bool {
+        #[cfg(feature = "display_html")]
+        return self.font_tag;
+        #[cfg(not(feature = "display_html"))]
+        return false;
+    }
 
     pub fn with_html_italic(
         &self,
@@ -180,7 +186,7 @@ impl DisplayConfiguration {
         colour: &str,
         rest: impl FnMut(&mut fmt::Formatter<'_>) -> fmt::Result,
     ) -> fmt::Result {
-        let (tag, attribute) = if self.font_tag {
+        let (tag, attribute) = if self.font_tag() {
             ("font", format!("color=\"{colour}\""))
         } else {
             ("span", format!("style=\"color:{colour}\""))
diff --git a/smt-log-parser/src/items/enode.rs b/smt-log-parser/src/items/enode.rs
index 5af78a35..7924a1b2 100644
--- a/smt-log-parser/src/items/enode.rs
+++ b/smt-log-parser/src/items/enode.rs
@@ -22,7 +22,8 @@ pub struct ENode {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[derive(Debug)]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
+#[derive(Debug, Clone, Copy)]
 pub struct Equality {
     pub(crate) _frame: StackIdx,
     pub to: ENodeIdx,
diff --git a/smt-log-parser/src/items/equality.rs b/smt-log-parser/src/items/equality.rs
index 0cf4c67e..0a2fe71c 100644
--- a/smt-log-parser/src/items/equality.rs
+++ b/smt-log-parser/src/items/equality.rs
@@ -159,6 +159,7 @@ impl TransitiveExpl {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy)]
 pub struct TransitiveExplSegment {
@@ -182,6 +183,7 @@ impl TransitiveExplSegment {
 pub type EqGivenUse = (EqGivenIdx, Option<NonMaxU32>);
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy)]
 pub enum TransitiveExplSegmentKind {
diff --git a/smt-log-parser/src/items/idx.rs b/smt-log-parser/src/items/idx.rs
index db6c91b4..66551c6f 100644
--- a/smt-log-parser/src/items/idx.rs
+++ b/smt-log-parser/src/items/idx.rs
@@ -5,6 +5,7 @@ use mem_dbg::{MemDbg, MemSize};
 macro_rules! idx {
     ($struct:ident, $prefix:tt) => {
         #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+        #[cfg_attr(feature = "mem_dbg", copy_type)]
         #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
         #[derive(Clone, Copy, Eq, PartialEq, PartialOrd, Ord, Hash)]
         // Note: we use `u32` since this the file would need to be > ~100GB to
diff --git a/smt-log-parser/src/items/inst.rs b/smt-log-parser/src/items/inst.rs
index 51a7785f..0feb3b90 100644
--- a/smt-log-parser/src/items/inst.rs
+++ b/smt-log-parser/src/items/inst.rs
@@ -120,8 +120,9 @@ impl MatchKind {
 /// - Term: one instantiation produced a term that the other triggered on
 /// - Equality: dependency based on an equality.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Copy)]
 pub enum BlameKind {
     Term { term: ENodeIdx },
     Equality { eq: EqTransIdx },
@@ -170,6 +171,7 @@ impl Index<usize> for Blame<'_> {
 /// An identifier for a Z3 quantifier instantiation (called "fingerprint" in the original Axiom Profiler).
 /// Represented as a 16-digit hexadecimal number in log files.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct Fingerprint(pub u64);
@@ -213,6 +215,7 @@ pub struct Instantiation {
 
 /// A Z3 instantiation.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy)]
 pub enum InstProofLink {
diff --git a/smt-log-parser/src/items/proof.rs b/smt-log-parser/src/items/proof.rs
index 34cc6c67..f38ca272 100644
--- a/smt-log-parser/src/items/proof.rs
+++ b/smt-log-parser/src/items/proof.rs
@@ -21,6 +21,7 @@ pub struct ProofStep {
 
 #[allow(non_camel_case_types)]
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy, EnumIter)]
 /// Taken from
diff --git a/smt-log-parser/src/items/stack.rs b/smt-log-parser/src/items/stack.rs
index 91ef6eec..46a8972b 100644
--- a/smt-log-parser/src/items/stack.rs
+++ b/smt-log-parser/src/items/stack.rs
@@ -4,6 +4,7 @@ use core::fmt;
 use mem_dbg::{MemDbg, MemSize};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Clone, Copy)]
 pub struct StackFrame {
     /// Is this frame definitely from CDCL? If this is false then it may still
@@ -26,6 +27,7 @@ impl StackFrame {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
 pub struct TimeRange {
     start: u32,
diff --git a/smt-log-parser/src/items/term.rs b/smt-log-parser/src/items/term.rs
index 74a41347..ac0f1a9f 100644
--- a/smt-log-parser/src/items/term.rs
+++ b/smt-log-parser/src/items/term.rs
@@ -18,6 +18,7 @@ pub struct Term {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 #[repr(u8)]
@@ -135,6 +136,7 @@ impl VarNames {
 
 /// Represents an ID string of the form `name#id` or `name#`.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy, Default, Hash, PartialEq, Eq)]
 pub struct TermId {
diff --git a/smt-log-parser/src/lib.rs b/smt-log-parser/src/lib.rs
index 0c4d394f..3adc92b0 100644
--- a/smt-log-parser/src/lib.rs
+++ b/smt-log-parser/src/lib.rs
@@ -18,8 +18,8 @@ mod mem_dbg;
 
 pub use error::{Error, FResult, FatalError, Result};
 pub use mem_dbg::{
-    BigRational, BoxSlice, DiGraph, FxHashMap, Graph, IString, NonMaxU32, NonMaxUsize, StringTable,
-    TiVec, UnGraph,
+    BigRational, BoxSlice, DiGraph, FxHashMap, FxHashSet, Graph, IString, NonMaxU32, NonMaxUsize,
+    StringTable, TiVec, UnGraph,
 };
 pub use parsers::z3::z3parser::Z3Parser;
 pub use parsers::LogParser;
diff --git a/smt-log-parser/src/mem_dbg/impl.rs b/smt-log-parser/src/mem_dbg/impl.rs
index d2325977..738e3f40 100644
--- a/smt-log-parser/src/mem_dbg/impl.rs
+++ b/smt-log-parser/src/mem_dbg/impl.rs
@@ -9,7 +9,8 @@ use crate::analysis::subgraph::TransitiveClosure;
 use crate::parsers::z3::VersionInfo;
 
 use super::{
-    BigRational, BoxSlice, FxHashMap, Graph, IString, NonMaxU32, NonMaxUsize, StringTable, TiVec,
+    BigRational, FxHashMap, FxHashSet, Graph, IString, NonMaxU32, NonMaxUsize,
+    StringTable, TiVec,
 };
 
 macro_rules! copy_impl {
@@ -35,16 +36,12 @@ copy_impl!(IString);
 impl MemDbgImpl for BigRational {}
 
 impl MemSize for BigRational {
-    fn mem_size(&self, flags: mem_dbg::SizeFlags) -> usize {
-        if flags.contains(mem_dbg::SizeFlags::FOLLOW_REFS) {
-            let numer = self.numer();
-            let denom = self.denom();
-            core::mem::size_of::<Self>()
-                + numer.iter_u64_digits().len() * core::mem::size_of::<u64>()
-                + denom.iter_u64_digits().len() * core::mem::size_of::<u64>()
-        } else {
-            core::mem::size_of::<Self>()
-        }
+    fn mem_size(&self, _flags: mem_dbg::SizeFlags) -> usize {
+        let numer = self.numer();
+        let denom = self.denom();
+        core::mem::size_of::<Self>()
+            + numer.iter_u64_digits().len() * core::mem::size_of::<u64>()
+            + denom.iter_u64_digits().len() * core::mem::size_of::<u64>()
     }
 }
 
@@ -116,6 +113,15 @@ impl<K: MemSize, V: MemSize> MemSize for FxHashMap<K, V> {
     }
 }
 
+// FxHashSet
+
+impl<K: MemSize> MemDbgImpl for FxHashSet<K> {}
+impl<K: MemSize> MemSize for FxHashSet<K> {
+    fn mem_size(&self, flags: mem_dbg::SizeFlags) -> usize {
+        core::mem::size_of::<Self>() + self.0.iter().map(|k| k.mem_size(flags)).sum::<usize>()
+    }
+}
+
 // StringTable
 
 impl MemDbgImpl for StringTable {}
@@ -154,17 +160,44 @@ impl CopyType for TransitiveClosure {
 
 // Graph
 
-impl<N, E, Ty: EdgeType, Ix: IndexType> MemDbgImpl for Graph<N, E, Ty, Ix> {}
-impl<N, E, Ty: EdgeType, Ix: IndexType> MemSize for Graph<N, E, Ty, Ix> {
+impl<N, E, Ty: EdgeType, Ix: IndexType> MemDbgImpl for Graph<N, E, Ty, Ix>
+where
+    N: MemSize,
+    E: MemSize,
+{
+}
+impl<N, E, Ty: EdgeType, Ix: IndexType> MemSize for Graph<N, E, Ty, Ix>
+where
+    N: MemSize,
+    E: MemSize,
+{
     fn mem_size(&self, flags: mem_dbg::SizeFlags) -> usize {
-        let (nodes, edges) = if flags.contains(mem_dbg::SizeFlags::CAPACITY) {
-            self.0.capacity()
+        let self_ = core::mem::size_of::<Self>();
+        let node_extra = core::mem::size_of::<Node<N, Ix>>() - core::mem::size_of::<N>();
+        let edge_extra = core::mem::size_of::<Edge<E, Ix>>() - core::mem::size_of::<E>();
+        let self_ = self_
+            + self
+                .0
+                .node_weights()
+                .map(|n| node_extra + n.mem_size(flags))
+                .sum::<usize>()
+            + self
+                .0
+                .edge_weights()
+                .map(|e| edge_extra + e.mem_size(flags))
+                .sum::<usize>();
+
+        let result = if flags.contains(mem_dbg::SizeFlags::CAPACITY) {
+            let (nodes, edges) = self.0.capacity();
+            let (nodes, edges) = (nodes - self.0.node_count(), edges - self.0.edge_count());
+            self_
+                + nodes * core::mem::size_of::<Node<N, Ix>>()
+                + edges * core::mem::size_of::<Edge<E, Ix>>()
         } else {
-            (self.0.node_count(), self.0.edge_count())
+            self_
         };
-        core::mem::size_of::<Self>()
-            + nodes * std::mem::size_of::<Node<N, Ix>>()
-            + edges * std::mem::size_of::<Edge<E, Ix>>()
+        assert!(result >= core::mem::size_of::<Self>());
+        result
     }
 }
 impl<N, E, Ty, Ix> CopyType for Graph<N, E, Ty, Ix> {
@@ -182,35 +215,3 @@ impl MemSize for VersionInfo {
 impl CopyType for VersionInfo {
     type Copy = False;
 }
-
-// BoxSlice
-
-impl<T> MemDbgImpl for BoxSlice<T>
-where
-    [T]: MemDbgImpl,
-{
-    fn _mem_dbg_rec_on(
-        &self,
-        writer: &mut impl core::fmt::Write,
-        total_size: usize,
-        max_depth: usize,
-        prefix: &mut String,
-        is_last: bool,
-        flags: mem_dbg::DbgFlags,
-    ) -> core::fmt::Result {
-        let self_: &[T] = self;
-        self_._mem_dbg_rec_on(writer, total_size, max_depth, prefix, is_last, flags)
-    }
-}
-impl<T> MemSize for BoxSlice<T>
-where
-    [T]: MemSize,
-{
-    fn mem_size(&self, flags: mem_dbg::SizeFlags) -> usize {
-        let self_: &[T] = self;
-        core::mem::size_of::<usize>() + self_.mem_size(flags)
-    }
-}
-impl<T: CopyType> CopyType for BoxSlice<T> {
-    type Copy = T::Copy;
-}
diff --git a/smt-log-parser/src/mem_dbg/mod.rs b/smt-log-parser/src/mem_dbg/mod.rs
index bc01248b..a00f14c6 100644
--- a/smt-log-parser/src/mem_dbg/mod.rs
+++ b/smt-log-parser/src/mem_dbg/mod.rs
@@ -172,6 +172,27 @@ impl<K, V> std::iter::IntoIterator for FxHashMap<K, V> {
     }
 }
 
+// FxHashSet
+
+derive_wrapper!(fxhash::FxHashSet<K>);
+impl<K> Default for FxHashSet<K> {
+    fn default() -> Self {
+        Self(fxhash::FxHashSet::default())
+    }
+}
+impl<K: Eq + std::hash::Hash> FromIterator<K> for FxHashSet<K> {
+    fn from_iter<T: IntoIterator<Item = K>>(iter: T) -> Self {
+        Self(fxhash::FxHashSet::from_iter(iter))
+    }
+}
+impl<K> std::iter::IntoIterator for FxHashSet<K> {
+    type Item = <Self::IntoIter as std::iter::IntoIterator>::Item;
+    type IntoIter = std::collections::hash_set::IntoIter<K>;
+    fn into_iter(self) -> Self::IntoIter {
+        self.0.into_iter()
+    }
+}
+
 // StringTable
 
 derive_wrapper!(
diff --git a/smt-log-parser/src/mem_dbg/utils.rs b/smt-log-parser/src/mem_dbg/utils.rs
index e6213d69..a44090dd 100644
--- a/smt-log-parser/src/mem_dbg/utils.rs
+++ b/smt-log-parser/src/mem_dbg/utils.rs
@@ -1,9 +1,13 @@
+#[cfg(feature = "mem_dbg")]
+use mem_dbg::{MemDbg, MemSize};
+
 use core::ops::{Deref, DerefMut};
 
 use super::{FxHashMap, TiVec};
 
 // BoxSlice
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum BoxSlice<T> {
diff --git a/smt-log-parser/src/parsers/z3/egraph.rs b/smt-log-parser/src/parsers/z3/egraph.rs
index a147cb7d..63d33fca 100644
--- a/smt-log-parser/src/parsers/z3/egraph.rs
+++ b/smt-log-parser/src/parsers/z3/egraph.rs
@@ -409,7 +409,7 @@ pub trait EqualityWalker<'a> {
     /// equality. If you wish to recurse into congruences then use the
     /// following structure:
     ///
-    /// ```
+    /// ```ignore
     /// let (eq, use_) = eq_use;
     /// match &self.equalities().given[eq] {
     ///     EqualityExpl::Congruence { uses, .. } => self.walk_congruence(uses, use_.unwrap(), forward),
diff --git a/smt-log-parser/src/parsers/z3/inter_line.rs b/smt-log-parser/src/parsers/z3/inter_line.rs
index fb9e1742..98c55bae 100644
--- a/smt-log-parser/src/parsers/z3/inter_line.rs
+++ b/smt-log-parser/src/parsers/z3/inter_line.rs
@@ -2,6 +2,7 @@
 use mem_dbg::{MemDbg, MemSize};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Default, Clone, Copy)]
 pub(super) struct InterLine {
     prev: Data,
@@ -22,12 +23,14 @@ impl InterLine {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Default, Clone, Copy)]
 pub(super) struct Data {
     pub(super) last_line_kind: LineKind,
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Default, Clone, Copy)]
 pub(super) enum LineKind {
     DecideAndOr,
diff --git a/smt-log-parser/src/parsers/z3/stm2.rs b/smt-log-parser/src/parsers/z3/stm2.rs
index ec6b6328..44f80a1e 100644
--- a/smt-log-parser/src/parsers/z3/stm2.rs
+++ b/smt-log-parser/src/parsers/z3/stm2.rs
@@ -182,6 +182,7 @@ impl EventLog {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Clone, Copy)]
 pub struct Event {
     /// The number of enodes created after this event
@@ -192,6 +193,7 @@ pub struct Event {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[derive(Debug, Clone, Copy)]
 pub enum EventKind {
     NewConst(TermIdx),
diff --git a/smt-log-parser/src/parsers/z3/synthetic.rs b/smt-log-parser/src/parsers/z3/synthetic.rs
index b9a912fe..a78e7809 100644
--- a/smt-log-parser/src/parsers/z3/synthetic.rs
+++ b/smt-log-parser/src/parsers/z3/synthetic.rs
@@ -29,12 +29,14 @@ pub struct SynthTerm {
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
 #[repr(transparent)]
 pub struct SynthIdx(TermIdx);
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
 // Note that we must preserve `size_of::<SynthTermKind>() == size_of::<TermKind>()`!