diff --git a/src/egraph.rs b/src/egraph.rs index d3213bed..f641775c 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -1007,7 +1007,7 @@ impl> EGraph { *existing_explain } else { let new_id = self.unionfind.make_set(); - explain.add(original.clone(), new_id); + explain.initialize_up_to(original.clone(), new_id); debug_assert_eq!(Id::from(self.nodes.len()), new_id); self.nodes.push(original); self.unionfind.union(id, new_id); @@ -1020,7 +1020,7 @@ impl> EGraph { } else { let id = self.make_new_eclass(enode, original.clone()); if let Some(explain) = self.explain.as_mut() { - explain.add(original, id); + explain.initialize_up_to(original, id); } // now that we updated explanations, run the analysis for the new eclass @@ -1034,6 +1034,9 @@ impl> EGraph { fn make_new_eclass(&mut self, enode: L, original: L) -> Id { let id = self.unionfind.make_set(); log::trace!(" ...adding to {}", id); + + self.nodes.push(original.clone()); + let class = EClass { id, nodes: vec![enode.clone()], @@ -1041,9 +1044,6 @@ impl> EGraph { parents: Default::default(), }; - debug_assert_eq!(Id::from(self.nodes.len()), id); - self.nodes.push(original); - // add this enode to the parent lists of its children enode.for_each(|child| { self[child].parents.push(id); diff --git a/src/explain.rs b/src/explain.rs index 5a617888..3e21352c 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -908,19 +908,40 @@ impl Explain { } } - pub(crate) fn add(&mut self, node: L, set: Id) -> Id { - assert_eq!(self.explainfind.len(), usize::from(set)); - self.uncanon_memo.insert(node, set); - self.explainfind.push(ExplainNode { - neighbors: vec![], - parent_connection: Connection { - justification: Justification::Congruence, - is_rewrite_forward: false, - next: set, - current: set, - }, - }); - set + // pub(crate) fn add(&mut self, node: L, set: Id) -> Id { + // assert_eq!(self.explainfind.len(), usize::from(set)); + // self.uncanon_memo.insert(node, set); + // self.explainfind.push(ExplainNode { + // neighbors: vec![], + // parent_connection: Connection { + // justification: Justification::Congruence, + // is_rewrite_forward: false, + // next: set, + // current: set, + // }, + // }); + // set + // } + + pub(crate) fn initialize_up_to(&mut self, node: L, set: Id) -> usize { + let mut ix = self.explainfind.len(); + let mut added = 0; + while ix <= usize::from(set) { + let set_ix = ix.into(); + self.uncanon_memo.insert(node.clone(), set_ix); + self.explainfind.push(ExplainNode { + neighbors: vec![], + parent_connection: Connection { + justification: Justification::Congruence, + is_rewrite_forward: false, + next: set_ix, + current: set_ix, + }, + }); + ix += 1; + added += 1; + } + added } // reverse edges recursively to make this node the leader