z3のレコードの "store"演算子に相当する

Question

配列の "store"演算子と同様のz3のレコードの演算子があるのだろうかと思います。つまり、レコードがあれば、ある要素を変更し、他のすべての要素がその値を保持する新しいレコードを返す方法はありますか？たとえば、

(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 (mk-pair 1 2))) 
(assert (= p2 (store p1 second 3))) 

最後の行は、私がしたいものの例です。これを行う方法はありますか？または、ユーザー定義コンストラクタは新しいレコードを作成する唯一の手段ですか？ありがとうございました。

Answer 1

あなたはとのあなたの運を試すことができます：

(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 (mk-pair 1 2))) 
(assert (= p2 ((_ update-field second) p1 3))) 

また、あなただけの指定したフィールドを除いて、古いものと同じフィールドを持つ新しいレコードを作成します。