diff --git a/README.md b/README.md index 60d240b..8b82e48 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. See [/egg](/egg) for details. +- **E-Graph Library** ([apyds-egg](https://pypi.org/project/apyds-egg/), [atsds-egg](https://www.npmjs.com/package/atsds-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 be36d7d..d92ea0e 100644 --- a/docs/support-packages/egg.md +++ b/docs/support-packages/egg.md @@ -14,9 +14,15 @@ pip install apyds-egg Requires Python 3.11-3.14. +### TypeScript/JavaScript + +```bash +npm install atsds-egg +``` + ## Usage -### Basic Example +### Python Example ```python import apyds @@ -47,9 +53,42 @@ eg.rebuild() assert eg.find(ax) == eg.find(bx) ``` +### TypeScript Example + +```typescript +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +// Create an E-Graph +const eg = new EGraph(); + +// Add terms to the E-Graph +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +const x = eg.add(new Term("x")); + +// Add compound terms +const ax = eg.add(new Term("(+ a x)")); +const bx = eg.add(new Term("(+ b x)")); + +// Initially, (+ a x) and (+ b x) are in different E-classes +if (eg.find(ax) === eg.find(bx)) throw new Error("Should be different"); + +// 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 +if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same"); +``` + ### 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 Example ```python eg = EGraph() @@ -73,6 +112,33 @@ assert eg.find(fa) == eg.find(fb) assert eg.find(gfa) == eg.find(gfb) ``` +#### TypeScript Example + +```typescript +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +const eg = new EGraph(); + +// Add terms with nested structure +const fa = eg.add(new Term("(f a)")); +const fb = eg.add(new Term("(f b)")); +const gfa = eg.add(new Term("(g (f a))")); +const gfb = eg.add(new Term("(g (f b))")); + +// Merge a and b +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +eg.merge(a, b); + +// Rebuild propagates equivalence +eg.rebuild(); + +// Now all derived terms are equivalent +if (eg.find(fa) !== eg.find(fb)) throw new Error("fa != fb"); +if (eg.find(gfa) !== eg.find(gfb)) throw new Error("gfa != gfb"); +``` + ## Core Concepts ### E-Graph Structure @@ -107,17 +173,24 @@ The hash-consing mechanism ensures that identical E-Nodes share the same E-class ## API Reference -### EGraph +### Python (apyds-egg) -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 +- `EGraph()`: 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 by processing the worklist -- `find(eclass: EClassId) -> EClassId`: Find the canonical E-class representative +- `rebuild() -> None`: Restore congruence closure +- `find(eclass: EClassId) -> EClassId`: Find canonical E-class representative + +### TypeScript (atsds-egg) + +- `new EGraph()`: Create a new E-Graph +- `add(term: atsds.Term): EClassId`: Add a term to the E-Graph +- `merge(a: EClassId, b: EClassId): EClassId`: Merge two E-classes +- `rebuild(): void`: Restore congruence closure +- `find(eclass: EClassId): EClassId`: Find canonical E-class representative ## Package Information - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/) +- **npm Package**: [atsds-egg](https://www.npmjs.com/package/atsds-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 index 5bf1f1d..d537225 100644 --- a/egg/README.md +++ b/egg/README.md @@ -10,8 +10,6 @@ This package implements the egg-style E-Graph data structure with deferred congr - **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 @@ -23,6 +21,12 @@ pip install apyds-egg Requires Python 3.11-3.14. +### TypeScript/JavaScript (npm) + +```bash +npm install atsds-egg +``` + ## Quick Start ### Python Example @@ -56,6 +60,37 @@ eg.rebuild() assert eg.find(ax) == eg.find(bx) ``` +### TypeScript Example + +```typescript +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +// Create an E-Graph +const eg = new EGraph(); + +// Add terms to the E-Graph +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +const x = eg.add(new Term("x")); + +// Add compound terms +const ax = eg.add(new Term("(+ a x)")); +const bx = eg.add(new Term("(+ b x)")); + +// Initially, (+ a x) and (+ b x) are in different E-classes +if (eg.find(ax) === eg.find(bx)) throw new Error("Should be different"); + +// 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 +if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same"); +``` + ## Core Concepts ### E-Graph @@ -69,7 +104,9 @@ An E-Graph is a data structure that efficiently represents and maintains equival ### 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 Example ```python eg = EGraph() @@ -90,22 +127,55 @@ eg.rebuild() assert eg.find(fa) == eg.find(fb) ``` +#### TypeScript Example + +```typescript +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +const eg = new EGraph(); + +// Add terms +const fa = eg.add(new Term("(f a)")); +const fb = eg.add(new Term("(f b)")); + +// Merge a and b +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +eg.merge(a, b); + +// Rebuild maintains congruence +eg.rebuild(); + +// Now (f a) and (f b) are equivalent +if (eg.find(fa) !== eg.find(fb)) throw new Error("Congruence failed"); +``` + ## API Overview -### EGraph +### Python (apyds-egg) -- `__init__()`: Create a new E-Graph +- `EGraph()`: 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 +### TypeScript (atsds-egg) + +- `new EGraph()`: Create a new E-Graph +- `add(term: atsds.Term): EClassId`: Add a term to the E-Graph +- `merge(a: EClassId, b: EClassId): EClassId`: Merge two E-classes +- `rebuild(): void`: Restore congruence closure +- `find(eclass: EClassId): EClassId`: Find canonical E-class representative + ## Building from Source ### Prerequisites - Python 3.11-3.14 -- apyds package +- Node.js and npm +- apyds and atsds packages ### Python Package @@ -125,6 +195,21 @@ uv run pytest uv run pytest --cov ``` +### TypeScript Package + +```bash +cd egg + +# Install dependencies +npm install + +# Build package +npm run build + +# Run tests +npm test +``` + ## License This project is licensed under the GNU Affero General Public License v3.0 or later (AGPL-3.0-or-later). @@ -133,6 +218,7 @@ This project is licensed under the GNU Affero General Public License v3.0 or lat - **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) (in `/egg` directory) - **Python Package**: [apyds-egg](https://pypi.org/project/apyds-egg/) +- **npm Package**: [atsds-egg](https://www.npmjs.com/package/atsds-egg) ## Author