レコードの配列ストアの等価物

Question

配列に新しい値を格納することができ、そうすると新しい配列が返されます。 MkApp関数を使用してレコードのセレクタにアクセスできることはわかっていますが、レコードの値をどのように置き換えることができますか？ 、私はレコードのN番目のコンポーネントを更新する統一的な方法がありますとは思わない

(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

：私は、.NETバインディングを使用していますが、問題の一例として、ここではいくつかのSMTでありますをに更新すると、基本的に "forall j、iはjとa [j]のいずれかであるとみなされます。したがって、新しい値またはa [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) 

これは、組み込みの更新機能を持つほど簡潔ではありませんが、OK。特に、あなたの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のペアが持つ必要があります。