z3

Question

में आंतरिक आंतरिक सॉल्वर सूत्रों को मुद्रित करना प्रमेय सिद्ध करने वाला टूल z3 एक सूत्र को हल करने में काफी समय ले रहा है, जो मुझे विश्वास है कि यह आसानी से संभालने में सक्षम होना चाहिए। Z3 पर मेरे इनपुट को बेहतर और संभवतः अनुकूलित करने के लिए, मैं आंतरिक बाधाओं को देखना चाहता था जो z3 अपनी हल करने की प्रक्रिया के हिस्से के रूप में उत्पन्न करता है। कमांड लाइन से z3 का उपयोग करते समय, मैं अपने बैक-एंड सॉल्वर के लिए जेड 3 उत्पन्न करने वाले सूत्र को कैसे प्रिंट करूं?

Answer 1

Z3 कमांड लाइन उपकरण में ऐसा विकल्प नहीं है। इसके अलावा, जेड 3 में कई सॉल्वर और प्री-प्रोसेसिंग चरण शामिल हैं। यह स्पष्ट नहीं है कि कौन सा कदम आपके लिए उपयोगी होगा। Z3 स्रोत कोड https://github.com/Z3Prover/z3 पर उपलब्ध है। जब डी 3 डीबग मोड में संकलित किया जाता है, तो यह अतिरिक्त कमांड लाइन विकल्प -tr:<tag> प्रदान करता है। इस विकल्प का चयन चुनिंदा डंप जानकारी के लिए किया जा सकता है।

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
       tout << "\nvar order:\n"; 
       display_vars(tout);); 

आदेश पंक्ति विकल्प -tr:nlsat ऊपर दिए गए निर्देश पर अमल करने जेड 3 निर्देश देगा: उदाहरण के लिए, स्रोत फ़ाइल nlsat_solver.cpp निम्नलिखित अनुदेश शामिल हैं। tout ट्रेस आउटपुट स्ट्रीम है। यह फ़ाइल .z3-trace में संग्रहीत किया जाएगा। Z3 स्रोत इन TRACE आदेशों से भरा है। चूंकि कोड उपलब्ध है, इसलिए हम कोड में अपने स्वयं के ट्रेस कमांड भी जोड़ सकते हैं।

यदि आप अपना उदाहरण पोस्ट करते हैं, तो मैं आपको बता सकता हूं कि कौन से Z3 घटक प्रीप्रोसेस और इसे हल करने के लिए उपयोग किए जाते हैं। फिर, हम चुन सकते हैं कि कौन से "टैग" हमें ट्रेसिंग के लिए सक्षम करना चाहिए।

संपादित (के बाद constraints पोस्ट किए गए थे): आपका उदाहरण मिश्रित पूर्णांक & असली nonlinear गणित में है। Z3 में नया nonlinear अंकगणित सॉल्वर (nlsat) to_int का समर्थन नहीं करता है। इस प्रकार, Z3 सामान्य उद्देश्य सॉल्वर का उपयोग आपकी समस्या को हल करने के लिए किया जाता है। हालांकि यह सॉल्वर लगभग हर चीज स्वीकार करता है, यह nonlinear असली अंकगणित के लिए भी पूरा नहीं है। इस सॉल्वर पर nonlinear समर्थन इस पर आधारित है: अंतराल विश्लेषण और ग्रोबनर आधार गणना। यह सॉल्वर फ़ोल्डर src/smt (unstable branch में) में कार्यान्वित किया गया है। अंकगणितीय मॉड्यूल theory_arith* फ़ाइलों में लागू किया गया है। एक अच्छा ट्रेसिंग कमांड लाइन विकल्प -tr:after_reduce है। यह प्री-प्रोसेसिंग के बाद बाधाओं का सेट प्रदर्शित करेगा। बाधा अंकगणितीय मॉड्यूल (theory_arith*) है।

अतिरिक्त टिप्पणी:

• समस्या एक अनिर्णनीय टुकड़ा में है: मिश्रित पूर्णांक & असली nonlinear गणित। यही है, इस खंड के लिए ध्वनि और पूर्ण सॉल्वर लिखना असंभव है। बेशक, हम एक सॉल्वर लिख सकते हैं जो अभ्यास में हमें मिलने वाले उदाहरण हल करता है। मेरा मानना ​​है कि to_int को संभालने के लिए nlsat का विस्तार करना संभव है।

• यदि आप to_int से बचते हैं, तो आप nlsat का उपयोग करने में सक्षम होंगे। समस्या nonlinear असली अंकगणित खंड में होगा। मैं समझता हूं कि यह कठिन हो सकता है, क्योंकि to_int आपके एन्कोडिंग में एक महत्वपूर्ण बात प्रतीत होता है।

• z3.codeplex.com पर "अस्थिर" शाखा में कोड "मास्टर" शाखा में आधिकारिक संस्करण की तुलना में काफी बेहतर संगठित है। मैं इसे जल्द ही "मास्टर" शाखा के साथ विलय कर दूंगा।यदि आप स्रोत कोड के साथ खेलना चाहते हैं तो आप "अस्थिर" शाखा पुनर्प्राप्त कर सकते हैं।

• "अस्थिर" शाखा एक नई बिल्ड सिस्टम का उपयोग करती है। आप ट्रेसिंग समर्थन के साथ रिलीज संस्करण बना सकते हैं। मेकफ़ाइल उत्पन्न करते समय आपको केवल -t विकल्प का उपयोग करना होगा।

अजगर स्क्रिप्ट/mk_make.py आयकर

• जब जेड 3 डिबग मोड में संकलित किया गया है, विकल्प AUTO_CONFIG=false डिफ़ॉल्ट रूप से। इस प्रकार, "रिलीज" मोड के व्यवहार को पुन: पेश करने के लिए, आपको कमांड लाइन विकल्प AUTO_CONFIG=true प्रदान करना होगा।