Improving the extractor - #956
Draft
yihozhang wants to merge 4 commits into
Draft
Conversation
…rd loop The extractor re-scanned every reachable function table on each Bellman-Ford pass through the bridge's for_each machinery, and looked up per-sort cost/topo maps by string name for every child of every row. Materialize each function's non-subsumed rows once per extractor build, resolve each child column's handling (eq/container/base) up front, and index the per-sort maps by a dense id. Relaxation order is unchanged, so extraction results are identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Track a version counter per eq sort, bumped on every cost update, and snapshot each function's dependency-sort versions just before its rows are relaxed. A function whose dependency sorts (eq children, plus eq sorts reachable inside container children) are unchanged since its last visit recomputes identical costs for every row, so it is skipped without altering the relaxation trace — topo ranks and extracted terms are byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replace the function-level dependency gate with row-level tracking: a reverse index maps each (sort, value) an extractable row reads — eq children plus eq values nested inside container children — to the rows reading it, and each cost update marks only those rows dirty. Sweeps visit dirty rows in the same (function, row) order as the naive passes, so the update trace, topo ranks, and extracted terms are unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
An extract command built a fresh Extractor — recomputing every cost via Bellman-Ford — even when nothing changed since the previous extract, which dominates programs that extract many roots after a run. Cache the extractor's data on the EGraph, keyed by root sort and a fingerprint of all backend table versions (any merged mutation, including union-find changes, alters some table's version). The cache deliberately clones empty so push/pop don't carry cost tables. Co-Authored-By: Claude Fable 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.
The extractor PR bundles four performance optimizations to the extractor's Bellman-Ford cost computation, all guaranteed to leave extraction results byte-identical:
In short: build cheaper (1), relax less (2, 3), and rebuild less often (4).