Accessing members of composite sorts (data types) in SMT-LIBv2

Question

According to sec. 3.9.3 of The SMT-LIBv2 Language and Tools: A Tutorial it is possible to declare a composite sort like this in SMT-LIBv2:

(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))

I am using CVC4 and it seems to accept this syntax. But how do I access the elements? I tried the following (and various variations of that and other things I found online):

(assert (_ state 1))
(assert (select 1 state))

But it looks like those operators only work on vectors and arrays. I can't find any example that uses such composite sorts and can't find anything about accessing those elements in the tutorial or the language standard. How is it done? Or did I completely misunderstand what this feature is for?

My application: I want to encode a temporal problem and want to do it in form of a state transition function that converts the old state into a new state, so I can write something like the following when experimenting with the system:

....
(declare-fun initial_state () MyStateSort)
(declare-fun state_after_step_1 () MyStateSort)
(declare-fun state_after_step_2 () MyStateSort)
(assert (= (MyTransitionFunc initial_state) state_after_step_1)
(assert (= (MyTransitionFunc state_after_step_1) state_after_step_2)

Answer 1

This is an answer to my own question. If anyone can post an example for a use-case of a user-defined sort with arity > 0, I'll happily accept that as answer.

After reading the SMT-LIBv2 standard more carefully I am now thinking that sort declarations with arity > 0 only have an application in theory definitions (for declaring sorts like Array), not in user-supplied code. The example in David Cok's Tutorial seems to be misleading, as it suggests that this can be used to declare composite sorts. I have not found any indication of that anywhere else. This includes the complete SMT-LIB benchmark that contains not a single sort declaration with arity > 0.

Instead of "composite sorts" one should use uninterpreted functions to create the equivalent of complex data structures. Example:

(set-logic QF_UF)
(declare-sort CONTAINER_SORT 0)
(declare-fun CONTAINER_MEMBER_1 (CONTAINER_SORT) Bool)
(declare-fun CONTAINER_MEMBER_2 (CONTAINER_SORT) Bool)
(declare-fun INSTANCE_1 () CONTAINER_SORT)
(declare-fun INSTANCE_2 () CONTAINER_SORT)

This will effectively declare the following 4 independent Bool expressions.

(CONTAINER_MEMBER_1 INSTANCE_1)
(CONTAINER_MEMBER_2 INSTANCE_1)

(CONTAINER_MEMBER_1 INSTANCE_2)
(CONTAINER_MEMBER_2 INSTANCE_2)