I am working in Z3 with extremely large formulae, so there is no way I can analyze them (indeed, printing them is hard). Thus, I would like to perform some high-level analysis using tools that Z3 may have.
Concretely, consider I have a formula phi and I perform simplify(phi). Is there any way I can measure the size of both formulae? Of course, there are different notions of size, but is there anyone built-in? I basically want to know if the application of simplify(phi) has modified the formula (since I am aware that using simplify(phi) does not guarantee anything [1,2]).
[1] How to simplify Or(Not(y), And(y, Not(x))) to Or(Not(y), Not(x)) with Z3? [2] Simplification with Z3 does not simplify as much as expected
Probes might be what you are searching for.
Probes allow for checking various measures related to a goal in Z3, and many different types of measures over the goals are implemented. [1]
Assuming you are interfacing to Z3 through the Python API, you can obtain a list of available probes through the command:
describe_probes()
Here is an example of usage of probes in Z3py:
from z3 import *
probe = Probe('num-exprs')
A, B = Bools('A B')
phi = Or(And(A, B), And(A, B))
phi_simple = simplify(phi)
print(probe(phi))
print(probe(phi_simple))
[1] https://microsoft.github.io/z3guide/docs/strategies/probes/