CODEWITHSUNDEEP
z3
zsf222
zsf222

Reputation: 401

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

I am new to Z3. This is my code:

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);
}

I would like to set up timeout for the tactic. As you can see from my code, I have tried several ways to make it work. I got to know the APIs from the official examples, how the C++ APIs use the C APIs, and also how KLEE sets up the timeout in their source code. But none of them works. It makes me hopeless especially because I referenced the implementations of KLEE, which didn't work either. My Z3's version is 4.8.5, on Ubuntu amd64.

Upvotes: 0

Views: 168

Answers (1)

Nuno Lopes
Nuno Lopes

Reputation: 868

I usually use:

Z3_global_param_set("timeout", "1000");

before context creation.

Edit:

A possible solution is to use Z3_tactic_apply_ex (api_tactic.cpp).

Also, we can use Z3_tactic_try_for to set up timeouts directly.

Upvotes: 1

Related Questions