问Z3 C API管理Z3_VAR_AST

EN

我建议你看看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变量名存储在量词http://en.wikipedia.org/wiki/De_Bruijn_index中。请注意，这些名称与Z3无关。存储它们只是为了使输出更好。z3printer.py中的代码将保留一个包含变量名称的堆栈。

关于Z3_FUNC_DECL_AST，它比Z3_VAR_AST更容易处理。这种类型的ASTs实际上是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使用了所有这些函数。