如何将 Z3_ast 导出为二进制文件以及如何在其中搜索 func 名称？答案

【问题标题】：How to export a Z3_ast to binary and how to search one for func names?如何将 Z3_ast 导出为二进制文件以及如何在其中搜索 func 名称？
【发布时间】：2019-08-20 09:05:51
【问题描述】：

在我正在进行的项目中，我需要使用 Z3 C++ API 做两件事：

将 Z3_ast 导出到二进制缓冲区
如果 Z3_ast 内部包含符号声明，则搜索它。

我目前如何执行此操作：我将 Z3_ast 转换为字符串，然后在需要的地方再次加载它。搜索是通过字符串搜索完成的。我认为有一种更有效的方法来处理这个问题。 python API 解决方案也会很有帮助，因为我可以跟踪实现它的 CPP 代码。

【问题讨论】：

答案归结为“遍历 AST”：编写一个递归过程，询问一个节点类型，然后遍历其子节点（如果有）。
是的，但我想了解这种 API 是否已经存在，或者我是否需要重新编译源代码并忍受代码分歧。
有一些访问器函数可以在 AST 节点上进行探查，但您必须自己编写 AST walk。 Z3 distribution 中有一个小示例可以帮助您入门。

标签： python c++ z3 symbolic-math

【解决方案1】：

执行此操作的正确方法是沿着 AST 走并挑选出节点。 Z3 API 提供了所有必要的识别器。请注意，将 AST 序列化为字符串并进行字符串搜索不仅速度很慢，而且如果他们更改表面语法的表示方式，也会非常容易出错。

前段时间有一个类似的问题，您可能想看看那里的答案以获得至少一个起点：How to use arg() function from z3?

【讨论】：

我现在明白了如何有效地搜索参数。但是如何将 Z3_AST 序列化为缓冲区？例如，我想通过网络发送 Z3_AST。走树并做我自己的序列化/反序列化似乎有点容易出错......
如果您有一个求解器对象s = Solver()，那么s.sexpr() 将为您提供其中所有约束的s 表达式渲染，您可以将其发送到您想要的任何地方。这个比较粗略，但是很有效！