Come ottenere risultati casuali da Microsoft Z3?

Question

In Microsoft Z3, quando proviamo a risolvere una formula, Z3 restituisce sempre i risultati nella stessa sequenza, quando ci sono due o più soluzioni soddisfacenti.

È possibile ottenere risultati casuali da Z3 in modo che per lo stesso input generi una sequenza di output diversa in un'esecuzione diversa.

Si noti che, sto usando API C o C#. Non sto usando Z3 usando smt2lib. Quindi, se puoi darmi un esempio di funzione API C o C# che può aggiungere randomizzazione, sarà più utile.

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) 

Tratto da here.