从 Z3 C API 包装实体

Question

我正在 Z3 中试验枚举排序，如 How to use enumerated constants after calling of some tactic in Z3? 中所述，我注意到我可能对如何正确使用 C 和 C++ api 有一些误解。让我们考虑以下示例。

   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;

我希望这两种代码变体能够用智能指针很好地包装 C 实体 Z3_func_decl，以便我可以与 C++ api 一起使用，但只有第一个变体似乎是正确的。所以我的问题是

1. 第二种方法不起作用是正确的行为吗？如果是这样，我怎样才能更好地理解为什么不应该这样做的原因？

2. 未包装的 C 实体会发生什么，例如 Z3_symbol e_name - 这里我不包装它，我不增加引用。那么内存会被妥善管理吗？使用它安全吗？什么时候对象会被销毁？

3. 一个小问题：我没有看到 C++ api 中的 to_symbol() 函数。这只是不必要的吗？

谢谢。

Answer 1

1. 每当我们创建一个新的 Z3 AST 时，如果 n 的引用计数器为 0，Z3 可能会垃圾收集一个 AST n。在有效的代码段中，我们在我们之前包装了 e_consts[0] 和 e_consts[1]创建任何新的 AST。当我们包装它们时，智能指针将碰撞它们的引用计数器。 这就是它起作用的原因。在崩溃的那段代码中，我们包装e_consts[0]，然后在包装e_consts[1]之前创建e_const0。因此，e_consts[1] 引用的 AST 在我们有机会创建 e_const1 之前被删除。

   顺便说一句，在下一个正式版本中，我们将支持在 C++ API 中创建枚举类型：http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

   此更改已在夜间构建中可用。

2. Z3_symbol 不是引用计数对象。它们是持久的，Z3 维护一个包含所有已创建符号的全局表。我们应该将符号视为唯一的字符串。

3. 请注意，我们可以使用类symbol 和构造函数symbol::symbol(context & c, Z3_symbol s)。函数to_* 用于包装使用带有智能指针的C API 创建的对象。我们通常有一个函数to_A，如果有一个C API 函数返回一个A 对象，并且C++ 中没有等效的函数/方法。