Z3 C API 管理 Z3_VAR_AST [英] Z3 C API manage Z3_VAR_AST

问题描述

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

I try to write a custom print for a Z3_ast of Z3 in C, but I do not know how to manage the Z3_ast_kind of Z3_VAR_AST and Z3_FUNC_DECL_AST, I only know how to print the Z3_sort of Z3_VAR_AST (Z3_get_sort), about this variable value I have no ideas ???. And about the Z3_FUNC_DECL_AST, I couldn't find any accessors can get the function name, number of parameters and the parameters. Could you guys please help me? Cheers

推荐答案

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

I suggest you take a look at the file 'python/z3printer.py' in the Z3 distribution. It defines a custom pretty printer in Python. The Z3 python API is just a layer on top of the C API. So, it should be straightforward to convert this printer in 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 中的代码将保存一个包含变量名称的堆栈.

returns the de-Brujin index for the variable. The meaning of the index is explained here: http://en.wikipedia.org/wiki/De_Bruijn_index The variable names are stored in the quantifier AST. Note that, the names are irrelevant for Z3. They are stored just to make the output nice. The code in z3printer.py will keeps a stack with the variable names.

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

Regarding Z3_FUNC_DECL_AST, it is easier to handle than Z3_VAR_AST. ASTs of this kind are actually Z3_func_decl. Then the following APIs can be used to extract the information you want:

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 使用了所有这些功能.

Again, the file z3printer.py uses all these functions.

这篇关于Z3 C API 管理 Z3_VAR_AST的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！