search

alt-romes / hegg

Fast equality saturation in Haskell
https://hackage.haskell.org/package/hegg
BSD 3-Clause "New" or "Revised" License
75 stars 8 forks source link

Analysis that store the height #36

Closed folivetti closed 6 months ago

folivetti commented 6 months ago

Hi,

I've implemented an Analysis instance that stores the maximum height of the e-class:

instance Analysis Integer SRTree where
    makeA = evalHeight
    joinA h1 h2 = max h1 h2
    modifyA cl eg = eg

evalHeight :: SRTree Integer -> Integer
evalHeight = \case
    Bin _ e1 e2 -> 1 + max e1 e2
    Uni _ e1 -> 1 + e1
    Var _ -> 1
    Const _ -> 1
    Param _ -> 1

This doesn't work and I suspect the reason is the appearance of loops when applying saturation. But, inspecting the library code it feels like this should terminate, as I understand the first e-graph is built from the bottom of the tree to the root, storing the height information in each e-class. If I have a new e-node that will connect to an e-class creating a loop, it would simply add one to the height already stored in data.

Is there any place that it triggers a new recalculation and possibly enters a loop?

folivetti commented 6 months ago

never mind, it actually works as intended. I'm getting a weird exponential growth because of another thing. I'll investigate and let you know if I figure it out

alt-romes commented 6 months ago

@folivetti thanks for looking into it more carefully :)

In these sorts of situations, I think it is a good idea to try and shrinken the example to pinpoint what exactly is making this go wrong (e.g. by commenting out rewrite rules...) even though it is still quite complicated.

Good luck, let me know if you find a problem