Z3採用C-API

在我們得到了Z3選項設置隨機種子 -Z3採用C-API

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

謝謝！

來源

2012-12-28 Raj

參數的名稱是:random-seed。該值也是unsigned int。

這就是說，下一個Z3版本（v4.3.2）將有更好的支持設置參數。這些改進已在unstable（在製品）分支http://z3.codeplex.com中提供。

來源

2012-12-28 16:52:25

只是爲了澄清，隨機種子保證我每次運行z3都會得到相同的模型？謝謝！ – rsinha

是的。 Z3應該是確定性的。給定一組輸入參數和一個平臺（例如Linux），Z3應該始終產生相同的結果。如果情況並非如此，那麼這是Z3中的一個錯誤，應該修復。我們修復了過去的錯誤。 –

回答

相關問題