【发布时间】：2013-04-15 16:24:46
【问题描述】：
有没有办法以人类可读的形式打印 AST，就像在 Python API 中一样？ 我想要类似的东西
(x = 3) ^ (f(3) > 2)
代替
(and (= x 3) (> (f 3) 2)
【问题讨论】：
-
实际上，前缀形式更像是一种“传统”的 AST 表示：它意味着运算符优先级、关联性等。
【发布时间】：2013-04-15 16:24:46
【问题描述】：
不，Z3 C/C++ API 没有此功能。 Z3 Python API 中的漂亮打印机是用 Python 实现的。它不是核心 API 的一部分。 Z3 Python 打印机在文件src/api/python/z3printer.py 中实现（参见here）。可以使用类似 C/C++ 的符号在 C/C++ 中重新实现它。
【讨论】：