Passing additional options to Z3

[ThomasHaas]

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 passing parallel.enable=true to let Z3 use parallel solving.

[kfriedberger]

JavaSMT currently has no way to pass additional parameters to Z3. However, we already plan a new release soon (with the latest Z3, updated some days ago) and this looks like a simple feature request, so I will try to add this feature within the next days.

[ThomasHaas]

Thanks, I'm looking forward to the new release :)

[kfriedberger]

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. Z3 uses strict types for options, such as Boolean, UInt, Double and String. The user (and also JavaSMT) needs to call the corresponding method to set an option. Additionally, Z3 provides several methods with an option-based argument, e.g., global for the whole context, per solver or per tactic application. This makes it complex to provide a usefull and simple-to-understand interface or option in JavaSMT.

I tried to guess the correct type based on Z3's own option descriptions from the solver itself. It looks like the mentioned option 'parallel.enable' is not listed there (Z3 v4.9.1).

[ThomasHaas]

I see the issue with the strongly typed options. Would it be possible to allow the user to specify a type like e.g.

parallel.enable=(bool)true 
// Could also use different syntax to give type information.
// If no type is given, it could also try to parse the content first as bool, then as integer, then as double and finally as string.
// Or it just always defaults to string.

It's also fine if the options are just global for now (or per solver if that is easier to implement)

The parallel.enable option is automatically generated. More details can be found in this StackOverflow Thread

[ThomasHaas]

It would be really nice if we could find some simple solution to passing options Z3.

Z3 uses strict types for options, such as Boolean, UInt, Double and String.

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 ints and doubles, but then I would either force the user to specify doubles with a decimal point, e.g., 1.0 instead of 1, or just not support double-typed options (the most important option types are bool and int anyway). Another alternative could be to use a Map<String, Object> for the parameters and check the actual type of the entry via instanceof. So the user can put more than just strings.

Additionally, Z3 provides several methods with an option-based argument, e.g., global for the whole context, per solver or per tactic application.

I think the per-solver config would be the best (similar to Solver.setParams in the Z3 Java API). But for simplicity, it might also be fine to use global settings. It is not the ideal solution, but I think it is still better than having no options at all :).