Skip to content

Commit

Permalink
Removed hack for now, fixed explanations
Browse files Browse the repository at this point in the history
  • Loading branch information
imbrem committed Feb 4, 2025
1 parent bb5c8b6 commit c03a39a
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 8 deletions.
11 changes: 3 additions & 8 deletions src/egraph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1020,7 +1020,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
} 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
Expand All @@ -1035,20 +1035,15 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
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);
Expand Down
21 changes: 21 additions & 0 deletions src/explain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -923,6 +923,27 @@ impl<L: Language> Explain<L> {
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;
Expand Down

0 comments on commit c03a39a

Please sign in to comment.