गैर-रैखिक अंकगणितीय

Question

के साथ जेड 3 प्रदर्शन हम जो भी मानते हैं उसके साथ प्रदर्शन समस्याओं में भाग ले रहे हैं जो गैर-रैखिक अंकगणितीय का व्यवहार करता है। यहां एक साधारण ठोस बूगी उदाहरण है, जब Z3 (संस्करण 4.1) के साथ सत्यापित किया गया है, इसे पूरा करने में लंबा समय लगता है (3 मिनट के क्रम में)।

const D: int; 
function f(n: int) returns (int) { n * D } 

procedure test() returns() 
{ 
    var a, b, c: int; 
    var M: [int]int; 
    var t: int; 

    assume 0 < a && 1000 * a < f(1); 
    assume 0 < c && 1000 * c < f(1); 
    assume f(100) * b == a * c; 

    assert M[t] > 0; 
} 

ऐसा लगता है कि समस्या कार्यों की एक बातचीत के कारण होता है, पूर्णांक चर पर सीमा धारणा के साथ-साथ (अज्ञात) पूर्णांक मूल्यों का गुणा। अंत में दावा साबित नहीं होना चाहिए। जल्दी से विफल होने की बजाय, ऐसा लगता है कि Z3 के पास किसी भी तरह की शर्तों को तुरंत चालू करने के तरीके हैं, क्योंकि इसकी स्मृति खपत लगभग 300 एमबी तक काफी तेजी से बढ़ती है, जिस बिंदु पर यह छोड़ देता है।

मुझे आश्चर्य है कि यह एक बग है, या फिर यह है कि जब ज़ेड 3 को उस विशेष दिशा में खोज को रोकना चाहिए, तो वर्तमान में समस्या को हल करने की कोशिश कर रहा है।

एक दिलचस्प बात यह है कि

function {:inline} f(n: int) returns (int) { n * D } 

का उपयोग करके समारोह को इनलाइन बनाता सत्यापन बहुत जल्दी समाप्त है।

पृष्ठभूमि: यह एक समस्या के लिए एक न्यूनतम परीक्षण मामला है जिसे हम अपने सत्यापनकर्ता चालीस में देखते हैं। वहां, बूगी कार्यक्रमों को एक समान प्रकार की कई धारणाओं के साथ संभावित रूप से अधिक लंबा मिलता है। अक्सर, सत्यापन बिल्कुल समाप्त नहीं होता प्रतीत होता है।

कोई विचार?

Answer 1

हां, गैर-समाप्ति नॉनलाइनर पूर्णांक अंकगणित के कारण है। जेड 3 में एक नया नॉनलाइनर सॉल्वर है, लेकिन यह "nonlinear असली अंकगणितीय" के लिए है, और केवल क्वांटिफ़ायर मुक्त समस्याओं में उपयोग किया जा सकता है जो केवल अंकगणित का उपयोग करते हैं (यानी, आपके उदाहरण में कोई अनियंत्रित फ़ंक्शन नहीं)। इस प्रकार, पुराने अंकगणित सॉल्वर का उपयोग आपके उदाहरण में किया जाता है। इस सॉल्वर को पूर्णांक अंकगणितीय के लिए बहुत सीमित समर्थन है। समस्या का आपका विश्लेषण सही है। Z3 को nonlinear पूर्णांक बाधाओं के ब्लॉक के लिए समाधान खोजने में परेशानी है। ध्यान दें कि यदि हम को f(100) * b <= a * c के साथ प्रतिस्थापित करते हैं, तो Z3 तुरंत "अज्ञात" उत्तर के साथ लौटाता है।

हम Z3 में nonlinear अंकगणितीय तर्क की संख्या को सीमित करके गैर-समाप्ति से बच सकते हैं। विकल्प NL_ARITH_ROUNDS=100 प्रत्येक Z3 क्वेरी के लिए अधिकतम 100 बार nonlinear मॉड्यूल का उपयोग करेगा। यह एक आदर्श समाधान नहीं है, लेकिन कम से कम, हम गैर-समाप्ति से बचते हैं।