Skip to content

Conversation

@pavpanchekha
Copy link
Contributor

This PR fixes a pretty major bug in Herbie, noted in #1372: Herbie has recently turned terrible at rewrites. I figured out why; it's the deduplicator. Basically, suppose we have a batch with both the expressions e1 = 1 and e2 = (1 + x) - x in it. (In fact e1 is a subexpression of e2.) Ok, well, we will prove that e2 = e1 in the rewriter. So we will construct the alt histories e1 -> e1 and also e2 -> e1. However, unfortunately, we then deduplicate by final expression, deleting the second (useful) alt and keeping only the first (dumb) one.

This PR fixes it in a fairly ham-fisted way by deduplicating less, which might mean Herbie runs for longer. But it's surely worth it.

@pavpanchekha pavpanchekha requested a review from AYadrov October 28, 2025 03:03
@pavpanchekha pavpanchekha marked this pull request as ready for review October 28, 2025 03:03
@pavpanchekha
Copy link
Contributor Author

Fun fact: the reason for the weird branch name is that I was convinced the issue was something about how the egraph is growing too fast, and was ready to do a super deep dive. And then it turns out... it's this other thing!

@pavpanchekha
Copy link
Contributor Author

Nightly results (vs main) are good but not life-changing. I still think we should merge, at least to fix #1372 but more importantly because I think this but is a big part of why Herbie does poorly without series expansion.

Copy link
Contributor

@AYadrov AYadrov left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I got it - we actually want to prune a substitution of a final in initial alt, it is too early to make any decision right after rewriting stage - we actually want to prune after reconstruct!, or, in other words, we want to prune after rewriting stage by (cons initial final) key

@pavpanchekha pavpanchekha merged commit 8d12a79 into main Oct 29, 2025
6 checks passed
@pavpanchekha pavpanchekha deleted the why-egraph-big branch October 29, 2025 02:40
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.

3 participants