In this section, we introduce a variety of logical theories encompassing the most common kinds of string constraints (as overviewed in [1]}). We define three sets of terms as follows. Let \(\mathcal {X} = \lbrace x_1,x_2,\ldots \rbrace \)  be an infinite set of string variables. Let \(\Sigma \)  be a finite alphabet. Let \(\mathcal {T}_{str}^\Sigma = \mathcal {X} \cup \Sigma ^*\)  be the set of basic string terms. Let \(\mathcal {T}_{str,con}^{\Sigma } = (\mathcal {X} \cup \Sigma )^*\)  be the set of extended string terms. Note that \(\mathcal {T}_{str,con}^{\Sigma }\)  is the closure of \(\mathcal {T}_{str}^\Sigma \)  under the concatenation \((\cdot )\)  operation. Let \(\mathcal {T}_{arith}^\Sigma = \lbrace k_0 + k_1|s_1| +k_2|s_2| + \ldots + k_n|s_n| \mid n \in \mathbb {N}_0, k_i \in \mathbb {Z}, \text{ and } s_i \in \mathcal {T}_{str}^\Sigma \rbrace \)  be the set of length terms. We interpret \(|s|\)  as the length of the string term \(s\) , so \(\mathcal {T}_{arith}^\Sigma \)  is the set of linear combinations of lengths of string terms. Note that since we can express the length of a concatenation of string terms as a linear combination of lengths of basic string terms, it is no restriction that \(s_i \in \mathcal {T}_{str}^\Sigma \)  rather than \(\mathcal {T}_{str,con}^\Sigma \)  (this allows us to consider theories containing length terms both with and without concatenation). We construct three types of atoms from terms as follows:
