search

egraphs-good / eggcc

MIT License
42 stars 8 forks source link

Context-sensitive substitution with cycle detection #390

Closed oflatt closed 6 months ago

oflatt commented 6 months ago

This PR adds new substitution rules that perform a substitution, copying all equalities to a new context. However, the main challenge is that cycles can occur when performing this copying. This PR solves the issue by detecting these cycles and unioning the two resulting contexts.

It can therefore copy over cycles to the new equivalent relation as well, and figure out when two contexts are equivalent due to cycles in the original egraph.

oflatt commented 6 months ago

I realized that the rules in this PR are not quite right I have an idea to fix it, marking as a draft for now.

oflatt commented 6 months ago

The version I just pushed seems good There may be some saturation issues lingering when you try to substitute the same thing twice

oflatt commented 6 months ago

Marked as ready- added another cyclic graph test

oflatt commented 6 months ago

@rtjoa is right on both counts. New plan:

  1. Close this PR and make a new one after loop args / func args are gone
  2. Separate substitution from making new contexts