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

optimize Expr.equal, cache Expr.simplify #285

Merged
merged 1 commit into from
Feb 12, 2025
Merged

Conversation

zapashcanon
Copy link
Collaborator

Thanks to hashconsing, we have the properties that e1 = e2 <=> e1 == e2, thus we can directly use phys_equal instead of checking the tag in Expr.equal.

I added a cache mechanism to Expr.simplify. As equal and hash are O(1), this is basically free.

The goal is for me to be able to call simplify a lot in Owi (even in cases where it may already have been simplified) without being afraid of re-doing too much work. It's a good way to fix the issue I'm having until we encode the simplification status in the type of expressions.

I believe we could internally optimize this further by sharing a cache between simplify and simplify_expr, but it not as trivial as it seem so I left it out for now.

I quickly checked on Owi and did not find any performance regression with this (and also no improvement but that's because I'm not going simplify that much for now, and because I probably don't have a lot of expressions appearing many times).

@filipeom
Copy link
Member

Thanks! 😃

@filipeom filipeom merged commit 9805061 into formalsec:main Feb 12, 2025
5 checks passed
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