Skip to content

Conversation

@pavpanchekha
Copy link
Contributor

@pavpanchekha pavpanchekha commented Nov 14, 2025

Well, this is maybe our fifth or sixth or something attempt. Frankly this shit goes back to like year 1 of the project with Alex's early simplifiers. Ten years. Fuck everything. Ok, here's the deal.

  • All of the base rules are sound. They sometimes use (sound-/ a b default) which means (/ a b) except when b is zero, then it's default instead. As far as I know there's no problems here.
  • But then I was running "unsound rules" (sound-/ a b default) → (/ a b). The idea was that putting this after all rewrites meant later rewrites couldn't exploit the resulting (/ 0 0) terms. So it was OK to add them now.
  • That's incorrect; while these terms won't be rewritten so can't cause issues that way, they can create unions between otherwise different terms. For example, 1 = (sound-/ 0 0 1) = (/ 0 0) = (sound-/ 0 0 2) = 2.
  • So, new approach: instead of rewriting sound-/ to / we rewrite in reverse, (/ a b) → (sound-/ a b 0). This is always safe by the standard definition. It doesn't actually even need to be a separate rewriting phase.
  • Then, when lowering, we ignore the final argument. Doesn't this still union the nodes? Won't (/.f64 0 0) be favored over large terms? I don't know. Hasn't happened yet. Praying. In egglog, at least, I think this all will be safe since it segregates FP and R terms.

Ok, so is that it? Is it done? No, for a few reasons. First of all, dropping the last argument unsoundly unions stuff. Still! Also I'm not even sure if that's fixable, at least in the egg encoding. But separately, it makes the results worse! A lot worse. Apparently the unsound merges nicely reduced the number of enodes, and with them gone the number of enodes has totally exploded. Or something? I'm not 100% sure.

So this PR includes a whole separate change, which I may split out if I have to, to reduce the number of nodes. Very simply, most of the nodes are added by the flip rules. Why? Very simple. Those rules fire for every addition and subtraction; those are common. But they also create new additions and subtractions, so they self-activate. And they also add a lot of nodes at once.

The obvious fix is—fire those more rarely by specifically selecting for square root terms. I'm not sure this will always be effective but it will for sure reduce the number of times these rules activate, which in term might result in more iterations run and therefore better results. We'll see.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants