In egraphs-good/egglog-python#397 I discovered a bug in Egglog around containers. Sometimes rules are not triggered when they should be. We can verify this by extracting a term, adding to a new e-graph, and then run the same rules and we will see we have new rewrites available.
This is what I am doing in the Python bindings to work around this for now, but it does make things slower.
Here's a small reproduction of the issue created by codex:
(sort E)
(sort VE (Vec E))
(constructor b () E)
(constructor k (E) E)
(constructor w (E) E)
(constructor l (VE) E)
(rewrite (w x) x)
(rewrite (l (vec-of (k x))) x)
(push)
(let $stuck (l (vec-of (w (k (b))))))
(run-schedule (saturate (run)))
(check (= $stuck (l (vec-of (k (b))))))
(fail (check (= $stuck (b))))
(pop)
(let $resolved (l (vec-of (k (b)))))
(run-schedule (saturate (run)))
(check (= $resolved (b)))
In egraphs-good/egglog-python#397 I discovered a bug in Egglog around containers. Sometimes rules are not triggered when they should be. We can verify this by extracting a term, adding to a new e-graph, and then run the same rules and we will see we have new rewrites available.
This is what I am doing in the Python bindings to work around this for now, but it does make things slower.
Here's a small reproduction of the issue created by codex: