z3 - Z3 C API 管理 Z3_VAR_AST

Question

我尝试在 C 中为 Z3 的 Z3_ast 编写自定义打印，但我不知道如何管理 Z3_VAR_AST 和 Z3_FUNC_DECL_AST 的 Z3_ast_kind，我只知道如何打印 Z3_VAR_AST (Z3_get_sort) 的 Z3_sort，关于我有这个变量值没有想法？？？而关于 Z3_FUNC_DECL_AST，我找不到任何访问器可以获取函数名、参数个数和参数。你们能帮帮我吗？干杯

Answer 1

我建议您查看 Z3 发行版中的文件“python/z3printer.py”。它在 Python 中定义了一个自定义的漂亮打印机。Z3 python API 只是 C API 之上的一层。所以，用 C 语言转换这台打印机应该很简单。

关于Z3_VAR_AST, 函数

unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a);

返回变量的 de-Brujin 索引。索引的含义在这里解释：http ://en.wikipedia.org/wiki/De_Bruijn_index 变量名存储在量词AST中。请注意，名称与 Z3 无关。它们被存储只是为了使输出更好。中的代码z3printer.py将保留一个带有变量名称的堆栈。

对于Z3_FUNC_DECL_AST，它比 更容易处理Z3_VAR_AST。这种 AST 实际上是Z3_func_decl. 然后可以使用以下 API 来提取您想要的信息：

Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d);

Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d);

unsigned Z3_API Z3_get_domain_size(__in Z3_context c, __in Z3_func_decl d);

unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d);

Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i);

同样，该文件z3printer.py使用了所有这些功能。