Z3 4.0 推入式求解器 [英] Z3 4.0 Push and Pop In Solver
问题描述
我想使用求解器针对 2 个不同的约束来验证我的问题.我为此编写了一个示例程序，其中我有一个变量 x，我想检查并获取 x = 0 和 x = 1 的模型.
I want to verify my problem using the solver for 2 different constraints. I wrote a sample program for the same, where I have a variable x which I want to check and get a model for x = 0 and x = 1.
我正在尝试在求解器中使用 Push 和 Pop.但是，我不确定如何准确地做到这一点.我已经编写了以下代码.当我尝试推送上下文并将其弹出时，我崩溃了.我不明白崩溃的原因，但它是一个段错误.即使我注释掉下面的推送和弹出指令，我仍然会崩溃.
I am trying to use Push and Pop in the Solver. However I am not sure about how to do it exactly. I have written the following code. When I try to push the context and pop it back, I get a crash. I do not understand the reason for the crash, but its a Seg Fault. Even if I comment out the push and pop instructions as below, I am still getting the crash.
有人可以指点一下解决问题吗.
Could someone please give some pointers to solve the problem.
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;
推荐答案
Z3 4.0 中的新 API 具有许多新功能.例如，它引入了几个新对象:Solvers、Goals、Tactics、Probes 等.此外，我们还为以前 API 中存在的 AST 和模型等对象引入了新的内存管理策略.新的内存管理策略基于引用计数.每个对象都有 Z3_ 和 Z3_ 形式的 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 发行版中.
The new API in Z3 4.0 has many new features. For example, it introduces several new objects: Solvers, Goals, Tactics, Probes, etc. Moreover, we also introduce a new memory management policy for objects such as ASTs and Models that existed in previous APIs. The new memory management policy is based on reference counting. Every object has APIs of the form Z3_<object>_inc_ref and Z3_<object>_dec_ref. We still support the old memory management policy for ASTs and Models. If the Z3_context is created using Z3_mk_context, then the old memory management policy is enabled for ASTs. If it is created using Z3_mk_context_rc, then Z3_inc_ref and Z3_dec_ref must be used to manage the reference counters. However, the new objects (Solvers, Goals, Tactics, etc) only support reference counting. We strongly encourage all users to move to the new reference counting memory management policy. So, all new objects only support this policy. Moreover, all managed APIs (.Net, Python and OCaml) are based on the reference counting policy. Note that, we provide a thin C++ layer on top of the C API. It "hides" all reference counting calls using "smart pointers". The source code for the C++ layer is included in the Z3 distribution.
话虽如此，您的程序崩溃是因为您没有增加对象 Z3_solver 的引用计数器.这是您程序的更正版本.我基本上将缺失的调用添加到 Z3_solver_inc_ref 和 Z3_solver_dec_ref.需要后者来避免内存泄漏.之后，我还使用 C++ API 包含了相同的程序.这要简单得多.C++ API 在 Z3 发行版的 include\z3++.h 文件中提供.示例包含在 examples\c++ 中.
That being said, your program crashes because you did not increment the reference counter of the object Z3_solver. Here is the corrected version of your program. I essentially added the missing calls to Z3_solver_inc_ref and Z3_solver_dec_ref. The latter is needed to avoid a memory leak. After it, I also included the same program using the C++ API. It is much simpler. The C++ API is provided in the file include\z3++.h in the Z3 distribution. Examples are included at 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;
这篇关于Z3 4.0 推入式求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
