Microsoft Z3からランダムな結果を得るには？

Question

Microsoft Z3では、数式を解こうとするとき、Z3は満足できる解が2つ以上ある場合、常に同じシーケンスで結果を返します。

Z3からランダムな結果を得ることができるので、同じ入力に対して異なる実行で異なる出力シーケンスが生成されます。

私はCまたはC＃APIを使用しています。私はsmt2libを使ってZ3を使っていません。したがって、ランダム化を追加できるCまたはC＃API関数の例を私に与えることができれば、より有用になります。

Answer 1

(set-option :smt.arith.random_initial_value true) 
(declare-const x Int) 
(declare-const y Int) 
(assert (> (+ x y) 0)) 
(check-sat-using (using-params qflra :random_seed 1)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 2)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 3)) 
(get-model) 

出所：here。