Equalvalent數組存儲記錄

Question

一個數組可以存儲一個新的值，並在這樣做返回一個新的數組。我知道我可以使用MkApp函數來訪問記錄的選擇器，然後如何替換記錄的值？我使用的是.NET綁定，但隨着問題的例子，這裏是一些SMT：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Int Int)) 
(declare-const p2 (Pair Int Int)) 
(assert (= p1 p2)) 
(assert (> (second p1) 20)) 
;How to replace (second p1) with 0 
(check-sat) 
(get-model) 

Answer 1

我不認爲有更新記錄的ñ個分量的統一方式，你基本上必須「展開」更新的定義：當更新數組a時，你基本上假設「所有的j，無論i是j還是a [j]因此是新值，或者[j]舊值「。由於創紀錄的有窮個元素，可以展開相應的更新定義：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 

(declare-const p1 (Pair Int Int)) 
(assert (= (first p1) 1)) 
(assert (= (second p1) 2)) ;; p1 is (1, 2) 

(declare-const p2 (Pair Int Int)) 
(assert 
    (and 
    (= (first p2) (first p1)) 
    (= (second p2) 0))) 

(check-sat) 
(get-model) ;; p2 could be (1, 0) 

這不是爲具有內置更新功能簡潔，但確定;特別是如果您的SMT代碼是由工具生成的。

你也可以引入更新的關係（函數符號和量詞會的工作，太多，但可能會出現問題，由於觸發）：

;; Read: "updating p1's second element to v yields p2" 
(define-fun setSecond ((p1 (Pair Int Int)) (v Int) (p2 (Pair Int Int))) Bool ;; analogous for setFirst 
    (and 
    (= (first p2) (first p1)) 
    (= (second p2) v))) 

(declare-const p3 (Pair Int Int)) 
(assert (setSecond p2 77 p3)) 

(check-sat) 
(get-model) ;; p3 is (1, 77) 

，或者更一般地說：

;; Read: "updating p1's ith element to v yields p2" 
(define-fun setNth ((p1 (Pair Int Int)) (i Int) (v Int) (p2 (Pair Int Int))) Bool 
    (and 
    (= (first p2) (ite (= i 1) v (first p1))) 
    (= (second p2) (ite (= i 2) v (second p1))))) 

(declare-const p4 (Pair Int Int)) 
(assert (setNth p3 1 -77 p4)) 

(check-sat) 
(get-model) ;; p4 is (-77, 77) 

和以前一樣，直接從特定記錄的定義中生成更新函數。

注意：多態函數尚未支持，您需要一個函數setNth_T1_T2每個元素類型T1，T2您的配對可以擁有。