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_sort（Z3_get_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 文件使用了所有这些功能。