Allow recursively adding new E-nodes in N::make

src/egraph.rs

@@ -1007,7 +1007,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
                     *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<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
@@ -1034,16 +1034,16 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
     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()],
             data: N::make(self, &original),
             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);

src/explain.rs

@@ -908,19 +908,40 @@ impl<L: Language> Explain<L> {
         }
     }
 
-    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