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

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如何在源代码中设置超时。但它们都不起作用。它让我毫无希望，特别是因为我引用了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直接设置超时。