c++ - 使用 C API 漂亮地打印 Z3

Question

有没有办法以人类可读的形式打印 AST，就像在 Python API 中一样？我想要类似的东西

(x = 3) ^ (f(3) > 2)

代替

(and (= x 3) (> (f 3) 2)

Answer 1

不，Z3 C/C++ API 没有此功能。Z3 Python API 中的漂亮打印机是用 Python 实现的。它不是核心 API 的一部分。Z3 Python 打印机在文件中实现src/api/python/z3printer.py（参见此处）。可以使用类似 C/C++ 的符号在 C/C++ 中重新实现它。