Enregistrements avec Z3

Question

J'ai regardé de très près la documentation et les guides et essayé moi-même quelques bonnes choses. Cependant, la solution à mes problèmes m'échappe.

C'est ce que le tutoriel dit en ce qui concerne les dossiers, mais il me ne sait pas à la façon de l'avoir mes besoins:

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Int Int)) 
(declare-const p2 (Pair Int Int)) 

Je cherche la syntaxe SMT-LIB2 pour déclarer un enregistrement 5 champs, 2 Ints et 3 Bools. Je voudrais ensuite avoir un tableau/ensemble de ces enregistrements. Je suis en outre à la recherche de la syntaxe que j'utiliserais pour faire une instruction $ \ forall $ sur un ensemble d'enregistrements.

J'ai fait de mon mieux avec les ressources données et je n'ai rien trouvé.

Merci.

Answer 1

Voici comment vous pouvez créer un enregistrement avec 2 ints et 3 bools:

(declare-datatypes() ((R5 (mk-R5 (el1 Int) (el2 Int) (el3 Bool) (el4 Bool) (el5 Bool))))) 

(declare-const r1 R5) 
(declare-const r2 R5) 

(assert (not (= r1 r2))) 

(check-sat) 
(get-model) 

Z3: répond

sat 
(model 
    (define-fun r2() R5 
    (mk-R5 1 0 false false false)) 
    (define-fun r1() R5 
    (mk-R5 0 0 false false false)) 
) 

Espérons que cela va vous aider à démarrer. En ce qui concerne les quantificateurs, ce sera similaire à tout autre usage de quantificateur; Il est préférable de poser des questions spécifiques pour obtenir de meilleures réponses.