Z3 4.0推送和弹出解算器

Question

我想使用解算器验证我的问题2个不同的约束.我写了一个示例程序一样,在这里我有一个变量x,我要检查,并得到一个模型x = 0和x = 1.

我试图在解算器中使用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;

Answer 1

Z3 4.0中的新API具有许多新功能.例如,它引入了几个新对象:求解器,目标,策略,探测器等.此外,我们还为先前API中存在的AST和模型等对象引入了新的内存管理策略.新的内存管理策略基于引用计数.每个对象都有表单Z3_<object>_inc_ref和的API Z3_<object>_dec_ref.我们仍然支持AST和模型的旧内存管理策略.如果Z3_context使用创建Z3_mk_context,则为AST启用旧的内存管理策略.如果使用创建Z3_mk_context_rc,然后Z3_inc_ref和Z3_dec_ref必须使用管理参考计数器.但是,新对象(Solvers,Goals,Tactics等)仅支持引用计数.我们强烈建议所有用户转到新的引用计数内存管理策略.因此,所有新对象仅支持此策略.此外,所有托管API(.Net,Python和OCaml)都基于引用计数策略.请注意,我们在C API之上提供了一个瘦C++层.它使用"智能指针""隐藏"所有引用计数调用.C++层的源代码包含在Z3发行版中.

话虽这么说,你的程序崩溃是因为你没有增加对象的引用计数器Z3_solver.这是您的程序的更正版本.我基本上添加了缺少的调用Z3_solver_inc_ref和Z3_solver_dec_ref.后者需要避免内存泄漏.之后,我还使用C++ API包含了相同的程序.它简单得多.include\z3++.hZ3发行版中的文件中提供了C++ API .例子包括在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;