Cách nhận kết quả ngẫu nhiên từ Microsoft Z3?

Question

Trong Microsoft Z3, khi chúng tôi cố gắng giải quyết một công thức, Z3 luôn trả về kết quả theo cùng trình tự, khi có hai hoặc nhiều giải pháp thỏa đáng.

Có thể nhận các kết quả ngẫu nhiên từ Z3 sao cho cho cùng một đầu vào, nó sẽ tạo ra chuỗi đầu ra khác nhau trong thực thi khác nhau.

Xin lưu ý rằng, tôi đang sử dụng API C hoặc C#. Tôi không sử dụng Z3 sử dụng smt2lib. Vì vậy, nếu bạn có thể cho tôi một ví dụ hàm C hoặc C# API có thể thêm ngẫu nhiên, nó sẽ hữu ích hơn.

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) 

Lấy từ here.