Records with Z3

Question

I have looked quite closely at the documentation and guides and tried a fair few things myself. However, the solution to my problems evades me.

This is what the tutorial says regarding records but it is unclear to me how to have it suit my needs:

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

I am looking for the SMT-LIB2 syntax for declaring a record of 5 fields, 2 Ints and 3 Bools.

I would then like to have an array/set of these records.

Am am furthermore looking for the syntax I would then use to make a $\forall$ statement over some set of records.

I tried my best with the resources given and have gotten nowhere.

Thanks.

Answer 1

Here's how you can create a record with 2 ints and 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 responds:

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

Hopefully this'll get you started. Regarding quantifiers, it'll be similar to all other quantifier usage; It's best to ask specific questions to get better answers.