z3 - Equivalent of "store" operator for Records in z3

Question

I am wondering if there is an operator for Records in z3 similar to the "store" operator for arrays. That is, given a record, is there any way to return a new record in which we've changed one element and all other elements retain their values? For instance:

(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)))

The last line above is an example of what I would like to do. Is there any way to do this? Or is the user-defined constructor the only means to construct a new record? Thank you.

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)))

または、指定されたフィールドを除いて、古いレコードと同じフィールドを持つ新しいレコードを作成するだけです。