1

我正在 Z3 中尝试枚举排序，如在 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() 函数。这只是不必要的吗？

谢谢你。

4

1 回答 1

2

  1. 每当我们创建一个新的 Z3 AST 时，n如果 的引用计数器为 0，Z3 可能会垃圾收集一个 AST。在这段有效的代码中，我们在创建任何新的 AST 之前进行包装n。当我们包装它们时，智能指针将碰撞它们的引用计数器。这就是它起作用的原因。在崩溃的那段代码中，我们 wrap ，然后在 wrap 之前创建。因此，在我们有机会创建.e_consts[0]e_consts[1]e_consts[0]e_const0e_consts[1]e_consts[1]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，如果有一个返回A对象的 C API 函数，并且在 C++ 中没有等效的函数/方法。

于 2013-03-14T15:30:45.690 回答