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 order of provers to reduce proof time #7

Merged
merged 1 commit into from
Jun 12, 2020

Conversation

yannickmoy
Copy link
Collaborator

Use of the tool SPAT showed that a lot of time was spend by CVC4 on some VC
that Z3 could prove easily. Changing the order was not a home run though, as
Z3 runs a long time on some VC in sparknack-utils.adb. Solution is to
special-case this unit to run the provers in the other order. On my laptop,
running time goes from 1 mn 50 s to 1 mn 3 s.

Use of the tool SPAT showed that a lot of time was spend by CVC4 on some VC
that Z3 could prove easily. Changing the order was not a home run though, as
Z3 runs a long time on some VC in sparknack-utils.adb. Solution is to
special-case this unit to run the provers in the other order. On my laptop,
running time goes from 1 mn 50 s to 1 mn 3 s.
@rod-chapman
Copy link
Owner

Does the --replay flag work reliably in Community 2020?

Copy link
Owner

@rod-chapman rod-chapman left a comment

Choose a reason for hiding this comment

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

Looks good to me. Can we re-enable the --replay flag as well now?

@rod-chapman rod-chapman merged commit b1386f0 into rod-chapman:master Jun 12, 2020
@yannickmoy
Copy link
Collaborator Author

Does the --replay flag work reliably in Community 2020?

you're referring to the crash you got with Community 2019? yes it should be gone.

Can we re-enable the --replay flag as well now?

First, you'll need to commit the Why3 session files, and then people will need to use Community 2020 for it to work. Not sure this is worth doing, given the drawbacks, especially the fact that people who use another version won't understand why it does not work at all.

@yannickmoy
Copy link
Collaborator Author

btw you could have a Makefile with a replay entry, for people who want to use replay. but not impose it in the project file. And this way people can also generate their own session files, and use replay for subsequent runs.

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