Add documentation for egg subpackage

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. See [/egg](/egg) for details.
 
 ## Development
 

docs/support-packages/egg.md

@@ -0,0 +1,123 @@
+# 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. Inspired by the [egg library](https://egraphs-good.github.io/).
+
+## 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)
+```
+
+## 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
+- **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
+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 (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.
+
+## 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
+
+## 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)

egg/README.md

@@ -0,0 +1,143 @@
+# 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. Inspired by the [egg library](https://egraphs-good.github.io/).
+
+## 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
+
+### 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
+
+## 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
+uv run pytest
+
+# Run with coverage
+uv run pytest --cov
+```
+
+## 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).

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