 # Regular constraint

Formally, a deterministic finite automaton (DFA) is described by a 5-tuple $LaTeX: M = (Q, \Sigma, \delta, q_0, F)$ where $LaTeX: Q$ is a finite set of states, $LaTeX: \Sigma$ is an alphabet, $LaTeX: \delta: Q \times \Sigma \rightarrow Q$ is a transition function, $LaTeX: q_0 \in Q$ is the initial state, and $LaTeX: {F} \subseteq Q$ is the set of final (or accepting) states. Given an input string, the automaton starts in the initial state $LaTeX: q_{0}$ and processes the string one symbol at the time, applying the transition function $LaTeX: \delta$ at each step to update the current state. If the last state reached belongs to the set of final states $LaTeX: F$, then the string is accepted. All strings that are accepted by M generates the language $LaTeX: {L}(M)$.
Now, let $LaTeX: M = (Q, \Sigma, \delta, q_0, F)$ be a DFA and let $LaTeX: X = \{x_1, s_2, \dots x_n\}$ be a set of variables with domain $LaTeX: D(x_{i}) \subseteq \Sigma$ for $LaTeX: 1\leq i \leq n$. Then $LaTeX: regular(X,M) = \{ (d_1, \dots, d_n) | \forall i, d_i \in D(x_i), d_1d_2 \dots d_n \in L(M) \}$.