Equivalent de l'opérateur "store" pour les enregistrements dans z3

Question

Je me demande s'il existe un opérateur pour les enregistrements dans z3 similaire à l'opérateur "store" pour les tableaux. Autrement dit, étant donné un enregistrement, y a-t-il un moyen de retourner un nouvel enregistrement dans lequel nous avons changé un élément et tous les autres éléments conservent leurs valeurs? Par exemple:

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

La dernière ligne ci-dessus est un exemple de ce que je voudrais faire. Est-ce qu'il y a un moyen de faire ça? Ou le constructeur défini par l'utilisateur est-il le seul moyen de construire un nouvel enregistrement? Je vous remercie.

Answer 1

Vous pouvez tenter votre chance avec:

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

Alternativement, vous venez de créer un nouvel enregistrement qui a les mêmes champs que l'ancien, à l'exception du champ spécifié.