Z3_ast संदर्भ Z3 के बाहर गिनती संदर्भों की गणना करता है?

Question

जेड 3 में 2 मोड हैं: स्वचालित संदर्भ गिनती और मैनुअल।

मैं समझता हूं कि मैन्युअल रेफ गिनती कैसे काम करती है। उदाहरण के लिए धन्यवाद।

लेकिन Z3 कैसे जानता है कि स्वत: रेफ-गिनती मामले में एएसटी नोड को कब हटाना है? चूंकि Z3_ast सी भाषा = से एक संरचना है>> जेड 3 के बाहर Z3_ast के सभी असाइनमेंट्स और उपयोगों को ट्रैक करना असंभव है।

या केवल Z3 के अंदर Z3 ट्रैक संदर्भ? यदि आप उदाहरण के लिए करते हैं तो रेफ काउंटर के लिए कोई अपडेट नहीं किया गया है: ast1 = ast2।

Answer 1

स्वचालित मोड एक बहुत ही सरल नीति का उपयोग करता है। जब भी उपयोगकर्ता को एएसटी वापस कर दिया जाता है, तो Z3 इसे एक स्टैक S पर संग्रहीत करता है और इसके संदर्भ काउंटर को बढ़ाता है। जब Z3_push फ़ंक्शन निष्पादित किया जाता है, तो Z3 स्टैक S के आकार को बचाता है। जब मिलान Z3_pop निष्पादित किया जाता है, तो स्टैक S का आकार पुनर्स्थापित किया जाता है, और स्टैक से पॉप किए गए एएसटी का संदर्भ काउंटर कम हो जाता है। इस मोड का उपयोग करना बहुत आसान है, लेकिन इसकी मुख्य समस्या है: मेमोरी खपत। उदाहरण के लिए, यदि Z3_push और Z3_pop का उपयोग नहीं किया जाता है, तो उपयोगकर्ता द्वारा बनाए गए सभी एएसटी को कभी भी हटाया नहीं जाएगा।