z3 - 等效于 z3 中记录的“存储”运算符

Question

我想知道 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)))

或者，您只需创建一个新记录，该记录与旧记录具有相同的字段，但指定的字段除外。