माइक्रोसॉफ्ट जेड 3 से यादृच्छिक परिणाम कैसे प्राप्त करें?

Question

माइक्रोसॉफ्ट जेड 3 में, जब हम सूत्र को हल करने का प्रयास करते हैं, तो Z3 हमेशा दो या अधिक संतोषजनक समाधान होने पर परिणाम को उसी अनुक्रम में देता है।

क्या Z3 से यादृच्छिक परिणाम प्राप्त करना संभव है ताकि एक ही इनपुट के लिए, यह विभिन्न निष्पादन में विभिन्न आउटपुट अनुक्रम उत्पन्न करेगा।

कृपया ध्यान दें कि, मैं सी या सी # एपीआई का उपयोग कर रहा हूँ। मैं smt2lib का उपयोग कर Z3 का उपयोग नहीं कर रहा हूँ। इसलिए यदि आप मुझे सी या सी # एपीआई फ़ंक्शन उदाहरण दे सकते हैं जो यादृच्छिकरण जोड़ सकता है, तो यह अधिक उपयोगी होगा।

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 से लिया गया। आप की तरह बीज निर्धारित करने की आवश्यकता