Z3py polish notation output

Question

The default output for z3py expression is in infix notation. Is there a option to set the output format to polish notation?

I assume there may be an option similar to set_option(html_mode=False) But haven't been able to find any supporting documentation detailing the options I can set.

Currently I am using .sexpr() to get the internal representation of the expression. But this has overhead when parsing as it contains extra information I need to filter.

Here is the example I am working with at currently http://rise4fun.com/Z3Py/BNn2

[[N ≤ 4, N ≥ 2]]

I would like it printed as <= N 4, >= N 2

Is there a option I can set to change the output of print? Or is the best approach to use the .sexpr() representation?

Answer 1

If your goal is to process the expression, then you can traverse the Z3 expression directly. It will be more efficient and less prone to errors. Here is a post that shows how to do it in C++:

• Traversing Z3_ast tree in C/C++

Here is an example using C#

• Is there a way of querying or accessing the structure of a Z3 expression via the API

Here is a related post showing how these APIs can be used from Python:

• Reading a Z3 file