From 3abe37947e4f49c4820c005d7def74f11de3bf78 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 22 Dec 2025 05:04:08 +0000 Subject: [PATCH 1/3] Initial plan From 6ba86c18fc348ed77d0674513a86e1476e3c94de Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 22 Dec 2025 05:08:53 +0000 Subject: [PATCH 2/3] Convert to traditional E-Graph with immediate repair Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- egg/apyds_egg/__init__.py | 61 ++++++++++++++++++++++++--------------- 1 file changed, 38 insertions(+), 23 deletions(-) diff --git a/egg/apyds_egg/__init__.py b/egg/apyds_egg/__init__.py index c147a06..fcb8a18 100644 --- a/egg/apyds_egg/__init__.py +++ b/egg/apyds_egg/__init__.py @@ -77,7 +77,6 @@ def __init__(self) -> None: self.classes: dict[EClassId, set[ENode]] = {} self.parents: dict[EClassId, set[tuple[ENode, EClassId]]] = defaultdict(set) self.hashcons: dict[ENode, EClassId] = {} - self.worklist: set[EClassId] = set() def _fresh_id(self) -> EClassId: """Generate a fresh E-class ID.""" @@ -141,7 +140,7 @@ def _add_enode(self, enode: ENode) -> EClassId: return eid def merge(self, a: EClassId, b: EClassId) -> EClassId: - """Merge two E-classes and schedule rebuilding. + """Merge two E-classes and immediately restore congruence. Args: a: The first E-class ID to merge. @@ -162,18 +161,19 @@ def merge(self, a: EClassId, b: EClassId) -> EClassId: self.parents[r] |= self.parents[rb] del self.parents[rb] - self.worklist.add(r) + # Immediately restore invariants + self._repair(r) return r def rebuild(self) -> None: - """Restore congruence by processing the worklist.""" - while self.worklist: - todo: set[EClassId] = {self.find(e) for e in self.worklist} - self.worklist.clear() + """Restore congruence (no-op in traditional E-Graph). - for eclass in todo: - self._repair(eclass) + In the traditional E-Graph implementation, congruence is maintained + immediately during merge operations, so this method is kept for + backward compatibility but does nothing. + """ + pass def are_equal(self, a: EClassId, b: EClassId) -> bool: """Check if two E-class IDs are equivalent. @@ -188,19 +188,34 @@ def are_equal(self, a: EClassId, b: EClassId) -> bool: return self.find(a) == self.find(b) def _repair(self, eclass: EClassId) -> None: - """Repair congruence for an E-class by updating parent nodes.""" - new_parents: dict[ENode, EClassId] = {} - - for pnode, peclass in list(self.parents[eclass]): - self.hashcons.pop(pnode, None) - - canon = pnode.canonicalize(self.find) - peclass = self.find(peclass) + """Immediately restore congruence by re-canonicalizing parents and merging congruent ones. - if canon in new_parents: - self.merge(peclass, new_parents[canon]) - else: - new_parents[canon] = peclass - self.hashcons[canon] = peclass + This method implements the traditional E-Graph repair algorithm: + - Re-canonicalize all parent nodes + - Merge congruent parents recursively + - Continue until no more changes occur - self.parents[eclass] = {(p, c) for p, c in new_parents.items()} + Args: + eclass: The E-class ID to repair. + """ + changed = True + while changed: + changed = False + new_parents: dict[ENode, EClassId] = {} + + for pnode, peclass in list(self.parents[eclass]): + # Remove old hashcons entry + self.hashcons.pop(pnode, None) + + canon = pnode.canonicalize(self.find) + peclass = self.find(peclass) + + if canon in new_parents: + # Upward merge required + self.merge(peclass, new_parents[canon]) + changed = True + else: + new_parents[canon] = peclass + self.hashcons[canon] = peclass + + self.parents[eclass] = {(p, c) for p, c in new_parents.items()} From ef893ab9cd41b17af4013e28930714c6cafb81ba Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 22 Dec 2025 05:26:25 +0000 Subject: [PATCH 3/3] Remove rebuild() method as it's no longer needed Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- egg/apyds_egg/__init__.py | 9 --------- egg/tests/test_egraph.py | 13 +++---------- 2 files changed, 3 insertions(+), 19 deletions(-) diff --git a/egg/apyds_egg/__init__.py b/egg/apyds_egg/__init__.py index fcb8a18..8c67020 100644 --- a/egg/apyds_egg/__init__.py +++ b/egg/apyds_egg/__init__.py @@ -166,15 +166,6 @@ def merge(self, a: EClassId, b: EClassId) -> EClassId: return r - def rebuild(self) -> None: - """Restore congruence (no-op in traditional E-Graph). - - In the traditional E-Graph implementation, congruence is maintained - immediately during merge operations, so this method is kept for - backward compatibility but does nothing. - """ - pass - def are_equal(self, a: EClassId, b: EClassId) -> bool: """Check if two E-class IDs are equivalent. diff --git a/egg/tests/test_egraph.py b/egg/tests/test_egraph.py index 985d8d1..fec8d25 100644 --- a/egg/tests/test_egraph.py +++ b/egg/tests/test_egraph.py @@ -139,7 +139,6 @@ def test_egraph_congruence(): assert eg.find(ax) != eg.find(bx) eg.merge(a, b) - eg.rebuild() assert eg.find(ax) == eg.find(bx) @@ -158,7 +157,6 @@ def test_egraph_congruence_nested(): bcc = eg.add(apyds.Term("(g (f b c) c)")) eg.merge(a, b) - eg.rebuild() assert eg.find(ac) == eg.find(bc) assert eg.find(acc) == eg.find(bcc) @@ -177,12 +175,10 @@ def test_egraph_multiple_merges(): assert eg.find(a) == eg.find(c) -def test_egraph_rebuild_empty_worklist(): +def test_egraph_immediate_congruence(): eg = EGraph() a = eg.add(apyds.Term("a")) - eg.rebuild() - assert eg.find(a) == a @@ -199,7 +195,6 @@ def test_egraph_complex_example(): assert eg.find(ax) != eg.find(bx) eg.merge(a, b) - eg.rebuild() assert eg.find(ax) == eg.find(bx) @@ -251,7 +246,6 @@ def test_egraph_associativity_example(): assert eg.find(xy_z) != eg.find(x_yz) eg.merge(xy_z, x_yz) - eg.rebuild() assert eg.find(xy_z) == eg.find(x_yz) @@ -302,7 +296,7 @@ def test_egraph_are_equal(): assert eg.are_equal(a, b) -def test_egraph_are_equal_after_rebuild(): +def test_egraph_are_equal_after_merge(): eg = EGraph() x = eg.add(apyds.Term("x")) @@ -317,7 +311,6 @@ def test_egraph_are_equal_after_rebuild(): # Merge a and b eg.merge(a, b) - eg.rebuild() - # After rebuild, ax and bx should be equal due to congruence + # After merge, ax and bx should be equal due to congruence assert eg.are_equal(ax, bx)