z3 - 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++ 中执行此操作的帖子：

• 在 C/C++ 中遍历 Z3_ast 树

这是一个使用 C# 的示例

• 有没有办法通过 API 查询或访问 Z3 表达式的结构

这是一篇相关文章，展示了如何在 Python 中使用这些 API：

• 读取 Z3 文件