Add prio-queue extractor and data/constructed #37
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.
Hey everyone,
We've added a new tree-extractor that seems to outperform the other two already in this repo.
The key idea is to always pick the smallest-cost e-node (using a priority queue), which prevents that we need to re-consider other e-nodes, hence eliminating the need to do a fixpoint algorithm.
This algorithm adds each e-node at most once to the priority queue.
It should (if I've not messed anything up), have a worst-case complexity of O(n*log(n)), where n is the number of e-nodes in the e-graph.
We get a speedup of 3810ms -> 3171ms compared to faster-bottom-up on my machine.
In addition we've added the "data/constructed" data example which showcases how the previous algorithms perform in their "worst-case" (~3s), and how the priority queue algorithm is better in these cases (~0.01s).