1

C APIを使用して、実行時にソルバーのタイムアウト値を変更することはできますか？タイムアウトを設定するために、以下を行うことができます-

Z3_config  cfg = Z3_mk_config();
Z3_set_param_value(cfg, "SOFT_TIMEOUT", "10000") // set timeout to 10 seconds
Z3_context ctx = Z3_mk_context(cfg);
....
Z3_check_and_get_model(ctx);
....
....
Z3_check_and_get_model(ctx);

ただし、コンテキストを保持したまま次のクエリのタイムアウトを変更したい場合、その間にタイムアウト値を変更することはできますか？

4

1 に答える 1

2

Z34.0への移行を検討してください。Z3 4.0には、ユーザーが同じZ3_contextで多くのソルバーを作成できる新しいAPIがあります。ソルバーごとに異なるタイムアウトを設定し、必要なときにいつでも更新できます。Z3 4.0には、CAPIをはるかに使いやすくするC++レイヤーも付属しています。タイムアウトを設定する短い例を次に示します。unknown私のマシンでは、1ミリ秒のタイムアウトが使用されsat、s.set(p)コマンドが削除されると、Z3が戻ります。

context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
solver s(c);

s.add(x >= 1);
s.add(y < x + 3);

params p(c);
p.set(":timeout", static_cast<unsigned>(1)); // in milliseconds
s.set(p);

std::cout << s.check() << std::endl;
于 2012-05-31T14:32:11.587 に答える