-
Notifications
You must be signed in to change notification settings - Fork 42
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
Passing additional options to Z3 #276
Comments
JavaSMT currently has no way to pass additional parameters to Z3. |
Thanks, I'm looking forward to the new release :) |
Thanks for your patience. I do not yet have a positive message for @ThomasHaas. This is just a intermediate report. Well, the option handling in Z3 is worse than expected. I tried to guess the correct type based on Z3's own option descriptions from the solver itself. |
I see the issue with the strongly typed options. Would it be possible to allow the user to specify a type like e.g.
It's also fine if the options are just global for now (or per solver if that is easier to implement) The |
It would be really nice if we could find some simple solution to passing options Z3.
What about the solution I presented above? If you do not like the user specifying (optional) types, I think a chain of try-parse methods that identify the parameter type should work. There might at best be conflicts between
I think the per-solver config would be the best (similar to |
The configuration option file lists ways to pass additional options to the various underlying solvers, however, it does not list
Z3
.Is it possible to pass arbitrary options to
Z3
? In particular, I'm interested passingparallel.enable=true
to letZ3
use parallel solving.The text was updated successfully, but these errors were encountered: