From bb5c8b6dd99d6fa3883d9bdd469260d723cd573c Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Wed, 29 Jan 2025 17:00:51 +0000 Subject: [PATCH 1/4] Allow recursively adding new E-nodes in N::make --- src/egraph.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/egraph.rs b/src/egraph.rs index d3213bed..9565fdc2 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -1034,15 +1034,20 @@ impl> EGraph { fn make_new_eclass(&mut self, enode: L, original: L) -> Id { let id = self.unionfind.make_set(); log::trace!(" ...adding to {}", id); + + // This is a hack to avoid needing a default for L, or to clone `original` + debug_assert_eq!(Id::from(self.nodes.len()), id); + self.nodes.push(enode.clone()); + let class = EClass { id, - nodes: vec![enode.clone()], + nodes: vec![enode], data: N::make(self, &original), parents: Default::default(), }; - debug_assert_eq!(Id::from(self.nodes.len()), id); - self.nodes.push(original); + let mut enode = original; + std::mem::swap(&mut enode, &mut self.nodes[id.0 as usize]); // add this enode to the parent lists of its children enode.for_each(|child| { From c03a39a1e41b83aecf8329e6159b9a096cbcd491 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 4 Feb 2025 11:15:56 +0000 Subject: [PATCH 2/4] Removed hack for now, fixed explanations --- src/egraph.rs | 11 +++-------- src/explain.rs | 21 +++++++++++++++++++++ 2 files changed, 24 insertions(+), 8 deletions(-) diff --git a/src/egraph.rs b/src/egraph.rs index 9565fdc2..bb16ce66 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -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 @@ -1035,20 +1035,15 @@ impl> EGraph { let id = self.unionfind.make_set(); log::trace!(" ...adding to {}", id); - // This is a hack to avoid needing a default for L, or to clone `original` - debug_assert_eq!(Id::from(self.nodes.len()), id); - self.nodes.push(enode.clone()); + self.nodes.push(original.clone()); let class = EClass { id, - nodes: vec![enode], + nodes: vec![enode.clone()], data: N::make(self, &original), parents: Default::default(), }; - let mut enode = original; - std::mem::swap(&mut enode, &mut self.nodes[id.0 as usize]); - // 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..9e0f2a2e 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -923,6 +923,27 @@ impl Explain { 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 fn make_leader(&mut self, node: Id) { let next = self.explainfind[usize::from(node)].parent_connection.next; From 15c508a04a0a1e45a3d38b175f8bd2bd6999884a Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 4 Feb 2025 11:18:21 +0000 Subject: [PATCH 3/4] Typo --- src/explain.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/explain.rs b/src/explain.rs index 9e0f2a2e..4e705d5e 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -926,7 +926,7 @@ impl Explain { 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) { + while ix <= usize::from(set) { let set_ix = ix.into(); self.uncanon_memo.insert(node.clone(), set_ix); self.explainfind.push(ExplainNode { From ba148c23bdcf9aa21f6a54318e35eeb597fd7cb1 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 4 Feb 2025 11:19:42 +0000 Subject: [PATCH 4/4] Typo --- src/egraph.rs | 2 +- src/explain.rs | 28 ++++++++++++++-------------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/egraph.rs b/src/egraph.rs index bb16ce66..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); diff --git a/src/explain.rs b/src/explain.rs index 4e705d5e..3e21352c 100644 --- a/src/explain.rs +++ b/src/explain.rs @@ -908,20 +908,20 @@ 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();