कौन सा तर्क z3 द्वारा समर्थित है?

Question

क्या z3 का समर्थन करने वाले सभी सिद्धांतों/तर्कों की पूरी सूची है? मैंने इस SMTLIB Tutorial से परामर्श लिया है जो कई तर्क प्रदान करता है, लेकिन मुझे विश्वास नहीं है कि सूची पूरी है। Z3 प्रलेखन स्वयं निर्दिष्ट नहीं करता है कि कौन से तर्क समर्थित हैं।

मैं पूछता हूं क्योंकि मेरे पास एक smt फ़ाइल है जिसे SMTLIB Tutorial (जब 'सेट-लॉजिक' के साथ निर्दिष्ट किया गया है) में किसी भी तर्क के तहत हल नहीं किया जा सकता है, लेकिन जब कोई तर्क निर्दिष्ट नहीं किया जाता है तो हल किया जा सकता है।

Answer 1

जेड 3 के लिए, मैंने प्रलेखन में ऐसी कोई सूची नहीं देखी है, लेकिन यदि आप वास्तव में जानना चाहते हैं तो आप इसे स्रोत कोड में पा सकते हैं। सूची check_logic.cpp की लाइन 65 के आसपास शुरू होती है। मैं तुम्हारे लिए सूची पार्स एक डरावना awk एक लाइनर का उपयोग कर, और (जेड 3 4.4.1 के बीच और 4.4.2) मई 20, 2016 के रूप में इस पाया:

"AUFLIA", "AUFLIRA", "AUFNIRA", "LRA", "QF_ABV", "QF_AUFBV", "QF_UFBV", "QF_AUFLIA", "QF_AX", "QF_BV", "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA", "QF_UF", "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", "QF_UFNRA", "UFLRA", "UFNIA", "UFBV", "QF_S"

आप को यह तुलना कर सकते हैं SMT-LIB 2 logics की आधिकारिक सूची।

शायद आपके लिए यह सबसे महत्वपूर्ण बात है कि आपके आवेदन के लिए "सर्वश्रेष्ठ तर्क" क्या है। ऐसा लगता है कि आपके पास बड़ी और अलग-अलग समस्याओं का सेट है जिसे आप ज़ेड 3 को जो भी रणनीति कर सकते हैं उसे लागू करने के लिए चाहते हैं। उस स्थिति में, अभी के लिए, निर्दिष्ट अनिश्चितता को छोड़ना सबसे अच्छा है। समस्या यह है कि एसएमटी-एलआईबी v2.0 में कोई सर्वव्यापी तर्क नहीं था - कुछ मानकों द्वारा सबसे बड़ा तर्क AUFNIRA था, लेकिन इसमें शामिल नहीं है, उदाहरण के लिए, बिट वैक्टर। नतीजतन, सीवीसी 4 ने एक गैर-मानक ALL_SUPPORTED तर्क पेश किया, और जब कोई तर्क निर्दिष्ट नहीं किया गया है तो Z3 समस्याओं के कुछ वर्गों के लिए सर्वश्रेष्ठ प्रदर्शन करता है। एसएमटी-एलआईबी 2.0 मानक की यह कमी एसएमटी-एलआईबी 2.5 में संबोधित की गई है, जिसे "ऑल" नामक एक नए तर्क के साथ संबोधित किया गया है। हालांकि, यह अभी तक Z3 या CVC4 द्वारा समर्थित नहीं है।

Answer 2

आप यह सुनिश्चित करने के लिए Z3 में एक तर्क निर्दिष्ट करते हैं कि Z3 एक विशेष रणनीति और इंजन का उपयोग करता है जो आम तौर पर इस तर्क में व्यक्त सूत्रों के वर्ग के लिए उपयोगी होता है। यदि कोई तर्क निर्दिष्ट नहीं है, तो Z3 डिफ़ॉल्ट मोड पर वापस आ जाता है। इस डिफ़ॉल्ट मोड से संबंधित कोई तर्क नहीं है: यह एकाधिक इंजन को एकीकृत करता है।