Why does egg not remove old nodes in process_unions?

[QuarticCat]

I read your paper and there's such a procedure but I didn't see that in your code. I tried to add self.memo.remove(&node); before node.update_children(|id| self.find_mut(id));, which gave me a small memory usage reduction and no performance regression. So I'm curious why you finally removed this procedure from your code.

[mwillsey]

Hmmm. That's curious. I think you're right, I can't see a reason why it would have been removed. Perhaps on accident.

[dewert99]

I'm not sure if this has anything to do with why this was removed, but I don't think self.memo.remove(&node); would remove all old nodes that are no longer needed. Before running rebuild_unions, memo stores the nodes as they would have been canonized at the last rebuild_unions, while node would have only been canonized when it was first added to the egraph, so removing node might still miss od nodes.