CODEWITHSUNDEEP
z3z3py
bettsmatt
bettsmatt

Reputation: 33

Z3py polish notation output

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?

Upvotes: 0

Views: 288

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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++:

Here is an example using C#

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

Upvotes: 0

Related Questions