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