z3 - 操作 Z3 数据结构的方法？

Question

如果新的操纵公式可以满足，我想将数学函数作为输入并在使用 z3 检查之前通过算法更改值。我希望有一些我可以使用的树结构。我不想自己制作，因为我想使用现有的解析器将公式转换为 z3 格式。有这样的事吗？或者我可以操纵 SMT 2.0 公式吗？谢谢！

标签： z3z3py

Answer 1

您可以通过它的 API 使用 Z3 的 AST。SMT2 格式虽然相对简单，所以编写自己的解析器和/或序列化器并不难（它非常接近 Lisp）。