"Dynamic modifiction" to standard tactics

[rainoftime]

Z3's tactic language is very flexible and powerful. However, it is a bit hard to modify the default tactics.
For example, if I want to change the behaviour of some standard tactics such as qfbv and qflia (e.g., add a sub-tactic in it, change the parameters for its sub-component, such as the solve-eqs tactic), I will have to modify the C++ code and re-compile Z3.

An available approach is to use the using command to change the parameters of the tactic. But such an approach is a bit limited.
Is there any other convenient and flexible way for modifying the default tactics? Thanks!

Maybe a possible direction is to introduce some `plugin-in system, just like the LLVM passes (e.g., we can compiler a user-defined pass as a .so file, and load the file dynamically.)