Use Z3 in parallel mode

[rnbguy]

Is your feature request related to a problem? Please describe

It would be nice to expose some z3 configuration at Apalache CLI.

For one, I want to run z3 in parallel mode. This can be done via setting parallel.enable to true.

Describe the solution you'd like

This can be exposed via --tuning-options.

Eg. apalache-mc simulate --tuning-options=search.solver.z3.parallel.enable=true ...

Describe the impact on your work

Faster z3 search on multi-core machines.

[thpani]

Hi Rano, thanks for bringing this up!

Do you have any evidence that we could benefit from parallel Z3 solving?

Last time I checked, Z3's parallel support was limited to a few theories (bitvectors, iirc). Also at SMT-COMP 2021, at least for QF_Equality+(Non)LinearArith all solvers seemd to run sequentially:

• https://smt-comp.github.io/2021/results/qf-equality-lineararith-single-query
• https://smt-comp.github.io/2021/results/qf-equality-nonlineararith-single-query

[rnbguy]

My SMT knowledge is very rusty :sweat_smile: I do not know the details of z3 parallel support. Not sure I can come up with an example in TLA+ that gets transformed into the supported theories.

If you think Apalache doesn't use these theories, you can put this feature request in the backlog.

[konnov]

This should be possible now with #2990. Actually, I only manage to activate z3.sat.threads = 8. The other parallelization flags are working with the z3 CLI, but not with the Java API. Perhaps, they only work for specific logics or solver modes.