diff --git a/docs/changelog.md b/docs/changelog.md index 5163d067..7d13d10b 100644 --- a/docs/changelog.md +++ b/docs/changelog.md @@ -4,6 +4,10 @@ _This project uses semantic versioning_ ## UNRELEASED +- Make shared-subexpression hoisting deterministic across Python processes, + stabilizing generated `let` bindings and serialized e-graph output + [#422](https://github.com/egraphs-good/egglog-python/pull/422). + - Upgrade to Egglog 3 and matching `egglog-experimental` APIs [#414](https://github.com/egraphs-good/egglog-python/pull/414). - BREAKING: container rebuilding is now handled by Egglog, so `Map.rebuild()`, diff --git a/python/egglog/egraph_state.py b/python/egglog/egraph_state.py index 0ed49a1a..ec8312ea 100644 --- a/python/egglog/egraph_state.py +++ b/python/egglog/egraph_state.py @@ -1711,9 +1711,7 @@ def _sanitize_egg_ident(input_string: str) -> str: def _exprs_multiple_parents(typed_expr: TypedExprDecl) -> list[TypedExprDecl]: - """ - Returns all expressions that have multiple parents (a list but semantically just an ordered set). - """ + """Return multiply-parented expressions in deterministic preorder for stable synthetic let names.""" parent_counts: dict[TypedExprDecl, int] = {} traversal_order: list[TypedExprDecl] = [] traversed: set[TypedExprDecl] = set() diff --git a/python/tests/test_high_level.py b/python/tests/test_high_level.py index 94fc71f4..6d9d5e35 100644 --- a/python/tests/test_high_level.py +++ b/python/tests/test_high_level.py @@ -3,7 +3,10 @@ import importlib import math +import os import pathlib +import subprocess +import sys from collections.abc import Callable, Iterator from copy import copy from dataclasses import dataclass @@ -936,6 +939,47 @@ def pair(cls, left: DuplicateEdge, right: DuplicateEdge) -> DuplicateEdge: ... assert sum(line.endswith(" $__expr_2 $__expr_2)") for line in lines) == 1 +_DETERMINISTIC_HOISTING_SCRIPT = """ +from __future__ import annotations + +from egglog import EGraph, Expr, StringLike + + +class B(Expr): + @classmethod + def var(cls, name: StringLike) -> B: ... + + def __and__(self, other: B) -> B: ... + + def __or__(self, other: B) -> B: ... + + +egraph = EGraph(save_egglog_string=True) +x, y = B.var("x"), B.var("y") +shared = x & y +expr = shared | y +for _ in range(24): + expr = (shared & expr) | (expr & (shared | x)) +egraph.let("$e", expr) +print(egraph.as_egglog_string, end="") +""" + + +def test_shared_subexpression_lowering_is_deterministic_across_processes() -> None: + transcripts = [ + subprocess.run( + [sys.executable, "-c", _DETERMINISTIC_HOISTING_SCRIPT], + capture_output=True, + text=True, + check=True, + env={**os.environ, "PYTHONHASHSEED": str(seed)}, + ).stdout + for seed in (1, 2, 3) + ] + + assert transcripts[1:] == transcripts[:-1] + + def test_freeze_omits_synthetic_let_bindings() -> None: class FreezeLetNum(Expr): @classmethod