Limiting saturation based on the cost function

[ckaran]

I just discovered egg this morning and read through the tutorials quickly and skimmed the docs, but I didn't see if there is a way of limiting the rewrite search based on the cost function. As I currently understand it, egg will always go to full saturation, meaning that by the time the Runner is done the e-graph will contain all possible rewrites of a given term. However, there are times when I can tell that if a term contains a given sequence of rewrite rules that it will already be more costly to use than some other rewrite, and so there's no point in exploring further. In essence, I want to treat e-graph as a highly compressed tree, do a breadth-first search, and as soon as any path becomes expensive enough, stop searching through any tree rooted at that node. My hope is that will be somewhat more efficient that exploring the entire search space, and then extracting the best result at the very end.

(BTW, I'm not a language or compiler guy, so if I'm using incorrect terminology, I apologize. I hope that the gist of what I'm trying to do make sufficient sense to you)

[pavpanchekha]

Typically users of egg do not run it to saturation—because that typically takes a long time, or even because they are using a set of rewrite rules where saturation never happens. (That's the situation in Herbie.) Instead you just run it for a while and extract the best when you stop. Since egg can handle pretty large e-graphs (like, about a million nodes?) that might be good enough for you.

The idea of targeting rewrites based on cost is still interesting, it just probably isn't necessary for your use case!

[ckaran]

OK, but if I understand egg's search algorithm correctly, it doesn't have a method of optimizing its search based on cost, correct? It just keeps applying rewrite rules until it hits a time out or reaches saturation, without regards to the costs of the graphs that have already been explored, correct? If you hit the timeout first, then all you're guaranteed is that you'll get the best of the graphs you've explored.

I'm hoping to figure out something that is more guided than that. Ideally, I'd like to figure out something equivalent to the idea of Dijkstra's algorithm or A*, so that the next rewrite rule that is explored is the one most likely to improve the current best rewrite. How to do this is a question I have no answer to. I don't even know if it's possible. At this point, I just want to know if egg will permit me to try to do it.

[pavpanchekha]

I think this would be pretty doable if you really wanted to do it—make your cost function into an analysis, so that it is computed at the end of every iteration, and then apply fewer matches to higher-cost nodes or something like that. Moreover, something like this has to account for the effectiveness of the extract-and-reexpand that many folks have applied with egg. We haven't ever done it, exactly, but there's good reason to think it would be effective for some problem.

[ckaran]

OK, once I get my other projects under control, I'll give it a shot. No promises on when that will happen though, too many projects going on!