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;

コードの 2 つのバリアントは、C エンティティ Z3_func_decl をスマート ポインターで適切にラップして、C++ API で使用できると思っていましたが、最初のバリアントだけが正しいようです。だから私の質問は

  1. これは、2 番目の方法が機能しない正しい動作ですか? もしそうなら、そうすべきではない理由をよりよく理解するにはどうすればよいですか？

  2. たとえば Z3_symbol e_name のように、ラップされていない C エンティティで何が起こるか - ここではラップせず、参照をインクリメントしません。それで、メモリは適切に管理されますか？安全に使用できますか？オブジェクトはいつ破棄されますか?

  3. ちょっとした質問: C++ API に to_symbol() 関数がありませんでした。不要なだけですか？

ありがとうございました。

4

1 に答える 1

2

  1. n新しい Z3 AST を作成するたびに、参照カウンターが 0 の場合、Z3 は AST をガベージ コレクションする可能性がnあります。動作するコードでは、新しい AST を作成する前にラップe_consts[0]します。e_consts[1]それらをラップすると、スマート ポインターはそれらの参照カウンターをバンプします。これが機能する理由です。クラッシュするコードでは、 をラップしてから、ラップする前に をe_consts[0]作成します。したがって、 によって参照される ASTは、 を作成する前に削除されます。e_const0e_consts[1]e_consts[1]e_const1

    ところで、次の公式リリースでは、C++ API での列挙型の作成がサポートされる予定です: http://z3.codeplex.com/SourceControl/changeset/b2810592e6bb

    この変更はナイトリー ビルドで既に利用可能です。

  2. Z3_symbolは参照カウント オブジェクトではありません。それらは永続的であり、Z3 は作成されたすべてのシンボルのグローバル テーブルを維持します。記号は一意の文字列と見なす必要があります。

  3. classsymbolと constructorを使用できることに注意してくださいsymbol::symbol(context & c, Z3_symbol s)。関数to_*は、C API を使用して作成されたオブジェクトをスマート ポインターでラップするために使用されます。to_Aオブジェクトを返す C API 関数がAあり、C++ に同等の関数/メソッドがない 場合、通常は関数があります。

于 2013-03-14T15:30:45.690 に答える