CODEWITHSUNDEEP
z3z3py
lllllllllllll
lllllllllllll

Reputation: 9140

How to print out the whole symbolic expression in Z3?

I am using Z3Py for some analysis task, and for many times, I would like to print out the symbolic expression. For example,

a = BitVecVal("test", 32) + 13
print a

However, I find that once the Z3 expression becomes quite large, it just cannot be print out fully. Instead, the "ellipsis" will be used quite often to simplify the expression...

So here is my question, how can I fully print out a Z3 expression? Is there any specific API I could leverage?

Upvotes: 0

Views: 1062

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The most scalable way is to use the SMT-LIB printer. For example:

 x = Int('x')
 for i in range(12):
    x = x + x

 print x.sexpr()

will print:

(let ((a!1 (+ (+ (+ x x) (+ x x)) (+ (+ x x) (+ x x)))))
(let ((a!2 (+ (+ (+ a!1 a!1) (+ a!1 a!1)) (+ (+ a!1 a!1) (+ a!1 a!1)))))
(let ((a!3 (+ (+ (+ a!2 a!2) (+ a!2 a!2)) (+ (+ a!2 a!2) (+ a!2 a!2)))))
  (+ (+ (+ a!3 a!3) (+ a!3 a!3)) (+ (+ a!3 a!3) (+ a!3 a!3))))))

You can control parameters on the formatter used by the pretty printer using the function 'set_pp_option'. You would have to look in the source code of z3printer.py to determine which options would do the trick.

Upvotes: 1

Related Questions