[Question]: How to know strategy to solve given formula?

[hagozaebii]

hello

As far as I know, there are various heuristics for solving formulas in z3, and I know that these are applied appropriately to the formula. These are expressed through a language called tactic, and the final sequence of heuristics used is known to be called strategy. I'm curious about the following:

1. Is there a way to see the strategy used when solving the formula in z3?
2. Is there a way to identify the heuristic being used while solving the formula in z3 in runtime?

Thanks for reading.

[NikolajBjorner]

1. Current approach: Use verbose output "-v 10" to list strategies used when a formula is solved.
2. This seems open ended. Statistics give some lens into it.

[hagozaebii]

@NikolajBjorner Thanks for your kindness. However, I still have a question. If you are okay, could you let me know something more?
I wanna know what strategy is used for solving formula in z3py. Is there any method to do?