Expand description
From the spec:
3.5 Sorts A major subset of the SMT-LIB language is the language of well-sorted terms, used to represent logical expressions. Such terms are typed, or sorted in logical terminology; that is, each is associated with a (unique) sort. The set of sorts consists itself of sort terms. In essence, a sort term is a sort symbol, a sort parameter, or a sort symbol applied to a sequence of sort terms. Syntactically, a sort symbol can be either the distinguished symbol Bool or any 〈identier 〉. A sort parameter can be any 〈symbol 〉 (which in turn, is an 〈identier 〉).
〈sort〉 ::= 〈identier 〉 | ( 〈identier 〉 〈sort〉+ )