A real e-matcher: matching a pattern against an e-class, not a term - #1103
Merged
Conversation
…opt-in #746 tier 2's own row names two things as remaining "in dependency order": no production caller for the reversible-rule mechanism, and folding on insertion. The second is done (this workspace's `work/egraph` harness, proven against a 16-expression corpus: 7 of 16 saturating under the full rule set became 15 of 16, neutral-element churn from 13-34% to 0%). This gives the first a real, if narrowly-scoped, answer. EGraph is that harness's design moved here unchanged: e-classes over a union-find, e-nodes hash-consed by operator and child class, congruence restored by Rebuild, neutral elements folded on insertion rather than discovered later by a rule. `MatchPattern.Construct` -- until now `private`, used to build a rule's right-hand side from bindings -- is exposed as `ConstructNode` so extraction rebuilds a node's type from the same registry the rest of the pattern-matching layer already trusts, rather than a second, independently-drifting list of the same operators. `Transformation.EqualitySaturation(WorkBudget, CostModel)` is the caller: builds an e-graph from the input, fires every rule whose `RewriteRuleGrowth` is `Collects` or `Rearranges` -- withholding `Expands` and `Unknown` for the same reason, unproven is not the same as safe -- against `AngouriMath.Core.Budgets.BudgetLedger`, the same budget type Gröbner elimination already answers to, and extracts the cheapest candidate under the given `CostModel`. Nothing runs this by default, the same standing as `RationalCanonicalization` and `Canonicalization`: `Simplify` applies a rule set once and moves on, so an expanding rule and a collecting one never meet, and equality saturation deletes exactly that ordering. What this is not, stated in its own doc comment rather than left implicit: the harness this is built from enumerates a class's terms and rewrites each, which finds what e-matching would but by materialising terms a real e-matcher never builds. That instrument moved here unchanged. A production e-matcher over `MatchPattern` is not this, and tier 2 still names it as the production caller's other missing half. Nor does a 16-expression textbook corpus settle whether this generalises to what `Simplify` is actually asked to handle -- the budget is the honest acknowledgment of that, not a solved problem's formality. One test flake chased down rather than papered over: `a / b / c` rewritten to `a / (b * c)` occasionally failed a numeric equality check under `dotnet test` and never once under 2,300+ raw concurrent calls to the same code in an isolated process. The two chains are the same value reached by differently-ordered complex divisions, and comparing them by the exact equality `ExpressionNumerical.AreEqual` uses is comparing two floating-point rounding paths, not the value each settles on. Fixed by verifying against `Entity.EqualsImprecisely` -- the tolerance this library already has for exactly that comparison -- not by loosening what the transformation itself promises. TDD throughout: EGraph's union-find, hash-consing, congruence rebuild and neutral folding (all five operator cases, including the two -- `0 - x`, `1 / x` -- that must not fold) each have a test that failed for the right reason before the line that makes it pass. `PublicApi.txt` regenerated for the one new public member.
Tried the obvious move: give RewriteRule a Reversed the same way AsAddressable() already gives it a Growth. Measured against the live registry rather than assumed to work -- grep says AsAddressable() is called exactly once, for RationalizeDenominator, and every other set's addressable Rules still comes from RuleRegistryGenerator reading a switch's arms, kept around after the exchange purely for that. Wiring Reversed into AsAddressable() alone therefore changes nothing for 29 of 30 sets, and the one it does reach has two code-built, non-reversible rules -- so the change measured zero reversible rules registry-wide and was reverted rather than shipped speculative. Recorded here rather than in a commit message that stops being read: what a real fix costs (extending the generator to compute reversibility from syntax, or re-deriving Rules from AsAddressable() for every converted set and reconciling two independent renderings that have never been compared), and why RationalizeDenominator specifically is the wrong set to prototype against. Not fixed here -- estimating which option is worth its cost is a separate question from measuring that the cheap option does not exist.
…erve EGraph.Extract rebuilt every node through a bare constructor, which restores neither Entity.Codomain nor the reference identity that keeps EulerIntrinsic out of a binder over the name e -- both confirmed wrong-answer bugs, both fixed with a regression test at the EGraph level and at the public Transformation.EqualitySaturation level. The other thirteen findings from the same review are recorded in EqualitySaturationReviewFindings.md rather than fixed here: several point at the same underlying gap (the e-graph's node model has nowhere to carry metadata beyond raw tree shape), which is a design question worth its own pass rather than a patch alongside these two. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Design document for the other half PR #1101's own doc comment names as missing -- matching MatchPattern against an e-class directly, rather than enumerating a class's terms and rewriting each. Scoped by two findings made before committing to it rather than assumed: Checked against the measurement rather than assumed to help: the original motivation (letting Growth.Expands rules join SafeRules safely) does not follow from switching matchers. The harness's measured blowup happened with hash-consing and congruence closure already in place, found through term enumeration -- an expand rule mostly produces genuinely new shapes each time, so congruence closure (which catches exact repeats) does not bound it either way. This document is scoped to what e-matching actually buys -- not materialising a term to find a rule's shape -- and says so rather than quietly keeping the original framing. Checked which rules even have a MatchPattern to e-match against: most of RewriteRules.All is still RuleRegistryGenerator output -- text rendered from a switch arm's Roslyn syntax, not a MatchPattern object -- per InversePairTable.md's measurement. The real patterns live in the internal Matching.MatchedRules catalogue, so EqualitySaturationTransformation's rule source moves there, which is a same-assembly reference needing no visibility widening. Not implemented here. GatheredPattern (n-ary chain matching) is out of scope -- already "the one shape that has to be enumerated" against a single concrete Entity per its own documentation, and matching it against a class that can bundle many equivalent tree shapes has no obvious bound the way NodePattern's does. A pattern containing one anywhere falls back to today's extract-then-TryApply path.
11 TDD tasks covering EBindings, NodeCount/Growth on MatchPattern and MatchedRule, the EGraph helpers e-matching needs, CanEMatch/EMatch/ ETryBuild on all four pattern kinds, MatchedRule.TryEMatchApply, and rewiring EqualitySaturationTransformation to source from Matching.MatchedRules. Also rebases this branch onto tier2-inverse-pair-table (#1101), which EGraph.cs and EqualitySaturationTransformation only exist on. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ed witness EMatch's eligibility check only asks whether *some* e-node in the class satisfies the required type; the cost-cheapest witness it extracts for a 'where' predicate can be a different e-node of the same class entirely, and Any<T>(name, where) compiles 'where' as an unguarded cast to T. ETryBuild already guarded this with required.IsInstanceOfType(witness) before calling where; EMatch now applies the same guard, declining the candidate instead of throwing InvalidCastException. Not reachable from today's registry rules -- covered here with a hand-built adversarial cost model, since it needs a class holding two congruent representations of different types, which real EqualitySaturation unions (Tasks 10-11) will produce.
…rectly Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…r class per round
…uilds the same Adapted two of the brief's three tests against what the registry and the e-graph actually contain, probed directly rather than assumed: - EMatchingAgreesWithMatching needed a guard the brief's text did not anticipate. EGraph.Add folds a neutral-element application into its other operand on insertion (`x * 1`, `x + 0` never get a Mulf/Sumf e-node at all -- deliberate, pre-existing behaviour, not part of this plan), and EGraph.Extract can only rebuild the 14 node types MatchPattern.Construct knows how to build, so any node type outside that list anywhere in the tree (Factorial, the boolean connectives, a comparison, a set operator) makes the class unreconstructible -- a gap EqualitySaturationReviewFindings.md already records. Both are properties of the EGraph and MatchPattern.Construct that Tasks 1-2 built, not defects in the e-matching added by Tasks 5-9. Skipping a corpus row where the graph does not faithfully represent what was inserted leaves 11 of 18 rows and 69 (rule, row) pairs genuinely checked, and it is exactly those seven rows that failed before the guard existed, and no others. - EMatchingFindsAMatchThatCrossesAUnion's `.First(RequiredRootType == Mulf)` picked whichever Mulf-rooted rule came first in registry order, which does not mean it matches `2 * x` on any graph -- filtered instead for a rule that actually fires on this one. - ETryBuildAgreesWithTryBuildOnTheSameBindings's `.First(Right.CanEMatch)` followed by a corpus lookup hit the same failure mode MatchedRuleTryEMatchApplyTest already found and fixed (its own comment: "the first few such rules ... fire on none of the eighteen corpus rows"): picked a rule with no corpus row to apply to and returned early, never calling TryEMatchApply. Fixed the same way: search (rule, source) pairs together for one that fires. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ting it Review finding: the guard that skips a corpus row because the e-graph cannot faithfully represent it (neutral-element folding, or a node type outside the 14-type reconstruction whitelist) produced a plain "Passed" indistinguishable from a row that ran the full 69-pair check. A future regression widening what EGraph.Add/Extract cannot represent would make this test keep reporting "18 passed" with no signal that coverage shrank. Added an explicit, named list of the seven rows expected to hit the guard, each with its own diagnosed cause, and assert row membership when the guard fires -- so an eighth, unlisted row hitting it fails loudly instead of silently joining the pass count. Verified the assertion is load-bearing by removing one entry (`phi(12)`) and confirming the test fails with a specific message naming that row, then restoring it. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The final whole-branch review found SafeRules collapsed to 23 rules because 266 of 298 registry rules are code-built and can't be classified by node-count Growth. Decided with Rafael: extend rather than ship as-is. Tasks 12-13 add a declared-Growth mechanism for code-built rules (mirroring how Soundness is already declared, not derived) and apply it to a first, conservatively-scoped batch. Task 14 closes the remaining findings (dropped exception guard, vacuous test, false doc comment) against the real final count. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…s, correct the doc comment
- ApplyCore's e-match branch now wraps TryEMatchApply in try/catch, mirroring the
fallback branch's existing guards around TryApply/AddEntity (final review finding I2).
Traced TryEMatchApply and EGraph.Extract by hand: Extract already swallows a failing
cost model internally, and Evaled is documented and implemented to be total, so the
named rule's own when clause cannot be forced to throw with real data today -- the
live hazard is the unguarded `when(forWhen)` call itself, reproduced directly against
a throwaway rule built the way MatchedRuleGrowthTest already builds one.
- Replaced the vacuous EqualitySaturationNowDrawsFromMatchingMatchedRules test (which
passed on Parse("x + 0") even with SafeRules empty, since EGraph.Add's neutral-fold
removes it before any rule runs) with a real sin(arcsin(x)) -> x case that e-matches
and is not folded away on insertion (final review finding C1, test half).
- Added SafeRulesHasAtLeastAFloor, a kept regression test against SafeRules.Count,
exposed to the Tests assembly via a small internal accessor since the field itself is
private on a private nested class. Measured (and force-failed once to confirm): 43
rules pass the filter today; floor set to 38 (final review finding C1, measurement
half).
- Corrected EqualitySaturation's doc comment, which still said a production e-matcher
"is not this" and cited a 16-expression measurement made under a since-superseded
rule population (final review finding I7). States the real filter (Growth, derived or
declared since Task 12, and Soundness), the real count (43, of which ~27-28 can
currently build a replacement -- the remaining ~15 build a boolean connective or a
turned-around equality and are correctly classified but blocked by EGraph's 14-type
reconstruction whitelist, a separate known limitation), and that the old harness
measurement should not be read as describing this population without being re-run.
Full suite: 8874 passed, 14 skipped (pre-existing), 0 failed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The doc comment said the original work/egraph measurement was made under "a much smaller rule set" than today's 43 -- it was actually made under a much larger one (313 rules, off the public registry's string-length Growth proxy, before the Soundness filter or e-matching existed). Fixed the direction and named what actually differs. A few comments cited "final review finding C1/I2" as if a reader could look that up -- those labels only ever existed in this session's local review ledger, never shipped. Reworded to describe the issue plainly instead of pointing at an unresolvable reference, and corrected a stale "23" (the count before it grew to 24) quoted forward rather than re-measured, in a comment whose whole point is that numbers must be measured. EMatching.md's present-tense claim about which registry EqualitySaturation draws from is now past tense with a pointer to where that changed. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A real e-matcher: matching a rewrite pattern against an e-graph class directly, instead of extracting a materialized term and matching against that. This is what
Transformation.EqualitySaturation's own doc comment (#1101) named as its production caller's other missing half.Stacked on #1101 (
tier2-inverse-pair-table), which is itself open and unmerged —EGraph.csandEqualitySaturationTransformationonly exist there. Do not merge this before #1101, and retarget tomasteronce #1101 lands.Spec:
Docs/Contributing/EMatching.md. Implementation plan and full review ledger available on request (kept in a localdocs/superpowers/directory not part of this diff's substance).What this adds
CanEMatch/EMatch/ETryBuildon all fourMatchPatternkinds (AnyPattern,ExactPattern,NodePatternimplement them for real;GatheredPatterndeclares itself unable to and throws if asked anyway).EBindings, an e-class-id-valued cons-list mirroring the existingBindings.MatchPattern.NodeCountand an exact, node-count-basedMatchedRule.Growth— replacing the public registry's cruder string-length proxy for rules with two real pattern sides.Growthfor code-built rules (a rule whose replacement is a C# lambda, not a pattern) — mirroring howSoundnessis already declared rather than derived. Applied to a first, individually-justified batch of 19 rules (13CollectsinMatchedRuleSet.Boolean, 6Rearranges).MatchedRule.TryEMatchApply, orchestrating e-matching per rule: finds candidates viaLeft.EMatch, lazily materializes real bindings only when awhencondition or a non-e-matchableRightneeds them, builds viaRight.ETryBuildor the existing code-delegate path.EqualitySaturationTransformationrewired to source fromMatching.MatchedRules.All(real patterns, filtered by exactGrowthandSoundness) instead of the publicRewriteRules.All(mostly rendered text), e-matching whereLeft.CanEMatchallows and falling back to the previous extract-then-match path otherwise.What this honestly does not claim
EGraph's reconstruction whitelist doesn't cover those node types — a separate, already-documented, pre-existing limitation, not something this PR introduces or fixes. The day that whitelist widens, those 15 go live simultaneously with no intervening measurement — that's the moment to re-run thework/egraphharness, not before.Growth.Expandsrules safe to include. Unrelated question; not reopened here.EGraphlimitation (neutral-fold on insertion) and are excluded via an explicitly asserted, named list rather than silently.Review process
Every task went through implementer → independent task-level review → (where findings surfaced) a fix round and scoped re-review. The task classifying real rules with a
Growthdeclaration (real safety stakes — a wrong classification risks the unbounded e-graph memory growth this whole mechanism exists to prevent) got its own dedicated, rule-by-rule audit independently re-deriving all 19 classifications from source; none was found wrong. A whole-branch review after the first pass found one Critical issue (the rule population had silently collapsed to 23 rules with no measurement and a vacuous verification test) — closed via the declared-Growth mechanism above, a corrected verification test, a measured floor assertion, and a corrected public doc comment. A final scoped re-review confirmed the fix closed it, with one residual doc-comment wording issue (a size comparison stated backwards) left as a known, non-blocking follow-up — happy to push a one-line fix for that on request.Test plan
ETryBuildagrees withTryBuildon the same bindings.PublicApi.txtunchanged — every new member isinternal.🤖 Generated with Claude Code