z3 (तर्क QF_BV)

Question

के साथ "अच्छा" असंत-कोर प्राप्त करना मैं SMTLIB 2 भाषा का उपयोग करके तर्क QF_BV में व्यक्त की गई समस्या को हल करने के लिए Z3 SMT सॉल्वर का उपयोग कर रहा हूं।

मॉडल असंतुष्ट है, और मैं सॉल्वर को असुरक्षित कोर बनाने की कोशिश कर रहा हूं।

मेरे मॉडल में कई 'अनिवार्य' बाधाएं हैं, जिन्हें मैं assert कथन का उपयोग करके निर्दिष्ट करता हूं।

असर-कोर पीढ़ी के लिए जिन विचारों पर विचार करना है, उन्हें (assert (! (EXPR) :named NAME)) निर्माण का उपयोग करके निर्दिष्ट किया गया है।

जेड 3 मुझे उम्मीद के अनुसार unsat देता है। हालांकि, ज़ेड 3 हमेशा एक 'तुच्छ' असंतुलित कोर को डंप करने लगता है जिसमें सभी नामांकित दावे शामिल हैं।

मुझे पता है कि मेरे नामित दावों का एक सबसेट मौजूद है, जो एक असुरक्षित कोर है। मुझे यस एसएमटी सॉल्वर का उपयोग करके यह कोर मिला, जो अक्सर मुझे अपेक्षाकृत छोटे असुरक्षित कोर देता है। यिस मॉडल जेड 3 मॉडल के समान है (एसएमटी 2 से यिस इनपुट भाषा में बहुत अधिक लाइन-दर-लाइन अनुवाद)।

"अच्छा" असुरक्षित-कोर एक सॉल्वर-विशिष्ट सुविधा का उत्पादन कर रहा है, या क्या कोई सामान्य सुझाव/परिवर्तन है जो मैं Z3 को बेहतर कोर देने में मदद करने के लिए कर सकता हूं?

Answer 1

Z3 और Yices 1.x असतत कोर की गणना के लिए एक ही दृष्टिकोण का उपयोग करें। उन सभी दावों को ट्रैक करें जिन्हें असंतोष के प्रमाण में उपयोग किया गया था। हालांकि, प्रत्येक प्रणाली द्वारा निर्मित सबूत काफी अलग हो सकते हैं। Z3 और Yices द्वारा प्रदान की गई क्षमताओं के शीर्ष पर न्यूनतम असतत कोर की गणना करने के लिए एल्गोरिदम हैं। यहां एक reference है।

संपादित करें: डिफ़ॉल्ट रूप से, Z3 समस्या को हल करने का प्रयास करने से पहले कई प्री-प्रोसेसिंग चरणों का उपयोग करता है। इनमें से कुछ कदम असंतुलित कोर की पीढ़ी को प्रभावित कर सकते हैं। विशेष रूप से, यह समस्या में समीकरणों का उपयोग कर स्थिरांक को समाप्त करता है। हम कहते हैं कि Z3 समीकरणों को हल करता है और चर को खत्म करता है। आपके script में, आप इस चरण को अक्षम करके एक छोटा कोर प्राप्त कर सकते हैं। हम इसे

(set-option :auto-config false) 

Z3 का उपयोग करके पूरा कर सकते हैं एक बहुत ही सामान्य विन्यास निष्पादित करेगा। बिट वेक्टर समस्याओं के लिए यह आम तौर पर एक अच्छा विचार है निष्क्रिय करने के लिए "relevacy प्रसार":

(set-option :relevancy 0) 

अंत में, हम अब सक्षम कर सकते हैं/चर उन्मूलन कदम, अक्षम और unsat कोर आकार पर प्रभाव देखते हैं।

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2 
(set-option :solver false) ;; Z3 will generate the core C1 C2