How to use tuples in SMT-lib?

Question

I am quite sure that it should be possible to describe tuples using SMT-lib syntax, especially for the Z3 solver. However, I can't really find a way of doing so. The only thing I found is this documentation page, but I don't get how to use it in z3 -in.

My struggles so far:

(declare-const t (Prod Int Bool))
(error "line 1 column 19: unknown sort 'Prod'")
(declare-const t (Tuple Int Bool))
(error "line 2 column 18: unknown sort 'Tuple'")
(declare-const t (Pair Int Bool))
(error "line 3 column 18: unknown sort 'Pair'")

Answer 1

In addition to what Christoph said, there's an example right in the SMTLib document: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

In Section 4.2.3, you can find:

(declare-datatype Pair (par (X Y) ((pair (first X) (second Y)))))

If you just want IntxBool, then you can simplify:

(declare-datatype PairIntBool (par () ((pair (first Int) (second Bool)))))

In general, you should read through Section 4.2.3 to learn about how to declare and use new data-types.

Answer 2

Your link points to the OCAML API, i.e. this has nothing to do with SMT. Tuples are a special case of datatypes, for which there is a section in the Z3 Guide.