From 3e0c879d96831949b8171f355e5c84146909b550 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:09:19 +0000
Subject: [PATCH 1/7] Initial plan


From d1b62ccf56ab158094bae0d718405a3113007155 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:13:20 +0000
Subject: [PATCH 2/7] Add documentation for egg subpackage

- Created README.md for egg subpackage with detailed API and usage examples
- Added docs/support-packages/egg.md documentation page
- Updated main README.md to include link to egg subpackage
- Updated mkdocs.yml to include egg documentation in navigation

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 README.md                    |   1 +
 docs/support-packages/egg.md | 167 ++++++++++++++++++++++++++++
 egg/README.md                | 204 +++++++++++++++++++++++++++++++++++
 mkdocs.yml                   |   1 +
 4 files changed, 373 insertions(+)
 create mode 100644 docs/support-packages/egg.md
 create mode 100644 egg/README.md

diff --git a/README.md b/README.md
index 26717fcd..b0809cae 100644
--- a/README.md
+++ b/README.md
@@ -347,6 +347,7 @@ Each example demonstrates logical inference using propositional logic axioms.
 ## Support Packages
 
 - **BNF Conversion Library** ([apyds-bnf](https://pypi.org/project/apyds-bnf/), [atsds-bnf](https://www.npmjs.com/package/atsds-bnf)): Bidirectional conversion between DS syntax formats. See [/bnf](/bnf) for details.
+- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/)): E-Graph implementation for efficient equality reasoning and term rewriting. See [/egg](/egg) for details.
 
 ## Development
 
diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
new file mode 100644
index 00000000..60c328b6
--- /dev/null
+++ b/docs/support-packages/egg.md
@@ -0,0 +1,167 @@
+# E-Graph Support Package
+
+The E-Graph support package provides efficient management and manipulation of equivalence classes of terms for the DS deductive system.
+
+An E-Graph (Equality Graph) is a data structure that efficiently represents equivalence classes of terms and automatically maintains congruence closure. This implementation follows the egg-style approach with deferred rebuilding for optimal performance.
+
+## Installation
+
+### Python
+
+```bash
+pip install apyds-egg
+```
+
+Requires Python 3.11-3.14.
+
+## Usage
+
+### Basic Example
+
+```python
+import apyds
+from apyds_egg import EGraph
+
+# Create an E-Graph
+eg = EGraph()
+
+# Add terms to the E-Graph
+a = eg.add(apyds.Term("a"))
+b = eg.add(apyds.Term("b"))
+x = eg.add(apyds.Term("x"))
+
+# Add compound terms
+ax = eg.add(apyds.Term("(+ a x)"))
+bx = eg.add(apyds.Term("(+ b x)"))
+
+# Initially, (+ a x) and (+ b x) are in different E-classes
+assert eg.find(ax) != eg.find(bx)
+
+# Merge a and b
+eg.merge(a, b)
+
+# Rebuild to restore congruence
+eg.rebuild()
+
+# Now (+ a x) and (+ b x) are in the same E-class
+assert eg.find(ax) == eg.find(bx)
+```
+
+### Congruence Closure
+
+The E-Graph automatically maintains congruence closure. When two E-Classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-Class:
+
+```python
+eg = EGraph()
+
+# Add terms with nested structure
+fa = eg.add(apyds.Term("(f a)"))
+fb = eg.add(apyds.Term("(f b)"))
+gfa = eg.add(apyds.Term("(g (f a))"))
+gfb = eg.add(apyds.Term("(g (f b))"))
+
+# Merge a and b
+a = eg.add(apyds.Term("a"))
+b = eg.add(apyds.Term("b"))
+eg.merge(a, b)
+
+# Rebuild propagates equivalence
+eg.rebuild()
+
+# Now all derived terms are equivalent
+assert eg.find(fa) == eg.find(fb)
+assert eg.find(gfa) == eg.find(gfb)
+```
+
+### Union-Find Example
+
+The package also exports the Union-Find data structure used internally:
+
+```python
+from apyds_egg import UnionFind, EClassId
+
+uf = UnionFind()
+a = EClassId(0)
+b = EClassId(1)
+c = EClassId(2)
+
+# Find returns canonical representative
+assert uf.find(a) == a
+
+# Union merges sets
+uf.union(a, b)
+assert uf.find(a) == uf.find(b)
+
+# Path compression for efficiency
+uf.union(b, c)
+assert uf.find(a) == uf.find(c)
+```
+
+## Core Concepts
+
+### E-Graph Structure
+
+An E-Graph consists of several key components:
+
+- **E-Nodes**: Represent terms with an operator and children
+- **E-Classes**: Equivalence classes of E-Nodes
+- **Hashcons**: Ensures uniqueness of E-Nodes
+- **Union-Find**: Manages E-Class equivalence relationships
+- **Parents**: Tracks which terms depend on each E-Class
+- **Worklist**: Manages deferred congruence rebuilding
+
+### Deferred Rebuilding
+
+The implementation uses egg-style deferred rebuilding:
+
+1. **Merge**: Combine two E-Classes and add to worklist
+2. **Rebuild**: Process worklist to restore congruence
+3. **Repair**: Re-canonicalize parent nodes and merge congruent ones
+
+This approach provides better performance than immediate rebuilding by batching congruence updates.
+
+### Adding Terms
+
+Terms are converted to E-Nodes and added to the E-Graph:
+
+- **Items and Variables**: Represented as E-Nodes with no children
+- **Lists**: Represented as E-Nodes with operator `"()"` and children for each list element
+
+The hashcons ensures that identical E-Nodes share the same E-Class ID.
+
+## API Reference
+
+### EGraph
+
+Main class for E-Graph operations:
+
+- `__init__()`: Create a new empty E-Graph
+- `add(term: apyds.Term) -> EClassId`: Add a term and return its E-Class ID
+- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-Classes
+- `rebuild() -> None`: Restore congruence closure by processing the worklist
+- `find(eclass: EClassId) -> EClassId`: Find the canonical E-Class representative
+
+### UnionFind[T]
+
+Generic Union-Find data structure:
+
+- `__init__()`: Create a new Union-Find structure
+- `find(x: T) -> T`: Find canonical representative with path compression
+- `union(a: T, b: T) -> T`: Union two sets and return the representative
+
+### ENode
+
+Immutable node in the E-Graph:
+
+- `op: str`: The operator/functor of the term
+- `children: tuple[EClassId, ...]`: Tuple of child E-Class IDs
+- `canonicalize(find: Callable[[EClassId], EClassId]) -> ENode`: Create a new E-Node with canonicalized children
+
+### EClassId
+
+Type alias for `int` representing E-Class identifiers.
+
+## Package Information
+
+- **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
+- **Source Code**: [GitHub - egg directory](https://github.com/USTC-KnowledgeComputingLab/ds/tree/main/egg)
diff --git a/egg/README.md b/egg/README.md
new file mode 100644
index 00000000..b2dcc3b0
--- /dev/null
+++ b/egg/README.md
@@ -0,0 +1,204 @@
+# E-Graph Support Package for DS
+
+An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
+
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning and term rewriting.
+
+## Features
+
+- **E-Graph Data Structure**: Manage equivalence classes of terms efficiently
+- **Union-Find**: Path-compressed union-find for disjoint set management
+- **Congruence Closure**: Automatic maintenance of congruence relationships
+- **Deferred Rebuilding**: egg-style deferred rebuilding for performance
+- **Python Integration**: Seamless integration with apyds terms
+- **Type-Safe**: Full type hints for Python 3.11+
+
+## Installation
+
+### Python (pip)
+
+```bash
+pip install apyds-egg
+```
+
+Requires Python 3.11-3.14.
+
+## Quick Start
+
+### Python Example
+
+```python
+import apyds
+from apyds_egg import EGraph
+
+# Create an E-Graph
+eg = EGraph()
+
+# Add terms to the E-Graph
+a = eg.add(apyds.Term("a"))
+b = eg.add(apyds.Term("b"))
+x = eg.add(apyds.Term("x"))
+
+# Add compound terms
+ax = eg.add(apyds.Term("(+ a x)"))
+bx = eg.add(apyds.Term("(+ b x)"))
+
+# Initially, (+ a x) and (+ b x) are in different E-classes
+assert eg.find(ax) != eg.find(bx)
+
+# Merge a and b
+eg.merge(a, b)
+
+# Rebuild to restore congruence
+eg.rebuild()
+
+# Now (+ a x) and (+ b x) are in the same E-class
+assert eg.find(ax) == eg.find(bx)
+```
+
+## Core Concepts
+
+### E-Graph
+
+An E-Graph is a data structure that efficiently represents and maintains equivalence classes of terms. It consists of:
+
+- **E-Nodes**: Nodes representing terms with an operator and children
+- **E-Classes**: Equivalence classes of E-Nodes
+- **Union-Find**: Data structure for managing E-Class equivalence
+- **Congruence**: Two terms are congruent if they have the same operator and their children are in equivalent E-Classes
+
+### Union-Find
+
+The Union-Find data structure manages disjoint sets with path compression:
+
+```python
+from apyds_egg import UnionFind, EClassId
+
+uf = UnionFind()
+a = EClassId(0)
+b = EClassId(1)
+
+# Find canonical representative
+assert uf.find(a) == a
+
+# Union two sets
+uf.union(a, b)
+assert uf.find(a) == uf.find(b)
+```
+
+### E-Nodes
+
+E-Nodes represent terms in the E-Graph:
+
+```python
+from apyds_egg import ENode, EClassId
+
+# Create an E-Node for the term (+ a b)
+a_id = EClassId(0)
+b_id = EClassId(1)
+node = ENode("+", (a_id, b_id))
+```
+
+### Congruence Closure
+
+The E-Graph maintains congruence closure automatically. When two E-Classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-Class:
+
+```python
+eg = EGraph()
+
+# Add terms
+fa = eg.add(apyds.Term("(f a)"))
+fb = eg.add(apyds.Term("(f b)"))
+
+# Merge a and b
+a = eg.add(apyds.Term("a"))
+b = eg.add(apyds.Term("b"))
+eg.merge(a, b)
+
+# Rebuild maintains congruence
+eg.rebuild()
+
+# Now (f a) and (f b) are equivalent
+assert eg.find(fa) == eg.find(fb)
+```
+
+## API Overview
+
+### EGraph
+
+- `__init__()`: Create a new E-Graph
+- `add(term: apyds.Term) -> EClassId`: Add a term to the E-Graph
+- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-Classes
+- `rebuild() -> None`: Restore congruence closure
+- `find(eclass: EClassId) -> EClassId`: Find canonical E-Class representative
+
+### UnionFind
+
+- `__init__()`: Create a new Union-Find structure
+- `find(x: T) -> T`: Find canonical representative with path compression
+- `union(a: T, b: T) -> T`: Union two sets
+
+### ENode
+
+- `op: str`: The operator of the term
+- `children: tuple[EClassId, ...]`: The children E-Class IDs
+- `canonicalize(find: Callable) -> ENode`: Canonicalize children
+
+### EClassId
+
+- Type alias for `int` representing E-Class identifiers
+
+## Building from Source
+
+### Prerequisites
+
+- Python 3.11-3.14
+- apyds package
+
+### Python Package
+
+```bash
+cd egg
+
+# Install dependencies
+uv sync --extra dev
+
+# Build package
+uv build
+
+# Run tests
+pytest
+
+# Run with coverage
+pytest --cov
+```
+
+### Running Tests
+
+```bash
+# Run all tests
+pytest
+
+# Run with coverage report
+pytest --cov=apyds_egg
+
+# Run specific test
+pytest tests/test_egraph.py::test_egraph_congruence
+```
+
+## License
+
+This project is licensed under the GNU Affero General Public License v3.0 or later (AGPL-3.0-or-later).
+
+## Repository
+
+- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/egg` directory)
+- **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
+
+## Author
+
+Hao Zhang <hzhangxyz@outlook.com>
+
+## Related
+
+This package is a support library for the [DS (Deductive System)](https://github.com/USTC-KnowledgeComputingLab/ds) project. For the main DS library with C++ core and bindings, see the [main repository](https://github.com/USTC-KnowledgeComputingLab/ds).
diff --git a/mkdocs.yml b/mkdocs.yml
index ee2d57dc..3cc5fab7 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -61,6 +61,7 @@ nav:
       - C++ API: api/cpp.md
   - Support Packages:
       - BNF: support-packages/bnf.md
+      - E-Graph: support-packages/egg.md
   - Examples:
       - Basis Examples: examples/basic.md
       - Sudoku: examples/sudoku.md

From 837a2bf6db3336d2f09c19252c8d02257cc7fce6 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:14:39 +0000
Subject: [PATCH 3/7] Address code review feedback

- Simplify GitHub repository link in egg/README.md
- Clarify hash-consing terminology in docs/support-packages/egg.md
- Expand Items and Variables explanation with examples

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 docs/support-packages/egg.md | 8 ++++----
 egg/README.md                | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index 60c328b6..60e96adb 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -105,7 +105,7 @@ An E-Graph consists of several key components:
 
 - **E-Nodes**: Represent terms with an operator and children
 - **E-Classes**: Equivalence classes of E-Nodes
-- **Hashcons**: Ensures uniqueness of E-Nodes
+- **Hash-consing (Hashcons)**: Ensures uniqueness of E-Nodes by mapping identical nodes to the same E-Class
 - **Union-Find**: Manages E-Class equivalence relationships
 - **Parents**: Tracks which terms depend on each E-Class
 - **Worklist**: Manages deferred congruence rebuilding
@@ -124,10 +124,10 @@ This approach provides better performance than immediate rebuilding by batching
 
 Terms are converted to E-Nodes and added to the E-Graph:
 
-- **Items and Variables**: Represented as E-Nodes with no children
-- **Lists**: Represented as E-Nodes with operator `"()"` and children for each list element
+- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or `` `x`` are represented as E-Nodes with no children
+- **Lists**: Compound terms like `(+ a b)` are represented as E-Nodes with operator `"()"` and children for each list element
 
-The hashcons ensures that identical E-Nodes share the same E-Class ID.
+The hash-consing mechanism ensures that identical E-Nodes share the same E-Class ID.
 
 ## API Reference
 
diff --git a/egg/README.md b/egg/README.md
index b2dcc3b0..aa006cf5 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -192,7 +192,7 @@ This project is licensed under the GNU Affero General Public License v3.0 or lat
 
 ## Repository
 
-- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/egg` directory)
+- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds)
 - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
 
 ## Author

From 2ca7157dce0566a3f7ae1a73068636c1cd017fdb Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:16:06 +0000
Subject: [PATCH 4/7] Fix markdown backtick formatting

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 docs/support-packages/egg.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index 60e96adb..531d5cfb 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -124,7 +124,7 @@ This approach provides better performance than immediate rebuilding by batching
 
 Terms are converted to E-Nodes and added to the E-Graph:
 
-- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or `` `x`` are represented as E-Nodes with no children
+- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or `` `x `` are represented as E-Nodes with no children
 - **Lists**: Compound terms like `(+ a b)` are represented as E-Nodes with operator `"()"` and children for each list element
 
 The hash-consing mechanism ensures that identical E-Nodes share the same E-Class ID.

From 325eb2f2115067d7193c5ae49385f4bffb2251b9 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:18:31 +0000
Subject: [PATCH 5/7] Improve consistency: use E-class instead of E-Class

- Updated all occurrences to use lowercase 'c' for consistency with source code
- Fixed variable example formatting in documentation

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 docs/support-packages/egg.md | 26 +++++++++++++-------------
 egg/README.md                | 16 ++++++++--------
 2 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index 531d5cfb..774d18f5 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -49,7 +49,7 @@ assert eg.find(ax) == eg.find(bx)
 
 ### Congruence Closure
 
-The E-Graph automatically maintains congruence closure. When two E-Classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-Class:
+The E-Graph automatically maintains congruence closure. When two E-classes are merged, the `rebuild()` method ensures that all congruent terms remain in the same E-class:
 
 ```python
 eg = EGraph()
@@ -104,17 +104,17 @@ assert uf.find(a) == uf.find(c)
 An E-Graph consists of several key components:
 
 - **E-Nodes**: Represent terms with an operator and children
-- **E-Classes**: Equivalence classes of E-Nodes
-- **Hash-consing (Hashcons)**: Ensures uniqueness of E-Nodes by mapping identical nodes to the same E-Class
-- **Union-Find**: Manages E-Class equivalence relationships
-- **Parents**: Tracks which terms depend on each E-Class
+- **E-classes**: Equivalence classes of E-Nodes
+- **Hash-consing (Hashcons)**: Ensures uniqueness of E-Nodes by mapping identical nodes to the same E-class
+- **Union-Find**: Manages E-class equivalence relationships
+- **Parents**: Tracks which terms depend on each E-class
 - **Worklist**: Manages deferred congruence rebuilding
 
 ### Deferred Rebuilding
 
 The implementation uses egg-style deferred rebuilding:
 
-1. **Merge**: Combine two E-Classes and add to worklist
+1. **Merge**: Combine two E-classes and add to worklist
 2. **Rebuild**: Process worklist to restore congruence
 3. **Repair**: Re-canonicalize parent nodes and merge congruent ones
 
@@ -124,10 +124,10 @@ This approach provides better performance than immediate rebuilding by batching
 
 Terms are converted to E-Nodes and added to the E-Graph:
 
-- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or `` `x `` are represented as E-Nodes with no children
+- **Items (constants/functors) and Variables**: Atomic terms like `a`, `b`, or backtick-prefixed variables like `x` are represented as E-Nodes with no children
 - **Lists**: Compound terms like `(+ a b)` are represented as E-Nodes with operator `"()"` and children for each list element
 
-The hash-consing mechanism ensures that identical E-Nodes share the same E-Class ID.
+The hash-consing mechanism ensures that identical E-Nodes share the same E-class ID.
 
 ## API Reference
 
@@ -136,10 +136,10 @@ The hash-consing mechanism ensures that identical E-Nodes share the same E-Class
 Main class for E-Graph operations:
 
 - `__init__()`: Create a new empty E-Graph
-- `add(term: apyds.Term) -> EClassId`: Add a term and return its E-Class ID
-- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-Classes
+- `add(term: apyds.Term) -> EClassId`: Add a term and return its E-class ID
+- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-classes
 - `rebuild() -> None`: Restore congruence closure by processing the worklist
-- `find(eclass: EClassId) -> EClassId`: Find the canonical E-Class representative
+- `find(eclass: EClassId) -> EClassId`: Find the canonical E-class representative
 
 ### UnionFind[T]
 
@@ -154,12 +154,12 @@ Generic Union-Find data structure:
 Immutable node in the E-Graph:
 
 - `op: str`: The operator/functor of the term
-- `children: tuple[EClassId, ...]`: Tuple of child E-Class IDs
+- `children: tuple[EClassId, ...]`: Tuple of child E-class IDs
 - `canonicalize(find: Callable[[EClassId], EClassId]) -> ENode`: Create a new E-Node with canonicalized children
 
 ### EClassId
 
-Type alias for `int` representing E-Class identifiers.
+Type alias for `int` representing E-class identifiers.
 
 ## Package Information
 
diff --git a/egg/README.md b/egg/README.md
index aa006cf5..cd0fd583 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -63,9 +63,9 @@ assert eg.find(ax) == eg.find(bx)
 An E-Graph is a data structure that efficiently represents and maintains equivalence classes of terms. It consists of:
 
 - **E-Nodes**: Nodes representing terms with an operator and children
-- **E-Classes**: Equivalence classes of E-Nodes
-- **Union-Find**: Data structure for managing E-Class equivalence
-- **Congruence**: Two terms are congruent if they have the same operator and their children are in equivalent E-Classes
+- **E-classes**: Equivalence classes of E-Nodes
+- **Union-Find**: Data structure for managing E-class equivalence
+- **Congruence**: Two terms are congruent if they have the same operator and their children are in equivalent E-classes
 
 ### Union-Find
 
@@ -101,7 +101,7 @@ node = ENode("+", (a_id, b_id))
 
 ### Congruence Closure
 
-The E-Graph maintains congruence closure automatically. When two E-Classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-Class:
+The E-Graph maintains congruence closure automatically. When two E-classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-class:
 
 ```python
 eg = EGraph()
@@ -128,9 +128,9 @@ assert eg.find(fa) == eg.find(fb)
 
 - `__init__()`: Create a new E-Graph
 - `add(term: apyds.Term) -> EClassId`: Add a term to the E-Graph
-- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-Classes
+- `merge(a: EClassId, b: EClassId) -> EClassId`: Merge two E-classes
 - `rebuild() -> None`: Restore congruence closure
-- `find(eclass: EClassId) -> EClassId`: Find canonical E-Class representative
+- `find(eclass: EClassId) -> EClassId`: Find canonical E-class representative
 
 ### UnionFind
 
@@ -141,12 +141,12 @@ assert eg.find(fa) == eg.find(fb)
 ### ENode
 
 - `op: str`: The operator of the term
-- `children: tuple[EClassId, ...]`: The children E-Class IDs
+- `children: tuple[EClassId, ...]`: The children E-class IDs
 - `canonicalize(find: Callable) -> ENode`: Canonicalize children
 
 ### EClassId
 
-- Type alias for `int` representing E-Class identifiers
+- Type alias for `int` representing E-class identifiers
 
 ## Building from Source
 

From c2c9475b7159cb8c21bb2b8b7786d2c1574d3be9 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:31:42 +0000
Subject: [PATCH 6/7] Address PR feedback: simplify documentation

- Remove "term rewriting" mentions (only supports equality reasoning)
- Add egg library reference link (https://egraphs-good.github.io/)
- Remove Union-Find and E-Nodes sections from Core Concepts
- Remove UnionFind, ENode, and EClassId from API Overview
- Update test commands to use "uv run pytest"
- Remove "Running Tests" section
- Add "(in /egg directory)" to repository link

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 README.md                    |  2 +-
 docs/support-packages/egg.md | 46 +-----------------------
 egg/README.md                | 69 +++---------------------------------
 3 files changed, 6 insertions(+), 111 deletions(-)

diff --git a/README.md b/README.md
index b0809cae..2059a777 100644
--- a/README.md
+++ b/README.md
@@ -347,7 +347,7 @@ Each example demonstrates logical inference using propositional logic axioms.
 ## Support Packages
 
 - **BNF Conversion Library** ([apyds-bnf](https://pypi.org/project/apyds-bnf/), [atsds-bnf](https://www.npmjs.com/package/atsds-bnf)): Bidirectional conversion between DS syntax formats. See [/bnf](/bnf) for details.
-- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/)): E-Graph implementation for efficient equality reasoning and term rewriting. See [/egg](/egg) for details.
+- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/)): E-Graph implementation for efficient equality reasoning. See [/egg](/egg) for details.
 
 ## Development
 
diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index 774d18f5..dbadc45a 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -2,7 +2,7 @@
 
 The E-Graph support package provides efficient management and manipulation of equivalence classes of terms for the DS deductive system.
 
-An E-Graph (Equality Graph) is a data structure that efficiently represents equivalence classes of terms and automatically maintains congruence closure. This implementation follows the egg-style approach with deferred rebuilding for optimal performance.
+An E-Graph (Equality Graph) is a data structure that efficiently represents equivalence classes of terms and automatically maintains congruence closure. This implementation follows the egg-style approach with deferred rebuilding for optimal performance. Based on the [egg library](https://egraphs-good.github.io/).
 
 ## Installation
 
@@ -73,30 +73,6 @@ assert eg.find(fa) == eg.find(fb)
 assert eg.find(gfa) == eg.find(gfb)
 ```
 
-### Union-Find Example
-
-The package also exports the Union-Find data structure used internally:
-
-```python
-from apyds_egg import UnionFind, EClassId
-
-uf = UnionFind()
-a = EClassId(0)
-b = EClassId(1)
-c = EClassId(2)
-
-# Find returns canonical representative
-assert uf.find(a) == a
-
-# Union merges sets
-uf.union(a, b)
-assert uf.find(a) == uf.find(b)
-
-# Path compression for efficiency
-uf.union(b, c)
-assert uf.find(a) == uf.find(c)
-```
-
 ## Core Concepts
 
 ### E-Graph Structure
@@ -141,26 +117,6 @@ Main class for E-Graph operations:
 - `rebuild() -> None`: Restore congruence closure by processing the worklist
 - `find(eclass: EClassId) -> EClassId`: Find the canonical E-class representative
 
-### UnionFind[T]
-
-Generic Union-Find data structure:
-
-- `__init__()`: Create a new Union-Find structure
-- `find(x: T) -> T`: Find canonical representative with path compression
-- `union(a: T, b: T) -> T`: Union two sets and return the representative
-
-### ENode
-
-Immutable node in the E-Graph:
-
-- `op: str`: The operator/functor of the term
-- `children: tuple[EClassId, ...]`: Tuple of child E-class IDs
-- `canonicalize(find: Callable[[EClassId], EClassId]) -> ENode`: Create a new E-Node with canonicalized children
-
-### EClassId
-
-Type alias for `int` representing E-class identifiers.
-
 ## Package Information
 
 - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
diff --git a/egg/README.md b/egg/README.md
index cd0fd583..d00e6f0a 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -2,7 +2,7 @@
 
 An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
 
-This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning and term rewriting.
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning. Based on the [egg library](https://egraphs-good.github.io/).
 
 ## Features
 
@@ -67,38 +67,6 @@ An E-Graph is a data structure that efficiently represents and maintains equival
 - **Union-Find**: Data structure for managing E-class equivalence
 - **Congruence**: Two terms are congruent if they have the same operator and their children are in equivalent E-classes
 
-### Union-Find
-
-The Union-Find data structure manages disjoint sets with path compression:
-
-```python
-from apyds_egg import UnionFind, EClassId
-
-uf = UnionFind()
-a = EClassId(0)
-b = EClassId(1)
-
-# Find canonical representative
-assert uf.find(a) == a
-
-# Union two sets
-uf.union(a, b)
-assert uf.find(a) == uf.find(b)
-```
-
-### E-Nodes
-
-E-Nodes represent terms in the E-Graph:
-
-```python
-from apyds_egg import ENode, EClassId
-
-# Create an E-Node for the term (+ a b)
-a_id = EClassId(0)
-b_id = EClassId(1)
-node = ENode("+", (a_id, b_id))
-```
-
 ### Congruence Closure
 
 The E-Graph maintains congruence closure automatically. When two E-classes are merged, the E-Graph rebuilds to ensure that congruent terms remain in the same E-class:
@@ -132,22 +100,6 @@ assert eg.find(fa) == eg.find(fb)
 - `rebuild() -> None`: Restore congruence closure
 - `find(eclass: EClassId) -> EClassId`: Find canonical E-class representative
 
-### UnionFind
-
-- `__init__()`: Create a new Union-Find structure
-- `find(x: T) -> T`: Find canonical representative with path compression
-- `union(a: T, b: T) -> T`: Union two sets
-
-### ENode
-
-- `op: str`: The operator of the term
-- `children: tuple[EClassId, ...]`: The children E-class IDs
-- `canonicalize(find: Callable) -> ENode`: Canonicalize children
-
-### EClassId
-
-- Type alias for `int` representing E-class identifiers
-
 ## Building from Source
 
 ### Prerequisites
@@ -167,23 +119,10 @@ uv sync --extra dev
 uv build
 
 # Run tests
-pytest
+uv run pytest
 
 # Run with coverage
-pytest --cov
-```
-
-### Running Tests
-
-```bash
-# Run all tests
-pytest
-
-# Run with coverage report
-pytest --cov=apyds_egg
-
-# Run specific test
-pytest tests/test_egraph.py::test_egraph_congruence
+uv run pytest --cov
 ```
 
 ## License
@@ -192,7 +131,7 @@ This project is licensed under the GNU Affero General Public License v3.0 or lat
 
 ## Repository
 
-- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds)
+- **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/egg` directory)
 - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/)
 
 ## Author

From de8116b636d6ea3ea9f5337d6451f8bfc9bf19e7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 22 Dec 2025 11:38:24 +0000
Subject: [PATCH 7/7] Change "Based on" to "Inspired by" for egg library
 reference

The implementation references the egg library but is not directly based on it.

Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com>
---
 docs/support-packages/egg.md | 2 +-
 egg/README.md                | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/support-packages/egg.md b/docs/support-packages/egg.md
index dbadc45a..be36d7df 100644
--- a/docs/support-packages/egg.md
+++ b/docs/support-packages/egg.md
@@ -2,7 +2,7 @@
 
 The E-Graph support package provides efficient management and manipulation of equivalence classes of terms for the DS deductive system.
 
-An E-Graph (Equality Graph) is a data structure that efficiently represents equivalence classes of terms and automatically maintains congruence closure. This implementation follows the egg-style approach with deferred rebuilding for optimal performance. Based on the [egg library](https://egraphs-good.github.io/).
+An E-Graph (Equality Graph) is a data structure that efficiently represents equivalence classes of terms and automatically maintains congruence closure. This implementation follows the egg-style approach with deferred rebuilding for optimal performance. Inspired by the [egg library](https://egraphs-good.github.io/).
 
 ## Installation
 
diff --git a/egg/README.md b/egg/README.md
index d00e6f0a..5bf1f1dd 100644
--- a/egg/README.md
+++ b/egg/README.md
@@ -2,7 +2,7 @@
 
 An E-Graph (Equality Graph) implementation for the DS deductive system, providing efficient management and manipulation of equivalence classes of terms.
 
-This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning. Based on the [egg library](https://egraphs-good.github.io/).
+This package implements the egg-style E-Graph data structure with deferred congruence closure, enabling efficient equality reasoning. Inspired by the [egg library](https://egraphs-good.github.io/).
 
 ## Features