An instance of IlcInverse represents an inverse constraint between an array on set variables and an array of variables. Informally, we say that an inverse constraint works on two arrays, say, f and invf, so that an element of f collects the indexes of the element of invf that points to the first element.

In formal terms, if the length of the array f is n, and the length of the array invf is m, then the inverse constraint makes sure that:

• for all i in the interval [0, n-1] and
• for all j in the interval [0, m-1], then
• j is in f[i] is equivalent to invf[j] == i.

If the length of the array f is n, and the length of the array invf is m, then this function returns a constraint that insures that:

• for all i in the interval [0, n-1], if f[i] is in [0, m-1] then invf[f[i]] == i;
• for all j in the interval [0, m-1], if invf[j] is in [0, n-1] then f[invf[j]] == j.