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

Changed Any Operator to be less Wasteful #1582

Merged
merged 6 commits into from
Jan 20, 2025
Merged

Conversation

jff-work
Copy link
Contributor

As suggested in issue:
#1552

The Any operator in Quint was evaluating a lot of statements in cases that could be skipped. I implemented the proposed solution and wrote some tests as well as reasoned about the probabilities of different statements being returned by Any, which remain the same for this implementation.
https://github.com/jff-work/quint-any-test

I'd probably run some more complicated tests before merging this.

@bugarela
Copy link
Collaborator

bugarela commented Jan 20, 2025

Hi! Thanks a lot for addressing this and documenting everything so well. I'll do some testing today - the failing tests don't mean there's anything wrong, but this does (as expected) change the way rand() is used, and therefore runs with a fixed seed will have different results under this new implementation. I just need to update the seeds in the failing tests.

Sorry for the delayed response, I was on vacation for a while. I'll get back soon with a proper review.

@bugarela
Copy link
Collaborator

I just tried this change on the (private) project where I noticed the slowdown caused by any and, for this instance, this change is a 2x speed up 🎉

Copy link
Collaborator

@bugarela bugarela left a comment

Choose a reason for hiding this comment

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

Looks great! I've updated the integration tests that relied on the seed and tested this on a couple of real projects, all seems great and the performance improved so much!

@bugarela bugarela enabled auto-merge January 20, 2025 17:36
@bugarela bugarela merged commit 9076637 into informalsystems:main Jan 20, 2025
14 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