Wrapping entities from Z3 C API

问题:

I'm experimenting with enumeration sorts in Z3 as described in How to use enumerated constants after calling of some tactic in Z3? and I noticed that I might have some misunderstanding on how to use C and C++ api properly. Let's consider the following example.

   context z3_cont;
   Z3_symbol e_names[2 ];
   Z3_func_decl e_consts[2];
   Z3_func_decl e_testers[2];

   e_names[0] = Z3_mk_string_symbol(z3_cont, "x1"); 
   e_names[1] = Z3_mk_string_symbol(z3_cont, "x2"); 
   Z3_symbol e_name = Z3_mk_string_symbol(z3_cont, "enum_type");  
   Z3_sort new_enum_sort = Z3_mk_enumeration_sort(z3_cont, e_name, 2, e_names, e_consts, e_testers);

   sort enum_sort = to_sort(z3_cont, new_enum_sort);
   expr e_const0(z3_cont), e_const1(z3_cont);

/* WORKS!
   func_decl a_decl = to_func_decl(z3_cont, e_consts[0]);
   func_decl b_decl = to_func_decl(z3_cont, e_consts[1]);
   e_const0 = a_decl(0, 0);
   e_const1 = b_decl(0, 0);   
*/
   // SEGFAULT when doing cout
   e_const0 = to_func_decl(z3_cont, e_consts[0])(0, 0);
   e_const1 = to_func_decl(z3_cont, e_consts[1])(0, 0);

   cout << e_const0 << " " << e_const1 << endl;

I expected the two variants of code to nicely wrap the C entity Z3_func_decl with a smart pointer so I can use with C++ api, however only the first variant seems to be correct. So my questions are

1. Is this a correct behavior that the second way doesn't work? If so, how can I better understand the reasons of why it shouldn't?

2. What happens with unwrapped C entities, as for example Z3_symbol e_name - here I don't wrap it, I don't increment references. So will the memory be managed properly? Is it safe to use it? when the object will be destroyed?

3. A minor question: I didn't see the to_symbol() function in C++ api. Is it just unnecessary?

Thank you.

回答1:

1. Whenever we create a new Z3 AST, Z3 may garbage collect an AST n if the reference counter of n is 0. In the piece of code that works, we wrap e_consts[0] and e_consts[1] before we create any new AST. When we wrap them, the smart pointer will bump their reference counter. This is why it works. In the piece of code that crashes, we wrap e_consts[0], and then create e_const0 before we wrap e_consts[1]. Thus, the AST referenced by e_consts[1] is deleted before we have the chance to create e_const1.

   BTW, in the next official release, we will have support for creating enumeration types in the C++ API: http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

   This change is already available in the nightly builds.

2. Z3_symbol is not a reference counted object. They are persistent, Z3 maintains a global table of all symbols created. We should view symbols as unique strings.

3. Note that we can use the class symbol and the constructor symbol::symbol(context & c, Z3_symbol s). The functions to_* are used to wrap objects created using the C API with smart pointers. We usually have a function to_A, if there is a C API function that returns an A object, and there is not function/method equivalent in the C++.