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).
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).