Unable to saturate
vitrun opened this issue · 5 comments
vitrun commented
Cases as simple as :(0+0+0) are unlikely to saturate. Let's go through the process:
0 + 0matchesa + a --> 2a, resulted in2 * 00 + 2 * 0matchesa + b * a --> (b + 1) * a, resulted in3 * 0- ..., 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) + 22 + (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 commented
Maybe we can prune those noisy 2 * 0, 3 * 0？
0x0f0f0f commented
Check this out!
egraphs-good/egg#60