Z3 API：是否可以检查 AST答案

【问题标题】：Z3 API: Is inspection of AST possibleZ3 API：是否可以检查 AST
【发布时间】：2015-12-05 03:42:24
【问题描述】：

在 Z3 中没有直接的方法来遍历已经存在的 Z3_ast 以获取表达式，这对我来说从 API 中似乎很清楚。然而，是否有一种间接的方法来例如拆分一个连词，用一个术语替换一个术语，例如通过Z3_parse_smtlib2_string 获得的Z3_ast 中的一个术语，或者作为用Z3_get_interpolant 获得的插值（这些是从 Z3 输出的，所以能够检查它们是有意义的）。

【问题讨论】：

标签： api z3 abstract-syntax-tree

【解决方案1】：

遍历是可能的，在 C API 中的函数是 Z3_get_app_num_args 和 Z3_get_app_arg。但是，这仅适用于 AST 是函数应用程序（应用程序，必要时通过 Z3_to_app 强制转换），其他 AST 类型可能没有要遍历的参数（例如，变量和数字，请参阅 Z3_ast_kind）。

【讨论】：

示例包含访问者模式。例如，在examples/c++ 下，您会找到名为“visit”的函数。 void visit(expr const & e) { if (e.is_app()) { unsigned num = e.num_args(); for (unsigned i = 0; i
谢谢，那么从其他 AST 构建的每个 AST 是否总是一个函数应用程序（例如 eq、lt、+、and）？我想这是有道理的。然后我想可以通过get_symbol（获取名称）和get_sort（获取排序）检查变量等，对吧？ @NikolajBjorner：我完全错过了一些例子。谢谢
不是，你说的都是函数式应用。其他包括数字、排序声明、函数声明、绑定（量化）变量和量化表达式（它们有一个主体，但没有参数），请参阅 Z3_ast_kind。
例如，我很困惑如何获得VAR_AST 的符号。
VAR_AST 是 de-brujin 索引的绑定变量，因此它们主要具有索引。要获取变量的名称，您需要相应的 QUANTIFIER_AST，它保存了可以通过 Z3_get_quantifier_bound_name 访问的名称列表。