Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix the Herbie egraphs so make works #45

Merged
merged 1 commit into from
Nov 8, 2024

Conversation

pavpanchekha
Copy link
Contributor

I misunderstood the file format, whoops!

@pavpanchekha
Copy link
Contributor Author

@mwillsey can you review & merge this? Basically I had enodes point to eclasses instead of having enodes point to enodes. This fixes #44

@oflatt
Copy link
Member

oflatt commented Nov 8, 2024

The enode-eclass stuff keeps biting us
I wonder if we should have a separate file format for proofs instead of trying to make this one support both. Though I still like the idea of having a shared representation

@mwillsey mwillsey merged commit ca39f56 into egraphs-good:main Nov 8, 2024
2 checks passed
@mwillsey
Copy link
Member

mwillsey commented Nov 8, 2024

I like keeping node-node. It's just more flexible. You can emulate node-class on top of it, but you can't go the other way.

@oflatt
Copy link
Member

oflatt commented Nov 8, 2024

Gus ran into the issue that egraphs with cycles are not representable, though. The work-around is to keep fresh symbols in the egraph where you created the cycles in the first place

But otherwise I agree

@mwillsey
Copy link
Member

mwillsey commented Nov 8, 2024

That doesn't strike me as an inherent problem of this format, you can write down node-node cycles just fine. Put perhaps other parts are assuming some kind of acyclicity.

@oflatt
Copy link
Member

oflatt commented Nov 8, 2024

Oh I see, they just won't be grounded terms

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