क्या Z3 बाध्य डेटा संरचनाओं पर पुनरावर्ती कार्यों की संतुष्टि की जांच कर सकता है?

Question

मुझे पता है कि Z3 cannot check the satisfiability of formulas that contain recursive functions। लेकिन, मुझे आश्चर्य है कि Z3 बाध्य डेटा संरचनाओं पर ऐसे सूत्रों को संभाल सकता है। उदाहरण के लिए, मैंने सूची के अंतिम तत्व को वापस करने के लिए my Z3 program में अधिकतम दो की लंबाई और last नामक एक फ़ंक्शन को परिभाषित किया है। हालांकि, last वाले सूत्र की संतुष्टि की जांच करने के लिए कहा जाने पर Z3 समाप्त नहीं होता है।

क्या Z3 में बाध्य सूचियों पर पुनरावर्ती कार्यों का उपयोग करने का कोई तरीका है?

Answer 1

(ध्यान दें कि यह आपके अन्य प्रश्न से भी संबंधित है।) हमने Leon verifier प्रोजेक्ट के हिस्से के रूप में ऐसे मामलों को देखा। हम वहां क्या कर रहे हैं क्वांटिफायर के उपयोग से बचने और रिकर्सिव फ़ंक्शन परिभाषाओं के बजाय "अनलॉकिंग": यदि हम सूत्र में शब्द लंबाई (एलएसटी) देखते हैं, तो हम इसे एक नई समानता पेश करके लंबाई की परिभाषा का उपयोग करके विस्तारित करते हैं: लंबाई (lst) = अगर (isnil (lst)) 0 और 1 + लंबाई (पूंछ (lst))। आप इसे मैन्युअल क्वांटिफायर तत्काल प्रक्रिया के रूप में देख सकते हैं।

आप सबसे अधिक दो पर लंबाई की सूची में रुचि रखते हैं, सभी नियमों के लिए मैनुअल इन्स्टेन्शियशन कर तो यह एक बार नई सूची शब्दों के लिए और अधिक करने के लिए पर्याप्त होना चाहिए, तो जब तक आप अवधि जोड़ने के रूप में:

isCons (lst) => ((iscon (पूंछ (lst)) => isnil (पूंछ (पूंछ (lst)))

प्रत्येक सूची के लिए। अभ्यास में आप निश्चित रूप से इन समानताओं को उत्पन्न नहीं करना चाहते हैं और मैन्युअल रूप से निहितार्थ; हमारे मामले में, हमने एक प्रोग्राम लिखा है जो आवश्यक रूप से ज़ेड 3 के आसपास एक लूप जोड़ रहा है जब आवश्यक हो तो ऐसे अधिकxixi जोड़ना।

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

आप हमारे पेपर Satisfiability Modulo Recursive Programs में अधिक जानकारी प्राप्त कर सकते हैं, या मुझे यहां और अधिक देने में खुशी है।

Answer 2

आपको एसीएल 2 में अनियंत्रित सूची सूत्रों के उप-वर्ग, सुल्फा पर एरिक रीबर के काम में रुचि हो सकती है। 'उन्होंने अपने पीएचडी थीसिस में दिखाया कि कैसे सूची-उन्मुख सूत्रों की एक बड़ी श्रेणी अनोलिंग द्वारा साबित की जा सकती है कार्य परिभाषाएं और एसएटी-आधारित विधियों को लागू करना। उन्होंने इन विधियों का उपयोग करते हुए सुल्फा वर्ग के लिए निर्णायकता साबित की।

देखें, उदाहरण के लिए, http://www.cs.utexas.edu/~reeber/IJCAR-2006.pdf।