Optimal rewriting under a set of inventions

[mlb2251]

Cathy:

When Stitch does rewriting with respect to a library, and if there are multiple library functions that could be used to rewrite a given program, does it find the shortest possible rewriting? Or does it use some other method (like ordering of the library)?
I'm remembering how at some point this was just iterating over a list of inventions -- but this would make me think that we'd want to order our library in terms of most potentially compressive to shortest in order to get maximal rewriting

It assumes that you found these inventions one after another (building on each other in the usual greedy way) so it loops over the inventions, rewriting the whole set of programs with one invention after another. This is how i did it because it's how the set of programs would look if you rewrote it throughout doing search, but if you have a use case where something different is preferable then Im happy to think about how to approch that!

Actually an egraph might be a really easy way to do this optimally if you didn't need it to be too fast (which you probably don't when you're rewriting, you're fine with it taking a few seconds)

Use cases:

• finding more optimal solutions eg where a later invention lets you realize that your earlier invention could be used in a new place
• rewriting the test set or any other new set of programs
• merging multiple libraries found by compressing different subsets
• This also seems like it'd be a nice feature to have in general! A nice optimality guarantee

Approach:

• Throw the set of programs in an egraph, run dynamic rewrites that match on the ?# version of the pattern and dynamically optionally rewrite them. Note that you could directly use ?x and ?y and such to get multiuse matches directly, but I think just giving everyone unique pattern variables in a better call to account for cases like 2nd-order refinement multiuse if that gets added in the future.
• I think this would converge rather fast since every rewrite is a shrinking rewrite

[mlb2251]

I actually think bottom up would work fine with this and egraphs are unnecessary