-
Notifications
You must be signed in to change notification settings - Fork 63
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
Set timeout on the fly, using command line interface #18
Comments
There is currently no such feature implemented in the SMT2 front-end. However, we can add this feature in the future via the terminate function callbacks in the SMT2 front-end. |
Thank you very much for your quick response, much appreciated! While you are at it, I'm also missing a feature to reset the solver, i.e., z3's (reset). My workflow is as follows:
However, I kind of want to avoid resetting them every time. I hope I am not asking to much. |
Can you provide a small SMT2 example for this workflow? That would be really helpful! |
Sure:
Maybe as context, I'm doing symbolic execution. However, in a multi threaded environment, i.e., I explore multiple paths simultaneously. I run multiple solver instances and tracking which solver has which symbols defined is too much of an overhead. Thus, I just cycle through the solvers, reseting them every time. |
Have you tried using push/pop instead of a reset? Or are the queries not related at all so that you always want to query a "fresh" instance of the solver? Here would be the version with push/pop:
|
Ohh yeah forgot about that mode, I tried it with z3, but performance really suffers (https://stackoverflow.com/questions/26416814/why-does-z3-check-slow-when-it-is-immediately-preceded-by-z3-push). Thanks! I will give it a try with boolector. |
Any update in the meantime? According to the help message there is the possibility of a time limit, but its an absolute timeout starting with the program execution:
It would be nice to have the ability to set a timeout which applies to commands like |
Hi @pointhi, This is definitely not an official answer, but I had a need for something like this, which ended-up with this branch: https://github.com/Boolector/boolector/compare/smtcomp19...andrewvaughanj:timeouts_for_term?expand=1 This adds:
(all values are in millis). Some important notes:
Let me know how you get on and, if it is successful, I can see about wrapping it up into an official PR. Cheers, Andrew |
I am currently in the process of migrating a project from z3 to boolector and was wondering if it offers a similar functionality to change timeout on the fly, e.g.:
I searched the API docs and found this, however, I was wondering if there is exists a comparable feature when using boolector from the command line with the smt2 flag.
The text was updated successfully, but these errors were encountered: