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