如何将Z3_ast导出为二进制以及如何搜索函数名称?

How to export a Z3_ast to binary and how to search one for func names?

本文关键字：搜索 何搜索 函数 二进制 Z3 ast      更新时间：2023-10-16

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

  • 将Z3_ast导出到二进制缓冲区
  • 搜索Z3_ast是否包含符号声明。

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

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

前段时间有一个类似的问题，你可能想看看那里的答案，至少得到一个起点：如何使用 z3 中的 arg(( 函数？

相关文章：