apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
441 stars 40 forks source link

Propagate z3 parameters in the tuning options #2990

Closed konnov closed 2 months ago

konnov commented 2 months ago

Closes #2315. This PR adds the ability to pass z3 tuning parameters right in the Apalache fine tuning parameters. This is a feature that we should have implemented long time ago.

The parameters are now parsed in FineTuningParser. Initially, I tried to use pureconfig. However, it is too opinionated and it needs more workarounds than it helps. Writing a trivial parameter parser is much easier than fiddling with pureconfig, e.g., propagating product hints via implicits.