Эквивалент оператора «store» для записей в z3

Question

Мне интересно, есть ли оператор для записей в z3, аналогичный оператору «store» для массивов. То есть, учитывая запись, есть ли способ вернуть новую запись, в которой мы изменили один элемент, и все остальные элементы сохраняют свои значения? Например:

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

В качестве альтернативы, вы просто создать новую запись, которая имеет то же поле, что и старый, за исключением указанного поля.