解決方案超時的Z3 C-API

Question

我在Linux上使用Z3 4.1 C-API。 我想爲解算器指定超時。

我正在使用以下命令，但是在命令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​​。
我找不到任何C-API的例子來在包含示例的test_capi.c文件中設置求解器超時。 任何人都可以幫忙嗎？

Answer 1

在做任何事情之前，您需要在求解器和參數上增加引用計數。 這是一段會經歷的片段。

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