निश्चित आकार के साथ एक सरणी बनाएं और इसे

Question

प्रारंभ करें मैं निश्चित आकार के साथ एक सरणी बनाने जा रहा हूं और इसे कुछ मानों के साथ प्रारंभ कर रहा हूं।

उदाहरण के लिए, निम्नलिखित सी ++ कोड:

a[0] = 10; 
a[1] = 23; 
a[2] = 27; 
a[3] = 12; 
a[4] = 19; 
a[5] = 31; 
a[6] = 41; 
a[7] = 7; 

वहाँ जेड 3 में कुछ उपयोगिताओं यह मॉडल करने के लिए कर रहे हैं?

Answer 1

जेड 3 सरणी सिद्धांत का समर्थन करता है, लेकिन आम तौर पर असंबद्ध सरणी, या सरणी को बहुत बड़ा करने के लिए उपयोग किया जाता है। बड़े से, मेरा मतलब है कि आपके सूत्र में सरणी पहुंच (यानी, चयन) की संख्या सरणी के वास्तविक आकार की तुलना में बहुत छोटी है। हमें खुद से पूछना चाहिए: "क्या हमें समस्या एक्स को मॉडलिंग/हल करने के लिए वास्तव में सरणी की आवश्यकता है?"। आपके उदाहरण में निश्चित आकार के सरणी के लिए, हम प्रत्येक सरणी स्थिति के लिए एक अलग चर का उपयोग कर सकते हैं। उदाहरण: a[0] के लिए a0, a[1] के लिए a1, आदि बेशक, अगर हम सिद्धांतों का उपयोग नहीं करते, तो एक सरणी का उपयोग इस तरह के रूप a[i] एक बड़ा अगर-तो-और कुछ अवधि जैसे

(ite (= i 0) a0 (ite (= i 1) a1 ...))

के रूप में एन्कोड किया जाना चाहिए एन्कोडिंग

यदि सरणी का आकार ज्ञात और छोटा है, तो यह आमतौर पर किसी समस्या को एन्कोड करने का सबसे प्रभावी तरीका है।

दूसरी ओर, यदि आप सरणी सिद्धांत उपयोग करने का निर्णय, तो आप अपने सवाल में प्रारंभ सांकेतिक शब्दों में बदलना कर सकते हैं के रूप में:

:

(declare-const a (Array Int Int)) 
(assert (= (select a 0) 10)) 
... 
(assert (= (select a 7) 7)) 

यहाँ पूरे उदाहरण श्रीमती 2.0 प्रारूप में इनकोडिंग है http://rise4fun.com/Z3/iwo

ध्यान दें कि इस सरणी पर एक अद्यतन को एन्कोड करने के लिए। उदाहरण के लिए, सी कथन a[3] = 5, हमें इस असाइनमेंट के बाद सरणी का प्रतिनिधित्व करने वाला एक नया सरणी चर बनाना होगा। सबसे कॉम्पैक्ट रास्ते का उपयोग करता store अभिव्यक्ति:

(declare-const a1 (Array Int Int)) 
(assert (= a1 (store a 3 5))) 

यहाँ अद्यतन के साथ पूर्ण उदाहरण है।

http://rise4fun.com/Z3/Kpln

तुम भी अजगर/C++ /। नेट एपीआई विचार कर सकते हैं। वे हमें आपके जैसे उदाहरणों को एक अधिक कॉम्पैक्ट तरीके से एन्कोड करने की अनुमति देते हैं। विचार उन कार्यों को कार्यान्वित करना है जो सामान्य रूप से प्रयुक्त पैटर्न जैसे कि सरणी प्रारंभिक एन्कोड करते हैं।

http://rise4fun.com/Z3Py/AAD