A first systematic approach for creating an automaton that only recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint could be to:

• First, create an automaton that recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}$ constraint.

• Second, create an automaton that recognises the solutions to the $\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint.

• Third, make the product of the two previous automata and minimise the resulting automaton.

However this approach is not going to scale well in practice since the automaton associated with the $\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint has a too big size. Therefore we propose an approach where we directly construct in a single step the automaton that only recognises the solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint. Note that we do not have any formal proof that the resulting automaton is always minimum.

Without loss of generality, assume that the collection of variables $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ contains at least one variable (i.e., $\left|\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}\right|\ge 1$). Let $l$, $m$, $n$, $\mathrm{𝑚𝑖𝑛}$ and $\mathrm{𝑚𝑎𝑥}$ respectively denote the minimum and maximum possible value of variable $\mathrm{𝙽𝚅𝙰𝙻}$, the number of variables of the collection $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$, the smallest value that can be assigned to the variables of $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$, and the largest value that can be assigned to the variables of $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$. Let $s=\mathrm{𝑚𝑎𝑥}-\mathrm{𝑚𝑖𝑛}+1$ denote the total number of potential values. Clearly, the maximum number of distinct values that can be assigned to the variables of the collection $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ cannot exceed the quantity $d=min(m,n,s)$. The $\frac{s·(s+1)}{2}-\frac{(s-d)·(s-d+1)}{2}+1$ states of the automaton that only accepts solutions to the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint can be defined in the following way:

• We have an initial state labelled by $s_{00}$.

• We have $\frac{s·(s+1)}{2}-\frac{(s-d)·(s-d+1)}{2}$ states labelled by $s_{ij}$ $(1\le i\le d,i\le j\le s)$. The first index $i$ of a state $s_{ij}$ corresponds to the number of distinct values already encountered, while the second index $j$ denotes the the current value (i.e., more precisely the index of the current value, where the minimum value has index 1).

Terminal states depend on the possible values of variable $\mathrm{𝙽𝚅𝙰𝙻}$ and correspond to those states $s_{ij}$ such that $i$ is a possible value for variable $\mathrm{𝙽𝚅𝙰𝙻}$. Note that we assume no further restriction on the domain of $\mathrm{𝙽𝚅𝙰𝙻}$ (otherwise the set of accepting states needs to be reduced in order to reflect the current set of possible values of $\mathrm{𝙽𝚅𝙰𝙻}$). Three classes of transitions are respectively defined in the following way:

1. There is a transition, labelled by $\mathrm{𝑚𝑖𝑛}+j-1$, from the initial state $s_{00}$ to the state $s_{1j}$ $(1\le j\le s)$.

2. There is a loop, labelled by $\mathrm{𝑚𝑖𝑛}+j-1$ for every state $s_{ij}$ $(1\le i\le d,i\le j\le s)$.

3. $\forall i\in [1,d-1],\forall j\in [i,s],\forall k\in [j+1,s]$ there is a transition labelled by $\mathrm{𝑚𝑖𝑛}+k-1$ from $s_{ij}$ to $s_{i+1k}$.

We respectively have $s$ transitions of class 1, $\frac{s·(s+1)}{2}-\frac{(s-d)·(s-d+1)}{2}$ transitions of class 2, and $\frac{(s-1)·s·(s+1)}{6}-\frac{(s-d)·(s-d+1)·(s-d+2)}{6}$ transitions of class 3.

Note that all states $s_{ij}$ such that $i+s-j<l$ can be discarded since they do not allow to reach the minimum number of distinct values required $l$.

Part (A) of Figure 5.187.3 depicts the automaton associated with the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint of the first example of the Example slot. For this purpose, we assume that variable $\mathrm{𝙽𝚅𝙰𝙻}$ is fixed to value 2 and that variables of the collection $\mathrm{𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂}$ take their values within interval $[6,8]$. Part (B) of Figure 5.187.3 represents the simplified automaton where all states that do not allow to reach an accepting state were removed. The corresponding $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚐𝚕𝚘𝚋𝚊𝚕}\_\mathrm{𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢}$ constraint holds since the corresponding sequence of visited states, $s_{00}$ $s_{11}$ $s_{11}$ $s_{23}$ $s_{23}$ $s_{23}$, ends up in an accepting state (i.e., accepting states are denoted graphically by a double circle).

Figure 5.187.3. Automaton – Part (A) – and simplified automaton – Part (B) – of the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$$(2,\langle 6,6,8,8,8\rangle )$ constraint of the first example of the Example slot: the path corresponding to the second argument $\langle \mathbf{6},\mathbf{6},\mathbf{8},\mathbf{8},\mathbf{8}\rangle$ is depicted by thick orange arcs, where the self-loop on state $s_{23}$ is applied twice

Figure 5.187.4 depicts a second deterministic automaton with one counter associated with the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚗𝚟𝚊𝚕𝚞𝚎}$ constraint, where the argument $\mathrm{𝙽𝚅𝙰𝙻}$ is unified to the final value of the counter.

Figure 5.187.4. Automaton (with one counter) of the $\mathrm{𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐}\_\mathrm{𝚟𝚊𝚕𝚞𝚎}$ constraint for a non-empty collection of variables