Z3py: print large formula with 144 variables

Question

I use the Z3 theorem prover and I have a large formula (114 variables). Can I print a large formula with all clauses? A normal print str(f) truncates the output, and only "..." is printed at the end, not all the clauses.

I tested print f.sexpr() and this always prints all the clauses. However only in the sexpr syntax.

Can I print all the clauses of a formula but avoid the s-expression syntax?

Note: the code example is much to small to show the problem, but posting a large formula takes too much space.

from z3 import *


C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))



f = simplify(C)

#
# PRINTING
#

# for large a formula with 114 variables, the output of str(f) gets truncated
# only "..." is displayed at the end, not all the clauses are shown
# this is printed in the format I need:
print str(f) 

# this always prints all the clauses, even for very large formulae
# here all clauses are printed, but not the format I need:
print f.sexpr()

# if you try the above two commands with a very large formula you see the difference!

Answer 1

Z3Py uses its own pretty printer for expressions. It is defined in the file src/api/python/z3printer.py. This pretty printer has several configuration parameters. You can set them using the following command:

set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

This will prevent the output to be truncated for large expressions. Remark: the Z3Py pretty printer is less efficient than the one available in the Z3 library. If performance is an issue, you should use the SMT2 format printer as suggested by Nuno Lopes.