Z3py波蘭表示法輸出

Question

z3py表達式的默認輸出爲中綴表示法。有沒有選擇將輸出格式設置爲波蘭語符號？

我假設可能有類似於set_option(html_mode=False)的選項但是一直沒有找到任何支持文檔詳細說明我可以設置的選項。

目前我使用.sexpr()來獲得表達式的內部表示。但是這在解析時有開銷，因爲它包含了我需要過濾的額外信息。

這裏是我與目前http://rise4fun.com/Z3Py/BNn2

[[N ≤ 4, N ≥ 2]]

我想它打印爲<= N 4, >= N 2

工作的例子有沒有我可以設置更改打印的輸出選項？ 或者是使用.sexpr()表示法的最佳方法？

Answer 1

如果您的目標是處理表達式，那麼您可以直接遍歷Z3表達式。它會更有效率，更不容易出錯。這裏展示瞭如何做到這一點的C++後：

• Traversing Z3_ast tree in C/C++

這裏使用一個例子C＃

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

下面是一個相關的帖子展示瞭如何從Python使用這些API：

• Reading a Z3 file