包装来自 Z3 C API 的实体 [英] Wrapping entities from Z3 C API

问题描述

我正在试验 Z3 中的枚举排序，如 如何在 Z3 中调用一些策略后使用枚举常量? 我注意到我可能对如何正确使用 C 和 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;

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

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. 这是第二种方法不起作用的正确行为吗?如果是这样，我如何才能更好地理解不应该这样做的原因?

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?

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

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?

一个小问题:我在 C++ api 中没有看到 to_symbol() 函数.只是没有必要吗?

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

谢谢.

推荐答案

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

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.

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

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.

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

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.

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

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++.

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