Skip to content

Conversation

@FTRobbin
Copy link
Collaborator

@FTRobbin FTRobbin commented May 22, 2025

This PR implements extraction as a top-level command in the frontend. It uses the default additive tree cost model and can only be triggered through (extract [term] [variant]).

Implementation overview:

  • Extract as an action has been removed.
  • query-extract as a top-level command has also been removed.
  • Extract is now a Command and is interpreted in the frontend run_command. Extract first runs two backend queries to resolve the eclass and the number of variants to be extracted and then calls ExtractorAlter to perform the extraction.
  • ExtractorAlter first needs to be initialized by passing the list of rootsorts to be extracted. It computes all relevant costs using Bellman-Ford and remembers the necessary information for reconstruction in this step. Then, it can be queried multiple times to reconstruct the terms in termdags. It does not hold a reference to EGraph, so it can be reused as long as the relevant tables do not change.
  • As an optimization, in the initialization step, ExtractorAlter first performs a BFS on the sorts to filter out tables unreachable from the root sort.
  • In the Bellman-Ford loop, it calls inner_sorts and inner_values on the sorts to unpack containers and calls the cost model for primitive, container, and function costs.
  • After Bellman-Ford finds a fixpoint, ExtractorAlter enumerates all rows again to copy information for reconstruction. Ties are broken arbitrarily.
  • For extracting a single lowest-cost term, it recursively reconstructs the lowest-cost enode for each eclass used in the lowest-cost enode of the root eclass and writes into a TermDag struct.
  • For extracting multiple "diverse" variants, it extracts the multiple enodes of the root eclass, in the order of lowest costs, using a single lowest-cost enode for other classes.

Additional remarks:

  • This implementation does not involve concurrency control or tunneling between the frontend and the backend, so the code logic is simplified compared to Extract action for the new backend #562.
  • This new architecture potentially allows extraction to be used more easily from RustAPI.
  • This implementation opens up the possibility of reusing extractor results, potentially subsuming Reuse Extractor whenever possible #563 after the new backend merge.
  • A caveat is that there is no easy way to port the old Extractor to this new architecture. So, no extraction in the old backend after this PR.

@FTRobbin FTRobbin changed the title Implement extraction as a top-level command in the frontend Extraction as a top-level command in the frontend for the new backend May 22, 2025
@FTRobbin FTRobbin marked this pull request as ready for review May 22, 2025 00:48
@FTRobbin FTRobbin requested a review from a team as a code owner May 22, 2025 00:48
@FTRobbin FTRobbin requested review from saulshanabrook and removed request for a team May 22, 2025 00:48
@FTRobbin FTRobbin requested review from oflatt and removed request for saulshanabrook May 22, 2025 00:48
Copy link
Collaborator

@Alex-Fischman Alex-Fischman left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not reviewed the actual extraction algorithm. My comments are about style and software engineering.

Copy link
Member

@oflatt oflatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

did a quick and rough review

Copy link
Member

@oflatt oflatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nice!

Copy link
Member

@oflatt oflatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oops, saw an opportunity

Copy link
Member

@oflatt oflatt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

never mind, the external function is necessary

@Alex-Fischman Alex-Fischman self-requested a review May 22, 2025 23:21
Copy link
Collaborator

@Alex-Fischman Alex-Fischman left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All of my comments have been resolved

@FTRobbin FTRobbin merged commit 41b3505 into backend-merge May 22, 2025
4 of 8 checks passed
@Alex-Fischman Alex-Fischman deleted the no_action_extraction branch May 22, 2025 23:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

6 participants