3

z3 v 4.1 を使用しています。C++ API を使用しており、コンテキストにいくつかの配列制約を追加しようとしています。

C++ API に select 関数と sort 関数がありません。C と C++ API を混ぜてみました。C API で提供されている例array_example1()で、コンテキスト変数をZ3_Context(つまり C API) からcontext(つまり C++ API) に変更すると、「create antecedent」ステートメントでセグメンテーション違反が発生します。

void array_example1(){

context ctx; //Z3_context ctx; 
Z3_sort int_sort, array_sort;
Z3_ast a1, a2, i1, v1, i2, v2, i3;
Z3_ast st1, st2, sel1, sel2;
Z3_ast antecedent, consequent;
Z3_ast ds[3];
Z3_ast thm;

printf("\narray_example1\n");
LOG_MSG("array_example1");

//ctx = mk_context();

int_sort    = Z3_mk_int_sort(ctx);
array_sort  = Z3_mk_array_sort(ctx, int_sort, int_sort);

a1          = mk_var(ctx, "a1", array_sort);
a2          = mk_var(ctx, "a2", array_sort);
i1          = mk_var(ctx, "i1", int_sort);
i2          = mk_var(ctx, "i2", int_sort);
i3          = mk_var(ctx, "i3", int_sort);
v1          = mk_var(ctx, "v1", int_sort);
v2          = mk_var(ctx, "v2", int_sort);

st1         = Z3_mk_store(ctx, a1, i1, v1);
st2         = Z3_mk_store(ctx, a2, i2, v2);

sel1        = Z3_mk_select(ctx, a1, i3);
sel2        = Z3_mk_select(ctx, a2, i3);

/* create antecedent */
antecedent  = Z3_mk_eq(ctx, st1, st2);

/* create consequent: i1 = i3 or  i2 = i3 or select(a1, i3) = select(a2, i3) */
ds[0]       = Z3_mk_eq(ctx, i1, i3);
ds[1]       = Z3_mk_eq(ctx, i2, i3);
ds[2]       = Z3_mk_eq(ctx, sel1, sel2);
consequent  = Z3_mk_or(ctx, 3, ds);

/* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) */
thm         = Z3_mk_implies(ctx, antecedent, consequent);
printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n");
printf("%s\n", Z3_ast_to_string(ctx, thm));
prove(ctx, thm, Z3_TRUE);

}

st1また、それらを変換してst2から変換しようZ3_ASTとexprしましたが、それでもセグメンテーション違反が発生します。C++ API を使用して select と store を使用するにはどうすればよいですか?

4

1 に答える 1

2

Z3には、プッシュ/ポップと参照カウントの2つのメモリ管理モードがあります。参照カウントはずっと後に導入されました。作成に使用されるCAPIメソッドは、使用されるZ3_Contextメモリ管理モードを定義します。APIは、ポリシーが使用されるZ3_mk_contextコンテキストを作成します。push/popつまり、ASTオブジェクトは、Z3_popが呼び出されると削除されます。マッチングの間に作成されたASTオブジェクトはすべてZ3_push削除されます。このポリシーは簡単に使用できますが、アプリケーションが未使用のメモリを解放できない場合があります。APIZ3_mk_context_rc参照カウントを使用してメモリを再利用するコンテキストを作成します。これは、Z34.xの公式アプローチです。さらに、Z3 4.xで導入された新しいオブジェクト（戦術、ソルバー、目標など）は、このアプローチのみをサポートします。C ++、C＃、OCaml、またはPythonAPIを使用している場合。次に、新しい参照カウントポリシーを使用するのは非常に簡単です。一方、C APIは、Z3_*inc_refとZ3_*dec_refAPIを明示的に呼び出す必要があるため、使用が困難です。それらの1つを見逃すと、クラッシュ（例のように）またはメモリリークが発生する可能性があります。C ++ APIでは、参照カウンターを自動的に管理するいくつかの「スマートポインター」を提供しています。

に置き換えたため、例がクラッシュZ3_context ctxしますcontext ctx。クラスのコンストラクターはの代わりにをcontext使用します。c ++ディレクトリ内のファイルは、C++とCAPIを組み合わせる方法を示しています（関数を参照）。この例では、C ++スマートポインターを使用して、CAPIによって返されるCオブジェクトをラップします。Z3_mk_context_rcZ3_contextexample.cppcapi_example()

最後に、C ++ APIは、配列式を作成するために次の関数を提供しました。

inline expr select(expr const & a, expr const & i) {
    check_context(a, i);
    Z3_ast r = Z3_mk_select(a.ctx(), a, i);
    a.check_error();
    return expr(a.ctx(), r);
}
inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
inline expr store(expr const & a, expr const & i, expr const & v) {
    check_context(a, i); check_context(a, v);
    Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
    a.check_error();
    return expr(a.ctx(), r);
}
inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
inline expr store(expr const & a, int i, int v) { 
    return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range())); 
}
于 2012-10-21T06:05:21.947 に答える