Z3 4.0 推入式求解器

Question

我想使用求解器针对 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;

Answer 1

Z3 4.0 中的新 API 具有许多新功能。例如，它引入了几个新对象：Solvers、Goals、Tactics、Probes 等。此外，我们还为以前 API 中存在的 AST 和模型等对象引入了新的内存管理策略。新的内存管理策略基于引用计数。每个对象都有Z3_<object>_inc_ref 和Z3_<object>_dec_ref 形式的API。我们仍然支持 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 包含了相同的程序。它要简单得多。 C++ API 在 Z3 发行版中的文件 include\z3++.h 中提供。示例包含在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;