3

2 つの異なる制約に対してソルバーを使用して問題を検証したいと考えています。同じサンプルプログラムを作成しました。変数 x があり、チェックしてモデルを取得したいx = 0x = 1.

Solver で Push と Pop を使用しようとしています。ただし、正確に行う方法についてはわかりません。次のコードを書きました。コンテキストをプッシュしてポップバックしようとすると、クラッシュします。クラッシュの理由はわかりませんが、Seg Fault です。以下のようにプッシュとポップの指示をコメントアウトしても、まだクラッシュします。

誰かが問題を解決するための指針を教えてください。

Z3_config cfg;
Z3_context ctx;
Z3_solver solver;
Z3_ast x, zero, one, x_eq_zero, x_eq_one;

cfg                = Z3_mk_config();
ctx                = Z3_mk_context(cfg);
Z3_del_config(cfg);
solver = Z3_mk_solver((Z3_context)ctx);

x           = mk_int_var(ctx, "x");
zero        = mk_int(ctx, 0);
one         = mk_int(ctx, 1);
x_eq_zero     = Z3_mk_eq(ctx, x, zero);
x_eq_one     = Z3_mk_eq(ctx, x, one);

//Z3_solver_push (ctx,  solver);

Z3_solver_assert(ctx, solver, x_eq_zero);
printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));

printf("%s \n", Z3_ast_to_string(ctx, x_eq_zero));

int result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));

// Z3_solver_pop (ctx, solver, 1);
// printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));
Z3_solver_assert(ctx, solver, x_eq_one);
result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));
return 0;
4

1 に答える 1

6

Z3 4.0 の新しい API には、多くの新機能があります。たとえば、ソルバー、ゴール、タクティクス、プローブなど、いくつかの新しいオブジェクトが導入されています。さらに、以前の API に存在していた AST やモデルなどのオブジェクトの新しいメモリ管理ポリシーも導入されています。新しいメモリ管理ポリシーは、参照カウントに基づいています。すべてのオブジェクトには、 と の形式の API がありZ3_<object>_inc_refますZ3_<object>_dec_ref。AST とモデルの古いメモリ管理ポリシーは引き続きサポートされます。を使用してZ3_contextを作成するZ3_mk_contextと、古いメモリ管理ポリシーが AST に対して有効になります。を使用して作成された場合Z3_mk_context_rcZ3_inc_refおよびZ3_dec_ref参照カウンターを管理するために使用する必要があります。ただし、新しいオブジェクト (ソルバー、ゴール、タクティクスなど) は参照カウントのみをサポートします。すべてのユーザーが、新しい参照カウント メモリ管理ポリシーに移行することを強くお勧めします。したがって、すべての新しいオブジェクトはこのポリシーのみをサポートします。さらに、すべてのマネージ API (.Net、Python、および OCaml) は、参照カウント ポリシーに基づいています。C API の上に薄い C++ レイヤーを提供することに注意してください。「スマートポインター」を使用して、すべての参照カウント呼び出しを「隠します」。C++ レイヤーのソース コードは、Z3 ディストリビューションに含まれています。

そうは言っても、 object の参照カウンターをインクリメントしなかったため、プログラムがクラッシュしますZ3_solver。これがあなたのプログラムの修正版です。基本的に、不足している呼び出しをZ3_solver_inc_refおよびに追加しましたZ3_solver_dec_ref。後者は、メモリ リークを回避するために必要です。その後、C++ API を使用した同じプログラムも含めました。それははるかに簡単です。C++ API はinclude\z3++.h、Z3 ディストリビューションのファイルで提供されます。に例が含まれていexamples\c++ます。

Z3_config cfg;
Z3_context ctx;
Z3_solver solver;
Z3_ast x, zero, one, x_eq_zero, x_eq_one;

cfg                = Z3_mk_config();
ctx                = Z3_mk_context(cfg);
Z3_del_config(cfg);
solver = Z3_mk_solver((Z3_context)ctx);
Z3_solver_inc_ref(ctx, solver);

x           = mk_int_var(ctx, "x");
zero        = mk_int(ctx, 0);
one         = mk_int(ctx, 1);
x_eq_zero     = Z3_mk_eq(ctx, x, zero);
x_eq_one     = Z3_mk_eq(ctx, x, one);

//Z3_solver_push (ctx,  solver);

Z3_solver_assert(ctx, solver, x_eq_zero);
printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));

printf("%s \n", Z3_ast_to_string(ctx, x_eq_zero));

int result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));

// Z3_solver_pop (ctx, solver, 1);
// printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));
Z3_solver_assert(ctx, solver, x_eq_one);
result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
// printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));
Z3_solver_dec_ref(ctx, solver);
return 0;

C++ バージョン

context c;
solver  s(c);
expr x = c.int_const("x");
expr x_eq_zero = x == 0;
expr x_eq_one  = x == 1;

s.add(x_eq_zero);
std::cout << "Scopes : " << Z3_solver_get_num_scopes(c, s) << "\n";
std::cout << x_eq_zero << "\n";
std::cout << s.check() << "\n";
std::cout << s.get_model() << "\n";

s.add(x_eq_one);
std::cout << s.check() << "\n";
return 0;
于 2012-06-04T14:59:42.947 に答える