Wie bekomme ich zufällige Ergebnisse von Microsoft Z3?

Question

In Microsoft Z3, wenn wir versuchen, eine Formel zu lösen, gibt Z3 immer die Ergebnisse in der gleichen Reihenfolge zurück, wenn es zwei oder mehr erfüllbare Lösungen gibt.

Ist es möglich, zufällige Ergebnisse von Z3 zu erhalten, so dass es für die gleiche Eingabe unterschiedliche Ausgabesequenzen in unterschiedlicher Ausführung generiert.

Bitte beachten Sie, dass ich C oder C# API verwende. Ich benutze Z3 nicht mit smt2lib. Also, wenn Sie mir ein C oder C# API-Funktionsbeispiel geben können, das Randomisierung hinzufügen kann, wird es nützlicher sein.

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) 

Aus here übernommen.