z3 - 如何将z3表达式转换为中缀表达式？

Question

我想将 Z3 中的 boolExpression 翻译成中缀表示。例如，有一个 z3 表达式 (>= t 3)，我想获取中缀字符串“t>=3”，是否有任何现有的 Z3 api 可以在 C# 中实现它？

Answer 1

不，官方 API 不支持以中缀表示法显示表达式。此功能可以在用于遍历表达式的 API 之上实现。Z3 Python API 实现了一个中缀打印机。实际上，它实现了两种：一种用于类似 Python 的语法，另一种用于类似 HTML 数学的语法。这些打印机的源代码包含在 Z3 发行版中。代码是用python编写的，但可以很容易地转换成任何编程语言。代码位于python\z3printer.py。