Unable to saturate

[vitrun]

Cases as simple as :(0+0+0) are unlikely to saturate. Let's go through the process:

1. 0 + 0 matches a + a --> 2a, resulted in 2 * 0
2. 0 + 2 * 0 matches a + b * a --> (b + 1) * a, resulted in 3 * 0
3. ..., resulted in 4 * 0

and it goes on forever.

Let's ignore a + b * a --> (b + 1) * a, and consider the commutative and associative rules only. They explode the egraph too. Adding three digits:

• (0 + 1) + 2
• (1 + 0) + 2
• 2 + (0 + 1)
• 2 + (1 + 0)
• (0 + (1 + 2)
• (0 + (2 + 1)
• (1 + 2) + 0)
• (2 + 1) + 0

How can we deal with this kind of situations?

[vitrun]

Maybe we can prune those noisy 2 * 0, 3 * 0？

[0x0f0f0f]

Check this out! https://github.com/egraphs-good/egg/discussions/60

[vitrun]

@0x0f0f0f Thanks. I read it through and it clears things up.

[vitrun]

@0x0f0f0f Thanks. I read it through and it clears things up.

[0x0f0f0f]

Can close? @vitrun