Z3 C API manage Z3_VAR_AST

Question

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

Answer 1

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.

Regarding Z3_VAR_AST, the function

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

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.

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);

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