установить тайм-аут для тактики ZT ctx-solver-упрощения - PullRequest
Новая
       13

установить тайм-аут для тактики ZT ctx-solver-упрощения

0 голосов
/ 18 апреля 2019

Я новичок в 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-интерфейсы из официальных примеров, как API-интерфейсы C ++ используют API-интерфейсы C, а также как KLEE устанавливает время ожидания в своем исходном коде.Но ни один из них не работает.Это делает меня безнадежным, особенно потому, что я ссылался на реализации KLEE, которые тоже не работали.Версия моего Z3 4.8.5, на Ubuntu amd64.

1 Ответ

1 голос
/ 18 апреля 2019

Обычно я использую: 

Z3_global_param_set("timeout", "1000");

перед созданием контекста.

Редактировать:

Возможное решение - использовать Z3_tactic_apply_ex ( api_tactic.cpp).

Кроме того, мы можем использовать Z3_tactic_try_for для прямой установки таймаутов.

...