क्या ज़ेड 3 को प्रीप्रोसेस समस्याओं के लिए इस्तेमाल किया जा सकता है?

Question

एसएमटी सॉल्वर पर नए शोध करने से कई बार इस तथ्य से बाधा आती है कि उपलब्ध समस्याओं के लिए बहुत सारी चाल और प्री-प्रोसेसिंग तकनीक की आवश्यकता होती है जो सीधे निर्णय प्रक्रियाओं से संबंधित नहीं होती हैं। ये अक्सर अप्रकाशित होते हैं या उचित रूप से कार्यान्वित करने और अनुकूलित करने के लिए समय लेते हैं, और इसके अतिरिक्त विभिन्न हलकों की तुलना और समझ को काफी मुश्किल बनाते हैं।

यह संभव एक पूर्व प्रोसेसर कि एक समस्या लेने के लिए और एक पूर्व संसाधित रूप में इसे बाहर डंप (एक है कि जेड 3 ही समस्या को हल करने का उपयोग करता है) के रूप में जेड 3 उपयोग करने के लिए है?

मुझे कोई कमांड लाइन विकल्प नहीं दिख रहा है, लेकिन मुझे लगता है कि इसे प्राप्त करने के लिए कुछ तरीके हो सकते हैं, रणनीतियों के माध्यम से, पायथन इंटरफेस के माध्यम से, या यहां तक ​​कि कुछ अतिरिक्त कोड भी लिख सकते हैं।

Answer 1

हां, Z3 को प्री-प्रोसेसर के रूप में उपयोग किया जा सकता है। आदेश apply उपयोगकर्ता को एक रणनीति लागू करने और इसे एक एसएमटी 2.0 बेंचमार्क के रूप में डंप करने की अनुमति देता है। यहाँ (भी http://rise4fun.com/Z3/eutO पर ऑनलाइन उपलब्ध) एक उदाहरण है:

(declare-const x Real) 
(declare-const y Real) 

(assert (forall ((n Real)) (or (< x n) (< n y)))) 
(assert (= (< x y) (< x 100.0))) 

(apply (then qe nnf) :print false :print-benchmark true) 

उपरोक्त उदाहरण में, QE (परिमाणक उन्मूलन) और NNF (निषेध सामान्य-फार्म) रणनीति इनपुट समस्या पर लागू होते हैं।

कुछ अतिरिक्त बिंदु:

• कई रणनीति केवल equisatisfiable परिणाम। इस प्रकार, परिणामी बेंचमार्क के लिए एक मॉडल मूल सूत्र के लिए एक मॉडल आवश्यक नहीं है। हम संबंधित "मॉडल-कनवर्टर" (विकल्प :print-model-converter true) को डंप करने के लिए Z3 से पूछ सकते हैं। मॉडल कनवर्टर मूल सूत्र के लिए मॉडल में परिणामी फॉर्मूला के लिए मॉडल को परिवर्तित करने के लिए Z3 द्वारा उपयोग किए गए चरणों को एन्कोड करता है। हालांकि, प्रिंटिंग मॉडल कनवर्टर्स के लिए कोई मानक नहीं है, और Z3 इन विवरणों को नहीं पढ़ सकता है। बेशक, हम प्रोग्रामेटिक एपीआई का उपयोग करके सबकुछ एक साथ चिपका सकते हैं।

• रणनीति का एक छोटा सा सेट उत्पादन के तहत (केवल बैठे परिणाम भरोसा किया जा सकता है) या अधिक (केवल unsat परिणाम पर भरोसा किया जा सकता है) अनुमान। वे आमतौर पर मॉडल या सबूत खोज में उपयोग किया जाता है। जब Z3 परिणामस्वरूप लक्ष्य प्रदर्शित करता है, तो यह परिणाम के साथ सूचित होगा सटीक (बैठे और असुरक्षित भरोसा किया जा सकता है)।