Sort (Satisfiability Modulo Theory)

Definition

Sort (Satisfiability Modulo Theory)

A sort is a named class of values in a many-sorted SMT signature $\Sigma$. If $s\in \mathcal{S}$ is a sort, an interpretation $\mathcal{M}$ assigns it a non-empty carrier $D_s^{\mathcal{M}}$. Variables and terms of sort $s$ take their values from this carrier.

Sorts enforce type-correct construction of terms. For a function declaration
$f:s_1\times \cdots \times s_n\to s$:

$$\mathrm{sort}(f(t_1,\dots ,t_n))=s\text{if}\mathrm{sort}(t_i)=s_i\text{ for every }i.$$

Thus, a sort says which kind of value an expression denotes and which
function arguments it may occupy; the associated theory determines the available operations and, for interpreted sorts, their intended meaning. Typical SMT sorts include $\mathsf{Int}$, $\mathsf{Real}$, $\mathsf{Bool}$, and fixed-width bit-vectors.