The type of terms.

The type of identifiers for constants.

The type of locations.

Constants, i.e non predefined symbols. This includes both constants defined by theories, defined locally in a problem, and also quantified variables.

Constants lexically recognised as numbers in different formats. According to the smtlib manual, these should not always be interpreted as numbers since their interpretation is actually dependent on the theory set by the problem.

Juxtaposition of terms, used to annotate terms with their type.

Application.

Local bindings. The bindings are a list of terms built using the colon function.

Universal quantification.

Existencial quantification.

Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch.

S-expressions. Used in smtlib's annotations,

Attach a list of attributes (also called annotations) to a term. As written in the smtlib manual, "Term attributes have no logical meaning -- semantically, attr t l is equivalent to t"