1

Z3オプションで取得します-

Search heuristics:
  -rd:num     random case-split frequency (default: 2).
  -rs:num     random seed.

ランダム シードを設定する C API があるかどうか疑問に思っていますか?

次の API を使用してタイムアウトを設定します。ランダムシードに似たものはありますか?

params = Z3_mk_params(ctx);         
Z3_params_set_uint(ctx, params, Z3_mk_string_symbol(ctx, ":timeout"),  timeout);            
Z3_solver_set_params(ctx, solver, params);

ありがとう ！

4

1 に答える 1

1

パラメータの名前は:random-seed. 値もunsigned int.

そうは言っても、次の Z3 バージョン (v4.3.2) では、パラメーター設定のサポートが大幅に改善されます。改善は、 http://z3.codeplex.comunstableの(進行中の) ブランチで既に利用できます。

于 2012-12-28T16:52:25.190 に答える