本文介绍了用于求解器超时的 Z3 C-API的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我在 Linux 上使用 Z3 4.1 C-API.我想为求解器指定超时时间.
I am using Z3 4.1 C-API on linux.I want to specify a timeout for a solver.
我正在使用以下命令,但是在命令 Z3_solver_set_params() 中出现分段错误.
I am using following commands, however I get a segmentation fault in the command Z3_solver_set_params().
Z3_context ctx = mk_context();
Z3_solver s = Z3_mk_solver(ctx);
Z3_params params = Z3_mk_params(ctx);
Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");
Z3_params_set_uint(ctx, params, r, static_cast<unsigned>(10));
Z3_solver_set_params(ctx, s, params);
我似乎没有正确使用 API.
我在包含示例的 test_capi.c 文件中找不到任何 C-API 示例来设置求解器超时.有人可以帮忙吗?
It seems that I am not using APIs correctly.
I couldn't find any example for C-APIs to set a solver timeout in test_capi.c file containing examples.Can anyone help?
推荐答案
在执行任何其他操作之前,您需要增加求解器和参数的引用计数.这是将要经历的片段.
You need to increment reference counts on the solver and parameters before doing anything else.Here is a snippet that will go through.
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
{
Z3_params params = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, params);
{
Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");
Z3_params_set_uint(ctx, params, r, 10);
Z3_solver_set_params(ctx, s, params);
Z3_params_dec_ref(ctx, params);
}
}
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
这篇关于用于求解器超时的 Z3 C-API的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!