從Z3 C API的實體包裝

我正在用How to use enumerated constants after calling of some tactic in Z3?中所述的Z3中的枚舉類型進行試驗，我注意到我可能對如何正確使用C和C++ api有一些誤解。我們來考慮下面的例子。從Z3 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使用，但僅第一種變似乎是正確的。所以我的問題是

這是正確的行爲，第二種方式不起作用？如果是這樣，我怎樣才能更好地理解爲什麼它不應該？
展開的C實體會發生什麼，例如Z3_symbol e_name - 在這裏我不包裝它，我不增加引用。那麼內存管理是否正確？使用它安全嗎？什麼時候物體會被毀壞？
一個小問題：我沒有在C++ api中看到to_symbol（）函數。這只是沒有必要嗎？

謝謝。

來源

2013-03-14 Egbert

每當我們創建一個新的AST Z3，Z3可以收集垃圾的AST n如果n引用計數器爲0。在一塊的，工程的代碼，我們總結e_consts[0]和e_consts[1]我們創建任何新的AST前。當我們包裹它們時，智能指針會撞到它們的參考計數器。這就是它工作的原因。在崩潰的代碼片段中，我們換行e_consts[0]，然後在我們換行e_consts[1]之前創建e_const0。因此，在我們有機會創建e_const1之前，刪除了由e_consts[1]引用的AST。

BTW，在未來正式發佈，我們將會對C++ API創建枚舉類型支持：http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

這種變化已經可以在每晚構建。
Z3_symbol不是引用計數的對象。它們是持久的，Z3維護一個全球所有符號創建表。我們應該把符號看作獨特的字符串。
請注意，我們可以使用類symbol和構造函數symbol::symbol(context & c, Z3_symbol s)。函數to_*用於將使用C API創建的對象與智能指針進行封裝。如果有一個返回A對象的C API函數，並且在C++中沒有等價的函數/方法，我們通常會有一個函數to_A。

來源

2013-03-14 15:30:45

謝謝你的清晰解釋。我根據上次編輯更新了回覆中的常量名稱，以便更容易理解代碼。 – Egbert 2013-03-16 07:59:59

是否足夠安全地假設Z3不會垃圾收集尚未引用計數的對象，而我將逐漸包裝它們（假設我在那裏有100個枚舉常量）。正如你所說 - Z3可以在參考計數器爲零時進行垃圾收集。Z3是多線程庫的權利，所以我只是想，如果GC恰好在單獨的線程中工作，並且在我有機會包裝它們之前收集Z3_AST，即使我計劃並且不做任何新的AST :) – Egbert 2013-03-16 08:15:24

是的，我們可以假設Z3不會在我們逐漸包裝對象時收集垃圾。如果我們調用分配另一個AST的API，Z3只會垃圾收集AST。關於多線程，Z3沒有單獨的垃圾收集線程。 – 2013-03-16 15:19:21

從Z3 C API的實體包裝

回答

相關問題