2

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 を正しく使用していないようです。
サンプルを含む test_capi.c ファイルで、C-API がソルバーのタイムアウトを設定する例を見つけることができませんでした。誰でも助けることができますか？

4

1 に答える 1

5

他の処理を行う前に、ソルバーとパラメーターの参照カウントをインクリメントする必要があります。これが通過するスニペットです。

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);
于 2012-08-31T02:23:42.820 に答える