एसएमटीआईएलबी सरणी सिद्धांत Z3

Question

एसएमटीआईएलबी सरणी का उपयोग करते समय, मैंने सिद्धांत और खान की जेड 3 की समझ के बीच एक अंतर देखा। मैं एसएमटीआईएलबी सरणी सिद्धांत [0] का उपयोग कर रहा हूं जो आधिकारिक वेबसाइट [1] पर पाया जा सकता है।

मुझे लगता है कि मेरी समस्या एक साधारण उदाहरण के साथ सबसे अच्छी तरह से सचित्र है।

(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
     (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 

पहली सरणी सूचकांक 1 और 0 के अन्य सभी सूचकांक के लिए कम से 2 लौटना चाहिए, दूसरा 1 सूचकांक 0, 2 पर सूचकांक 1, और 0 पर अन्य सभी सूचकांकों के लिए वापस आ जाएगी। सूचकांक 0 पर select कॉलिंग इस की पुष्टि लगता है:

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     0 
    ) 
) 
(assert 
    (= 
     1 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

जेड 3 रिटर्न दोनों के लिए sat।

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

जैसी उम्मीद थी, जेड 3 (मामले में यह मायने रखती है, मैं लिनक्स amd64 पर संस्करण 3.2 का उपयोग कर रहा में) इस मामले में unsat जवाब देता है। इसके बाद, इन दो सरणियों की तुलना करें:

(assert 
    (= 
     (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
       (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 
    ) 
) 

जेड 3 मुझे sat, जो मैं "इन दो सरणियों बराबर की तुलना करें" के रूप में व्याख्या बताता है। हालांकि, मैं उम्मीद करता हूं कि इन सरणी बराबर की तुलना न करें। मैं SMTLIB सरणी सिद्धांत है, जो कहते हैं आधार पर आप इसका:

- (forall ((a (Array s1 s2)) (b (Array s1 s2))) 
    (=> (forall ((i s1)) (= (select a i) (select b i))) 
      (= a b))) 

तो, सादे अंग्रेजी में कुछ इस तरह का मतलब होगा "दो सरणियों अगर बराबर की तुलना करेगा, और केवल अगर वे सभी सूचकांकों के लिए बराबर हैं।" क्या कोई मुझे यह समझा सकता है? क्या मैं सिद्धांत को याद कर रहा हूं या गलत समझ रहा हूं? मैं इस मुद्दे पर आपके विचारों के लिए आभारी हूं।

सादर, लियोन

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org

Answer 1

समस्या की रिपोर्ट करने के लिए धन्यवाद। यह सरणी प्रीप्रोसेसर में एक बग है। वास्तविक सॉल्वर लागू होने से पहले प्रीप्रोसेसर सरणी अभिव्यक्ति को सरल बनाता है। बग केवल उन्हीं समस्याओं को प्रभावित करता है जो निरंतर सरणी का उपयोग करते हैं (उदाहरण के लिए, ((as const (Array Int Int)) 0))। आप लगातार सरणी का उपयोग न करके बग को काम कर सकते हैं। मैंने बग तय किया, और फिक्स अगले रिलीज में उपलब्ध होगा।