为 Z3 的 ctx-solver-simplify 策略设置超时

Question

我是Z3新手。这是我的代码：

void timeout_c_api() {
    Z3_config  cfg;

    cfg = Z3_mk_config();
    Z3_set_param_value(cfg, "model", "true");
    Z3_set_param_value(cfg, "timeout", "1");
    Z3_global_param_set("timeout","1");

    Z3_context ctx;
    ctx = Z3_mk_context(cfg);
    auto t_params = Z3_mk_params(ctx);
    Z3_params_inc_ref(ctx, t_params);
    auto param_symbol = Z3_mk_string_symbol(ctx, "timeout");
    Z3_params_set_uint (ctx, t_params, param_symbol, 1);

    Z3_tactic tactic = Z3_mk_tactic(ctx, "ctx-solver-simplify");
    Z3_tactic_inc_ref(ctx, tactic);
    Z3_goal g = Z3_mk_goal(ctx, false, false, false);
    Z3_goal_inc_ref(ctx, g);
    Z3_ast ast;
    Z3_symbol symbols[3];
    symbols[0] = Z3_mk_string_symbol(ctx, "a");
    symbols[1] = Z3_mk_string_symbol(ctx, "b");
    symbols[2] = Z3_mk_string_symbol(ctx, "c");
    Z3_func_decl decls[3];
    auto x  = mk_int_var(ctx, "a");
    decls[0] = Z3_get_app_decl(ctx, Z3_to_app(ctx, x));
    auto y  = mk_int_var(ctx, "b");
    decls[1] = Z3_get_app_decl(ctx, Z3_to_app(ctx, y));
    auto z  = mk_int_var(ctx, "c");
    decls[2] = Z3_get_app_decl(ctx, Z3_to_app(ctx, z));
    auto thm = Z3_parse_smtlib2_string(ctx,
                                       "(declare-const a Int)\n"
                                       "(declare-const b Int)\n"
                                       "(declare-const c Int)(assert (or (and (> (+ c b) 2) (< (* (* (+ c b) c) ( * ( * ( + c -1) ( + b -1)) ( + ( + c b) -1))) 1234567)) ( and (not ( > ( + c b) 2)) ( < ( * ( * ( + c b) c) ( * ( + ( + c b) 1) b)) 1234567))))",
                                       0, nullptr, nullptr,
                                       0, symbols, decls);
    ast = Z3_ast_vector_get(ctx, thm, 0);
    Z3_goal_assert(ctx, g, ast);
    Z3_apply_result apply_result1 = Z3_tactic_apply(ctx, tactic, g);
    Z3_string z3_string = Z3_apply_result_to_string(ctx, apply_result1);
    std::cout<<z3_string<<"\n";
    Z3_goal_assert(ctx, g, ast);
}

我想为战术设置超时。正如您从我的代码中看到的那样，我尝试了几种方法来使其工作。我从官方示例中了解了 API，C++ API 如何使用 C API，以及 KLEE 如何在其源代码中设置超时。但其中 none 有效。这让我感到绝望，尤其是因为我引用了 KLEE 的实现，但它也不起作用。我的 Z3 版本是 4.8.5，在 Ubuntu amd64 上。

Answer 1

我通常使用：

Z3_global_param_set("timeout", "1000");

在上下文创建之前。

编辑：

一个可能的解决方案是使用 Z3_tactic_apply_ex (api_tactic.cpp)。

另外，我们可以使用Z3_tactic_try_for直接设置超时。

为 Z3 的 ctx-solver-simplify 策略设置超时

set timeout for Z3's ctx-solver-simplify tactic

z3