How to measure size of formula in Z3?

Question

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

Answer 1

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/